awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r_1 r : α → α → Prop
rk : α → ℕ
s : Set α
n : ℕ
f : ℕ → α
hf : IsBadSeq r s f
h : ∃ (k : ℕ) (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k
h1 :
  ∀ m < n,
    f m =
      Classical.choose (p := fun (x : ℕ → α) ↦
        (∀ m < n, f m = x m) ∧
          IsBadSeq r s x ∧
            rk (x n) =
              Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = n_1) h)
        ⋯ m
h2 :
  IsBadSeq r s
    (Classical.choose (p := fun (x : ℕ → α) ↦
      (∀ m < n, f m = x m) ∧
        IsBadSeq r s x ∧
          rk (x n) =
            Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = n_1) h)
      ⋯)
⊢ { g : ℕ → α // (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ IsMinBadSeq r rk s n g }
have h3 : rk
    (Classical.choose (p := fun (x : ℕ → α) ↦
      (∀ m < n, f m = x m) ∧
        IsBadSeq r s x ∧
          rk (x n) =
            Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = n_1) h)
      sorry n) =
  Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = n_1) h
Tactic: obtain ⟨h1, h2, h3⟩ := Classical.choose_spec (Nat.find_spec h)
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r_1 r : α → α → Prop
rk : α → ℕ
s : Set α
n : ℕ
f : ℕ → α
hf : IsBadSeq r s f
h : ∃ (k : ℕ) (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k
h1 :
  ∀ m < n,
    f m =
      Classical.choose (p := fun (x : ℕ → α) ↦
        (∀ m < n, f m = x m) ∧
          IsBadSeq r s x ∧
            rk (x n) =
              Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = n_1) h)
        ⋯ m
h2 :
  IsBadSeq r s
    (Classical.choose (p := fun (x : ℕ → α) ↦
      (∀ m < n, f m = x m) ∧
        IsBadSeq r s x ∧
          rk (x n) =
            Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = n_1) h)
      ⋯)
h3 :
  rk
      (Classical.choose (p := fun (x : ℕ → α) ↦
        (∀ m < n, f m = x m) ∧
          IsBadSeq r s x ∧
            rk (x n) =
              Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = n_1) h)
        ⋯ n) =
    Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = n_1) h
⊢ { g : ℕ → α // (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ IsMinBadSeq r rk s n g }
have refine : ∀ (g : ℕ → α)
  (hg1 :
    ∀ m < n,
      Classical.choose (p := fun (x : ℕ → α) ↦
          (∀ m < n, f m = x m) ∧
            IsBadSeq r s x ∧
              rk (x n) =
                Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = n_1) h)
          sorry m =
        g m)
  (hg2 :
    rk (g n) <
      rk
        (Classical.choose (p := fun (x : ℕ → α) ↦
          (∀ m < n, f m = x m) ∧
            IsBadSeq r s x ∧
              rk (x n) =
                Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = n_1) h)
          sorry n))
  (con : IsBadSeq r s g), False
Tactic: refine ⟨Classical.choose (Nat.find_spec h), h1, by convert! h2, fun g hg1 hg2 con => ?_⟩
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r_1 r : α → α → Prop
rk : α → ℕ
s : Set α
n : ℕ
f : ℕ → α
hf : IsBadSeq r s f
h : ∃ (k : ℕ) (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k
h1 :
  ∀ m < n,
    f m =
      Classical.choose (p := fun (x : ℕ → α) ↦
        (∀ m < n, f m = x m) ∧
          IsBadSeq r s x ∧
            rk (x n) =
              Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = n_1) h)
        ⋯ m
h2 :
  IsBadSeq r s
    (Classical.choose (p := fun (x : ℕ → α) ↦
      (∀ m < n, f m = x m) ∧
        IsBadSeq r s x ∧
          rk (x n) =
            Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = n_1) h)
      ⋯)
h3 :
  rk
      (Classical.choose (p := fun (x : ℕ → α) ↦
        (∀ m < n, f m = x m) ∧
          IsBadSeq r s x ∧
            rk (x n) =
              Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = n_1) h)
        ⋯ n) =
    Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = n_1) h
g : ℕ → α
hg1 :
  ∀ m < n,
    Classical.choose (p := fun (x : ℕ → α) ↦
        (∀ m < n, f m = x m) ∧
          IsBadSeq r s x ∧
            rk (x n) =
              Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = n_1) h)
        ⋯ m =
      g m
hg2 :
  rk (g n) <
    rk
      (Classical.choose (p := fun (x : ℕ → α) ↦
        (∀ m < n, f m = x m) ∧
          IsBadSeq r s x ∧
            rk (x n) =
              Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = n_1) h)
        ⋯ n)
con : IsBadSeq r s g
⊢ False
have refine : rk (g n) < Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = n_1) h
Tactic: refine Nat.find_min h ?_ ⟨g, fun m mn => (h1 m mn).trans (hg1 m mn), con, rfl⟩
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r_1 r : α → α → Prop
rk : α → ℕ
s : Set α
n : ℕ
f : ℕ → α
hf : IsBadSeq r s f
⊢ { g : ℕ → α // (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ IsMinBadSeq r rk s n g }
have have : (h : ∃ (k : ℕ) (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k) →
  { g : ℕ → α // (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ IsMinBadSeq r rk s n g }
Tactic: classical
    have h : ∃ (k : ℕ) (g : ℕ → α), (∀ m, m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k :=
      ⟨_, f, fun _ _ => rfl, hf, rfl⟩
    obtain ⟨h1, h2, h3⟩ := Classical.choose_spec (Nat.find_spec h)
    refine ⟨Classical.choose (Nat.find_spec h), h1, by convert! h2, fun g hg1 hg2 con => ?_⟩
    refine Nat.find_min h ?_ ⟨g, fun m mn => (h1 m mn).trans (hg1 m mn), con, rfl⟩
    rwa [← h3]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r_1 r : α → α → Prop
rk : α → ℕ
s : Set α
n : ℕ
f : ℕ → α
hf : IsBadSeq r s f
have have₁ have₂ :
  (h : ∃ (k : ℕ) (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k) →
    { g : ℕ → α // (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ IsMinBadSeq r rk s n g }
⊢ { g : ℕ → α // (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ IsMinBadSeq r rk s n g }
have have₃ : (h : ∃ (k : ℕ) (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k) →
  (h1 :
      ∀ m < n,
        f m =
          Classical.choose (p := fun (x : ℕ → α) ↦
            (∀ m < n, f m = x m) ∧
              IsBadSeq r s x ∧
                rk (x n) =
                  Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = n_1)
                    h)
            sorry m) →
    (h2 :
        IsBadSeq r s
          (Classical.choose (p := fun (x : ℕ → α) ↦
            (∀ m < n, f m = x m) ∧
              IsBadSeq r s x ∧
                rk (x n) =
                  Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = n_1)
                    h)
            sorry)) →
      (h3 :
          rk
              (Classical.choose (p := fun (x : ℕ → α) ↦
                (∀ m < n, f m = x m) ∧
                  IsBadSeq r s x ∧
                    rk (x n) =
                      Nat.find (p := fun (n_1 : ℕ) ↦
                        ∃ (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = n_1) h)
                sorry n) =
            Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = n_1) h) →
        { g : ℕ → α // (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ IsMinBadSeq r rk s n g }
Tactic: classical
    have h : ∃ (k : ℕ) (g : ℕ → α), (∀ m, m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k :=
      ⟨_, f, fun _ _ => rfl, hf, rfl⟩
    obtain ⟨h1, h2, h3⟩ := Classical.choose_spec (Nat.find_spec h)
    refine ⟨Classical.choose (Nat.find_spec h), h1, by convert! h2, fun g hg1 hg2 con => ?_⟩
    refine Nat.find_min h ?_ ⟨g, fun m mn => (h1 m mn).trans (hg1 m mn), con, rfl⟩
    rwa [← h3]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : 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 }
have refine_1 : { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f }
Tactic: refine Nat.rec ?_ fun n fn => ?_
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
refine_1 : { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f }
⊢ (n : ℕ) → { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }
have refine_2 : (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: refine Nat.rec ?_ fun n fn => ?_
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : 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 (motive := fun (x : ℕ) ↦ { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s x f })
      (Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f)
        (↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) : ℕ → α) ⋯)
      (fun (n : ℕ) (fn : { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }) ↦
        Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f)
          (↑(minBadSeqOfBadSeq r rk s (n + 1) (↑fn : ℕ → α) ⋯) : ℕ → α) ⋯)
      t
m n : ℕ
mn : m ≤ n
⊢ (↑(fs m) : ℕ → α) m = (↑(fs n) : ℕ → α) m
have obtain : ∀ (k : ℕ) (mn : m ≤ m + k), (↑(fs m) : ℕ → α) m = (↑(fs (m + k)) : ℕ → α) m
Tactic: obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le mn
Cleared hypotheses: n, mn
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : 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 (motive := fun (x : ℕ) ↦ { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s x f })
      (Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f)
        (↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) : ℕ → α) ⋯)
      (fun (n : ℕ) (fn : { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }) ↦
        Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f)
          (↑(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
have succ : (↑(minBadSeqOfBadSeq r rk s (m + k + 1) (↑(fs (m + k)) : ℕ → α) sorry) : ℕ → α) 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))]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : 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 (motive := fun (x : ℕ) ↦ { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s x f })
      (Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f)
        (↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) : ℕ → α) ⋯)
      (fun (n : ℕ) (fn : { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }) ↦
        Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f)
          (↑(minBadSeqOfBadSeq r rk s (n + 1) (↑fn : ℕ → α) ⋯) : ℕ → α) ⋯)
      t
m k : ℕ
⊢ (↑(fs m) : ℕ → α) m = (↑(fs (m + k)) : ℕ → α) m
have zero : (↑(fs m) : ℕ → α) m = (↑(fs (m + 0)) : ℕ → α) m
Tactic: induction k with
    | zero => rfl
    | succ k ih =>
      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))]
      rfl
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : 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 (motive := fun (x : ℕ) ↦ { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s x f })
      (Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f)
        (↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) : ℕ → α) ⋯)
      (fun (n : ℕ) (fn : { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }) ↦
        Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f)
          (↑(minBadSeqOfBadSeq r rk s (n + 1) (↑fn : ℕ → α) ⋯) : ℕ → α) ⋯)
      t
m k : ℕ
zero : (↑(fs m) : ℕ → α) m = (↑(fs (m + 0)) : ℕ → α) m
⊢ (↑(fs m) : ℕ → α) m = (↑(fs (m + k)) : ℕ → α) m
have succ : ∀ (k : ℕ) (ih : (↑(fs m) : ℕ → α) m = (↑(fs (m + k)) : ℕ → α) m), (↑(fs m) : ℕ → α) m = (↑(fs (m + (k + 1))) : ℕ → α) m
Tactic: induction k with
    | zero => rfl
    | succ k ih =>
      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))]
      rfl
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
Goal:
α : 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 (motive := fun (x : ℕ) ↦ { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s x f })
      (Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f)
        (↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) : ℕ → α) ⋯)
      (fun (n : ℕ) (fn : { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }) ↦
        Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f)
          (↑(minBadSeqOfBadSeq r rk s (n + 1) (↑fn : ℕ → α) ⋯) : ℕ → α) ⋯)
      t
⊢ ∃ (f : ℕ → α), IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
have h : ∀ (m n : ℕ), m ≤ n → (↑(fs m) : ℕ → α) m = (↑(fs n) : ℕ → α) m
Tactic: have h : ∀ m n, m ≤ n → (fs m).1 m = (fs n).1 m := fun m n mn => by
    obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le mn; clear mn
    induction k with
    | zero => rfl
    | succ k ih =>
      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))]
      rfl
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : 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 (motive := fun (x : ℕ) ↦ { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s x f })
      (Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f)
        (↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) : ℕ → α) ⋯)
      (fun (n : ℕ) (fn : { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }) ↦
        Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f)
          (↑(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
have refine_1 : ∀ (m n : ℕ) (mn : m < n), ¬r ((fun (n : ℕ) ↦ (↑(fs n) : ℕ → α) n) m) ((fun (n : ℕ) ↦ (↑(fs n) : ℕ → α) n) n)
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 => ?_⟩
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : 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 (motive := fun (x : ℕ) ↦ { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s x f })
      (Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f)
        (↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) : ℕ → α) ⋯)
      (fun (n : ℕ) (fn : { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }) ↦
        Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f)
          (↑(minBadSeqOfBadSeq r rk s (n + 1) (↑fn : ℕ → α) ⋯) : ℕ → α) ⋯)
      t
h : ∀ (m n : ℕ), m ≤ n → (↑(fs m) : ℕ → α) m = (↑(fs n) : ℕ → α) m
refine_1 : ∀ (m n : ℕ) (mn : m < n), ¬r ((fun (n : ℕ) ↦ (↑(fs n) : ℕ → α) n) m) ((fun (n : ℕ) ↦ (↑(fs n) : ℕ → α) n) n)
⊢ ∃ (f : ℕ → α), IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
have refine_2 : ∀ (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 ⟨fun n => (fs n).1 n, ⟨fun n => (fs n).2.1.1 n, fun m n mn => ?_⟩, fun n g hg1 hg2 => ?_⟩
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : 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 (motive := fun (x : ℕ) ↦ { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s x f })
      (Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f)
        (↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) : ℕ → α) ⋯)
      (fun (n : ℕ) (fn : { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }) ↦
        Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f)
          (↑(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)
have refine_1 : ¬r ((↑(fs n) : ℕ → α) m) ((↑(fs n) : ℕ → α) n)
Tactic: rw [h m n mn.le]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : 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 (motive := fun (x : ℕ) ↦ { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s x f })
      (Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f)
        (↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) : ℕ → α) ⋯)
      (fun (n : ℕ) (fn : { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }) ↦
        Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f)
          (↑(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
have refine_2 : ∀ (m : ℕ) (mn : m < n), (↑(fs n) : ℕ → α) m = g m
Tactic: refine (fs n).2.2 g (fun m mn => ?_) hg2
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : 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 (motive := fun (x : ℕ) ↦ { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s x f })
      (Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f)
        (↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) : ℕ → α) ⋯)
      (fun (n : ℕ) (fn : { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }) ↦
        Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f)
          (↑(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
have refine_2 : (↑(fs m) : ℕ → α) m = g m
Tactic: rw [← h m n mn.le, ← hg1 m mn]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : 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 (motive := fun (x : ℕ) ↦ { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s x f })
      (Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f)
        (↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) : ℕ → α) ⋯)
      (fun (n : ℕ) (fn : { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }) ↦
        Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f)
          (↑(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
refine_2 : (↑(fs m) : ℕ → α) m = g m
⊢ (↑(fs n) : ℕ → α) m = g m
have refine_2₁ : (↑(fs m) : ℕ → α) m = (fun (n : ℕ) ↦ (↑(fs n) : ℕ → α) n) m
Tactic: rw [← h m n mn.le, ← hg1 m mn]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ s.PartiallyWellOrderedOn r ↔ ¬∃ (f : ℕ → α), IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
have rw : (∃ (x : ℕ → α), IsBadSeq r s x) ↔ ∃ (f : ℕ → α), IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
Tactic: rw [iff_forall_not_isBadSeq, ← not_exists, not_congr]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ (x : ℕ → α), IsBadSeq r s x) ↔ ∃ (f : ℕ → α), IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
have mp : (∃ (x : ℕ → α), IsBadSeq r s x) → ∃ (f : ℕ → α), IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
mp : (∃ (x : ℕ → α), IsBadSeq r s x) → ∃ (f : ℕ → α), IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
⊢ (∃ (x : ℕ → α), IsBadSeq r s x) ↔ ∃ (f : ℕ → α), IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
have mpr : (∃ (f : ℕ → α), IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f) → ∃ (x : ℕ → α), IsBadSeq r s x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
inst : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
⊢ PartiallyWellOrderedOn {l : List α | ∀ x ∈ l, x ∈ s} (List.SublistForall₂ r)
have inl : IsEmpty α → PartiallyWellOrderedOn {l : List α | ∀ x ∈ l, x ∈ s} (List.SublistForall₂ r)
Tactic: rcases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
inst : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
inl : IsEmpty α → PartiallyWellOrderedOn {l : List α | ∀ x ∈ l, x ∈ s} (List.SublistForall₂ r)
⊢ PartiallyWellOrderedOn {l : List α | ∀ x ∈ l, x ∈ s} (List.SublistForall₂ r)
have inr : Nonempty α → PartiallyWellOrderedOn {l : List α | ∀ x ∈ l, x ∈ s} (List.SublistForall₂ r)
Tactic: rcases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
inst : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h_1 : Nonempty α
⊢ PartiallyWellOrderedOn {l : List α | ∀ x ∈ l, x ∈ s} (List.SublistForall₂ r)
have inr : ∀ (inhabited_h : Inhabited α), PartiallyWellOrderedOn {l : List α | ∀ x ∈ l, x ∈ s} (List.SublistForall₂ r)
Tactic: inhabit α