-- Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
/-- If the sequence of ordinal-indexed approximations takes a value twice,
then it actually stabilised at that value. -/
lemma lfpApprox_mem_fixedPoints_of_eq {a b c : Ordinal}
    (h_init : x ≤ f x) (h_ab : a < b) (h_ac : a ≤ c) (h_fab : lfpApprox f x a = lfpApprox f x b) :
    lfpApprox f x c ∈ fixedPoints f

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
h_init : x ≤ f x
h_ab : a < b
h_ac : a ≤ c
h_fab : lfpApprox f x a = lfpApprox f x b
⊢ lfpApprox f x (a + 1) = lfpApprox f x a

Tactic:
exact Monotone.eq_of_le_of_le (lfpApprox_monotone f x)
  h_fab (SuccOrder.le_succ a) (SuccOrder.succ_le_of_lt h_ab)

Result:
no goals

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
h_init : x ≤ f x
h_ab : a < b
h_ac : a ≤ c
h_fab : lfpApprox f x a = lfpApprox f x b
lfpApprox_mem_fixedPoint : lfpApprox f x a ∈ fixedPoints ⇑f
⊢ lfpApprox f x c ∈ fixedPoints ⇑f

Tactic:
rw [lfpApprox_eq_of_mem_fixedPoints f x h_init]

Result:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
h_init : x ≤ f x
h_ab : a < b
h_ac : a ≤ c
h_fab : lfpApprox f x a = lfpApprox f x b
lfpApprox_mem_fixedPoint : lfpApprox f x a ∈ fixedPoints ⇑f
⊢ lfpApprox f x ?m.14454 ∈ fixedPoints ⇑f

case h_ab
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
h_init : x ≤ f x
h_ab : a < b
h_ac : a ≤ c
h_fab : lfpApprox f x a = lfpApprox f x b
lfpApprox_mem_fixedPoint : lfpApprox f x a ∈ fixedPoints ⇑f
⊢ ?m.14454 ≤ c

case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
h_init : x ≤ f x
h_ab : a < b
h_ac : a ≤ c
h_fab : lfpApprox f x a = lfpApprox f x b
lfpApprox_mem_fixedPoint : lfpApprox f x a ∈ fixedPoints ⇑f
⊢ lfpApprox f x ?m.14454 ∈ fixedPoints ⇑f

α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
h_init : x ≤ f x
h_ab : a < b
h_ac : a ≤ c
h_fab : lfpApprox f x a = lfpApprox f x b
lfpApprox_mem_fixedPoint : lfpApprox f x a ∈ fixedPoints ⇑f
⊢ Ordinal.{u}

Proof state:
case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
h_init : x ≤ f x
h_ab : a < b
h_ac : a ≤ c
h_fab : lfpApprox f x a = lfpApprox f x b
lfpApprox_mem_fixedPoint : lfpApprox f x a ∈ fixedPoints ⇑f
⊢ lfpApprox f x a ∈ fixedPoints ⇑f

Tactic:
exact lfpApprox_mem_fixedPoint

Result:
no goals

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
h_init : x ≤ f x
h_ab : a < b
h_ac : a ≤ c
h_fab : lfpApprox f x a = lfpApprox f x b
⊢ lfpApprox f x c ∈ fixedPoints ⇑f

Tactic:
have lfpApprox_mem_fixedPoint :
    lfpApprox f x a ∈ fixedPoints f := by
  rw [mem_fixedPoints_iff, ← lfpApprox_add_one f x h_init]
  exact Monotone.eq_of_le_of_le (lfpApprox_monotone f x)
    h_fab (SuccOrder.le_succ a) (SuccOrder.succ_le_of_lt h_ab)

Result:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
h_init : x ≤ f x
h_ab : a < b
h_ac : a ≤ c
h_fab : lfpApprox f x a = lfpApprox f x b
lfpApprox_mem_fixedPoint : lfpApprox f x a ∈ fixedPoints ⇑f
⊢ lfpApprox f x c ∈ fixedPoints ⇑f

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
h_init : x ≤ f x
h_ab : a < b
h_ac : a ≤ c
h_fab : lfpApprox f x a = lfpApprox f x b
lfpApprox_mem_fixedPoint : lfpApprox f x a ∈ fixedPoints ⇑f
⊢ lfpApprox f x ?m.14454 ∈ fixedPoints ⇑f

Tactic:
exact lfpApprox_mem_fixedPoint

Result:
no goals

Proof state:
case h_ab
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
h_init : x ≤ f x
h_ab : a < b
h_ac : a ≤ c
h_fab : lfpApprox f x a = lfpApprox f x b
lfpApprox_mem_fixedPoint : lfpApprox f x a ∈ fixedPoints ⇑f
⊢ a ≤ c

Tactic:
exact h_ac

Result:
no goals

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
h_init : x ≤ f x
h_ab : a < b
h_ac : a ≤ c
h_fab : lfpApprox f x a = lfpApprox f x b
⊢ lfpApprox f x a ∈ fixedPoints ⇑f

Tactic:
rw [mem_fixedPoints_iff, ← lfpApprox_add_one f x h_init]

Result:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b c : Ordinal.{u}
h_init : x ≤ f x
h_ab : a < b
h_ac : a ≤ c
h_fab : lfpApprox f x a = lfpApprox f x b
⊢ lfpApprox f x (a + 1) = lfpApprox f x a