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

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 → ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
hy : iterates f y
z : α
hz : c z
h : ¬y ⊑ z
⊢ z ⊑ y

Tactic:
cases ih z hz y hy

Result:
case inl
α : 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 → ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
hy : iterates f y
z : α
hz : c z
h : ¬y ⊑ z
h✝ : z ⊑ y
⊢ z ⊑ y

case inr
α : 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 → ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
hy : iterates f y
z : α
hz : c z
h : ¬y ⊑ z
h✝ : y ⊑ z
⊢ z ⊑ y

Proof state:
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
⊢ chain (iterates f)

Tactic:
intros x y hx hy

Result:
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x y : α
hx : iterates f x
hy : iterates f y
⊢ x ⊑ y ∨ y ⊑ x

Proof state:
case inl.h.a
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x✝ x : α
hx : iterates f x
ih : ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y✝ y : α
hy : iterates f y
a_ih✝ : f x ⊑ y ∨ y ⊑ f x
h✝ : x ⊑ y
⊢ x ⊑ y

Tactic:
assumption

Result:
no goals

Proof state:
case inl
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x✝ x : α
hx : iterates f x
ih : ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y✝ y : α
hy : iterates f y
a_ih✝ : f x ⊑ y ∨ y ⊑ f x
h✝ : x ⊑ y
⊢ f x ⊑ f y ∨ f y ⊑ f x

Tactic:
left

Result:
case inl.h
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x✝ x : α
hx : iterates f x
ih : ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y✝ y : α
hy : iterates f y
a_ih✝ : f x ⊑ y ∨ y ⊑ f x
h✝ : x ⊑ y
⊢ f x ⊑ f y

Proof state:
case neg.h
α : 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 → ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
hy : iterates f y
h : ¬∃ z, c z ∧ y ⊑ z
⊢ csup c ⊑ y

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 → ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
hy : iterates f y
h : ¬∃ z, c z ∧ y ⊑ z
⊢ ∀ (y_1 : α), c y_1 → y_1 ⊑ y

Proof state:
case inr.h
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x✝ x : α
hx : iterates f x
ih : ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y✝ y : α
hy : iterates f y
a_ih✝ : f x ⊑ y ∨ y ⊑ f x
h✝ : y ⊑ x
⊢ f y ⊑ f x

Tactic:
apply hf

Result:
case inr.h.a
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x✝ x : α
hx : iterates f x
ih : ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y✝ y : α
hy : iterates f y
a_ih✝ : f x ⊑ y ∨ y ⊑ f x
h✝ : y ⊑ x
⊢ y ⊑ x

Proof state:
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x✝ x : α
hx : iterates f x
ih : ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
c : α → Prop
hchain : chain c
hi : ∀ (x : α), c x → iterates f x
ih2 : ∀ (x_1 : α), c x_1 → f x ⊑ x_1 ∨ x_1 ⊑ f x
h : ¬∃ z, c z ∧ f x ⊑ z
⊢ ∀ (y : α), c y → y ⊑ f x

Tactic:
intro z hz

Result:
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x✝ x : α
hx : iterates f x
ih : ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
c : α → Prop
hchain : chain c
hi : ∀ (x : α), c x → iterates f x
ih2 : ∀ (x_1 : α), c x_1 → f x ⊑ x_1 ∨ x_1 ⊑ f x
h : ¬∃ z, c z ∧ f x ⊑ z
z : α
hz : c z
⊢ z ⊑ f x

Proof state:
case pos.h.intro.intro
α : 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 → ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
hy : iterates f y
z : α
hz : c z
hfz : y ⊑ z
⊢ z ⊑ csup c

Tactic:
apply le_csup hchain hz

Result:
no goals

Proof state:
case inl
α : 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 → ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
hy : iterates f y
z : α
hz : c z
h : ¬y ⊑ z
h✝ : z ⊑ y
⊢ z ⊑ y

case inr
α : 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 → ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
hy : iterates f y
z : α
hz : c z
h : ¬y ⊑ z
h✝ : y ⊑ z
⊢ z ⊑ y

Tactic:
next => assumption

Result:
case inr
α : 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 → ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
hy : iterates f y
z : α
hz : c z
h : ¬y ⊑ z
h✝ : y ⊑ z
⊢ z ⊑ y

Proof state:
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x✝ x : α
hx : iterates f x
ih : ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
c : α → Prop
hchain : chain c
hi : ∀ (x : α), c x → iterates f x
ih2 : ∀ (x_1 : α), c x_1 → f x ⊑ x_1 ∨ x_1 ⊑ f x
h : ∀ (x_1 : α), ¬(c x_1 ∧ f x ⊑ x_1)
z : α
hz : c z
⊢ z ⊑ f x

Tactic:
specialize h z

Result:
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x✝ x : α
hx : iterates f x
ih : ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
c : α → Prop
hchain : chain c
hi : ∀ (x : α), c x → iterates f x
ih2 : ∀ (x_1 : α), c x_1 → f x ⊑ x_1 ∨ x_1 ⊑ f x
z : α
hz : c z
h : ¬(c z ∧ f x ⊑ z)
⊢ z ⊑ f x

Proof state:
case pos
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x✝ x : α
hx : iterates f x
ih : ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
c : α → Prop
hchain : chain c
hi : ∀ (x : α), c x → iterates f x
ih2 : ∀ (x_1 : α), c x_1 → f x ⊑ x_1 ∨ x_1 ⊑ f x
h : ∃ z, c z ∧ f x ⊑ z
⊢ f x ⊑ csup c ∨ csup c ⊑ f x

Tactic:
left

Result:
case pos.h
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x✝ x : α
hx : iterates f x
ih : ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
c : α → Prop
hchain : chain c
hi : ∀ (x : α), c x → iterates f x
ih2 : ∀ (x_1 : α), c x_1 → f x ⊑ x_1 ∨ x_1 ⊑ f x
h : ∃ z, c z ∧ f x ⊑ z
⊢ f x ⊑ csup c

Proof state:
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x✝ x : α
hx : iterates f x
ih : ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y✝ y : α
hy : iterates f y
a_ih✝ : f x ⊑ y ∨ y ⊑ f x
⊢ f x ⊑ f y ∨ f y ⊑ f x

Tactic:
cases ih y hy

Result:
case inl
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x✝ x : α
hx : iterates f x
ih : ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y✝ y : α
hy : iterates f y
a_ih✝ : f x ⊑ y ∨ y ⊑ f x
h✝ : x ⊑ y
⊢ f x ⊑ f y ∨ f y ⊑ f x

case inr
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x✝ x : α
hx : iterates f x
ih : ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y✝ y : α
hy : iterates f y
a_ih✝ : f x ⊑ y ∨ y ⊑ f x
h✝ : y ⊑ x
⊢ f x ⊑ f y ∨ f y ⊑ 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 → ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
hy : iterates f y
h : ¬∃ z, c z ∧ y ⊑ z
⊢ ∀ (y_1 : α), c y_1 → y_1 ⊑ y

Tactic:
intro z hz

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 → ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
hy : iterates f y
h : ¬∃ z, c z ∧ y ⊑ z
z : α
hz : c z
⊢ z ⊑ y