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
p : ℕ
inst_2 : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
⊢ ∃ (n : ℕ), 1 ≤ n ∧ Membership.mem (γ := Subring D) k (a ^ p ^ n)
have obtain : ∀ (n : ℕ) (hn : Membership.mem (γ := Subring D) k (a ^ p ^ n)),
  ∃ (n : ℕ), 1 ≤ n ∧ Membership.mem (γ := Subring D) k (a ^ p ^ n)
Tactic: obtain ⟨n, hn⟩ := exists_pow_mem_center_of_inseparable p a hinsep
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (hypothesis)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
p : ℕ
inst_2 : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
hn : Membership.mem (γ := Subring D) k (a ^ HPow.hPow (β := ℕ) p 0)
⊢ False
have hn₁ : Membership.mem (γ := Subring D) k a
Tactic: rw [pow_zero, pow_one] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (hypothesis)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
p : ℕ
inst_2 : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
n : ℕ
hn : Membership.mem (γ := Subring D) k (a ^ p ^ n)
⊢ ∃ (n : ℕ), 1 ≤ n ∧ Membership.mem (γ := Subring D) k (a ^ p ^ n)
have nzero : n ≠ 0
Tactic: have nzero : n ≠ 0 := by
    rintro rfl
    rw [pow_zero, pow_one] at hn
    exact ha hn
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
⊢ ∃ (m : ℕ),
    1 ≤ m ∧
      ∀ (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
have obtain : ∀ (m : ℕ) (hm : 1 ≤ m ∧ Membership.mem (γ := Subring D) k (a ^ p ^ m)),
  ∃ (m : ℕ),
    1 ≤ m ∧
      ∀ (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
Tactic: obtain ⟨m, hm⟩ := exists_pow_mem_center_of_inseparable' p ha hinsep
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
m : ℕ
hm : 1 ≤ m ∧ Membership.mem (γ := Subring D) k (a ^ p ^ m)
⊢ ∃ (m : ℕ),
    1 ≤ m ∧
      ∀ (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
have refine : ∀ (n : ℕ) (hn : 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
Tactic: refine ⟨m, ⟨hm.1, fun n hn ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
m : ℕ
hm : 1 ≤ m ∧ Membership.mem (γ := Subring D) k (a ^ p ^ m)
n : ℕ
hn : p ^ m ≤ n
⊢ Eq (α := D → D) (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[p ^ m] 0
have h : ∀ (x : D), (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[p ^ m] x = 0 x
Tactic: ext x
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
m : ℕ
hm : 1 ≤ m ∧ Membership.mem (γ := Subring D) k (a ^ p ^ m)
n : ℕ
hn : p ^ m ≤ n
x : D
⊢ (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[p ^ m] x = 0 x
have h : a ^ p ^ m * x - a ^ p ^ m * x = 0
Tactic: rw [ad_eq_lmul_left_sub_lmul_right, ← Module.End.pow_apply, Pi.sub_apply,
      sub_pow_expChar_pow_of_commute p m (commute_mulLeft_right a a), sub_apply,
      pow_mulLeft, mulLeft_apply, pow_mulRight, mulRight_apply, Pi.zero_apply,
      Subring.mem_center_iff.1 hm.2 x]
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (hypothesis)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
m : ℕ
hm : 1 ≤ m ∧ Membership.mem (γ := Subring D) k (a ^ p ^ m)
n : ℕ
hn : 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
have inter : Eq (α := D → D) (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[p ^ m] 0
Tactic: have inter : (ad k D a)^[p ^ m] = 0 := by
    ext x
    rw [ad_eq_lmul_left_sub_lmul_right, ← Module.End.pow_apply, Pi.sub_apply,
      sub_pow_expChar_pow_of_commute p m (commute_mulLeft_right a a), sub_apply,
      pow_mulLeft, mulLeft_apply, pow_mulRight, mulRight_apply, Pi.zero_apply,
      Subring.mem_center_iff.1 hm.2 x]
    exact sub_eq_zero_of_eq rfl
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
m : ℕ
hm : 1 ≤ m ∧ Membership.mem (γ := Subring D) k (a ^ p ^ m)
n : ℕ
hn : p ^ m ≤ n
inter : Eq (α := D → D) (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[p ^ m] 0
⊢ Eq (α := D → D) (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n] 0
have rw : Eq (α := D → D) (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - p ^ m + p ^ m] 0
Tactic: rw [(Nat.sub_eq_iff_eq_add hn).1 rfl, Function.iterate_add, inter, Pi.comp_zero,
    iterate_map_zero, Function.const_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
m : ℕ
hm : 1 ≤ m ∧ Membership.mem (γ := Subring D) k (a ^ p ^ m)
n : ℕ
hn : p ^ m ≤ n
inter : Eq (α := D → D) (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[p ^ m] 0
rw :
  Eq (α := D → D) (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - p ^ m + p ^ m]
    0
⊢ Eq (α := D → D) (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n] 0
have rw₁ : Eq (α := D → D)
  ((⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - p ^ m] ∘
    (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[p ^ m])
  0
Tactic: rw [(Nat.sub_eq_iff_eq_add hn).1 rfl, Function.iterate_add, inter, Pi.comp_zero,
    iterate_map_zero, Function.const_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
m : ℕ
hm : 1 ≤ m ∧ Membership.mem (γ := Subring D) k (a ^ p ^ m)
n : ℕ
hn : p ^ m ≤ n
inter : Eq (α := D → D) (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[p ^ m] 0
rw :
  Eq (α := D → D) (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - p ^ m + p ^ m]
    0
rw₁ :
  Eq (α := D → D)
    ((⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - p ^ m] ∘
      (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[p ^ m])
    0
⊢ Eq (α := D → D) (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n] 0
have rw₂ : Eq (α := D → D) ((⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - p ^ m] ∘ 0) 0
Tactic: rw [(Nat.sub_eq_iff_eq_add hn).1 rfl, Function.iterate_add, inter, Pi.comp_zero,
    iterate_map_zero, Function.const_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
m : ℕ
hm : 1 ≤ m ∧ Membership.mem (γ := Subring D) k (a ^ p ^ m)
n : ℕ
hn : p ^ m ≤ n
inter : Eq (α := D → D) (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[p ^ m] 0
rw :
  Eq (α := D → D) (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - p ^ m + p ^ m]
    0
rw₁ :
  Eq (α := D → D)
    ((⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - p ^ m] ∘
      (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[p ^ m])
    0
rw₂ :
  Eq (α := D → D) ((⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - p ^ m] ∘ 0) 0
⊢ Eq (α := D → D) (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n] 0
have rw₃ : Eq (α := D → D)
  (Function.const D ((⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - p ^ m] 0))
  0
Tactic: rw [(Nat.sub_eq_iff_eq_add hn).1 rfl, Function.iterate_add, inter, Pi.comp_zero,
    iterate_map_zero, Function.const_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
m : ℕ
hm : 1 ≤ m ∧ Membership.mem (γ := Subring D) k (a ^ p ^ m)
n : ℕ
hn : p ^ m ≤ n
inter : Eq (α := D → D) (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[p ^ m] 0
rw :
  Eq (α := D → D) (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - p ^ m + p ^ m]
    0
rw₁ :
  Eq (α := D → D)
    ((⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - p ^ m] ∘
      (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[p ^ m])
    0
rw₂ :
  Eq (α := D → D) ((⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - p ^ m] ∘ 0) 0
rw₃ :
  Eq (α := D → D)
    (Function.const D
      ((⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - p ^ m] 0))
    0
⊢ Eq (α := D → D) (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n] 0
have rw₄ : Eq (α := D → D) (Function.const D 0) 0
Tactic: rw [(Nat.sub_eq_iff_eq_add hn).1 rfl, Function.iterate_add, inter, Pi.comp_zero,
    iterate_map_zero, Function.const_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
m : ℕ
hm : 1 ≤ m ∧ Membership.mem (γ := Subring D) k (a ^ p ^ m)
n : ℕ
hn : p ^ m ≤ n
inter : Eq (α := D → D) (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[p ^ m] 0
rw :
  Eq (α := D → D) (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - p ^ m + p ^ m]
    0
rw₁ :
  Eq (α := D → D)
    ((⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - p ^ m] ∘
      (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[p ^ m])
    0
rw₂ :
  Eq (α := D → D) ((⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - p ^ m] ∘ 0) 0
rw₃ :
  Eq (α := D → D)
    (Function.const D
      ((⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - p ^ m] 0))
    0
rw₄ : Eq (α := D → D) (Function.const D 0) 0
⊢ Eq (α := D → D) (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n] 0
have rw₅ : Eq.{u_1 + 1} (α := D → D) 0 0
Tactic: rw [(Nat.sub_eq_iff_eq_add hn).1 rfl, Function.iterate_add, inter, Pi.comp_zero,
    iterate_map_zero, Function.const_zero]
-- 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 ⊤
⊢ ∃ x ∉ k, IsSeparable (↥k) x
have obtain : ∀ (p : ℕ) (hp : ExpChar D p), ∃ x ∉ k, IsSeparable (↥k) x
Tactic: obtain ⟨p, hp⟩ := ExpChar.exists D
-- 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
⊢ ∃ x ∉ k, IsSeparable (↥k) x
have by_contra! : ∀ (insep : ∀ (x : D) (_ : x ∉ k), ¬IsSeparable (↥k) x), False
Tactic: by_contra! insep
-- 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) (_ : x ∉ k), ¬IsSeparable (↥k) x
⊢ False
have insep₁ : ∀ (x : D), IsSeparable (↥k) x → Membership.mem (γ := Subring D) k x
Tactic: replace insep : ∀ x : D, IsSeparable k x → x ∈ k :=
    fun x h ↦ Classical.byContradiction fun hx ↦ insep x hx h
Cleared hypotheses: insep
-- 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
⊢ False
have obtain : ∀ (a : D) (ha : a ∉ k), False
Tactic: obtain ⟨a, ha⟩ := not_forall.mp <| mt (Subring.eq_top_iff' k).mpr H
-- 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
⊢ False
have ha₀ : a ≠ 0
Tactic: have ha₀ : a ≠ 0 := fun nh ↦ nh ▸ ha <| Subring.zero_mem k
-- 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),
    Ne (α := D) ((((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D) b : D) (0 : D)
have ha₁ : ∃ (x : D), ¬x * a = a * x
Tactic: rw [Subring.mem_center_iff, not_forall] at ha
Cleared hypotheses: ha, ha₀
-- 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 : ∃ (x : D), ¬x * a = a * x
ha₀ : a ≠ 0
⊢ ∃ (b : D),
    Ne (α := D) ((((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D) b : D) (0 : D)
have h : Ne (α := D)
  ((((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)
      (ha.choose (p := fun (x : D) ↦ ¬x * a = a * x)) :
    D)
  (0 : D)
Tactic: use ha.choose
-- 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 : ∃ (x : D), ¬x * a = a * x
ha₀ : a ≠ 0
⊢ Ne (α := D)
    ((((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)
        (ha.choose (p := fun (x : D) ↦ ¬x * a = a * x)) :
      D)
    (0 : D)
have h : a * ha.choose (p := fun (x : D) ↦ ¬x * a = a * x) - ha.choose (p := fun (x : D) ↦ ¬x * a = a * x) * a ≠ 0
Tactic: change a * ha.choose - ha.choose * a ≠ 0
-- 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
⊢ False
have obtain : ∀ (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
Tactic: obtain ⟨b, hb1⟩ : ∃ b : D, ad k D a b ≠ 0 := by
    rw [Subring.mem_center_iff, not_forall] at ha
    use ha.choose
    change a * ha.choose - ha.choose * a ≠ 0
    simpa only [ne_eq, sub_eq_zero] using Ne.symm ha.choose_spec
-- 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 : ℕ),
    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 obtain : ∀ (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),
  ∃ (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
Tactic: obtain ⟨m, -, hm2⟩ := exist_pow_eq_zero_of_le p ha insep
-- 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
⊢ (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[p ^ m + 1] b = 0
have rw : Eq.{u_1 + 1} (α := D) (0 b) 0
Tactic: rw [hm2 (p ^ m + 1) (Nat.le_add_right _ _), Pi.zero_apply]
-- 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
rw : Eq.{u_1 + 1} (α := D) (0 b) 0
⊢ (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[p ^ m + 1] b = 0
have rw₁ : Eq.{u_1 + 1} (α := D) 0 0
Tactic: rw [hm2 (p ^ m + 1) (Nat.le_add_right _ _), Pi.zero_apply]
-- 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
⊢ ∃ (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 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
Tactic: 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]⟩⟩
-- 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: refine ⟨Nat.find h_exist, ⟨(Nat.find_spec h_exist).1, ?_, (Nat.find_spec h_exist).2⟩⟩
-- 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
⊢ (⇑((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 ht : 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;
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
Tactic: set t := (Nat.find h_exist - 1 : ℕ) with ht