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)
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
⊢ a * d - d * a = a
have nth_rw : a * d - d * a = a * 1
Tactic: nth_rw 3 [← mul_one a]
-- 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
⊢ 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 -
      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]
-- 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)
⊢ 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]
-- 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)
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
⊢ False
have deq : a * d - d * a = a
Tactic: have deq : a * d - d * a = a := by
    nth_rw 3 [← mul_one a]
    rw [hd_def, ← eq1, mul_sub, mul_assoc _ _ a, sub_right_inj, hc',
      ← mul_assoc, ← mul_assoc, ← mul_assoc]
-- 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)
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
deq : a * d - d * a = a
⊢ False
have deq₁ : a⁻¹ * (a * d - d * a) = a⁻¹ * a
Tactic: apply_fun (a⁻¹ * ·) at deq
Cleared hypotheses: deq
-- 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)
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
deq : a⁻¹ * (a * d - d * a) = a⁻¹ * a
⊢ False
have deq₁ : d = 1 + a⁻¹ * d * a
Tactic: rw [mul_sub, ← mul_assoc, inv_mul_cancel₀ ha₀, one_mul, ← mul_assoc, sub_eq_iff_eq_add] at deq
Cleared hypotheses: deq
-- 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
deq : d = 1 + a⁻¹ * d * a
⊢ False
have obtain : ∀ (r : ℕ) (hr : Membership.mem (γ := Subring D) k (d ^ p ^ r)), False
Tactic: obtain ⟨r, hr⟩ := exists_pow_mem_center_of_inseparable p d 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), 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
deq : d = 1 + a⁻¹ * d * a
r : ℕ
hr : Membership.mem (γ := Subring D) k (d ^ p ^ r)
⊢ False
have deq₁ : d ^ p ^ r = (1 + a⁻¹ * d * a) ^ p ^ r
Tactic: apply_fun (· ^ (p ^ r)) at deq
Cleared hypotheses: deq
-- 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)
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
r : ℕ
hr : Membership.mem (γ := Subring D) k (d ^ p ^ r)
deq : d ^ p ^ r = (1 + a⁻¹ * d * a) ^ p ^ r
⊢ False
have deq₁ : Eq.{u_1 + 1} (α := D) 1 0
Tactic: rw [add_pow_expChar_pow_of_commute p r (Commute.one_left _), one_pow,
    GroupWithZero.conj_pow₀ ha₀, ← hr.comm, mul_assoc, inv_mul_cancel₀ ha₀, mul_one,
    right_eq_add] at deq
Cleared hypotheses: deq
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (hypothesis)
Goal:
L : Type u_2
D : Type u_3
inst : Field L
inst_1 : DivisionRing D
inst_2 : Algebra L D
inst_3 : Algebra.IsAlgebraic L D
inst_4 : IsCentral L D
hneq : Ne.{u_3 + 1} (α := Subalgebra L D) ⊥ ⊤
⊢ ∃ x ∉ ⊥, IsSeparable L x
have hcenter : Eq (α := Subalgebra L D) (Subalgebra.center L D) ⊥
Tactic: have hcenter : Subalgebra.center L D = ⊥ := le_bot_iff.mp IsCentral.out
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (hypothesis)
Goal:
L : Type u_2
D : Type u_3
inst : Field L
inst_1 : DivisionRing D
inst_2 : Algebra L D
inst_3 : Algebra.IsAlgebraic L D
inst_4 : IsCentral L D
hneq : Ne.{u_3 + 1} (α := Subalgebra L D) ⊥ ⊤
hcenter : Eq (α := Subalgebra L D) (Subalgebra.center L D) ⊥
⊢ ∃ x ∉ ⊥, IsSeparable L x
have ntrivial : Ne (α := Subring D) k ⊤
Tactic: have ntrivial : Subring.center D ≠ ⊤ :=
    congr(Subalgebra.toSubring $hcenter).trans_ne (Subalgebra.toSubring_injective.ne hneq)
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (hypothesis)
Goal:
L : Type u_2
D : Type u_3
inst : Field L
inst_1 : DivisionRing D
inst_2 : Algebra L D
inst_3 : Algebra.IsAlgebraic L D
inst_4 : IsCentral L D
hneq : Ne.{u_3 + 1} (α := Subalgebra L D) ⊥ ⊤
hcenter : Eq (α := Subalgebra L D) (Subalgebra.center L D) ⊥
ntrivial : Ne (α := Subring D) k ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := Subalgebra.equivOfEq ⊥ (Subalgebra.center L D) ⋯
equiv : RingEquiv.{u_2, u_3} L ↥k := (AlgEquiv.trans (AlgEquiv.symm (botEquiv L D)) φ).toRingEquiv
x : Algebra.{u_2, u_3} L ↥k := equiv.toRingHom.toAlgebra
x_1 : Algebra.{u_3, u_2} (↥k) L := equiv.symm.toRingHom.toAlgebra
⊢ ∃ x ∉ ⊥, IsSeparable L x
have x : IsScalarTower L (↥k) D
Tactic: have _ : IsScalarTower L (center D) D := .of_algebraMap_eq fun _ ↦ rfl
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (goal)
Goal:
L : Type u_2
D : Type u_3
inst : Field L
inst_1 : DivisionRing D
inst_2 : Algebra L D
inst_3 : Algebra.IsAlgebraic L D
inst_4 : IsCentral L D
hneq : Ne.{u_3 + 1} (α := Subalgebra L D) ⊥ ⊤
hcenter : Eq (α := Subalgebra L D) (Subalgebra.center L D) ⊥
ntrivial : Ne (α := Subring D) k ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := Subalgebra.equivOfEq ⊥ (Subalgebra.center L D) ⋯
equiv : RingEquiv.{u_2, u_3} L ↥k := (AlgEquiv.trans (AlgEquiv.symm (botEquiv L D)) φ).toRingEquiv
x_1 : Algebra.{u_2, u_3} L ↥k := equiv.toRingHom.toAlgebra
x_2 : Algebra.{u_3, u_2} (↥k) L := equiv.symm.toRingHom.toAlgebra
h : IsScalarTower L (↥k) D
x : ↥k
⊢ Eq (α := D) ((algebraMap (↥k) D : (a : ↥k) → D) x : D)
    ((algebraMap L D : (a : L) → D) ((algebraMap (↥k) L : (a : ↥k) → L) x : L) : D)
have rw : Eq (α := D) ((algebraMap (↥k) D : (a : ↥k) → D) x : D)
  ((algebraMap (↥k) D : (a : ↥k) → D) ((algebraMap L ↥k : (a : L) → ↥k) ((algebraMap (↥k) L : (a : ↥k) → L) x) : ↥k) :
    D)
Tactic: rw [IsScalarTower.algebraMap_apply L (center D)]
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (goal)
Goal:
L : Type u_2
D : Type u_3
inst : Field L
inst_1 : DivisionRing D
inst_2 : Algebra L D
inst_3 : Algebra.IsAlgebraic L D
inst_4 : IsCentral L D
hneq : Ne.{u_3 + 1} (α := Subalgebra L D) ⊥ ⊤
hcenter : Eq (α := Subalgebra L D) (Subalgebra.center L D) ⊥
ntrivial : Ne (α := Subring D) k ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := Subalgebra.equivOfEq ⊥ (Subalgebra.center L D) ⋯
equiv : RingEquiv.{u_2, u_3} L ↥k := (AlgEquiv.trans (AlgEquiv.symm (botEquiv L D)) φ).toRingEquiv
x_1 : Algebra.{u_2, u_3} L ↥k := equiv.toRingHom.toAlgebra
x_2 : Algebra.{u_3, u_2} (↥k) L := equiv.symm.toRingHom.toAlgebra
h : IsScalarTower L (↥k) D
x : ↥k
⊢ Eq (α := D) ((algebraMap (↥k) D : (a : ↥k) → D) x : D)
    ((algebraMap (↥k) D : (a : ↥k) → D) ((algebraMap L ↥k : (a : L) → ↥k) ((algebraMap (↥k) L : (a : ↥k) → L) x) : ↥k) :
      D)
have h : x = (algebraMap L ↥k : (a : L) → ↥k) ((algebraMap (↥k) L : (a : ↥k) → L) x)
Tactic: congr
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (hypothesis)
Goal:
L : Type u_2
D : Type u_3
inst : Field L
inst_1 : DivisionRing D
inst_2 : Algebra L D
inst_3 : Algebra.IsAlgebraic L D
inst_4 : IsCentral L D
hneq : Ne.{u_3 + 1} (α := Subalgebra L D) ⊥ ⊤
hcenter : Eq (α := Subalgebra L D) (Subalgebra.center L D) ⊥
ntrivial : Ne (α := Subring D) k ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := Subalgebra.equivOfEq ⊥ (Subalgebra.center L D) ⋯
equiv : RingEquiv.{u_2, u_3} L ↥k := (AlgEquiv.trans (AlgEquiv.symm (botEquiv L D)) φ).toRingEquiv
x : Algebra.{u_2, u_3} L ↥k := equiv.toRingHom.toAlgebra
x_1 : Algebra.{u_3, u_2} (↥k) L := equiv.symm.toRingHom.toAlgebra
h : IsScalarTower L (↥k) D
⊢ ∃ x ∉ ⊥, IsSeparable L x
have x : IsScalarTower (↥k) L D
Tactic: have _ : IsScalarTower (center D) L D := .of_algebraMap_eq fun x ↦ by
    rw [IsScalarTower.algebraMap_apply L (center D)]
    congr
    exact (equiv.apply_symm_apply x).symm
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (hypothesis)
Goal:
L : Type u_2
D : Type u_3
inst : Field L
inst_1 : DivisionRing D
inst_2 : Algebra L D
inst_3 : Algebra.IsAlgebraic L D
inst_4 : IsCentral L D
hneq : Ne.{u_3 + 1} (α := Subalgebra L D) ⊥ ⊤
hcenter : Eq (α := Subalgebra L D) (Subalgebra.center L D) ⊥
ntrivial : Ne (α := Subring D) k ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := Subalgebra.equivOfEq ⊥ (Subalgebra.center L D) ⋯
equiv : RingEquiv.{u_2, u_3} L ↥k := (AlgEquiv.trans (AlgEquiv.symm (botEquiv L D)) φ).toRingEquiv
x : Algebra.{u_2, u_3} L ↥k := equiv.toRingHom.toAlgebra
x_1 : Algebra.{u_3, u_2} (↥k) L := equiv.symm.toRingHom.toAlgebra
h : IsScalarTower L (↥k) D
h_1 : IsScalarTower (↥k) L D
⊢ ∃ x ∉ ⊥, IsSeparable L x
have x : Algebra.IsAlgebraic (↥k) D
Tactic: have _ : Algebra.IsAlgebraic (center D) D := .tower_top (K := L) _
-- Lean 4 proof step from Mathlib.FieldTheory.JacobsonNoether (goal)
Goal:
L : Type u_2
D : Type u_3
inst : Field L
inst_1 : DivisionRing D
inst_2 : Algebra L D
inst_3 : Algebra.IsAlgebraic L D
inst_4 : IsCentral L D
hneq : Ne.{u_3 + 1} (α := Subalgebra L D) ⊥ ⊤
hcenter : Eq (α := Subalgebra L D) (Subalgebra.center L D) ⊥
ntrivial : Ne (α := Subring D) k ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := Subalgebra.equivOfEq ⊥ (Subalgebra.center L D) ⋯
equiv : RingEquiv.{u_2, u_3} L ↥k := (AlgEquiv.trans (AlgEquiv.symm (botEquiv L D)) φ).toRingEquiv
x : Algebra.{u_2, u_3} L ↥k := equiv.toRingHom.toAlgebra
x_1 : Algebra.{u_3, u_2} (↥k) L := equiv.symm.toRingHom.toAlgebra
h : IsScalarTower L (↥k) D
h_1 : IsScalarTower (↥k) L D
h_2 : Algebra.IsAlgebraic (↥k) D
⊢ ∃ x ∉ ⊥, IsSeparable L x
have obtain : ∀ (x : D) (hxd : x ∉ k) (hx : IsSeparable (↥k) x), ∃ x ∉ ⊥, IsSeparable L x
Tactic: obtain ⟨x, hxd, hx⟩ := exists_separable_and_not_isCentral D ntrivial