awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hb :
  (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n] b ≠ 0 ∧
    (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0
hb₁ :
  let c := (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n] b;
  c ≠ 0 ∧ (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n + 1] b = 0
⊢ False
have hc_def : let c := (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n] b;
c = (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n] b
Tactic: set c := (ad k D a)^[n] b with hc_def
Cleared hypotheses: hb
-- 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 := ⋯ }
⊢ a * c = c * a
have h : a * c - c * a = 0
Tactic: apply eq_of_sub_eq_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 ⊤
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 := ⋯ }
⊢ a * c - c * a = 0
have h : HSub.hSub (α := D) (β := D) ((mulLeft (↥k) a : (a : D) → D) c : D) ((mulRight (↥k) a : (a : D) → D) c : D) = 0
Tactic: rw [← mulLeft_apply (R := k), ← mulRight_apply (R := k)]
-- 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 := ⋯ }
this : Eq (α := D) ((((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D) c : D) (0 : D)
⊢ HSub.hSub (α := D) (β := D) ((mulLeft (↥k) a : (a : D) → D) c : D) ((mulRight (↥k) a : (a : D) → D) c : D) = 0
have rw : HSub.hSub (α := D) (β := D) ((mulLeft (↥k) a : (a : D) → D) c : D) ((mulRight (↥k) a : (a : D) → D) c : D) =
  (((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D) c
Tactic: rw [← this]
-- 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 := ⋯ }
⊢ HSub.hSub (α := D) (β := D) ((mulLeft (↥k) a : (a : D) → D) c : D) ((mulRight (↥k) a : (a : D) → D) c : D) = 0
have h : Eq (α := D) ((((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D) c : D) (0 : D)
Tactic: suffices ad k D a c = 0 from by
      rw [← this]; simp [LieRing.of_associative_ring_bracket]
-- 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 := ⋯ }
⊢ Eq (α := D) ((((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D) c : D) (0 : D)
have h : (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n.succ] b = 0
Tactic: rw [← Function.iterate_succ_apply' (ad k D a) n b, hb.2]
-- 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 := ⋯ }
h : (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n.succ] b = 0
⊢ Eq (α := D) ((((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D) c : D) (0 : D)
have h₁ : Eq.{u_1 + 1} (α := D) 0 0
Tactic: rw [← Function.iterate_succ_apply' (ad k D a) n b, hb.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)
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 := ⋯ }
⊢ False
have hc : a * c = c * a
Tactic: have hc : a * c = c * a := by
    apply eq_of_sub_eq_zero
    rw [← mulLeft_apply (R := k), ← mulRight_apply (R := k)]
    suffices ad k D a c = 0 from by
      rw [← this]; simp [LieRing.of_associative_ring_bracket]
    rw [← Function.iterate_succ_apply' (ad k D a) n b, hb.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)
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
⊢ False
have hd_def : let d := c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b;
d = c⁻¹ * a * (⇑((ad (↥k) D : (a : D) → Module.End (↥k) D) a : Module.End (↥k) D) : (a : D) → D)^[n - 1] b
Tactic: set d := c⁻¹ * a * (ad k D a)^[n - 1] b with hd_def
-- 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
⊢ c⁻¹ * a = a * c⁻¹
have hc₁ : c⁻¹ * (a * c) * c⁻¹ = c⁻¹ * (c * a) * c⁻¹
Tactic: apply_fun (c⁻¹ * · * c⁻¹) at hc
Cleared hypotheses: hc
-- 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
⊢ False
have hc' : 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
-- 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⁻¹
⊢ 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
have 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)
Tactic: rw [hc_def, ← Nat.sub_add_cancel hn, Function.iterate_succ_apply' (ad k D a) _ b]
-- 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⁻¹
⊢ False
have 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
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
-- 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
⊢ 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
have 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
Tactic: simp_rw [mul_assoc, (mul_sub_left_distrib c⁻¹ _ _).symm, c_eq, inv_mul_cancel_of_invertible]
-- 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
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
⊢ 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
have 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
Tactic: simp_rw [mul_assoc, (mul_sub_left_distrib c⁻¹ _ _).symm, c_eq, inv_mul_cancel_of_invertible]
-- 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
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
⊢ 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
have simp_rw₂ : c⁻¹ * c = 1
Tactic: simp_rw [mul_assoc, (mul_sub_left_distrib c⁻¹ _ _).symm, c_eq, inv_mul_cancel_of_invertible]
-- 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
⊢ False
have 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
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]