awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.JacobsonNoether
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
obtain :
  ∀ (n : ℕ) (hn : Membership.mem (γ := Subring D) k (a ^ p ^ n)),
    ∃ (n : ℕ), 1 ≤ n ∧ 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

Premises used: JacobsonNoether.exists_pow_mem_center_of_inseparable
-- Module: Mathlib.FieldTheory.JacobsonNoether
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)
⊢ Membership.mem (γ := Subring D) k a

Tactic:
rw [pow_zero, pow_one] at hn

Premises used: pow_zero, pow_one
-- Module: Mathlib.FieldTheory.JacobsonNoether
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
⊢ False

Tactic:
ha hn
-- Module: Mathlib.FieldTheory.JacobsonNoether
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
⊢ False

Tactic:
exact ha hn
-- Module: Mathlib.FieldTheory.JacobsonNoether
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 ≠ 0

Tactic:
have nzero : n ≠ 0 := by
    rintro rfl
    rw [pow_zero, pow_one] at hn
    exact ha hn
-- Module: Mathlib.FieldTheory.JacobsonNoether
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)
nzero : n ≠ 0
⊢ ∃ (n : ℕ), 1 ≤ n ∧ Membership.mem (γ := Subring D) k (a ^ p ^ n)

Tactic:
⟨n, ⟨Nat.one_le_iff_ne_zero.mpr nzero, hn⟩⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Nat.one_le_iff_ne_zero
-- Module: Mathlib.FieldTheory.JacobsonNoether
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)
nzero : n ≠ 0
⊢ ∃ (n : ℕ), 1 ≤ n ∧ Membership.mem (γ := Subring D) k (a ^ p ^ n)

Tactic:
exact ⟨n, ⟨Nat.one_le_iff_ne_zero.mpr nzero, hn⟩⟩
-- Module: Mathlib.FieldTheory.JacobsonNoether
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
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
⊢ ∃ (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

Premises used: JacobsonNoether.exists_pow_mem_center_of_inseparable'
-- Module: Mathlib.FieldTheory.JacobsonNoether
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

Tactic:
⟨m, ⟨hm.1, fun n hn ↦ ?_⟩⟩

Premises used: And.left, And.intro, Exists.intro
-- Module: Mathlib.FieldTheory.JacobsonNoether
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)
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
⊢ ∃ (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:
refine ⟨m, ⟨hm.1, fun n hn ↦ ?_⟩⟩
-- Module: Mathlib.FieldTheory.JacobsonNoether
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
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
⊢ Eq (α := D → D) (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[p ^ m] 0

Tactic:
ext x
-- Module: Mathlib.FieldTheory.JacobsonNoether
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
h : a ^ p ^ m * x - a ^ p ^ m * x = 0
⊢ (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[p ^ m] x = 0 x

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]

Premises used: Subring.mem_center_iff, sub_pow_expChar_pow_of_commute, LinearMap.pow_mulRight, LinearMap.commute_mulLeft_right, LieAlgebra.ad_eq_lmul_left_sub_lmul_right, Pi.zero_apply, Module.End.pow_apply, LinearMap.mulLeft_apply, And.right, LinearMap.mulRight_apply, Iff.mp, LinearMap.sub_apply, LinearMap.pow_mulLeft, Pi.sub_apply
-- Module: Mathlib.FieldTheory.JacobsonNoether
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
⊢ a ^ p ^ m * x - a ^ p ^ m * x = 0

Tactic:
sub_eq_zero_of_eq rfl

Premises used: sub_eq_zero_of_eq, rfl
-- Module: Mathlib.FieldTheory.JacobsonNoether
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
⊢ a ^ p ^ m * x - a ^ p ^ m * x = 0

Tactic:
exact sub_eq_zero_of_eq rfl

Premises used: sub_eq_zero_of_eq, rfl
-- Module: Mathlib.FieldTheory.JacobsonNoether
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

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
-- Module: Mathlib.FieldTheory.JacobsonNoether
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
rw₅ rw₆ : Eq.{u_1 + 1} (α := D → 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

Tactic:
rw [(Nat.sub_eq_iff_eq_add hn).1 rfl, Function.iterate_add, inter, Pi.comp_zero,
    iterate_map_zero, Function.const_zero]

Premises used: Nat.sub_eq_iff_eq_add, Function.iterate_add, Pi.comp_zero, iterate_map_zero, Iff.mp, Function.const_zero, rfl
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
H : Ne (α := Subring D) k ⊤
obtain : ∀ (p : ℕ) (hp : ExpChar D p), ∃ x ∉ k, IsSeparable (↥k) x
⊢ ∃ x ∉ k, IsSeparable (↥k) x

Tactic:
obtain ⟨p, hp⟩ := ExpChar.exists D

Premises used: ExpChar.exists
-- Module: Mathlib.FieldTheory.JacobsonNoether
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Algebra.IsAlgebraic (↥k) D
H : Ne (α := Subring D) k ⊤
p : ℕ
hp : ExpChar D p
by_contra! : ∀ (insep : ∀ (x : D) (_ : x ∉ k), ¬IsSeparable (↥k) x), False
⊢ ∃ x ∉ k, IsSeparable (↥k) x

Tactic:
by_contra! insep
-- Module: Mathlib.FieldTheory.JacobsonNoether
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
⊢ ∀ (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
-- Module: Mathlib.FieldTheory.JacobsonNoether
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
obtain : ∀ (a : D) (ha : a ∉ k), False
⊢ False

Tactic:
obtain ⟨a, ha⟩ := not_forall.mp <| mt (Subring.eq_top_iff' k).mpr H

Premises used: Iff.mp, Classical.not_forall
-- Module: Mathlib.FieldTheory.JacobsonNoether
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
⊢ a ≠ 0

Tactic:
have ha₀ : a ≠ 0 := fun nh ↦ nh ▸ ha <| Subring.zero_mem k
-- Module: Mathlib.FieldTheory.JacobsonNoether
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
⊢ ∃ (x : D), ¬x * a = a * x

Tactic:
rw [Subring.mem_center_iff, not_forall] at ha

Premises used: Subring.mem_center_iff, Classical.not_forall
-- Module: Mathlib.FieldTheory.JacobsonNoether
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
ha₁ : ∃ (x : D), ¬x * a = a * x
⊢ a ≠ 0

Tactic:
rw [Subring.mem_center_iff, not_forall] at ha

Premises used: Subring.mem_center_iff, Classical.not_forall
-- Module: Mathlib.FieldTheory.JacobsonNoether
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
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)
⊢ ∃ (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)

Tactic:
use ha.choose

Premises used: Exists.choose
-- Module: Mathlib.FieldTheory.JacobsonNoether
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
h : a * ha.choose (p := fun (x : D) ↦ ¬x * a = a * x) - ha.choose (p := fun (x : D) ↦ ¬x * a = a * x) * 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)

Tactic:
change a * ha.choose - ha.choose * a ≠ 0

Premises used: Exists.choose
-- Module: Mathlib.FieldTheory.JacobsonNoether
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
⊢ a * ha.choose (p := fun (x : D) ↦ ¬x * a = a * x) - ha.choose (p := fun (x : D) ↦ ¬x * a = a * x) * a ≠ 0

Tactic:
simpa only [ne_eq, sub_eq_zero] using Ne.symm ha.choose_spec

Premises used: Exists.choose_spec, sub_eq_zero, Ne.symm, ne_eq
-- Module: Mathlib.FieldTheory.JacobsonNoether
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
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
⊢ 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
-- Module: Mathlib.FieldTheory.JacobsonNoether
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)
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
⊢ ∃ (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

Premises used: JacobsonNoether.exist_pow_eq_zero_of_le
-- Module: Mathlib.FieldTheory.JacobsonNoether
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
rw₁ rw₂ : Eq.{u_1 + 1} (α := D) 0 0
⊢ (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[p ^ m + 1] b = 0

Tactic:
rw [hm2 (p ^ m + 1) (Nat.le_add_right _ _), Pi.zero_apply]

Premises used: Nat.le_add_right, Pi.zero_apply, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.FieldTheory.JacobsonNoether
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 + 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]⟩⟩
-- Module: Mathlib.FieldTheory.JacobsonNoether
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

Tactic:
⟨Nat.find h_exist, ⟨(Nat.find_spec h_exist).1, ?_, (Nat.find_spec h_exist).2⟩⟩

Premises used: And.right, And.left, And.intro, Nat.find, Exists.intro, Nat.find_spec
-- Module: Mathlib.FieldTheory.JacobsonNoether
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

Tactic:
refine ⟨Nat.find h_exist, ⟨(Nat.find_spec h_exist).1, ?_, (Nat.find_spec h_exist).2⟩⟩
-- Module: Mathlib.FieldTheory.JacobsonNoether
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
⊢ 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

Premises used: HSub.hSub, Nat.find, OfNat.ofNat
-- Module: Mathlib.FieldTheory.JacobsonNoether
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
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
⊢ (⇑((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