-- Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
theorem lfpApprox_eq_of_mem_fixedPoints {a b : Ordinal} (h_init : x ≤ f x) (h_ab : a ≤ b)
    (h : lfpApprox f x a ∈ fixedPoints f) : lfpApprox f x b = lfpApprox f x a

Proof state:
case pos
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
h_init : x ≤ f x
h : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ k < b, a ≤ k → lfpApprox f x k = lfpApprox f x a
h_ab : a ≤ b
a' : Ordinal.{u}
ha'b : a' < b
haa : a' < a
⊢ lfpApprox f x (a' + 1) ≤ lfpApprox f x a

Tactic:
apply lfpApprox_monotone

Result:
case pos.a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
h_init : x ≤ f x
h : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ k < b, a ≤ k → lfpApprox f x k = lfpApprox f x a
h_ab : a ≤ b
a' : Ordinal.{u}
ha'b : a' < b
haa : a' < a
⊢ a' + 1 ≤ a

Proof state:
case pos.a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
h_init : x ≤ f x
h : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ k < b, a ≤ k → lfpApprox f x k = lfpApprox f x a
h_ab : a ≤ b
a' : Ordinal.{u}
ha'b : a' < b
haa : a' < a
⊢ a' + 1 ≤ a

Tactic:
simp only [Ordinal.add_one_eq_succ, succ_le_iff]

Result:
case pos.a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
h_init : x ≤ f x
h : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ k < b, a ≤ k → lfpApprox f x k = lfpApprox f x a
h_ab : a ≤ b
a' : Ordinal.{u}
ha'b : a' < b
haa : a' < a
⊢ a' < a

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

Tactic:
apply le_antisymm

Result:
case h.a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
h_init : x ≤ f x
h : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ k < b, a ≤ k → lfpApprox f x k = lfpApprox f x a
h_ab : a ≤ b
⊢ lfpApprox f x b ≤ lfpApprox f x a

case h.a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
h_init : x ≤ f x
h : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ k < b, a ≤ k → lfpApprox f x k = lfpApprox f x a
h_ab : a ≤ b
⊢ lfpApprox f x a ≤ lfpApprox f x b

Proof state:
case pos.a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
h_init : x ≤ f x
h : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ k < b, a ≤ k → lfpApprox f x k = lfpApprox f x a
h_ab : a ≤ b
a' : Ordinal.{u}
ha'b : a' < b
haa : a' < a
⊢ a' < a

Tactic:
exact haa

Result:
no goals

Proof state:
case h.a.a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
h_init : x ≤ f x
h : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ k < b, a ≤ k → lfpApprox f x k = lfpApprox f x a
h_ab : a ≤ b
a' : Ordinal.{u}
ha'b : a' < b
⊢ f (lfpApprox f x a') ≤ lfpApprox f x a

Tactic:
by_cases haa : a' < a

Result:
case pos
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
h_init : x ≤ f x
h : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ k < b, a ≤ k → lfpApprox f x k = lfpApprox f x a
h_ab : a ≤ b
a' : Ordinal.{u}
ha'b : a' < b
haa : a' < a
⊢ f (lfpApprox f x a') ≤ lfpApprox f x a

case neg
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
h_init : x ≤ f x
h : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ k < b, a ≤ k → lfpApprox f x k = lfpApprox f x a
h_ab : a ≤ b
a' : Ordinal.{u}
ha'b : a' < b
haa : ¬a' < a
⊢ f (lfpApprox f x a') ≤ lfpApprox f x a

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

Tactic:
simp only [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 h.a.a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
h_init : x ≤ f x
h : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ k < b, a ≤ k → lfpApprox f x k = lfpApprox f x a
h_ab : a ≤ b
⊢ x ≤ lfpApprox f x a ∧ ∀ a_1 < b, f (lfpApprox f x a_1) ≤ lfpApprox f x a

Proof state:
case pos
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
h_init : x ≤ f x
h : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ k < b, a ≤ k → lfpApprox f x k = lfpApprox f x a
h_ab : a ≤ b
a' : Ordinal.{u}
ha'b : a' < b
haa : a' < a
⊢ f (lfpApprox f x a') ≤ lfpApprox f x a

Tactic:
rw [← lfpApprox_add_one f x h_init]

Result:
case pos
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
h_init : x ≤ f x
h : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ k < b, a ≤ k → lfpApprox f x k = lfpApprox f x a
h_ab : a ≤ b
a' : Ordinal.{u}
ha'b : a' < b
haa : a' < a
⊢ lfpApprox f x (a' + 1) ≤ lfpApprox f x a

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

Tactic:
apply sSup_le

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

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

Tactic:
exact lfpApprox_monotone f x h_ab

Result:
no goals

Proof state:
case h.a.a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
h_init : x ≤ f x
h : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ k < b, a ≤ k → lfpApprox f x k = lfpApprox f x a
h_ab : a ≤ b
⊢ ∀ a_1 < b, f (lfpApprox f x a_1) ≤ lfpApprox f x a

Tactic:
intro a' ha'b

Result:
case h.a.a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
h_init : x ≤ f x
h : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ k < b, a ≤ k → lfpApprox f x k = lfpApprox f x a
h_ab : a ≤ b
a' : Ordinal.{u}
ha'b : a' < b
⊢ f (lfpApprox f x a') ≤ lfpApprox f x a

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
h_init : x ≤ f x
h_ab : a ≤ b
h : lfpApprox f x a ∈ fixedPoints ⇑f
⊢ lfpApprox f x b = lfpApprox f x a

Tactic:
rw [mem_fixedPoints_iff] at h

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

Proof state:
case neg
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
h_init : x ≤ f x
h : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ k < b, a ≤ k → lfpApprox f x k = lfpApprox f x a
h_ab : a ≤ b
a' : Ordinal.{u}
ha'b : a' < b
haa : ¬a' < a
⊢ f (lfpApprox f x a') ≤ lfpApprox f x a

Tactic:
rw [IH a' ha'b (le_of_not_lt haa), h]

Result:
no goals