-- Mathlib/Order/WellFounded.lean
theorem wellFounded_iff_no_descending_seq :
    WellFounded r ↔ IsEmpty { f : ℕ → α // ∀ n, r (f (n + 1)) (f n) }

Proof state:
α : Type u_1
r : α → α → Prop
⊢ (∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m) ↔ IsEmpty { f // ∀ (n : ℕ), r (f (n + 1)) (f n) }

Tactic:
refine ⟨fun hr ↦ ⟨fun ⟨f, hf⟩ ↦ ?_⟩, ?_⟩

Result:
case refine_1
α : Type u_1
r : α → α → Prop
hr : ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m
x✝ : { f // ∀ (n : ℕ), r (f (n + 1)) (f n) }
f : ℕ → α
hf : ∀ (n : ℕ), r (f (n + 1)) (f n)
⊢ False

case refine_2
α : Type u_1
r : α → α → Prop
⊢ IsEmpty { f // ∀ (n : ℕ), r (f (n + 1)) (f n) } → ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m

Proof state:
case refine_1.intro.intro.intro
α : Type u_1
r : α → α → Prop
hr : ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m
x✝ : { f // ∀ (n : ℕ), r (f (n + 1)) (f n) }
f : ℕ → α
hf : ∀ (n : ℕ), r (f (n + 1)) (f n)
n : ℕ
hn : ∀ x ∈ Set.range f, ¬r x (f n)
⊢ False

Tactic:
exact hn _ (Set.mem_range_self (n + 1)) (hf n)

Result:
no goals

Proof state:
case refine_2
α : Type u_1
r : α → α → Prop
⊢ (∃ s, s.Nonempty ∧ ∀ m ∈ s, ∃ x ∈ s, r x m) → Nonempty { f // ∀ (n : ℕ), r (f (n + 1)) (f n) }

Tactic:
rintro ⟨s, hs, hs'⟩

Result:
case refine_2.intro.intro
α : Type u_1
r : α → α → Prop
s : Set α
hs : s.Nonempty
hs' : ∀ m ∈ s, ∃ x ∈ s, r x m
⊢ Nonempty { f // ∀ (n : ℕ), r (f (n + 1)) (f n) }

Proof state:
α : Type u_1
r : α → α → Prop
⊢ WellFounded r ↔ IsEmpty { f // ∀ (n : ℕ), r (f (n + 1)) (f n) }

Tactic:
rw [WellFounded.wellFounded_iff_has_min]

Result:
α : Type u_1
r : α → α → Prop
⊢ (∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m) ↔ IsEmpty { f // ∀ (n : ℕ), r (f (n + 1)) (f n) }

Proof state:
case refine_2.intro.intro
α : Type u_1
r : α → α → Prop
s : Set α
hs : s.Nonempty
hs' : ∀ m ∈ s, ∃ x ∈ s, r x m
f : ℕ → ↑s := fun t => Nat.rec (Classical.indefiniteDescription (Membership.mem s) hs) (fun n IH => ⟨⋯.choose, ⋯⟩) t
⊢ Nonempty { f // ∀ (n : ℕ), r (f (n + 1)) (f n) }

Tactic:
exact ⟨⟨Subtype.val ∘ f, fun n ↦ (hs' _ (f n).2).choose_spec.2⟩⟩

Result:
no goals

Proof state:
case refine_2.intro.intro
α : Type u_1
r : α → α → Prop
s : Set α
hs : s.Nonempty
hs' : ∀ m ∈ s, ∃ x ∈ s, r x m
⊢ Nonempty { f // ∀ (n : ℕ), r (f (n + 1)) (f n) }

Tactic:
let f : ℕ → s := Nat.rec (Classical.indefiniteDescription _ hs) fun n IH ↦
  ⟨(hs' _ IH.2).choose, (hs' _ IH.2).choose_spec.1⟩

Result:
case refine_2.intro.intro
α : Type u_1
r : α → α → Prop
s : Set α
hs : s.Nonempty
hs' : ∀ m ∈ s, ∃ x ∈ s, r x m
f : ℕ → ↑s := fun t => Nat.rec (Classical.indefiniteDescription (Membership.mem s) hs) (fun n IH => ⟨⋯.choose, ⋯⟩) t
⊢ Nonempty { f // ∀ (n : ℕ), r (f (n + 1)) (f n) }

Proof state:
case refine_1
α : Type u_1
r : α → α → Prop
hr : ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m
x✝ : { f // ∀ (n : ℕ), r (f (n + 1)) (f n) }
f : ℕ → α
hf : ∀ (n : ℕ), r (f (n + 1)) (f n)
⊢ False

Tactic:
obtain ⟨_, ⟨n, rfl⟩, hn⟩ := hr _ (Set.range_nonempty f)

Result:
case refine_1.intro.intro.intro
α : Type u_1
r : α → α → Prop
hr : ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m
x✝ : { f // ∀ (n : ℕ), r (f (n + 1)) (f n) }
f : ℕ → α
hf : ∀ (n : ℕ), r (f (n + 1)) (f n)
n : ℕ
hn : ∀ x ∈ Set.range f, ¬r x (f n)
⊢ False

Proof state:
case refine_2
α : Type u_1
r : α → α → Prop
⊢ IsEmpty { f // ∀ (n : ℕ), r (f (n + 1)) (f n) } → ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m

Tactic:
contrapose!

Result:
case refine_2
α : Type u_1
r : α → α → Prop
⊢ (∃ s, s.Nonempty ∧ ∀ m ∈ s, ∃ x ∈ s, r x m) → ¬IsEmpty { f // ∀ (n : ℕ), r (f (n + 1)) (f n) }

Proof state:
case refine_2
α : Type u_1
r : α → α → Prop
⊢ (∃ s, s.Nonempty ∧ ∀ m ∈ s, ∃ x ∈ s, r x m) → ¬IsEmpty { f // ∀ (n : ℕ), r (f (n + 1)) (f n) }

Tactic:
rw [not_isEmpty_iff]

Result:
case refine_2
α : Type u_1
r : α → α → Prop
⊢ (∃ s, s.Nonempty ∧ ∀ m ∈ s, ∃ x ∈ s, r x m) → Nonempty { f // ∀ (n : ℕ), r (f (n + 1)) (f n) }