-- Mathlib/Order/WellFoundedSet.lean
theorem exists_min_bad_of_exists_bad (r : α → α → Prop) (rk : α → ℕ) (s : Set α) :
    (∃ f, IsBadSeq r s f) → ∃ f, IsBadSeq r s f ∧ ∀ n, IsMinBadSeq r rk s n f

Proof state:
case intro
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn => ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
⊢ ∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f

Tactic:
refine ⟨fun n => (fs n).1 n, ⟨fun n => (fs n).2.1.1 n, fun m n mn => ?_⟩, fun n g hg1 hg2 => ?_⟩

Result:
case intro.refine_1
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn => ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
m n : ℕ
mn : m < n
⊢ ¬r ((fun n => ↑(fs n) n) m) ((fun n => ↑(fs n) n) n)

case intro.refine_2
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn => ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
n : ℕ
g : ℕ → α
hg1 : ∀ m < n, (fun n => ↑(fs n) n) m = g m
hg2 : rk (g n) < rk ((fun n => ↑(fs n) n) n)
⊢ ¬IsBadSeq r s g

Proof state:
case intro.succ
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn => ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
m k : ℕ
ih : ↑(fs m) m = ↑(fs (m + k)) m
⊢ ↑(minBadSeqOfBadSeq r rk s (m + k + 1) ↑(fs (m + k)) ⋯) m = ↑(fs (m + (k + 1))) m

Tactic:
rfl

Result:
no goals

Proof state:
case intro.zero
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn => ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
m : ℕ
⊢ ↑(fs m) m = ↑(fs (m + 0)) m

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
⊢ (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }

Tactic:
refine Nat.rec ?_ fun n fn => ?_

Result:
case refine_1
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
⊢ { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f }

case refine_2
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
n : ℕ
fn : { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }
⊢ { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f }

Proof state:
case intro.refine_1
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn => ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
m n : ℕ
mn : m < n
⊢ ¬r (↑(fs n) m) (↑(fs n) n)

Tactic:
exact (fs n).2.1.2 m n mn

Result:
no goals

Proof state:
case refine_1
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
⊢ { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f }

Tactic:
exact ⟨(minBadSeqOfBadSeq r rk s 0 f0 hf0).1, (minBadSeqOfBadSeq r rk s 0 f0 hf0).2.2⟩

Result:
no goals

Proof state:
case intro.refine_1
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn => ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
m n : ℕ
mn : m < n
⊢ ¬r ((fun n => ↑(fs n) n) m) ((fun n => ↑(fs n) n) n)

Tactic:
dsimp

Result:
case intro.refine_1
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn => ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
m n : ℕ
mn : m < n
⊢ ¬r (↑(fs m) m) (↑(fs n) n)

Proof state:
case refine_2
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
n : ℕ
fn : { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }
⊢ { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f }

Tactic:
exact ⟨(minBadSeqOfBadSeq r rk s (n + 1) fn.1 fn.2.1).1,
  (minBadSeqOfBadSeq r rk s (n + 1) fn.1 fn.2.1).2.2⟩

Result:
no goals

Proof state:
case intro.refine_2
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn => ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
n : ℕ
g : ℕ → α
hg1 : ∀ m < n, (fun n => ↑(fs n) n) m = g m
hg2 : rk (g n) < rk ((fun n => ↑(fs n) n) n)
⊢ ¬IsBadSeq r s g

Tactic:
refine (fs n).2.2 g (fun m mn => ?_) hg2

Result:
case intro.refine_2
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn => ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
n : ℕ
g : ℕ → α
hg1 : ∀ m < n, (fun n => ↑(fs n) n) m = g m
hg2 : rk (g n) < rk ((fun n => ↑(fs n) n) n)
m : ℕ
mn : m < n
⊢ ↑(fs n) m = g m

Proof state:
case intro.succ
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn => ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
m k : ℕ
ih : ↑(fs m) m = ↑(fs (m + k)) m
⊢ ↑(fs m) m = ↑(fs (m + (k + 1))) m

Tactic:
rw [ih, (minBadSeqOfBadSeq r rk s (m + k + 1) (fs (m + k)).1 (fs (m + k)).2.1).2.1 m
  (Nat.lt_succ_iff.2 (Nat.add_le_add_left k.zero_le m))]

Result:
case intro.succ
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn => ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
m k : ℕ
ih : ↑(fs m) m = ↑(fs (m + k)) m
⊢ ↑(minBadSeqOfBadSeq r rk s (m + k + 1) ↑(fs (m + k)) ⋯) m = ↑(fs (m + (k + 1))) m

Proof state:
case intro.refine_1
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn => ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
m n : ℕ
mn : m < n
⊢ ¬r (↑(fs m) m) (↑(fs n) n)

Tactic:
rw [h m n mn.le]

Result:
case intro.refine_1
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t =>
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn => ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
m n : ℕ
mn : m < n
⊢ ¬r (↑(fs n) m) (↑(fs n) n)