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
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
⊢ c⁻¹ * (a * c) * c⁻¹ = c⁻¹ * (c * a) * c⁻¹

Tactic:
apply_fun (c⁻¹ * · * c⁻¹) at hc

Premises used: HMul.hMul, Inv.inv
-- 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)
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 := ⋯ }
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 * c) * c⁻¹ = c⁻¹ * (c * a) * c⁻¹
⊢ c⁻¹ * a = a * c⁻¹

Tactic:
rw [mul_assoc, mul_assoc, mul_inv_cancel₀ hb.1, mul_one, ← mul_assoc,
      inv_mul_cancel₀ hb.1, one_mul] at hc

Premises used: mul_inv_cancel₀, mul_assoc, And.left, mul_one, inv_mul_cancel₀, one_mul
-- 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)
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 := ⋯ }
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⁻¹ * a = a * c⁻¹

Tactic:
hc
-- 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)
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 := ⋯ }
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⁻¹ * a = a * c⁻¹

Tactic:
exact hc
-- 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)
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
⊢ c⁻¹ * a = a * c⁻¹

Tactic:
have hc' : c⁻¹ * a = a * c⁻¹ := by
    apply_fun (c⁻¹ * · * c⁻¹) at hc
    rw [mul_assoc, mul_assoc, mul_inv_cancel₀ hb.1, mul_one, ← mul_assoc,
      inv_mul_cancel₀ hb.1, one_mul] at hc
    exact hc
-- 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)
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⁻¹
rw :
  a *
        (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) :
              (a : D) → D)^[n - Nat.succ 0 + Nat.succ 0 - 1]
          b -
      (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) :
              (a : D) → D)^[n - Nat.succ 0 + Nat.succ 0 - 1]
          b *
        a =
    (((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)
      ((⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - Nat.succ 0] b)
⊢ 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

Tactic:
rw [hc_def, ← Nat.sub_add_cancel hn, Function.iterate_succ_apply' (ad k D a) _ b]

Premises used: Nat.sub_add_cancel
-- 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)
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⁻¹
⊢ a *
        (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) :
              (a : D) → D)^[n - Nat.succ 0 + Nat.succ 0 - 1]
          b -
      (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) :
              (a : D) → D)^[n - Nat.succ 0 + Nat.succ 0 - 1]
          b *
        a =
    (((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)
      ((⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - Nat.succ 0] b)

Tactic:
rfl
-- 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)
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⁻¹
⊢ 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

Tactic:
have c_eq : a * (ad k D a)^[n - 1] b - (ad k D a)^[n - 1] b * a = c := by
    rw [hc_def, ← Nat.sub_add_cancel hn, Function.iterate_succ_apply' (ad k D a) _ b]; rfl
-- 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)
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
simp_rw :
  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
simp_rw₁ :
  c⁻¹ *
      (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) =
    1
simp_rw₂ : c⁻¹ * c = 1
⊢ 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

Tactic:
simp_rw [mul_assoc, (mul_sub_left_distrib c⁻¹ _ _).symm, c_eq, inv_mul_cancel_of_invertible]

Premises used: mul_assoc, mul_sub_left_distrib, Inv.inv, inv_mul_cancel_of_invertible, Eq.symm
-- 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)
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
⊢ 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

Tactic:
have eq1 : c⁻¹ * a * (ad k D a)^[n - 1] b - c⁻¹ * (ad k D a)^[n - 1] b * a = 1 := by
    simp_rw [mul_assoc, (mul_sub_left_distrib c⁻¹ _ _).symm, c_eq, inv_mul_cancel_of_invertible]
-- 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)
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
nth_rw : a * d - d * a = a * 1
⊢ a * d - d * a = a

Tactic:
nth_rw 3 [← mul_one a]

Premises used: mul_one
-- 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)
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

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]
-- 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)
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
⊢ a⁻¹ * (a * d - d * a) = a⁻¹ * a

Tactic:
apply_fun (a⁻¹ * ·) at deq

Premises used: HMul.hMul, Inv.inv
-- 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)
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
⊢ 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

Premises used: mul_sub, mul_assoc, sub_eq_iff_eq_add, inv_mul_cancel₀, one_mul
-- 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)
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
obtain : ∀ (r : ℕ) (hr : Membership.mem (γ := Subring D) k (d ^ p ^ r)), False
⊢ False

Tactic:
obtain ⟨r, hr⟩ := exists_pow_mem_center_of_inseparable p d insep

Premises used: JacobsonNoether.exists_pow_mem_center_of_inseparable