-- Mathlib/Control/LawfulFix.lean
theorem fix_eq_ωSup : Part.fix f = ωSup (approxChain f)

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ Part.fix (⇑f) x ≤ ?m.8712

Tactic:
apply hx

Result:
no goals

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ∀ (i : ℕ), (approxChain f) i ≤ Part.fix ⇑f

Tactic:
simp only [Fix.approxChain, OrderHom.coe_mk]

Result:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ∀ (i : ℕ), { toFun := approx ⇑f, monotone' := ⋯ } i ≤ Part.fix ⇑f

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ Part.fix (⇑f) x ≤ approx (⇑f) i.succ x

Tactic:
trans

Result:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ Part.fix (⇑f) x ≤ ?m.8712

α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ ?m.8712 ≤ approx (⇑f) i.succ x

α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ Part (β x)

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ approx (⇑f) i.succ x ≤ ωSup (approxChain f) x

Tactic:
apply le_ωSup_of_le i.succ

Result:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ approx (⇑f) i.succ x ≤ ((approxChain f).map (Pi.evalOrderHom x)) i.succ

Proof state:
case a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ωSup (approxChain f) ≤ Part.fix ⇑f

Tactic:
apply ωSup_le _ _ _

Result:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ∀ (i : ℕ), (approxChain f) i ≤ Part.fix ⇑f

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ Part.fix ⇑f = ωSup (approxChain f)

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ Part.fix ⇑f ≤ ωSup (approxChain f)

case a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ωSup (approxChain f) ≤ Part.fix ⇑f

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ approx (⇑f) i x ≤ approx (⇑f) i.succ x

Tactic:
apply approx_mono' f

Result:
no goals

Proof state:
case a.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ Part.fix (⇑f) x ≤ ωSup (approxChain f) x

Tactic:
trans approx f i.succ x

Result:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ Part.fix (⇑f) x ≤ approx (⇑f) i.succ x

α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ approx (⇑f) i.succ x ≤ ωSup (approxChain f) x

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ approx (⇑f) i.succ x ≤ ((approxChain f).map (Pi.evalOrderHom x)) i.succ

Tactic:
dsimp [approx]

Result:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ f (approx (⇑f) i) x ≤ (approxChain f) (i + 1) x

Proof state:
case a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
⊢ Part.fix (⇑f) x ≤ ωSup (approxChain f) x

Tactic:
obtain ⟨i, hx⟩ := exists_fix_le_approx f x

Result:
case a.intro
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ Part.fix (⇑f) x ≤ ωSup (approxChain f) x

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ f (approx (⇑f) i) x ≤ (approxChain f) (i + 1) x

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
y : ℕ
x : α
⊢ { toFun := approx ⇑f, monotone' := ⋯ } y x ≤ Part.fix (⇑f) x

Tactic:
apply approx_le_fix f

Result:
no goals

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ∀ (i : ℕ), { toFun := approx ⇑f, monotone' := ⋯ } i ≤ Part.fix ⇑f

Tactic:
intro y x

Result:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
y : ℕ
x : α
⊢ { toFun := approx ⇑f, monotone' := ⋯ } y x ≤ Part.fix (⇑f) x

Proof state:
case a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ Part.fix ⇑f ≤ ωSup (approxChain f)

Tactic:
intro x

Result:
case a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
⊢ Part.fix (⇑f) x ≤ ωSup (approxChain f) x