-- Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
theorem lfpApprox_add_one (h : x ≤ f x) (a : Ordinal) :
    lfpApprox f x (a+1) = f (lfpApprox f x a)

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

Tactic:
apply le_sSup

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

Proof state:
case a.a.h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h : x ≤ f x
a : Ordinal.{u}
⊢ ∃ b ≤ a, f (lfpApprox f x b) = f (lfpApprox f x a)

Tactic:
use a

Result:
no goals

Proof state:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h : x ≤ f x
a : Ordinal.{u}
⊢ lfpApprox f x (a + 1) ≤ f (lfpApprox f x a)

Tactic:
conv => left; rw [lfpApprox]

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

Proof state:
case a.a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h : x ≤ f x
a : Ordinal.{u}
⊢ f (lfpApprox f x a) ∈ {x_1 | ∃ b ≤ a, f (lfpApprox f x b) = x_1} ∨ f (lfpApprox f x a) ∈ {x}

Tactic:
apply Or.inl

Result:
case a.a.h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h : x ≤ f x
a : Ordinal.{u}
⊢ f (lfpApprox f x a) ∈ {x_1 | ∃ b ≤ a, f (lfpApprox f x b) = x_1}

Proof state:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h : x ≤ f x
a : Ordinal.{u}
⊢ f (lfpApprox f x a) ≤ lfpApprox f x (a + 1)

Tactic:
conv => right; rw [lfpApprox]

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

Proof state:
case a.a.right
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h✝ : x ≤ f x
a a' : Ordinal.{u}
h : a' ≤ a
⊢ f (lfpApprox f x a') ≤ f (lfpApprox f x a)

Tactic:
apply f.2

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

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

Tactic:
simp only [Ordinal.add_one_eq_succ, lt_succ_iff, exists_prop]

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

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h : x ≤ f x
a : Ordinal.{u}
⊢ lfpApprox f x (a + 1) = f (lfpApprox f x a)

Tactic:
apply le_antisymm

Result:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h : x ≤ f x
a : Ordinal.{u}
⊢ lfpApprox f x (a + 1) ≤ f (lfpApprox f x a)

case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h : x ≤ f x
a : Ordinal.{u}
⊢ f (lfpApprox f x a) ≤ lfpApprox f x (a + 1)

Proof state:
case a.a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h : x ≤ f x
a : Ordinal.{u}
⊢ x ≤ f (lfpApprox f x a) ∧ ∀ a_1 ≤ a, f (lfpApprox f x a_1) ≤ f (lfpApprox f x a)

Tactic:
apply And.intro

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

case a.a.right
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h : x ≤ f x
a : Ordinal.{u}
⊢ ∀ a_1 ≤ a, f (lfpApprox f x a_1) ≤ f (lfpApprox f x a)

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

Tactic:
apply sSup_le

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

Proof state:
case a.a.h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h : x ≤ f x
a : Ordinal.{u}
⊢ f (lfpApprox f x a) ∈ {x_1 | ∃ b ≤ a, f (lfpApprox f x b) = x_1}

Tactic:
simp only [Set.mem_setOf_eq]

Result:
case a.a.h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h : x ≤ f x
a : Ordinal.{u}
⊢ ∃ b ≤ a, f (lfpApprox f x b) = f (lfpApprox f x a)

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

Tactic:
rw [Set.mem_union]

Result:
case a.a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h : x ≤ f x
a : Ordinal.{u}
⊢ f (lfpApprox f x a) ∈ {x_1 | ∃ b ≤ a, f (lfpApprox f x b) = x_1} ∨ f (lfpApprox f x a) ∈ {x}

Proof state:
case a.a.left
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h : x ≤ f x
a : Ordinal.{u}
⊢ f x ≤ f (lfpApprox f x a)

Tactic:
apply Monotone.imp f.monotone

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

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

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

Result:
case a.a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h : x ≤ f x
a : Ordinal.{u}
⊢ x ≤ f (lfpApprox f x a) ∧ ∀ a_1 ≤ a, f (lfpApprox f x a_1) ≤ f (lfpApprox f x a)

Proof state:
case a.a.right.a.a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h✝ : x ≤ f x
a a' : Ordinal.{u}
h : a' ≤ a
⊢ a' ≤ a

Tactic:
exact h

Result:
no goals

Proof state:
case a.a.left
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h : x ≤ f x
a : Ordinal.{u}
⊢ x ≤ lfpApprox f x a

Tactic:
exact le_lfpApprox f x

Result:
no goals

Proof state:
case a.a.left
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h : x ≤ f x
a : Ordinal.{u}
⊢ x ≤ f (lfpApprox f x a)

Tactic:
apply le_trans h

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

Proof state:
case a.a.right
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h : x ≤ f x
a : Ordinal.{u}
⊢ ∀ a_1 ≤ a, f (lfpApprox f x a_1) ≤ f (lfpApprox f x a)

Tactic:
intros a' h

Result:
case a.a.right
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h✝ : x ≤ f x
a a' : Ordinal.{u}
h : a' ≤ a
⊢ f (lfpApprox f x a') ≤ f (lfpApprox f x a)

Proof state:
case a.a.right.a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h✝ : x ≤ f x
a a' : Ordinal.{u}
h : a' ≤ a
⊢ lfpApprox f x a' ≤ lfpApprox f x a

Tactic:
apply lfpApprox_monotone

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