-- 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 }
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)
              ⋯ 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 }
⊢ { 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 : ℕ → α)
  (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: 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]