diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index 5232e371ae..7b6506cc03 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Main.lean
@@ -184,25 +184,25 @@ def checkTerminationByHints (preDefs : Array PreDefinition) : CoreM Unit := do
   let preDefsWithout := preDefs.filter (·.termination.terminationBy?.isNone)
   let structural :=
     preDefWith.termination.terminationBy? matches some {structural := true, ..}
-  -- Information whether the current one is partial, least or greatest
-  let partialFixpoint := preDefWith.termination.partialFixpoint?.any fun x => isPartial x.fixpointType
-  let leastFixpoint := preDefWith.termination.partialFixpoint?.any fun x => isLeast x.fixpointType
-  let greatestFixpoint := preDefWith.termination.partialFixpoint?.any fun x => isGreatest x.fixpointType
+  -- Information whether the current one is partial, inductive or coinductive
+  let partialFixpoint := preDefWith.termination.partialFixpoint?.any fun x => isPartialFixpoint x.fixpointType
+  let inductiveFixpoint := preDefWith.termination.partialFixpoint?.any fun x => isInductiveFixpoint x.fixpointType
+  let coinductiveFixpoint := preDefWith.termination.partialFixpoint?.any fun x => isCoinductiveFixpoint x.fixpointType
   for preDef in preDefs do
     -- if some has at termination by clause
     if let .some termBy := preDef.termination.terminationBy? then
-      -- but something in the clique is partial/least/greatest, then we report error
+      -- but something in the clique is partial/inductive/coinductive, then we report error
       if let .some partialFixpointStx := preDef.termination.partialFixpoint? then
         match partialFixpointStx.fixpointType with
         | .partialFixpoint => throwErrorAt partialFixpointStx.ref m!"conflicting annotations: this function cannot \
           be both terminating and a partial fixpoint"
-        | .leastFixpoint => throwErrorAt partialFixpointStx.ref m!"conflicting annotations: this function cannot \
-          be both terminating and a least fixpoint"
-        | .greatestFixpoint => throwErrorAt partialFixpointStx.ref m!"conflicting annotations: this function cannot \
-          be both terminating and a greatest fixpoint"
+        | .inductiveFixpoint => throwErrorAt partialFixpointStx.ref m!"conflicting annotations: this function cannot \
+          be both terminating and an inductive fixpoint"
+        | .coinductiveFixpoint => throwErrorAt partialFixpointStx.ref m!"conflicting annotations: this function cannot \
+          be both terminating and a coinductive fixpoint"
 
       -- if has no annotations
-      if !structural && !partialFixpoint && !leastFixpoint && !greatestFixpoint && !preDefsWithout.isEmpty then
+      if !structural && !partialFixpoint && !inductiveFixpoint && !coinductiveFixpoint && !preDefsWithout.isEmpty then
         let m := MessageData.andList (preDefsWithout.toList.map (m!"{·.declName}"))
         let doOrDoes := if preDefsWithout.size = 1 then "does" else "do"
         logErrorAt termBy.ref m!"incomplete set of termination hints:\n\
@@ -224,57 +224,57 @@ def checkTerminationByHints (preDefs : Array PreDefinition) : CoreM Unit := do
             structurally recursive, so no explicit termination proof is needed."
 
     -- If one is partial, but others are not
-    if partialFixpoint && !preDef.termination.partialFixpoint?.any fun x => isPartial x.fixpointType then
+    if partialFixpoint && !preDef.termination.partialFixpoint?.any fun x => isPartialFixpoint x.fixpointType then
       throwErrorAt preDef.ref m!"Incompatible termination hint; this function is mutually \
         recursive with {preDefWith.declName}, which is marked as \
         `partial_fixpoint` so this one also needs to be marked \
         `partial_fixpoint`."
 
     -- If one is least, but others are not
-    if leastFixpoint && !preDef.termination.partialFixpoint?.any fun x => isLatticeTheoretic x.fixpointType then
+    if inductiveFixpoint && !preDef.termination.partialFixpoint?.any fun x => isLatticeTheoretic x.fixpointType then
       throwErrorAt preDef.ref m!"Incompatible termination hint; this function is mutually \
         recursive with {preDefWith.declName}, which is marked as
-        `least_fixpoint` so this one also needs to be marked \
-        `least_fixpoint` or `greatest_fixpoint`."
+        `inductive_fixpoint` so this one also needs to be marked \
+        `inductive_fixpoint` or `coinductive_fixpoint`."
 
     -- If one is greatest, but others are not
-    if greatestFixpoint && !preDef.termination.partialFixpoint?.any fun x => isLatticeTheoretic x.fixpointType then
+    if coinductiveFixpoint && !preDef.termination.partialFixpoint?.any fun x => isLatticeTheoretic x.fixpointType then
       throwErrorAt preDef.ref m!"Incompatible termination hint; this function is mutually \
         recursive with {preDefWith.declName}, which is marked as \
-        `greatest_fixpoint` so this one also needs to be marked \
-        `least_fixpoint` or `greatest_fixpoint`."
+        `coinductive_fixpoint` so this one also needs to be marked \
+        `inductive_fixpoint` or `coinductive_fixpoint`."
 
     -- checking for unnecessary `decreasing_by` clause
-    if preDef.termination.partialFixpoint?.any fun x => isPartial x.fixpointType then
+    if preDef.termination.partialFixpoint?.any fun x => isPartialFixpoint x.fixpointType then
         if let .some decr := preDef.termination.decreasingBy? then
           logErrorAt decr.ref m!"Invalid `decreasing_by`; this function is marked as \
             partial_fixpoint, so no explicit termination proof is needed."
 
-    if preDef.termination.partialFixpoint?.any fun x => isLeast x.fixpointType then
+    if preDef.termination.partialFixpoint?.any fun x => isInductiveFixpoint x.fixpointType then
       if let .some decr := preDef.termination.decreasingBy? then
         logErrorAt decr.ref m!"Invalid `decreasing_by`; this function is marked as \
-          least_fixpoint, so no explicit termination proof is needed."
+          inductive_fixpoint, so no explicit termination proof is needed."
 
-    if preDef.termination.partialFixpoint?.any fun x => isLeast x.fixpointType then
+    if preDef.termination.partialFixpoint?.any fun x => isInductiveFixpoint x.fixpointType then
       if let .some decr := preDef.termination.decreasingBy? then
         logErrorAt decr.ref m!"Invalid `decreasing_by`; this function is marked as \
-          greatest_fixpoint, so no explicit termination proof is needed."
+          coinductive_fixpoint, so no explicit termination proof is needed."
 
     -- if the selected one is not marked as partial fixpoint
     if !partialFixpoint then
       if let some stx := preDef.termination.partialFixpoint? then
-        if isPartial stx.fixpointType then
+        if isPartialFixpoint stx.fixpointType then
           throwErrorAt stx.ref m!"Incompatible termination hint; this function is mutually \
             recursive with {preDefWith.declName}, which is not also marked as \
             `partial_fixpoint`, so this one cannot be either."
 
     -- if the selected one is not marked as partial fixpoint
-    unless leastFixpoint || greatestFixpoint do
+    unless inductiveFixpoint || coinductiveFixpoint do
       if let some stx := preDef.termination.partialFixpoint? then
         if isLatticeTheoretic stx.fixpointType then
           throwErrorAt stx.ref m!"Incompatible termination hint; this function is mutually \
             recursive with {preDefWith.declName}, which is not also marked as \
-            `least_fixpoint` or `greatest_fixpoint`, so this one cannot be either."
+            `inductive_fixpoint` or `coinductive_fixpoint`, so this one cannot be either."
 
 /--
 Elaborates the `TerminationHint` in the clique to `TerminationMeasures`
diff --git a/src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean b/src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean
index 77c2969c99..623bab1b21 100644
--- a/src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean
+++ b/src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean
@@ -53,14 +53,13 @@ def CCPOProdProjs (n : Nat) (inst : Expr) : Array Expr := Id.run do
 Unfolds an appropriate `PartialOrder` instance on predicates to quantifications and implications.
 I.e. `ImplicationOrder.instPartialOrder.rel P Q` becomes
 `∀ x y, P x y → Q x y`.
-
 In the premise of the Park induction principle (`lfp_le_of_le_monotone`) we use a monotone map defining the predicate in the eta expanded form. In such a case, besides desugaring the predicate, we need to perform a weak head reduction.
 The optional parameter `reduceConclusion` (false by default) indicates whether we need to perform this reduction.
 -/
 def unfoldPredRel (predType : Expr) (body : Expr) (fixpointType : PartialFixpointType) (reduceConclusion : Bool := false) : MetaM Expr := do
   match fixpointType with
   | .partialFixpoint => throwError "Trying to apply lattice induction to a non-lattice fixpoint. Please report this issue."
-  | .leastFixpoint | .greatestFixpoint =>
+  | .inductiveFixpoint | .coinductiveFixpoint =>
     unless body.isAppOfArity ``PartialOrder.rel 4 do
       throwError "{body} is not an application of partial order"
     let lhsTypes ← forallTelescope predType fun ts _ =>  ts.mapM inferType
@@ -68,15 +67,15 @@ def unfoldPredRel (predType : Expr) (body : Expr) (fixpointType : PartialFixpoin
     let bodyArgs := body.getAppArgs
     withLocalDeclsDND (names.zip lhsTypes) fun exprs => do
       let mut applied  := match fixpointType with
-        | .leastFixpoint => (bodyArgs[2]!, bodyArgs[3]!)
-        | .greatestFixpoint => (bodyArgs[3]!, bodyArgs[2]!)
+        | .inductiveFixpoint => (bodyArgs[2]!, bodyArgs[3]!)
+        | .coinductiveFixpoint => (bodyArgs[3]!, bodyArgs[2]!)
         | .partialFixpoint => panic! "Cannot apply lattice induction to a non-lattice fixpoint"
       for e in exprs do
         applied := (mkApp applied.1 e, mkApp applied.2 e)
       if reduceConclusion then
         match fixpointType with
-        | .leastFixpoint => applied := ((←whnf applied.1), applied.2)
-        | .greatestFixpoint => applied := (applied.1, (←whnf applied.2))
+        | .inductiveFixpoint => applied := ((←whnf applied.1), applied.2)
+        | .coinductiveFixpoint => applied := (applied.1, (←whnf applied.2))
         | .partialFixpoint => throwError "Cannot apply lattice induction to a non-lattice fixpoint"
       mkForallFVars exprs (←mkArrow applied.1 applied.2)
 
@@ -93,8 +92,18 @@ private def numberNames (n : Nat) (base : String) : Array Name :=
   .ofFn (n := n) fun ⟨i, _⟩ =>
     if n == 1 then .mkSimple base else .mkSimple s!"{base}_{i+1}"
 
-def deriveInduction (name : Name) : MetaM Unit :=
-  let inductName := name ++ `fixpoint_induct
+def getInductionPrinciplePostfix (name : Name) : MetaM Name := do
+  let some eqnInfo := eqnInfoExt.find? (← getEnv) name | throwError "{name} is not defined by partial_fixpoint, inductive_fixpoint, nor coinductive_fixpoint"
+  let idx := eqnInfo.declNames.idxOf name
+  let some res := eqnInfo.fixpointType[idx]? | throwError "Cannot get fixpoint type for {name}"
+  match res with
+  | .partialFixpoint => return `fixpoint_induct
+  | .inductiveFixpoint => return `induct
+  | .coinductiveFixpoint => return `coinduct
+
+def deriveInduction (name : Name) : MetaM Unit := do
+  let postFix ← getInductionPrinciplePostfix name
+  let inductName := name ++ postFix
   realizeConst name inductName do
   trace[Elab.definition.partialFixpoint] "Called deriveInduction for {inductName}"
   prependError m!"Cannot derive fixpoint induction principle (please report this issue)" do
@@ -250,7 +259,17 @@ def isInductName (env : Environment) (name : Name) : Bool := Id.run do
   match s with
   | "fixpoint_induct" =>
     if let some eqnInfo := eqnInfoExt.find? env p then
-      return p == eqnInfo.declNames[0]!
+      return p == eqnInfo.declNames[0]! && isPartialFixpoint (eqnInfo.fixpointType[0]!)
+    return false
+  | "coinduct" =>
+    if let some eqnInfo := eqnInfoExt.find? env p then
+      let idx := eqnInfo.declNames.idxOf p
+      return isCoinductiveFixpoint eqnInfo.fixpointType[idx]!
+    return false
+  | "induct" =>
+    if let some eqnInfo := eqnInfoExt.find? env p then
+      let idx := eqnInfo.declNames.idxOf p
+      return isInductiveFixpoint eqnInfo.fixpointType[idx]!
     return false
   | _ => return false
 
diff --git a/src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean b/src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean
index 33748bc7b0..8f9c196bc4 100644
--- a/src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean
+++ b/src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean
@@ -75,7 +75,7 @@ private def mkMonoPProd : (hmono₁ hmono₂ : Expr × Expr) → MetaM (Expr ×
   return (← inferType hmonoProof, hmonoProof)
 
 def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do
-  -- We expect all functions in the clique to have `partial_fixpoint` or `greatest_fixpoint` syntax
+  -- We expect all functions in the clique to have `partial_fixpoint`, `inductive_fixpoint` or `coinductive_fixpoint` syntax
   let hints := preDefs.filterMap (·.termination.partialFixpoint?)
   assert! preDefs.size = hints.size
   -- We check if any fixpoints were defined lattice-theoretically
@@ -90,13 +90,13 @@ def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do
       let type ← instantiateForall preDef.type xs
       let inst ←
         match hints[i]!.fixpointType with
-        | .greatestFixpoint =>
+        | .coinductiveFixpoint =>
           unless type.isProp do
-            throwError "`greatest_fixpoint` can be only used to define predicates"
+            throwError "`coinductive_fixpoint` can be only used to define predicates"
           pure (mkConst ``ReverseImplicationOrder.instCompleteLattice)
-        | .leastFixpoint =>
+        | .inductiveFixpoint =>
           unless type.isProp do
-            throwError "`least_fixpoint` can be only used to define predicates"
+            throwError "`inductive_fixpoint` can be only used to define predicates"
           pure (mkConst ``ImplicationOrder.instCompleteLattice)
         | .partialFixpoint => try
             synthInstance (← mkAppM ``CCPO #[type])
diff --git a/src/Lean/Elab/PreDefinition/TerminationHint.lean b/src/Lean/Elab/PreDefinition/TerminationHint.lean
index d54624d9bd..f756ead5b2 100644
--- a/src/Lean/Elab/PreDefinition/TerminationHint.lean
+++ b/src/Lean/Elab/PreDefinition/TerminationHint.lean
@@ -35,11 +35,11 @@ structure DecreasingBy where
 
 inductive PartialFixpointType where
   | partialFixpoint
-  | greatestFixpoint
-  | leastFixpoint
+  | coinductiveFixpoint
+  | inductiveFixpoint
   deriving Inhabited
 
-/-- A single `partial_fixpoint`, `greatest_fixpoint` or `least_fixpoint` clause -/
+/-- A single `partial_fixpoint`, `inductive_fixpoint` or `coinductive_fixpoint` clause -/
 structure PartialFixpoint where
   ref               : Syntax
   term?             : Option Term
@@ -69,20 +69,20 @@ structure TerminationHints where
   extraParams : Nat
   deriving Inhabited
 
-def isLeast : PartialFixpointType → Bool
-  | .leastFixpoint => true
+def isInductiveFixpoint : PartialFixpointType → Bool
+  | .inductiveFixpoint => true
   | _ => false
 
-def isGreatest : PartialFixpointType → Bool
-  | .greatestFixpoint => true
+def isCoinductiveFixpoint : PartialFixpointType → Bool
+  | .coinductiveFixpoint => true
   | _ => false
 
-def isPartial : PartialFixpointType → Bool
+def isPartialFixpoint : PartialFixpointType → Bool
   | .partialFixpoint => true
   | _ => false
 
-def isLatticeTheoretic (p : PartialFixpointType ) : Bool :=
-  isLeast p ∨ isGreatest p
+def isLatticeTheoretic (p : PartialFixpointType) : Bool :=
+  isInductiveFixpoint p ∨ isCoinductiveFixpoint p
 
 def TerminationHints.none : TerminationHints := ⟨.missing, .none, .none, .none, .none, 0⟩
 
@@ -99,8 +99,8 @@ def TerminationHints.ensureNone (hints : TerminationHints) (reason : String) : C
   | .none, .none, .none, .some partialFixpoint =>
     match partialFixpoint.fixpointType with
     | .partialFixpoint => logWarningAt partialFixpoint.ref m!"unused `partial_fixpoint`, function is {reason}"
-    | .greatestFixpoint => logWarningAt partialFixpoint.ref m!"unused `greatest_fixpoint`, function is {reason}"
-    | .leastFixpoint  => logWarningAt partialFixpoint.ref m!"unused `least_fixpoint`, function is {reason}"
+    | .coinductiveFixpoint => logWarningAt partialFixpoint.ref m!"unused `coinductive_fixpoint`, function is {reason}"
+    | .inductiveFixpoint  => logWarningAt partialFixpoint.ref m!"unused `inductive_fixpoint`, function is {reason}"
   | _, _, _, _=>
     logWarningAt hints.ref m!"unused termination hints, function is {reason}"
 
@@ -160,14 +160,14 @@ def elabTerminationHints {m} [Monad m] [MonadError m] (stx : TSyntax ``suffix) :
         pure (some {ref := t, structural := s.isSome, vars := #[], body})
       | `(terminationBy?|termination_by?) => pure none
       | `(partialFixpoint|partial_fixpoint $[monotonicity $_]?) => pure none
-      | `(greatestFixpoint|greatest_fixpoint $[monotonicity $_]?) => pure none
-      | `(leastFixpoint|least_fixpoint $[monotonicity $_]?) => pure none
+      | `(coinductiveFixpoint|coinductive_fixpoint $[monotonicity $_]?) => pure none
+      | `(inductiveFixpoint|inductive_fixpoint $[monotonicity $_]?) => pure none
       | _ => throwErrorAt t "unexpected `termination_by` syntax"
       else pure none
     let partialFixpoint? : Option PartialFixpoint ← if let some t := t? then match t with
       | `(partialFixpoint|partial_fixpoint $[monotonicity $term?]?) => pure (some {ref := t, term?, fixpointType := .partialFixpoint})
-      | `(greatestFixpoint|greatest_fixpoint $[monotonicity $term?]?) => pure (some {ref := t, term?, fixpointType := .greatestFixpoint})
-      | `(leastFixpoint|least_fixpoint $[monotonicity $term?]?) => pure (some {ref := t, term?, fixpointType := .leastFixpoint})
+      | `(coinductiveFixpoint|coinductive_fixpoint $[monotonicity $term?]?) => pure (some {ref := t, term?, fixpointType := .coinductiveFixpoint})
+      | `(inductiveFixpoint|inductive_fixpoint $[monotonicity $term?]?) => pure (some {ref := t, term?, fixpointType := .inductiveFixpoint})
       | _ => pure none
       else pure none
     let decreasingBy? ← d?.mapM fun d => match d with
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 022aec9729..58deaae2e3 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -802,9 +802,9 @@ The coinductive predicate is defined as the greatest fixed point of a monotone f
 By default, monotonicity is verified automatically. However, users can provide custom proofs
 of monotonicity if needed.
 -/
-def greatestFixpoint := leading_parser
+def coinductiveFixpoint := leading_parser
   withPosition (
-    "greatest_fixpoint" >>
+    "coinductive_fixpoint" >>
     optional (checkColGt "indentation" >> nonReservedSymbol "monotonicity " >>
               checkColGt "indented monotonicity proof" >> termParser))
 
@@ -819,9 +819,9 @@ The inductive predicate is defined as the least fixed point of a monotone functi
 By default, monotonicity is verified automatically. However, users can provide custom proofs
 of monotonicity if needed.
 -/
-def leastFixpoint := leading_parser
+def inductiveFixpoint := leading_parser
   withPosition (
-    "least_fixpoint" >>
+    "inductive_fixpoint" >>
     optional (checkColGt "indentation" >> nonReservedSymbol "monotonicity " >>
               checkColGt "indented monotonicity proof" >> termParser))
 
@@ -841,7 +841,7 @@ Forces the use of well-founded recursion and is hence incompatible with
 Termination hints are `termination_by` and `decreasing_by`, in that order.
 -/
 @[builtin_doc] def suffix := leading_parser
-  optional (ppDedent ppLine >> (terminationBy? <|> terminationBy <|> partialFixpoint <|> greatestFixpoint <|> leastFixpoint)) >> optional decreasingBy
+  optional (ppDedent ppLine >> (terminationBy? <|> terminationBy <|> partialFixpoint <|> coinductiveFixpoint <|> inductiveFixpoint)) >> optional decreasingBy
 
 end Termination
 namespace Term
diff --git a/tests/lean/run/coinductive_predicates.lean b/tests/lean/run/coinductive_predicates.lean
index 324cae7d73..1e5e8a1c0b 100644
--- a/tests/lean/run/coinductive_predicates.lean
+++ b/tests/lean/run/coinductive_predicates.lean
@@ -1,27 +1,25 @@
 -- Coinductive predicate definition
 def infseq {α} (R : α → α → Prop) : α → Prop :=
   λ x : α => ∃ y, R x y ∧ infseq R y
-  greatest_fixpoint
+  coinductive_fixpoint
 
 -- Application of the rewrite rule
 def infseq_fixpoint {α} (R : α → α → Prop) (x : α) :
   infseq R x = ∃ y, R x y ∧ infseq R y := by
     rw [infseq]
 
+#check infseq.coinduct
+
 -- The associated coinduction principle
-theorem infseq.coind {α} (h : α → Prop) (R : α → α → Prop)
-  (prem : ∀ (x : α), h x → ∃ y, R x y ∧ h y) : ∀ x, h x → infseq R x := by
-  apply infseq.fixpoint_induct
-  exact prem
 /--
-info: infseq.fixpoint_induct.{u_1} {α : Sort u_1} (R : α → α → Prop) (x : α → Prop)
-  (y : ∀ (x_1 : α), x x_1 → ∃ y, R x_1 y ∧ x y) (x✝ : α) : x x✝ → infseq R x✝
+info: infseq.coinduct.{u_1} {α : Sort u_1} (R : α → α → Prop) (x : α → Prop) (y : ∀ (x_1 : α), x x_1 → ∃ y, R x_1 y ∧ x y)
+  (x✝ : α) : x x✝ → infseq R x✝
 -/
-#guard_msgs in #check infseq.fixpoint_induct
+#guard_msgs in #check infseq.coinduct
 
 -- Simple proof by coinduction
 theorem cycle_infseq {R : α → α → Prop} (x : α) : R x x → infseq R x := by
-  apply @infseq.fixpoint_induct α R (λ m => R m m)
+  apply @infseq.coinduct α R (λ m => R m m)
   intro x _
   apply Exists.intro x
   trivial
@@ -34,13 +32,13 @@ inductive star (R : α → α → Prop) : α → α → Prop where
 -- Inductive predicate, as a least fixpoint
 def star_ind (tr : α → α → Prop) (q₁ q₂ : α) : Prop :=
  ∃ (z : α), q₁ = q₂ ∨ (tr q₁ z ∧ star_ind tr z q₂)
-least_fixpoint
+inductive_fixpoint
 
 /--
-info: star_ind.fixpoint_induct.{u_1} {α : Sort u_1} (tr : α → α → Prop) (q₂ : α) (x : α → Prop)
+info: star_ind.induct.{u_1} {α : Sort u_1} (tr : α → α → Prop) (q₂ : α) (x : α → Prop)
   (y : ∀ (x_1 : α), (∃ z, x_1 = q₂ ∨ tr x_1 z ∧ x z) → x x_1) (x✝ : α) : (fun q₁ => star_ind tr q₁ q₂) x✝ → x x✝
 -/
-#guard_msgs in #check star_ind.fixpoint_induct
+#guard_msgs in #check star_ind.induct
 
 -- From one you can prove the other
 theorem star_implies_star' (R : α → α → Prop) : ∀ a b : α, star R a b → star_ind R a b := by
@@ -109,7 +107,7 @@ def all_seq_inf (R : α → α → Prop) (x : α) : Prop :=
   ∀ y : α, star R x y → ∃ z, R y z
 
 def infseq_if_all_seq_inf (R : α → α → Prop) : ∀ x,  all_seq_inf R x → infseq R x := by
-  apply infseq.fixpoint_induct
+  apply infseq.coinduct
   intro x H
   unfold all_seq_inf at H
   have H' := H x (by simp [star.star_refl])
@@ -132,7 +130,7 @@ theorem infseq_coinduction_principle_2:
   ∀ (a : α), x a → infseq R a := by
     intro X
     intro h₁ a rel
-    apply @infseq.fixpoint_induct _ _ (fun a => ∃ b, star R a b ∧ X b)
+    apply @infseq.coinduct _ _ (fun a => ∃ b, star R a b ∧ X b)
     case x =>
       apply Exists.elim (h₁ a rel)
       intro a' ⟨h₁, h₂⟩
@@ -164,10 +162,10 @@ def language_equivalent (automaton : DFA Q A) (q₁ q₂ : Q)  : Prop :=
   let ⟨o₁, t₁⟩ := automaton q₁
   let ⟨o₂, t₂⟩ := automaton q₂
   o₁ = o₂ ∧ (∀ a : A, language_equivalent automaton (t₁ a) (t₂ a))
-greatest_fixpoint
+coinductive_fixpoint
 
 /--
-info: language_equivalent.fixpoint_induct {Q A : Type} (automaton : DFA Q A) (x : Q → Q → Prop)
+info: language_equivalent.coinduct {Q A : Type} (automaton : DFA Q A) (x : Q → Q → Prop)
   (y :
     ∀ (x_1 x_2 : Q),
       x x_1 x_2 →
@@ -175,17 +173,17 @@ info: language_equivalent.fixpoint_induct {Q A : Type} (automaton : DFA Q A) (x
   (x✝ x✝¹ : Q) : x x✝ x✝¹ → language_equivalent automaton x✝ x✝¹
 -/
 #guard_msgs in
-#check language_equivalent.fixpoint_induct
+#check language_equivalent.coinduct
 
 namespace mixed1
   mutual
     def tick : Prop :=
       ¬tock
-    greatest_fixpoint
+    coinductive_fixpoint
 
     def tock : Prop :=
       ¬tick
-    least_fixpoint
+    inductive_fixpoint
   end
 end mixed1
 
@@ -193,11 +191,11 @@ namespace mixed2
   mutual
     def tick : Prop :=
       ¬tock
-    greatest_fixpoint
+    inductive_fixpoint
 
     def tock : Prop :=
       ¬tick
-    least_fixpoint
+    coinductive_fixpoint
   end
 end mixed2
 
@@ -205,11 +203,11 @@ namespace mixed3
   mutual
     def tick : Prop :=
       tock → tick
-    greatest_fixpoint
+    coinductive_fixpoint
 
     def tock : Prop :=
       tick → tock
-    least_fixpoint
+    inductive_fixpoint
   end
 end mixed3
 
@@ -217,10 +215,10 @@ namespace mixed4
   mutual
     def tick : Prop :=
       tock → tick
-    least_fixpoint
+    inductive_fixpoint
 
     def tock : Prop :=
       tick → tock
-    greatest_fixpoint
+    coinductive_fixpoint
   end
 end mixed4
diff --git a/tests/lean/run/coinductive_predicates_errors.lean b/tests/lean/run/coinductive_predicates_errors.lean
index 045a98b407..3978e0e602 100644
--- a/tests/lean/run/coinductive_predicates_errors.lean
+++ b/tests/lean/run/coinductive_predicates_errors.lean
@@ -1,36 +1,36 @@
 /-!
-This file contains tests for typical mistakes one might do when using `least_fixpoint`/`greatest_fixpoint`/`partial_fixpoint` machinery, that is:
- - Try to use `greatest_fixpoint`/`least_fixpoint` to define functions instead of predicates
- - Apply `greatest_fixpoint`/`least_fixpoint` to non-recursive functions
- - Mix `partial_fixpoint` with `greatest_fixpoint`/`least_fixpoint` in the same clique
+This file contains tests for typical mistakes one might do when using `inductive_fixpoint`/`coinductive_fixpoint`/`partial_fixpoint` machinery, that is:
+ - Try to use `coinductive_fixpoint`/`inductive_fixpoint` to define functions instead of predicates
+ - Apply `coinductive_fixpoint`/`inductive_fixpoint` to non-recursive functions
+ - Mix `partial_fixpoint` with `coinductive_fixpoint`/`inductive_fixpoint` in the same clique
 -/
 
 /--
-error: `greatest_fixpoint` can be only used to define predicates
+error: `coinductive_fixpoint` can be only used to define predicates
 -/
 #guard_msgs in
 def f (x : Nat) : Nat :=
   f (x + 1)
-greatest_fixpoint
+coinductive_fixpoint
 
 /--
-error: `least_fixpoint` can be only used to define predicates
+error: `inductive_fixpoint` can be only used to define predicates
 -/
 #guard_msgs in
 def g (x : Nat) : Nat :=
   g (x + 1)
-least_fixpoint
+inductive_fixpoint
 
 /--
-warning: unused `greatest_fixpoint`, function is not recursive
+warning: unused `coinductive_fixpoint`, function is not recursive
 -/
 #guard_msgs in
 def h (x : Nat) : Prop := x > 42
-  greatest_fixpoint
+  coinductive_fixpoint
 
 /--
-warning: unused `least_fixpoint`, function is not recursive
+warning: unused `inductive_fixpoint`, function is not recursive
 -/
 #guard_msgs in
 def h' (x : Nat) : Prop := x > 42
-  least_fixpoint
+  inductive_fixpoint
diff --git a/tests/lean/run/issue8490.lean b/tests/lean/run/issue8490.lean
index c3c75dae0e..73e85c6127 100644
--- a/tests/lean/run/issue8490.lean
+++ b/tests/lean/run/issue8490.lean
@@ -10,7 +10,7 @@ def asimp_const : Aexp -> Aexp
 @[simp]
 def optimal' (a : Aexp) : Prop :=
   optimal' a ∧ True
-least_fixpoint
+inductive_fixpoint
 
 /-- info: Try this: simp_all only [asimp_const, reduceCtorEq] -/
 #guard_msgs in
diff --git a/tests/lean/run/mutual_termination_by_errors.lean b/tests/lean/run/mutual_termination_by_errors.lean
index 139027bd8c..359892252e 100644
--- a/tests/lean/run/mutual_termination_by_errors.lean
+++ b/tests/lean/run/mutual_termination_by_errors.lean
@@ -131,20 +131,20 @@ mutual
   partial_fixpoint
 
   def g (x : Nat) : Prop := f (x + 1)
-  least_fixpoint
+  inductive_fixpoint
 end
 end Test6
 
 
 namespace Test7
 /--
-error: Incompatible termination hint; this function is mutually recursive with Test7.f, which is marked as `greatest_fixpoint` so this one also needs to be marked `least_fixpoint` or `greatest_fixpoint`.
+error: Incompatible termination hint; this function is mutually recursive with Test7.f, which is marked as `coinductive_fixpoint` so this one also needs to be marked `inductive_fixpoint` or `coinductive_fixpoint`.
 -/
 #guard_msgs in
 mutual
   def f (x : Nat) : Prop :=
     g (x + 1)
-  greatest_fixpoint
+  coinductive_fixpoint
 
   def g (x : Nat) : Prop :=
     f (x + 1)
@@ -170,7 +170,7 @@ end Test8
 
 namespace Test9
 /--
-error: Incompatible termination hint; this function is mutually recursive with Test9.f, which is not also marked as `least_fixpoint` or `greatest_fixpoint`, so this one cannot be either.
+error: Incompatible termination hint; this function is mutually recursive with Test9.f, which is not also marked as `inductive_fixpoint` or `coinductive_fixpoint`, so this one cannot be either.
 -/
 #guard_msgs in
 mutual
@@ -180,19 +180,19 @@ mutual
 
   def g (x : Nat) : Prop :=
     f (x + 1)
-    least_fixpoint
+    inductive_fixpoint
 end
 end Test9
 
 namespace Test10
 /--
-error: Incompatible termination hint; this function is mutually recursive with Test10.f, which is marked as `greatest_fixpoint` so this one also needs to be marked `least_fixpoint` or `greatest_fixpoint`.
+error: Incompatible termination hint; this function is mutually recursive with Test10.f, which is marked as `coinductive_fixpoint` so this one also needs to be marked `inductive_fixpoint` or `coinductive_fixpoint`.
 -/
 #guard_msgs in
 mutual
   def f (x : Nat) : Prop :=
     g (x + 1)
-    greatest_fixpoint
+    coinductive_fixpoint
 
   def g (x : Nat) : Prop :=
     f (x + 1)
diff --git a/tests/lean/run/partial_fixpoint_prop.lean b/tests/lean/run/partial_fixpoint_prop.lean
index e28bc1d83a..186a93d800 100644
--- a/tests/lean/run/partial_fixpoint_prop.lean
+++ b/tests/lean/run/partial_fixpoint_prop.lean
@@ -5,11 +5,11 @@ Tests that `partial_fixpoint` is not picking up the partial order structure on P
 -- This works as `∨` is monotone in its arguments with respect to the (`ImplicationOrder`/`ReverseImplicationOrder` on `Prop`.
 def f (x : Nat) : Prop :=
   f (x + 1) ∨ f ( x + 2)
-  greatest_fixpoint
+  coinductive_fixpoint
 
 def f' (x : Nat) : Prop :=
   f' (x + 1) ∨ f' ( x + 2)
-  least_fixpoint
+  inductive_fixpoint
 
 /--
 error: Could not prove 'f''' to be monotone in its recursive calls: