-- 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)
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n] b
x : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
hc : a * c = c * a
d : D := c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b
hc' : c⁻¹ * a = a * c⁻¹
c_eq :
  a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b -
      (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b * a =
    c
eq1 :
  c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b -
      c⁻¹ * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b * a =
    1
rw :
  a * (c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b) -
      c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b * a =
    a * 1
rw₁ :
  a * (c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b) -
      c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b * a =
    a *
      (c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b -
        c⁻¹ * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b * a)
rw₂ :
  a * (c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b) -
      c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b * a =
    a * (c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b) -
      a * (c⁻¹ * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b * a)
⊢ a * d - d * a = a * 1
have rw₃ : a * (c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b) -
    c⁻¹ * a * ((⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b * a) =
  a * (c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b) -
    a * (c⁻¹ * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b * a)
Tactic: rw [hd_def, ← eq1, mul_sub, mul_assoc _ _ a, sub_right_inj, hc',
      ← mul_assoc, ← mul_assoc, ← mul_assoc]