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

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

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 : α
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✝ : z ⊑ f x
⊢ z ⊑ f x

Tactic:
next => contradiction

Result:
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 : α
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✝ : z ⊑ f x
⊢ z ⊑ f x

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

Tactic:
assumption

Result:
no goals

Proof state:
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 : α
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✝ : z ⊑ f x
⊢ z ⊑ f x

Tactic:
next => assumption

Result:
no goals

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

Tactic:
apply csup_le hchain _

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

Tactic:
induction hy

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

case sup
α : 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
hc✝ : chain c✝
hi✝ : ∀ (x : α), c✝ x → iterates f x
hi_ih✝ : ∀ (x_1 : α), c✝ x_1 → f x ⊑ x_1 ∨ x_1 ⊑ f x
⊢ f x ⊑ csup c✝ ∨ csup c✝ ⊑ f 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
z : α
hz : c z
h : ¬f x ⊑ z
h✝ : z ⊑ f x
⊢ z ⊑ f x

Tactic:
assumption

Result:
no goals

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

Tactic:
apply rel_trans hfz

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

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

Tactic:
right

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

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

Tactic:
right

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

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

Tactic:
obtain ⟨z, hz, hfz⟩ := h

Result:
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
⊢ 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 : α
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:
rw [not_and] 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
z : α
hz : c z
h : c z → ¬f x ⊑ z
⊢ z ⊑ f x

Proof state:
case pos.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
⊢ y ⊑ csup c

Tactic:
obtain ⟨z, hz, hfz⟩ := h

Result:
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
⊢ 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 : ¬∃ z, c z ∧ y ⊑ z
z : α
hz : c z
⊢ z ⊑ y

Tactic:
rw [not_exists] 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
h : ∀ (x : α), ¬(c x ∧ y ⊑ x)
z : α
hz : c 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 : ¬y ⊑ z
h✝ : z ⊑ y
⊢ z ⊑ y

Tactic:
assumption

Result:
no goals