diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 26e987c0a985..7852398300d4 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -1089,15 +1089,18 @@ def InvImage {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β
   fun a₁ a₂ => r (f a₁) (f a₂)
 
 /--
-The transitive closure `r⁺` of a relation `r` is the smallest relation which is
-transitive and contains `r`. `r⁺ a z` if and only if there exists a sequence
+The transitive closure `TransGen r` of a relation `r` is the smallest relation which is
+transitive and contains `r`. `TransGen r a z` if and only if there exists a sequence
 `a r b r ... r z` of length at least 1 connecting `a` to `z`.
 -/
-inductive TC {α : Sort u} (r : α → α → Prop) : α → α → Prop where
-  /-- If `r a b` then `r⁺ a b`. This is the base case of the transitive closure. -/
-  | base  : ∀ a b, r a b → TC r a b
+inductive Relation.TransGen {α : Sort u} (r : α → α → Prop) : α → α → Prop
+  /-- If `r a b` then `TransGen r a b`. This is the base case of the transitive closure. -/
+  | single {a b} : r a b → TransGen r a b
   /-- The transitive closure is transitive. -/
-  | trans : ∀ a b c, TC r a b → TC r b c → TC r a c
+  | tail {a b c} : TransGen r a b → r b c → TransGen r a c
+
+/-- Deprecated synonym for `Relation.TransGen`. -/
+@[deprecated Relation.TransGen (since := "2024-07-16")] abbrev TC := @Relation.TransGen
 
 /-! # Subtype -/
 
diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index 0bd4b3c767a8..8190b0948247 100644
--- a/src/Init/WF.lean
+++ b/src/Init/WF.lean
@@ -148,22 +148,26 @@ end InvImage
   wf  := InvImage.wf f h.wf
 
 -- The transitive closure of a well-founded relation is well-founded
-namespace TC
-variable {α : Sort u} {r : α → α → Prop}
-
-theorem accessible {z : α} (ac : Acc r z) : Acc (TC r) z := by
-  induction ac with
-  | intro x acx ih =>
-    apply Acc.intro x
-    intro y rel
-    induction rel with
-    | base a b rab => exact ih a rab
-    | trans a b c rab _ _ ih₂ => apply Acc.inv (ih₂ acx ih) rab
-
-theorem wf (h : WellFounded r) : WellFounded (TC r) :=
-  ⟨fun a => accessible (apply h a)⟩
-end TC
-
+open Relation
+
+theorem Acc.transGen (h : Acc r a) : Acc (TransGen r) a := by
+  induction h with
+  | intro x _ H =>
+    refine Acc.intro x fun y hy ↦ ?_
+    cases hy with
+    | single hyx =>
+      exact H y hyx
+    | tail hyz hzx =>
+      exact (H _ hzx).inv hyz
+
+theorem acc_transGen_iff : Acc (TransGen r) a ↔ Acc r a :=
+  ⟨Subrelation.accessible TransGen.single, Acc.transGen⟩
+
+theorem WellFounded.transGen (h : WellFounded r) : WellFounded (TransGen r) :=
+  ⟨fun a ↦ (h.apply a).transGen⟩
+
+@[deprecated Acc.transGen (since := "2024-07-16")] abbrev TC.accessible := @Acc.transGen
+@[deprecated WellFounded.transGen (since := "2024-07-16")] abbrev TC.wf := @WellFounded.transGen
 namespace Nat
 
 -- less-than is well-founded