-- Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
theorem lfpApprox_mono_mid : Monotone (lfpApprox f)

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

Tactic:
exact le_sup_of_le_left h

Result:
no goals

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

Tactic:
intro i' h_i'

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

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

Tactic:
rw [lfpApprox, lfpApprox]

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

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

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

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

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ Monotone (lfpApprox f)

Tactic:
intro x₁ x₂ h a

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

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

Tactic:
use i'

Result:
no goals

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

Tactic:
apply le_sSup_of_le

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

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

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

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

Tactic:
constructor

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

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

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

Tactic:
exact f.monotone (ih i' h_i')

Result:
no goals

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

Tactic:
apply le_sup_of_le_right

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

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

Tactic:
apply sSup_le

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