-- Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
theorem lfpApprox_le_of_mem_fixedPoints {a : α}
    (h_a : a ∈ fixedPoints f) (h_le_init : x ≤ a) (i : Ordinal) : lfpApprox f x i ≤ a

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

Tactic:
apply sSup_le

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

Proof state:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
h_a : a ∈ fixedPoints ⇑f
h_le_init : x ≤ a
i : Ordinal.{u}
⊢ lfpApprox f x i ≤ a

Tactic:
induction i using Ordinal.induction with
| h i IH =>
  rw [lfpApprox]
  apply sSup_le
  simp only [exists_prop]
  intro y h_y
  simp only [Set.mem_union, Set.mem_setOf_eq, Set.mem_singleton_iff] at h_y
  cases h_y with
  | inl h_y =>
    let ⟨j, h_j_lt, h_j⟩ := h_y
    rw [← h_j, ← h_a]
    exact f.monotone' (IH j h_j_lt)
  | inr h_y =>
    rw [h_y]
    exact h_le_init

Result:
no goals

Proof state:
case h.a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
h_a : a ∈ fixedPoints ⇑f
h_le_init : x ≤ a
i : Ordinal.{u}
IH : ∀ k < i, lfpApprox f x k ≤ a
y : α
h_y : y ∈ {x_1 | ∃ b < i, f (lfpApprox f x b) = x_1} ∪ {x}
⊢ y ≤ a

Tactic:
simp only [Set.mem_union, Set.mem_setOf_eq, Set.mem_singleton_iff] at h_y

Result:
case h.a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
h_a : a ∈ fixedPoints ⇑f
h_le_init : x ≤ a
i : Ordinal.{u}
IH : ∀ k < i, lfpApprox f x k ≤ a
y : α
h_y : (∃ b < i, f (lfpApprox f x b) = y) ∨ y = x
⊢ y ≤ a

Proof state:
case h.a.inl
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
h_a : a ∈ fixedPoints ⇑f
h_le_init : x ≤ a
i : Ordinal.{u}
IH : ∀ k < i, lfpApprox f x k ≤ a
y : α
h_y : ∃ b < i, f (lfpApprox f x b) = y
j : Ordinal.{u}
h_j_lt : j < i
h_j : f (lfpApprox f x j) = y
⊢ y ≤ a

Tactic:
rw [← h_j, ← h_a]

Result:
case h.a.inl
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
h_a : a ∈ fixedPoints ⇑f
h_le_init : x ≤ a
i : Ordinal.{u}
IH : ∀ k < i, lfpApprox f x k ≤ a
y : α
h_y : ∃ b < i, f (lfpApprox f x b) = y
j : Ordinal.{u}
h_j_lt : j < i
h_j : f (lfpApprox f x j) = y
⊢ f (lfpApprox f x j) ≤ f a

Proof state:
case h.a.inl
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
h_a : a ∈ fixedPoints ⇑f
h_le_init : x ≤ a
i : Ordinal.{u}
IH : ∀ k < i, lfpApprox f x k ≤ a
y : α
h_y : ∃ b < i, f (lfpApprox f x b) = y
⊢ y ≤ a

Tactic:
let ⟨j, h_j_lt, h_j⟩ := h_y

Result:
case h.a.inl
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
h_a : a ∈ fixedPoints ⇑f
h_le_init : x ≤ a
i : Ordinal.{u}
IH : ∀ k < i, lfpApprox f x k ≤ a
y : α
h_y : ∃ b < i, f (lfpApprox f x b) = y
j : Ordinal.{u}
h_j_lt : j < i
h_j : f (lfpApprox f x j) = y
⊢ y ≤ a

Proof state:
case h.a.inl
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
h_a : a ∈ fixedPoints ⇑f
h_le_init : x ≤ a
i : Ordinal.{u}
IH : ∀ k < i, lfpApprox f x k ≤ a
y : α
h_y : ∃ b < i, f (lfpApprox f x b) = y
j : Ordinal.{u}
h_j_lt : j < i
h_j : f (lfpApprox f x j) = y
⊢ f (lfpApprox f x j) ≤ f a

Tactic:
exact f.monotone' (IH j h_j_lt)

Result:
no goals

Proof state:
case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
h_a : a ∈ fixedPoints ⇑f
h_le_init : x ≤ a
i : Ordinal.{u}
IH : ∀ k < i, lfpApprox f x k ≤ a
⊢ lfpApprox f x i ≤ a

Tactic:
rw [lfpApprox]

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

Proof state:
case h.a.inr
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
h_a : a ∈ fixedPoints ⇑f
h_le_init : x ≤ a
i : Ordinal.{u}
IH : ∀ k < i, lfpApprox f x k ≤ a
y : α
h_y : y = x
⊢ x ≤ a

Tactic:
exact h_le_init

Result:
no goals

Proof state:
case h.a.inr
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
h_a : a ∈ fixedPoints ⇑f
h_le_init : x ≤ a
i : Ordinal.{u}
IH : ∀ k < i, lfpApprox f x k ≤ a
y : α
h_y : y = x
⊢ y ≤ a

Tactic:
rw [h_y]

Result:
case h.a.inr
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
h_a : a ∈ fixedPoints ⇑f
h_le_init : x ≤ a
i : Ordinal.{u}
IH : ∀ k < i, lfpApprox f x k ≤ a
y : α
h_y : y = x
⊢ x ≤ a

Proof state:
case h.a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
h_a : a ∈ fixedPoints ⇑f
h_le_init : x ≤ a
i : Ordinal.{u}
IH : ∀ k < i, lfpApprox f x k ≤ a
y : α
h_y : (∃ b < i, f (lfpApprox f x b) = y) ∨ y = x
⊢ y ≤ a

Tactic:
cases h_y with
| inl h_y =>
  let ⟨j, h_j_lt, h_j⟩ := h_y
  rw [← h_j, ← h_a]
  exact f.monotone' (IH j h_j_lt)
| inr h_y =>
  rw [h_y]
  exact h_le_init

Result:
no goals

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

Tactic:
intro y h_y

Result:
case h.a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
h_a : a ∈ fixedPoints ⇑f
h_le_init : x ≤ a
i : Ordinal.{u}
IH : ∀ k < i, lfpApprox f x k ≤ a
y : α
h_y : y ∈ {x_1 | ∃ b < i, f (lfpApprox f x b) = x_1} ∪ {x}
⊢ y ≤ a

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

Tactic:
simp only [exists_prop]

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