-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
H : Ne (α := Subring D) k ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : Ne (α := D) ((((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D) b : D) (0 : D)
m : ℕ
hm2 :
  ∀ (n : ℕ),
    p ^ m ≤ n → Eq (α := D → D) (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n] 0
h_exist :
  ∃ (n : ℕ), 0 < n ∧ (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0
refine :
  (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) :
          (a : D) →
            D)^[Nat.find (p := fun (n : ℕ) ↦
          0 < n ∧ (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0)
          h_exist]
      b ≠
    0
refine₁ :
  let t :=
    Nat.find (p := fun (n : ℕ) ↦
        0 < n ∧ (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0)
        h_exist -
      1;
  ∀
    (ht :
      t =
        Nat.find (p := fun (n : ℕ) ↦
            0 < n ∧ (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0)
            h_exist -
          1),
    (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) :
            (a : D) →
              D)^[Nat.find (p := fun (n : ℕ) ↦
            0 < n ∧ (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0)
            h_exist]
        b ≠
      0
pos :
  let t :=
    Nat.find (p := fun (n : ℕ) ↦
        0 < n ∧ (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0)
        h_exist -
      1;
  ∀
    (ht :
      t =
        Nat.find (p := fun (n : ℕ) ↦
            0 < n ∧ (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0)
            h_exist -
          1)
    (h_pos : 0 < t),
    (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) :
            (a : D) →
              D)^[Nat.find (p := fun (n : ℕ) ↦
            0 < n ∧ (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0)
            h_exist]
        b ≠
      0
⊢ ∃ (n : ℕ),
    0 < n ∧
      (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n] b ≠ 0 ∧
        (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0
have neg : let t :=
  Nat.find (p := fun (n : ℕ) ↦
      0 < n ∧ (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0)
      h_exist -
    1;
∀
  (ht :
    t =
      Nat.find (p := fun (n : ℕ) ↦
          0 < n ∧ (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0)
          h_exist -
        1)
  (h_pos : t ≤ 0),
  (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) :
          (a : D) →
            D)^[Nat.find (p := fun (n : ℕ) ↦
          0 < n ∧ (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0)
          h_exist]
      b ≠
    0
Tactic: classical
    refine ⟨Nat.find h_exist, ⟨(Nat.find_spec h_exist).1, ?_, (Nat.find_spec h_exist).2⟩⟩
    set t := (Nat.find h_exist - 1 : ℕ) with ht
    by_cases! h_pos : 0 < t
    · convert! (ne_eq _ _) ▸ not_and.mp (Nat.find_min h_exist (m := t) (by lia)) h_pos
      lia
    · suffices h_find : Nat.find h_exist = 1 by
        rwa [h_find]
      rw [Nat.le_zero, ht, Nat.sub_eq_zero_iff_le] at h_pos
      linarith [(Nat.find_spec h_exist).1]