awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
have pos : ∀ (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
Tactic: by_cases! h_pos : 0 < t
-- 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
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
pos :
  ∀ (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
⊢ (⇑((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
have neg : ∀ (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: by_cases! h_pos : 0 < t
-- 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
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
have h : 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 =
  t + 1
Tactic: convert! (ne_eq _ _) ▸ not_and.mp (Nat.find_min h_exist (m := t) (by lia)) h_pos
-- 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
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
h_find :
  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
have rwa : (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[1] b ≠ 0
Tactic: rwa [h_find]
-- 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
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
have neg : 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
Tactic: suffices h_find : Nat.find h_exist = 1 by
        rwa [h_find]
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (hypothesis)
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
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
⊢ 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
have h_pos₁ : 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
Tactic: rw [Nat.le_zero, ht, Nat.sub_eq_zero_iff_le] at h_pos
Cleared hypotheses: h_pos
-- 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
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 :
  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
⊢ 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
have linarith : 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 →
  -1 +
        (HAdd.hAdd (α := ℤ)
            (↑(Nat.find (p := fun (n : ℕ) ↦
                  LT.lt (α := ℤ) 0 (↑n : ℤ) ∧
                    (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0)
                  sorry) :
              ℤ)
            1 -
          1) +
      (HAdd.hAdd (α := ℤ) 0 1 -
        (↑(Nat.find (p := fun (n : ℕ) ↦
              LT.lt (α := ℤ) 0 (↑n : ℤ) ∧
                (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0)
              sorry) :
          ℤ)) =
    0
Tactic: linarith [(Nat.find_spec h_exist).1]
-- 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
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 :
  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
linarith :
  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 →
    -1 +
          (HAdd.hAdd (α := ℤ)
              (↑(Nat.find (p := fun (n : ℕ) ↦
                    LT.lt (α := ℤ) 0 (↑n : ℤ) ∧
                      (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0)
                    ⋯) :
                ℤ)
              1 -
            1) +
        (HAdd.hAdd (α := ℤ) 0 1 -
          (↑(Nat.find (p := fun (n : ℕ) ↦
                LT.lt (α := ℤ) 0 (↑n : ℤ) ∧
                  (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0)
                ⋯) :
            ℤ)) =
      0
⊢ 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
have linarith₁ : 1 <
    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 +
        HSub.hSub (α := ℤ)
          (↑(Nat.find (p := fun (n : ℕ) ↦
                LT.lt (α := ℤ) 0 (↑n : ℤ) ∧
                  (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0)
                sorry) :
            ℤ)
          1 +
      (HAdd.hAdd (α := ℤ) 1 1 -
        (↑(Nat.find (p := fun (n : ℕ) ↦
              LT.lt (α := ℤ) 0 (↑n : ℤ) ∧
                (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0)
              sorry) :
          ℤ)) =
    0
Tactic: linarith [(Nat.find_spec h_exist).1]
-- 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
⊢ ∃ (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 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
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]
-- 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
⊢ ∃ (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 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
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]
-- 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
⊢ ∃ (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 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
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]
-- 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)
⊢ False
have obtain : ∀ (n : ℕ) (hn : 0 < n)
  (hb :
    (⇑((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),
  False
Tactic: obtain ⟨n, hn, hb⟩ : ∃ n, 0 < n ∧ (ad k D a)^[n] b ≠ 0 ∧ (ad k D a)^[n + 1] b = 0 := by
    obtain ⟨m, -, hm2⟩ := exist_pow_eq_zero_of_le p ha insep
    have h_exist : ∃ n, 0 < n ∧ (ad k D a)^[n + 1] b = 0 := ⟨p ^ m,
      ⟨expChar_pow_pos D p m, by rw [hm2 (p ^ m + 1) (Nat.le_add_right _ _), Pi.zero_apply]⟩⟩
    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]