awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
hs : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
this : ∀ (k : ℕ), ∃ (m : ℕ), k < m ∧ f m ∈ s
⊢ ¬BddAbove (f ⁻¹' s)

Tactic:
simpa [not_bddAbove_iff, and_comm]

Premises used: and_comm, not_bddAbove_iff
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
rw : (∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)) ↔ ∀ (f : ℕ → α), ¬IsBadSeq r s f
⊢ s.PartiallyWellOrderedOn r ↔ ∀ (f : ℕ → α), ¬IsBadSeq r s f

Tactic:
rw [partiallyWellOrderedOn_iff_exists_lt]

Premises used: Set.partiallyWellOrderedOn_iff_exists_lt
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
f : ℕ → α
⊢ ((∀ (n : ℕ), f n ∈ s) → ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)) ↔ ¬IsBadSeq r s f

Tactic:
simp [IsBadSeq]

Premises used: Set.PartiallyWellOrderedOn.IsBadSeq
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
⊢ (∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)) ↔ ∀ (f : ℕ → α), ¬IsBadSeq r s f

Tactic:
exact forall_congr' fun f => by simp [IsBadSeq]

Premises used: forall_congr'
-- Module: Mathlib.Order.WellFoundedSet
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
⊢ ∃ (k : ℕ) (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k

Tactic:
have h : ∃ (k : ℕ) (g : ℕ → α), (∀ m, m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k :=
      ⟨_, f, fun _ _ => rfl, hf, rfl⟩
-- Module: Mathlib.Order.WellFoundedSet
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
⊢ ∀ 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

Tactic:
obtain ⟨h1, h2, h3⟩ := Classical.choose_spec (Nat.find_spec h)

Premises used: Classical.choose_spec, Nat.find_spec
-- Module: Mathlib.Order.WellFoundedSet
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
⊢ 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)
      ⋯)

Tactic:
obtain ⟨h1, h2, h3⟩ := Classical.choose_spec (Nat.find_spec h)

Premises used: Classical.choose_spec, Nat.find_spec
-- Module: Mathlib.Order.WellFoundedSet
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)
      ⋯)
⊢ 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

Tactic:
obtain ⟨h1, h2, h3⟩ := Classical.choose_spec (Nat.find_spec h)

Premises used: Classical.choose_spec, Nat.find_spec
-- Module: Mathlib.Order.WellFoundedSet
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
⊢ 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)
      ⋯)

Tactic:
h2
-- Module: Mathlib.Order.WellFoundedSet
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
⊢ 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)
      ⋯)

Tactic:
convert! h2
-- Module: Mathlib.Order.WellFoundedSet
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
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)
            ⋯ 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
⊢ { g : ℕ → α // (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ IsMinBadSeq r rk s n g }

Tactic:
refine ⟨Classical.choose (Nat.find_spec h), h1, by convert! h2, fun g hg1 hg2 con => ?_⟩
-- Module: Mathlib.Order.WellFoundedSet
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

Tactic:
Nat.find_min h ?_ ⟨g, fun m mn => (h1 m mn).trans (hg1 m mn), con, rfl⟩

Premises used: Nat.find_min, And.intro, Exists.intro, rfl, Eq.trans
-- Module: Mathlib.Order.WellFoundedSet
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
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
⊢ False

Tactic:
refine Nat.find_min h ?_ ⟨g, fun m mn => (h1 m mn).trans (hg1 m mn), con, rfl⟩

Premises used: Nat.find_min, And.intro, Exists.intro, rfl, Eq.trans
-- Module: Mathlib.Order.WellFoundedSet
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
rwa rwa₁ rwa₂ rwa₃ :
  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)
⊢ 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:
rwa [← h3]
-- Module: Mathlib.Order.WellFoundedSet
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 }
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 }
⊢ (n : ℕ) → { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }

Tactic:
refine Nat.rec ?_ fun n fn => ?_
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : 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⟩
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : 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⟩
-- Module: Mathlib.Order.WellFoundedSet
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
obtain : ∀ (k : ℕ) (mn : m ≤ m + k), (↑(fs m) : ℕ → α) m = (↑(fs (m + k)) : ℕ → α) m
⊢ (↑(fs m) : ℕ → α) m = (↑(fs n) : ℕ → α) m

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le mn

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.Order.WellFoundedSet
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 : ℕ
⊢ (↑(fs m) : ℕ → α) m = (↑(fs (m + 0)) : ℕ → α) m

Tactic:
rfl
-- Module: Mathlib.Order.WellFoundedSet
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
succ : (↑(minBadSeqOfBadSeq r rk s (m + k + 1) (↑(fs (m + k)) : ℕ → α) ⋯) : ℕ → α) m = (↑(fs (m + (k + 1))) : ℕ → α) 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))]

Premises used: Iff.mpr, Nat.zero_le, Nat.lt_succ_iff, And.left, HAdd.hAdd, Set.PartiallyWellOrderedOn.minBadSeqOfBadSeq, OfNat.ofNat, Subtype.val, Nat.add_le_add_left, Subtype.property
-- Module: Mathlib.Order.WellFoundedSet
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
⊢ (↑(minBadSeqOfBadSeq r rk s (m + k + 1) (↑(fs (m + k)) : ℕ → α) ⋯) : ℕ → α) m = (↑(fs (m + (k + 1))) : ℕ → α) m

Tactic:
rfl
-- Module: Mathlib.Order.WellFoundedSet
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
succ :
  ∀ (k : ℕ) (ih : (↑(fs m) : ℕ → α) m = (↑(fs (m + k)) : ℕ → α) m),
    (↑(fs m) : ℕ → α) m = (↑(fs (m + (k + 1))) : ℕ → α) m
⊢ (↑(fs m) : ℕ → α) m = (↑(fs (m + k)) : ℕ → α) 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

Premises used: Iff.mpr, Nat.zero_le, Nat.lt_succ_iff, And.left, HAdd.hAdd, Set.PartiallyWellOrderedOn.minBadSeqOfBadSeq, OfNat.ofNat, Subtype.val, Nat.add_le_add_left, Subtype.property
-- Module: Mathlib.Order.WellFoundedSet
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 : ℕ), 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