-- Mathlib/Order/OrderIsoNat.lean
theorem acc_iff_no_decreasing_seq {x} :
    Acc r x ↔ IsEmpty { f : ((· > ·) : ℕ → ℕ → Prop) ↪r r // x ∈ Set.range f }

Proof state:
case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
f : { a // ¬Acc r a } → { a // ¬Acc r a }
h : ∀ (x : { a // ¬Acc r a }), r ↑(f x) ↑x
⊢ IsEmpty { f // x ∈ Set.range ⇑f } → Acc r x

Tactic:
refine fun E =>
  by_contradiction fun hx => E.elim' ⟨natGT (fun n => (f^[n] ⟨x, hx⟩).1) fun n => ?_, 0, rfl⟩

Result:
case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
f : { a // ¬Acc r a } → { a // ¬Acc r a }
h : ∀ (x : { a // ¬Acc r a }), r ↑(f x) ↑x
E : IsEmpty { f // x ∈ Set.range ⇑f }
hx : ¬Acc r x
n : ℕ
⊢ r ((fun n => ↑(f^[n] ⟨x, hx⟩)) (n + 1)) ((fun n => ↑(f^[n] ⟨x, hx⟩)) n)

Proof state:
case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
⊢ IsEmpty { f // x ∈ Set.range ⇑f } → Acc r x

Tactic:
have : ∀ x : { a // ¬Acc r a }, ∃ y : { a // ¬Acc r a }, r y.1 x.1 := by
  rintro ⟨x, hx⟩
  cases exists_not_acc_lt_of_not_acc hx with
  | intro w h => exact ⟨⟨w, h.1⟩, h.2⟩

Result:
case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
this : ∀ (x : { a // ¬Acc r a }), ∃ y, r ↑y ↑x
⊢ IsEmpty { f // x ∈ Set.range ⇑f } → Acc r x

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
⊢ Acc r x ↔ IsEmpty { f // x ∈ Set.range ⇑f }

Tactic:
constructor

Result:
case mp
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
⊢ Acc r x → IsEmpty { f // x ∈ Set.range ⇑f }

case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
⊢ IsEmpty { f // x ∈ Set.range ⇑f } → Acc r x

Proof state:
case mp.false.mk.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x✝¹ : α
h : Acc r x✝¹
x : α
x✝ : ∀ (y : α), r y x → Acc r y
IH : ∀ (y : α), r y x → IsEmpty { f // y ∈ Set.range ⇑f }
f : (fun x1 x2 => x1 > x2) ↪r r
k : ℕ
hf : f k = x
⊢ False

Tactic:
exact IsEmpty.elim' (IH (f (k + 1)) (hf ▸ f.map_rel_iff.2 (Nat.lt_succ_self _))) ⟨f, _, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
⊢ ∀ (x : { a // ¬Acc r a }), ∃ y, r ↑y ↑x

Tactic:
rintro ⟨x, hx⟩

Result:
case mk
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x✝ x : α
hx : ¬Acc r x
⊢ ∃ y, r ↑y ↑⟨x, hx⟩

Proof state:
case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
f : { a // ¬Acc r a } → { a // ¬Acc r a }
h : ∀ (x : { a // ¬Acc r a }), r ↑(f x) ↑x
E : IsEmpty { f // x ∈ Set.range ⇑f }
hx : ¬Acc r x
n : ℕ
⊢ r ↑((f ∘ f^[n]) ⟨x, hx⟩) ↑(f^[n] ⟨x, hx⟩)

Tactic:
apply h

Result:
no goals

Proof state:
case mp
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x✝¹ : α
h : Acc r x✝¹
x : α
x✝ : ∀ (y : α), r y x → Acc r y
IH : ∀ (y : α), r y x → IsEmpty { f // y ∈ Set.range ⇑f }
⊢ IsEmpty { f // x ∈ Set.range ⇑f }

Tactic:
constructor

Result:
case mp.false
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x✝¹ : α
h : Acc r x✝¹
x : α
x✝ : ∀ (y : α), r y x → Acc r y
IH : ∀ (y : α), r y x → IsEmpty { f // y ∈ Set.range ⇑f }
⊢ { f // x ∈ Set.range ⇑f } → False

Proof state:
case mk
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x✝ x : α
hx : ¬Acc r x
⊢ ∃ y, r ↑y ↑⟨x, hx⟩

Tactic:
cases exists_not_acc_lt_of_not_acc hx with
| intro w h => exact ⟨⟨w, h.1⟩, h.2⟩

Result:
no goals

Proof state:
case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
f : { a // ¬Acc r a } → { a // ¬Acc r a }
h : ∀ (x : { a // ¬Acc r a }), r ↑(f x) ↑x
E : IsEmpty { f // x ∈ Set.range ⇑f }
hx : ¬Acc r x
n : ℕ
⊢ r ((fun n => ↑(f^[n] ⟨x, hx⟩)) (n + 1)) ((fun n => ↑(f^[n] ⟨x, hx⟩)) n)

Tactic:
simp only [Function.iterate_succ']

Result:
case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
f : { a // ¬Acc r a } → { a // ¬Acc r a }
h : ∀ (x : { a // ¬Acc r a }), r ↑(f x) ↑x
E : IsEmpty { f // x ∈ Set.range ⇑f }
hx : ¬Acc r x
n : ℕ
⊢ r ↑((f ∘ f^[n]) ⟨x, hx⟩) ↑(f^[n] ⟨x, hx⟩)

Proof state:
case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
this : ∀ (x : { a // ¬Acc r a }), ∃ y, r ↑y ↑x
⊢ IsEmpty { f // x ∈ Set.range ⇑f } → Acc r x

Tactic:
choose f h using this

Result:
case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
f : { a // ¬Acc r a } → { a // ¬Acc r a }
h : ∀ (x : { a // ¬Acc r a }), r ↑(f x) ↑x
⊢ IsEmpty { f // x ∈ Set.range ⇑f } → Acc r x

Proof state:
case mk.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x✝ x : α
hx : ¬Acc r x
w : α
h : ¬Acc r w ∧ r w x
⊢ ∃ y, r ↑y ↑⟨x, hx⟩

Tactic:
exact ⟨⟨w, h.1⟩, h.2⟩

Result:
no goals

Proof state:
case mp
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x : α
⊢ Acc r x → IsEmpty { f // x ∈ Set.range ⇑f }

Tactic:
refine fun h => h.recOn fun x _ IH => ?_

Result:
case mp
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x✝¹ : α
h : Acc r x✝¹
x : α
x✝ : ∀ (y : α), r y x → Acc r y
IH : ∀ (y : α), r y x → IsEmpty { f // y ∈ Set.range ⇑f }
⊢ IsEmpty { f // x ∈ Set.range ⇑f }

Proof state:
case mp.false
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x✝¹ : α
h : Acc r x✝¹
x : α
x✝ : ∀ (y : α), r y x → Acc r y
IH : ∀ (y : α), r y x → IsEmpty { f // y ∈ Set.range ⇑f }
⊢ { f // x ∈ Set.range ⇑f } → False

Tactic:
rintro ⟨f, k, hf⟩

Result:
case mp.false.mk.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
x✝¹ : α
h : Acc r x✝¹
x : α
x✝ : ∀ (y : α), r y x → Acc r y
IH : ∀ (y : α), r y x → IsEmpty { f // y ∈ Set.range ⇑f }
f : (fun x1 x2 => x1 > x2) ↪r r
k : ℕ
hf : f k = x
⊢ False