-- Mathlib/Order/OmegaCompletePartialOrder.lean
theorem ωSup_iterate_mem_fixedPoint (h : x ≤ f x) :
    ωSup (iterateChain f x h) ∈ fixedPoints f

Proof state:
case a.a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
this : (iterateChain (↑f) x h) n.succ = f ((iterateChain (↑f) x h) n)
⊢ f ((iterateChain (↑f) x h) n) ≤ ωSup (iterateChain (↑f) x h)

Tactic:
rw [← this]

Result:
case a.a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
this : (iterateChain (↑f) x h) n.succ = f ((iterateChain (↑f) x h) n)
⊢ (iterateChain (↑f) x h) n.succ ≤ ωSup (iterateChain (↑f) x h)

Proof state:
case a.a.zero
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ f x ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Tactic:
change ((iterateChain f x h).map f) 0 ≤ ωSup ((iterateChain f x h).map (f : α →o α))

Result:
case a.a.zero
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ((iterateChain (↑f) x h).map ↑f) 0 ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Proof state:
case a.a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ∀ (i : ℕ), (iterateChain (↑f) x h) i ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Tactic:
rintro (_ | n)

Result:
case a.a.zero
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ (iterateChain (↑f) x h) 0 ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

case a.a.succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
⊢ (iterateChain (↑f) x h) (n + 1) ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Proof state:
case a.a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ∀ (i : ℕ), ((iterateChain (↑f) x h).map ↑f) i ≤ ωSup (iterateChain (↑f) x h)

Tactic:
intro n

Result:
case a.a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
⊢ ((iterateChain (↑f) x h).map ↑f) n ≤ ωSup (iterateChain (↑f) x h)

Proof state:
case a.a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
⊢ f ((iterateChain (↑f) x h) n) ≤ ωSup (iterateChain (↑f) x h)

Tactic:
have : iterateChain f x h (n.succ) = f (iterateChain f x h n) :=
  Function.iterate_succ_apply' ..

Result:
case a.a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
this : (iterateChain (↑f) x h) n.succ = f ((iterateChain (↑f) x h) n)
⊢ f ((iterateChain (↑f) x h) n) ≤ ωSup (iterateChain (↑f) x h)

Proof state:
case a.a.zero
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ (iterateChain (↑f) x h) 0 ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Tactic:
apply le_trans h

Result:
case a.a.zero
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ f x ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Proof state:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ωSup ((iterateChain (↑f) x h).map ↑f) = ωSup (iterateChain (↑f) x h)

Tactic:
apply le_antisymm

Result:
case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ωSup ((iterateChain (↑f) x h).map ↑f) ≤ ωSup (iterateChain (↑f) x h)

case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ωSup (iterateChain (↑f) x h) ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Proof state:
case a.a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
⊢ ((iterateChain (↑f) x h).map ↑f) n ≤ ωSup (iterateChain (↑f) x h)

Tactic:
simp only [Chain.map_coe, OrderHomClass.coe_coe, comp_apply]

Result:
case a.a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
⊢ f ((iterateChain (↑f) x h) n) ≤ ωSup (iterateChain (↑f) x h)

Proof state:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ωSup (iterateChain (↑f) x h) ∈ fixedPoints ⇑f

Tactic:
rw [mem_fixedPoints, IsFixedPt, f.continuous]

Result:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ωSup ((iterateChain (↑f) x h).map ↑f) = ωSup (iterateChain (↑f) x h)

Proof state:
case a.a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
this : (iterateChain (↑f) x h) n.succ = f ((iterateChain (↑f) x h) n)
⊢ (iterateChain (↑f) x h) n.succ ≤ ωSup (iterateChain (↑f) x h)

Tactic:
apply le_ωSup

Result:
no goals

Proof state:
case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ωSup ((iterateChain (↑f) x h).map ↑f) ≤ ωSup (iterateChain (↑f) x h)

Tactic:
apply ωSup_le

Result:
case a.a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ∀ (i : ℕ), ((iterateChain (↑f) x h).map ↑f) i ≤ ωSup (iterateChain (↑f) x h)

Proof state:
case a.a.zero
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ((iterateChain (↑f) x h).map ↑f) 0 ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Tactic:
apply le_ωSup

Result:
no goals

Proof state:
case a.a.succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
⊢ (iterateChain (↑f) x h) (n + 1) ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Tactic:
have : iterateChain f x h (n.succ) = (iterateChain f x h).map f n :=
  Function.iterate_succ_apply' ..

Result:
case a.a.succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
this : (iterateChain (↑f) x h) n.succ = ((iterateChain (↑f) x h).map ↑f) n
⊢ (iterateChain (↑f) x h) (n + 1) ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Proof state:
case a.a.succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
this : (iterateChain (↑f) x h) n.succ = ((iterateChain (↑f) x h).map ↑f) n
⊢ (iterateChain (↑f) x h) (n + 1) ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Tactic:
rw [this]

Result:
case a.a.succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
this : (iterateChain (↑f) x h) n.succ = ((iterateChain (↑f) x h).map ↑f) n
⊢ ((iterateChain (↑f) x h).map ↑f) n ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Proof state:
case a.a.succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
this : (iterateChain (↑f) x h) n.succ = ((iterateChain (↑f) x h).map ↑f) n
⊢ ((iterateChain (↑f) x h).map ↑f) n ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Tactic:
apply le_ωSup

Result:
no goals

Proof state:
case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ωSup (iterateChain (↑f) x h) ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Tactic:
apply ωSup_le

Result:
case a.a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ∀ (i : ℕ), (iterateChain (↑f) x h) i ≤ ωSup ((iterateChain (↑f) x h).map ↑f)