-- 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✝ 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

Tactic:
specialize h 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
z : α
hz : c z
h : ¬f x ⊑ z
⊢ z ⊑ 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
z : α
hz : c z
h : ¬(c z ∧ y ⊑ z)
⊢ z ⊑ y

Tactic:
rw [not_and] at h

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
z : α
hz : c z
h : c z → ¬y ⊑ z
⊢ z ⊑ y

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 : c z → ¬y ⊑ z
⊢ z ⊑ y

Tactic:
specialize h 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
z : α
hz : c 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 : ¬∃ z, c z ∧ f x ⊑ z
z : α
hz : c z
⊢ z ⊑ f x

Tactic:
rw [not_exists] at h

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 : ∀ (x_1 : α), ¬(c x_1 ∧ f x ⊑ x_1)
z : α
hz : c z
⊢ z ⊑ f x

Proof state:
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 => contradiction

Result:
no goals

Proof state:
case neg
α : 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:
right

Result:
case neg.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
⊢ csup c ⊑ f x

Proof state:
case pos.h.intro.intro
α : 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
hfz : f x ⊑ z
⊢ z ⊑ csup c

Tactic:
apply le_csup hchain hz

Result:
no goals

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
⊢ f x ⊑ csup c ∨ csup c ⊑ f x

Tactic:
by_cases h : ∃ z, c z ∧ f x ⊑ z

Result:
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

case neg
α : 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

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
⊢ csup c ⊑ y ∨ y ⊑ csup c

Tactic:
by_cases h : ∃ z, c z ∧ rel y z

Result:
case pos
α : 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 ∨ y ⊑ csup c

case neg
α : 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 ∨ y ⊑ 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 → ∀ (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:
contradiction

Result:
no goals

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

Tactic:
induction hx generalizing y

Result:
case step
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
x x✝ : α
a✝ : iterates f x✝
a_ih✝ : ∀ (y : α), iterates f y → x✝ ⊑ y ∨ y ⊑ x✝
y : α
hy : iterates f y
⊢ f x✝ ⊑ y ∨ y ⊑ 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 → ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
hy : iterates f y
⊢ csup c✝ ⊑ y ∨ y ⊑ 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 → ∀ (y : α), iterates f y → x ⊑ y ∨ y ⊑ x
y : α
hy : iterates f y
h : ∀ (x : α), ¬(c x ∧ y ⊑ x)
z : α
hz : c z
⊢ z ⊑ y

Tactic:
specialize h z

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
z : α
hz : c z
h : ¬(c z ∧ 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
z : α
hz : c z
h : ¬f x ⊑ z
h✝ : f x ⊑ z
⊢ z ⊑ f x

Tactic:
contradiction

Result:
no goals

Proof state:
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

Tactic:
apply hf

Result:
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