-- Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
theorem lfpApprox_ord_eq_lfp : lfpApprox f ⊥ (ord <| succ #α) = f.lfp

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ lfpApprox f ⊥ (succ #α).ord = lfp f

Tactic:
apply le_antisymm

Result:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ lfpApprox f ⊥ (succ #α).ord ≤ lfp f

case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ lfp f ≤ lfpApprox f ⊥ (succ #α).ord

Proof state:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h_fix : ∃ y, lfpApprox f ⊥ (succ #α).ord = ↑y
x : ↑(fixedPoints ⇑f)
h_x : lfpApprox f ⊥ (succ #α).ord = ↑x
⊢ lfp f ≤ ↑x

Tactic:
exact lfp_le_fixed f x.prop

Result:
no goals

Proof state:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h_fix : ∃ y, lfpApprox f ⊥ (succ #α).ord = ↑y
x : ↑(fixedPoints ⇑f)
h_x : lfpApprox f ⊥ (succ #α).ord = ↑x
⊢ lfp f ≤ lfpApprox f ⊥ (succ #α).ord

Tactic:
rw [h_x]

Result:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h_fix : ∃ y, lfpApprox f ⊥ (succ #α).ord = ↑y
x : ↑(fixedPoints ⇑f)
h_x : lfpApprox f ⊥ (succ #α).ord = ↑x
⊢ lfp f ≤ ↑x

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ ∃ y, lfpApprox f ⊥ (succ #α).ord = ↑y

Tactic:
simpa only [Subtype.exists, mem_fixedPoints, exists_prop, exists_eq_right'] using
  lfpApprox_ord_mem_fixedPoint f ⊥ bot_le

Result:
no goals

Proof state:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h_lfp : ∃ y, lfp f = ↑y
⊢ lfpApprox f ⊥ (succ #α).ord ≤ lfp f

Tactic:
let ⟨y, h_y⟩ := h_lfp

Result:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h_lfp : ∃ y, lfp f = ↑y
y : ↑(fixedPoints ⇑f)
h_y : lfp f = ↑y
⊢ lfpApprox f ⊥ (succ #α).ord ≤ lfp f

Proof state:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h_fix : ∃ y, lfpApprox f ⊥ (succ #α).ord = ↑y
⊢ lfp f ≤ lfpApprox f ⊥ (succ #α).ord

Tactic:
let ⟨x, h_x⟩ := h_fix

Result:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h_fix : ∃ y, lfpApprox f ⊥ (succ #α).ord = ↑y
x : ↑(fixedPoints ⇑f)
h_x : lfpApprox f ⊥ (succ #α).ord = ↑x
⊢ lfp f ≤ lfpApprox f ⊥ (succ #α).ord

Proof state:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h_lfp : ∃ y, lfp f = ↑y
y : ↑(fixedPoints ⇑f)
h_y : lfp f = ↑y
⊢ lfpApprox f ⊥ (succ #α).ord ≤ ↑y

Tactic:
exact lfpApprox_le_of_mem_fixedPoints f ⊥ y.2 bot_le (ord <| succ #α)

Result:
no goals

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ ∃ y, lfp f = ↑y

Tactic:
use ⊥

Result:
case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ lfp f = ↑⊥

Proof state:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ lfpApprox f ⊥ (succ #α).ord ≤ lfp f

Tactic:
have h_lfp : ∃ y : fixedPoints f, f.lfp = y := by use ⊥; exact rfl

Result:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h_lfp : ∃ y, lfp f = ↑y
⊢ lfpApprox f ⊥ (succ #α).ord ≤ lfp f

Proof state:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ lfp f ≤ lfpApprox f ⊥ (succ #α).ord

Tactic:
have h_fix : ∃ y : fixedPoints f, lfpApprox f ⊥ (ord <| succ #α) = y := by
  simpa only [Subtype.exists, mem_fixedPoints, exists_prop, exists_eq_right'] using
    lfpApprox_ord_mem_fixedPoint f ⊥ bot_le

Result:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h_fix : ∃ y, lfpApprox f ⊥ (succ #α).ord = ↑y
⊢ lfp f ≤ lfpApprox f ⊥ (succ #α).ord

Proof state:
case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ lfp f = ↑⊥

Tactic:
exact rfl

Result:
no goals

Proof state:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h_lfp : ∃ y, lfp f = ↑y
y : ↑(fixedPoints ⇑f)
h_y : lfp f = ↑y
⊢ lfpApprox f ⊥ (succ #α).ord ≤ lfp f

Tactic:
rw [h_y]

Result:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h_lfp : ∃ y, lfp f = ↑y
y : ↑(fixedPoints ⇑f)
h_y : lfp f = ↑y
⊢ lfpApprox f ⊥ (succ #α).ord ≤ ↑y