-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Basic.lean
theorem rel_f_of_iterates {f : α → α} (hf : monotone f) {x : α} (hx : iterates f x) : x ⊑ f x

Proof state:
case step
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x x✝ : α
a✝ : iterates f x✝
a_ih✝ : x✝ ⊑ f x✝
⊢ f x✝ ⊑ f (f x✝)

case sup
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x : α
c✝ : α → Prop
hc✝ : chain c✝
hi✝ : ∀ (x : α), c✝ x → iterates f x
hi_ih✝ : ∀ (x : α), c✝ x → x ⊑ f x
⊢ csup c✝ ⊑ f (csup c✝)

Tactic:
case step ih =>
  apply hf
  assumption

Result:
case sup
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x : α
c✝ : α → Prop
hc✝ : chain c✝
hi✝ : ∀ (x : α), c✝ x → iterates f x
hi_ih✝ : ∀ (x : α), c✝ x → x ⊑ f x
⊢ csup c✝ ⊑ f (csup c✝)

Proof state:
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x x✝ : α
a✝ : iterates f x✝
ih : x✝ ⊑ f x✝
⊢ f x✝ ⊑ f (f x✝)

Tactic:
apply hf

Result:
case a
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x x✝ : α
a✝ : iterates f x✝
ih : x✝ ⊑ f x✝
⊢ x✝ ⊑ f x✝

Proof state:
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x : α
c : α → Prop
hchain : chain c
hi : ∀ (x : α), c x → iterates f x
ih : ∀ (x : α), c x → x ⊑ f x
⊢ csup c ⊑ f (csup c)

Tactic:
apply csup_le hchain

Result:
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x : α
c : α → Prop
hchain : chain c
hi : ∀ (x : α), c x → iterates f x
ih : ∀ (x : α), c x → x ⊑ f x
⊢ ∀ (y : α), c y → y ⊑ f (csup c)

Proof state:
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x : α
c : α → Prop
hchain : chain c
hi : ∀ (x : α), c x → iterates f x
ih : ∀ (x : α), c x → x ⊑ f x
y : α
hy : c y
⊢ y ⊑ f (csup c)

Tactic:
apply rel_trans (ih y hy)

Result:
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x : α
c : α → Prop
hchain : chain c
hi : ∀ (x : α), c x → iterates f x
ih : ∀ (x : α), c x → x ⊑ f x
y : α
hy : c y
⊢ f y ⊑ f (csup c)

Proof state:
case sup
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x : α
c✝ : α → Prop
hc✝ : chain c✝
hi✝ : ∀ (x : α), c✝ x → iterates f x
hi_ih✝ : ∀ (x : α), c✝ x → x ⊑ f x
⊢ csup c✝ ⊑ f (csup c✝)

Tactic:
case sup c hchain hi ih =>
  apply csup_le hchain
  intro y hy
  apply rel_trans (ih y hy)
  apply hf
  apply le_csup hchain hy

Result:
no goals

Proof state:
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x : α
c : α → Prop
hchain : chain c
hi : ∀ (x : α), c x → iterates f x
ih : ∀ (x : α), c x → x ⊑ f x
⊢ ∀ (y : α), c y → y ⊑ f (csup c)

Tactic:
intro y hy

Result:
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x : α
c : α → Prop
hchain : chain c
hi : ∀ (x : α), c x → iterates f x
ih : ∀ (x : α), c x → x ⊑ f x
y : α
hy : c y
⊢ y ⊑ f (csup c)

Proof state:
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x : α
c : α → Prop
hchain : chain c
hi : ∀ (x : α), c x → iterates f x
ih : ∀ (x : α), c x → x ⊑ f x
y : α
hy : c y
⊢ f y ⊑ f (csup c)

Tactic:
apply hf

Result:
case a
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x : α
c : α → Prop
hchain : chain c
hi : ∀ (x : α), c x → iterates f x
ih : ∀ (x : α), c x → x ⊑ f x
y : α
hy : c y
⊢ y ⊑ csup c

Proof state:
case a
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x x✝ : α
a✝ : iterates f x✝
ih : x✝ ⊑ f x✝
⊢ x✝ ⊑ f x✝

Tactic:
assumption

Result:
no goals

Proof state:
case a
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x : α
c : α → Prop
hchain : chain c
hi : ∀ (x : α), c x → iterates f x
ih : ∀ (x : α), c x → x ⊑ f x
y : α
hy : c y
⊢ y ⊑ csup c

Tactic:
apply le_csup hchain hy

Result:
no goals

Proof state:
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x : α
hx : iterates f x
⊢ x ⊑ f x

Tactic:
induction hx

Result:
case step
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x x✝ : α
a✝ : iterates f x✝
a_ih✝ : x✝ ⊑ f x✝
⊢ f x✝ ⊑ f (f x✝)

case sup
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x : α
c✝ : α → Prop
hc✝ : chain c✝
hi✝ : ∀ (x : α), c✝ x → iterates f x
hi_ih✝ : ∀ (x : α), c✝ x → x ⊑ f x
⊢ csup c✝ ⊑ f (csup c✝)