Theorem: isInfiniteDescendingChain_of_non_acc (Logic/Vorspiel/Order.lean)

State before:
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
this : ∀ (i : ℕ), (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
⊢ IsInfiniteDescendingChain r (descendingChain r z)
Tactic:
intro i
State after:
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
this : ∀ (i : ℕ), (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
i : ℕ
⊢ r (descendingChain r z (i + 1)) (descendingChain r z i)

State before:
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
this : ∀ (i : ℕ), (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
i : ℕ
⊢ r (descendingChain r z (i + 1)) (descendingChain r z i)
Tactic:
simpa using (this (i + 1)).1
State after:
no goals

State before:
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
⊢ ∀ (i : ℕ), (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
Tactic:
intro i
State after:
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
i : ℕ
⊢ (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)

State before:
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
i : ℕ
⊢ (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
Tactic:
induction' i with i ih
State after:
case zero
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
⊢ (0 ≠ 0 → r (descendingChain r z 0) (descendingChain r z (Nat.pred 0))) ∧ ¬Acc r (descendingChain r z 0)

case succ
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
i : ℕ
ih : (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
⊢ (i + 1 ≠ 0 → r (descendingChain r z (i + 1)) (descendingChain r z (i + 1).pred)) ∧
    ¬Acc r (descendingChain r z (i + 1))

State before:
case zero
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
⊢ (0 ≠ 0 → r (descendingChain r z 0) (descendingChain r z (Nat.pred 0))) ∧ ¬Acc r (descendingChain r z 0)
Tactic:
simpa using hz
State after:
no goals

State before:
case succ
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
i : ℕ
ih : (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
⊢ (i + 1 ≠ 0 → r (descendingChain r z (i + 1)) (descendingChain r z (i + 1).pred)) ∧
    ¬Acc r (descendingChain r z (i + 1))
Tactic:
simp[descendingChain]
State after:
case succ
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
i : ℕ
ih : (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
⊢ r (Classical.epsilon fun y => r y (descendingChain r z i) ∧ ¬Acc r y) (descendingChain r z i) ∧
    ¬Acc r (Classical.epsilon fun y => r y (descendingChain r z i) ∧ ¬Acc r y)

State before:
case succ
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
i : ℕ
ih : (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
⊢ r (Classical.epsilon fun y => r y (descendingChain r z i) ∧ ¬Acc r y) (descendingChain r z i) ∧
    ¬Acc r (Classical.epsilon fun y => r y (descendingChain r z i) ∧ ¬Acc r y)
Tactic:
have : ∃ y, y ≺ (descendingChain r z i) ∧ ¬Acc r y := (not_acc_iff r).mp ih.2
State after:
case succ
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
i : ℕ
ih : (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
this : ∃ y, r y (descendingChain r z i) ∧ ¬Acc r y
⊢ r (Classical.epsilon fun y => r y (descendingChain r z i) ∧ ¬Acc r y) (descendingChain r z i) ∧
    ¬Acc r (Classical.epsilon fun y => r y (descendingChain r z i) ∧ ¬Acc r y)

State before:
case succ
α : Sort u
r : α → α → Prop
z : α
hz : ¬Acc r z
i : ℕ
ih : (i ≠ 0 → r (descendingChain r z i) (descendingChain r z i.pred)) ∧ ¬Acc r (descendingChain r z i)
this : ∃ y, r y (descendingChain r z i) ∧ ¬Acc r y
⊢ r (Classical.epsilon fun y => r y (descendingChain r z i) ∧ ¬Acc r y) (descendingChain r z i) ∧
    ¬Acc r (Classical.epsilon fun y => r y (descendingChain r z i) ∧ ¬Acc r y)
Tactic:
exact Classical.epsilon_spec this
State after:
no goals