-- Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
theorem lfpApprox_mono_left : Monotone (lfpApprox : (α →o α) → _)

Proof state:
case h.a
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
ih : ∀ k < i, lfpApprox f x k ≤ lfpApprox g x k
⊢ ∀ a < i, f (lfpApprox f x a) ≤ x ⊔ sSup {x_1 | ∃ b < i, g (lfpApprox g x b) = x_1}

Tactic:
intro i' h_lt

Result:
case h.a
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
ih : ∀ k < i, lfpApprox f x k ≤ lfpApprox g x k
i' : Ordinal.{u}
h_lt : i' < i
⊢ f (lfpApprox f x i') ≤ x ⊔ sSup {x_1 | ∃ b < i, g (lfpApprox g x b) = x_1}

Proof state:
case h
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
ih : ∀ k < i, lfpApprox f x k ≤ lfpApprox g x k
⊢ lfpApprox f x i ≤ lfpApprox g x i

Tactic:
rw [lfpApprox, lfpApprox]

Result:
case h
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
ih : ∀ k < i, lfpApprox f x k ≤ lfpApprox g x k
⊢ sSup ({x_1 | ∃ b, ∃ (_ : b < i), f (lfpApprox f x b) = x_1} ∪ {x}) ≤
    sSup ({x_1 | ∃ b, ∃ (_ : b < i), g (lfpApprox g x b) = x_1} ∪ {x})

Proof state:
case h
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
ih : ∀ k < i, lfpApprox f x k ≤ lfpApprox g x k
⊢ sSup ({x_1 | ∃ b, ∃ (_ : b < i), f (lfpApprox f x b) = x_1} ∪ {x}) ≤
    sSup ({x_1 | ∃ b, ∃ (_ : b < i), g (lfpApprox g x b) = x_1} ∪ {x})

Tactic:
apply sSup_le

Result:
case h.a
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
ih : ∀ k < i, lfpApprox f x k ≤ lfpApprox g x k
⊢ ∀ b ∈ {x_1 | ∃ b, ∃ (_ : b < i), f (lfpApprox f x b) = x_1} ∪ {x},
    b ≤ sSup ({x_1 | ∃ b, ∃ (_ : b < i), g (lfpApprox g x b) = x_1} ∪ {x})

Proof state:
case h.a.h.hb
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
ih : ∀ k < i, lfpApprox f x k ≤ lfpApprox g x k
i' : Ordinal.{u}
h_lt : i' < i
⊢ ?h.a.h.b ∈ {x_1 | ∃ b < i, g (lfpApprox g x b) = x_1}

Tactic:
use i'

Result:
no goals

Proof state:
case h.a
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
ih : ∀ k < i, lfpApprox f x k ≤ lfpApprox g x k
⊢ ∀ b ∈ {x_1 | ∃ b, ∃ (_ : b < i), f (lfpApprox f x b) = x_1} ∪ {x},
    b ≤ sSup ({x_1 | ∃ b, ∃ (_ : b < i), g (lfpApprox g x b) = x_1} ∪ {x})

Tactic:
simp only [exists_prop, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq, sSup_insert,
  forall_eq_or_imp, le_sup_left, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
  true_and]

Result:
case h.a
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
ih : ∀ k < i, lfpApprox f x k ≤ lfpApprox g x k
⊢ ∀ a < i, f (lfpApprox f x a) ≤ x ⊔ sSup {x_1 | ∃ b < i, g (lfpApprox g x b) = x_1}

Proof state:
α : Type u
inst✝ : CompleteLattice α
⊢ Monotone lfpApprox

Tactic:
intro f g h x a

Result:
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
a : Ordinal.{u}
⊢ lfpApprox f x a ≤ lfpApprox g x a

Proof state:
case h.a.h.h
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
ih : ∀ k < i, lfpApprox f x k ≤ lfpApprox g x k
i' : Ordinal.{u}
h_lt : i' < i
⊢ g (lfpApprox f x i') ≤ g (lfpApprox g x i')

Tactic:
exact g.monotone (ih i' h_lt)

Result:
no goals

Proof state:
case h.a.h.h
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
ih : ∀ k < i, lfpApprox f x k ≤ lfpApprox g x k
i' : Ordinal.{u}
h_lt : i' < i
⊢ g.toFun (lfpApprox f x i') ≤ g (lfpApprox g x i')

Tactic:
simp only [OrderHom.toFun_eq_coe]

Result:
case h.a.h.h
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
ih : ∀ k < i, lfpApprox f x k ≤ lfpApprox g x k
i' : Ordinal.{u}
h_lt : i' < i
⊢ g (lfpApprox f x i') ≤ g (lfpApprox g x i')

Proof state:
case h.a.h.h
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
ih : ∀ k < i, lfpApprox f x k ≤ lfpApprox g x k
i' : Ordinal.{u}
h_lt : i' < i
⊢ f (lfpApprox f x i') ≤ g (lfpApprox g x i')

Tactic:
apply le_trans (h _)

Result:
case h.a.h.h
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
ih : ∀ k < i, lfpApprox f x k ≤ lfpApprox g x k
i' : Ordinal.{u}
h_lt : i' < i
⊢ g.toFun (lfpApprox f x i') ≤ g (lfpApprox g x i')

Proof state:
case h.a.h
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
ih : ∀ k < i, lfpApprox f x k ≤ lfpApprox g x k
i' : Ordinal.{u}
h_lt : i' < i
⊢ f (lfpApprox f x i') ≤ sSup {x_1 | ∃ b < i, g (lfpApprox g x b) = x_1}

Tactic:
apply le_sSup_of_le

Result:
case h.a.h.hb
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
ih : ∀ k < i, lfpApprox f x k ≤ lfpApprox g x k
i' : Ordinal.{u}
h_lt : i' < i
⊢ ?h.a.h.b ∈ {x_1 | ∃ b < i, g (lfpApprox g x b) = x_1}

case h.a.h.h
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
ih : ∀ k < i, lfpApprox f x k ≤ lfpApprox g x k
i' : Ordinal.{u}
h_lt : i' < i
⊢ f (lfpApprox f x i') ≤ ?h.a.h.b

case h.a.h.b
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
ih : ∀ k < i, lfpApprox f x k ≤ lfpApprox g x k
i' : Ordinal.{u}
h_lt : i' < i
⊢ α

Proof state:
case h.a
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
ih : ∀ k < i, lfpApprox f x k ≤ lfpApprox g x k
i' : Ordinal.{u}
h_lt : i' < i
⊢ f (lfpApprox f x i') ≤ x ⊔ sSup {x_1 | ∃ b < i, g (lfpApprox g x b) = x_1}

Tactic:
apply le_sup_of_le_right

Result:
case h.a.h
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
ih : ∀ k < i, lfpApprox f x k ≤ lfpApprox g x k
i' : Ordinal.{u}
h_lt : i' < i
⊢ f (lfpApprox f x i') ≤ sSup {x_1 | ∃ b < i, g (lfpApprox g x b) = x_1}