awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
r : R
rw : Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) ((algebraMap R A : (a : R) → A) (r * 1) : A) : M) (0 : M)
⊢ Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) ((algebraMap R A : (a : R) → A) r : A) : M) (0 : M)
have rw₁ : Eq.{u_4 + 1} (α := M)
  ((D : (a : A) → M)
      (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) 1 : A)) :
    M)
  (0 : M)
Tactic: rw [← mul_one r, map_mul, map_one, ← smul_def, map_smul, map_one_eq_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
r : R
rw : Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) ((algebraMap R A : (a : R) → A) (r * 1) : A) : M) (0 : M)
rw₁ :
  Eq.{u_4 + 1} (α := M)
    ((D : (a : A) → M)
        (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) 1 : A)) :
      M)
    (0 : M)
⊢ Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) ((algebraMap R A : (a : R) → A) r : A) : M) (0 : M)
have rw₂ : Eq.{u_4 + 1} (α := M)
  ((D : (a : A) → M) (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) (1 : A)) : M) (0 : M)
Tactic: rw [← mul_one r, map_mul, map_one, ← smul_def, map_smul, map_one_eq_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
r : R
rw : Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) ((algebraMap R A : (a : R) → A) (r * 1) : A) : M) (0 : M)
rw₁ :
  Eq.{u_4 + 1} (α := M)
    ((D : (a : A) → M)
        (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) 1 : A)) :
      M)
    (0 : M)
rw₂ :
  Eq.{u_4 + 1} (α := M)
    ((D : (a : A) → M) (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) (1 : A)) : M) (0 : M)
⊢ Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) ((algebraMap R A : (a : R) → A) r : A) : M) (0 : M)
have rw₃ : Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) (HSMul.hSMul (β := A) r 1) : M) (0 : M)
Tactic: rw [← mul_one r, map_mul, map_one, ← smul_def, map_smul, map_one_eq_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
r : R
rw : Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) ((algebraMap R A : (a : R) → A) (r * 1) : A) : M) (0 : M)
rw₁ :
  Eq.{u_4 + 1} (α := M)
    ((D : (a : A) → M)
        (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) 1 : A)) :
      M)
    (0 : M)
rw₂ :
  Eq.{u_4 + 1} (α := M)
    ((D : (a : A) → M) (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) (1 : A)) : M) (0 : M)
rw₃ : Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) (HSMul.hSMul (β := A) r 1) : M) (0 : M)
⊢ Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) ((algebraMap R A : (a : R) → A) r : A) : M) (0 : M)
have rw₄ : HSMul.hSMul (β := M) r ((D : (a : A) → M) 1 : M) = 0
Tactic: rw [← mul_one r, map_mul, map_one, ← smul_def, map_smul, map_one_eq_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
r : R
rw : Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) ((algebraMap R A : (a : R) → A) (r * 1) : A) : M) (0 : M)
rw₁ :
  Eq.{u_4 + 1} (α := M)
    ((D : (a : A) → M)
        (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) 1 : A)) :
      M)
    (0 : M)
rw₂ :
  Eq.{u_4 + 1} (α := M)
    ((D : (a : A) → M) (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) (1 : A)) : M) (0 : M)
rw₃ : Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) (HSMul.hSMul (β := A) r 1) : M) (0 : M)
rw₄ : HSMul.hSMul (β := M) r ((D : (a : A) → M) 1 : M) = 0
⊢ Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) ((algebraMap R A : (a : R) → A) r : A) : M) (0 : M)
have rw₅ : HSMul.hSMul (β := M) r 0 = 0
Tactic: rw [← mul_one r, map_mul, map_one, ← smul_def, map_smul, map_one_eq_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
r : R
rw : Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) ((algebraMap R A : (a : R) → A) (r * 1) : A) : M) (0 : M)
rw₁ :
  Eq.{u_4 + 1} (α := M)
    ((D : (a : A) → M)
        (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((algebraMap R A : (a : R) → A) 1 : A)) :
      M)
    (0 : M)
rw₂ :
  Eq.{u_4 + 1} (α := M)
    ((D : (a : A) → M) (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) (1 : A)) : M) (0 : M)
rw₃ : Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) (HSMul.hSMul (β := A) r 1) : M) (0 : M)
rw₄ : HSMul.hSMul (β := M) r ((D : (a : A) → M) 1 : M) = 0
rw₅ : HSMul.hSMul (β := M) r 0 = 0
⊢ Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) ((algebraMap R A : (a : R) → A) r : A) : M) (0 : M)
have rw₆ : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [← mul_one r, map_mul, map_one, ← smul_def, map_smul, map_one_eq_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
n : ℕ
⊢ Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) (↑n : A) : M) (0 : M)
have rw : Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) (HSMul.hSMul (β := A) n 1) : M) (0 : M)
Tactic: rw [← nsmul_one, D.map_smul_of_tower n, map_one_eq_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
n : ℕ
rw : Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) (HSMul.hSMul (β := A) n 1) : M) (0 : M)
⊢ Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) (↑n : A) : M) (0 : M)
have rw₁ : HSMul.hSMul (β := M) n ((D : (a : A) → M) 1 : M) = 0
Tactic: rw [← nsmul_one, D.map_smul_of_tower n, map_one_eq_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
n : ℕ
rw : Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) (HSMul.hSMul (β := A) n 1) : M) (0 : M)
rw₁ : HSMul.hSMul (β := M) n ((D : (a : A) → M) 1 : M) = 0
⊢ Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) (↑n : A) : M) (0 : M)
have rw₂ : HSMul.hSMul (β := M) n 0 = 0
Tactic: rw [← nsmul_one, D.map_smul_of_tower n, map_one_eq_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
n : ℕ
rw : Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) (HSMul.hSMul (β := A) n 1) : M) (0 : M)
rw₁ : HSMul.hSMul (β := M) n ((D : (a : A) → M) 1 : M) = 0
rw₂ : HSMul.hSMul (β := M) n 0 = 0
⊢ Eq.{u_4 + 1} (α := M) ((D : (a : A) → M) (↑n : A) : M) (0 : M)
have rw₃ : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [← nsmul_one, D.map_smul_of_tower n, map_one_eq_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
a : A
⊢ (D : (a : A) → M) (HPow.hPow (β := ℕ) a 0) =
    HSMul.hSMul (α := ℕ) 0 (HSMul.hSMul (β := M) (a ^ HSub.hSub (α := ℕ) 0 1) ((D : (a : A) → M) a : M))
have zero : (D : (a : A) → M) 1 = HSMul.hSMul (α := ℕ) 0 (HSMul.hSMul.{u_2, u_4, u_4} (α := A) (β := M) 1 ((D : (a : A) → M) a : M))
Tactic: rw [pow_zero, map_one_eq_zero, zero_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
a : A
zero :
  (D : (a : A) → M) 1 =
    HSMul.hSMul (α := ℕ) 0 (HSMul.hSMul.{u_2, u_4, u_4} (α := A) (β := M) 1 ((D : (a : A) → M) a : M))
⊢ (D : (a : A) → M) (HPow.hPow (β := ℕ) a 0) =
    HSMul.hSMul (α := ℕ) 0 (HSMul.hSMul (β := M) (a ^ HSub.hSub (α := ℕ) 0 1) ((D : (a : A) → M) a : M))
have zero₁ : 0 = HSMul.hSMul (α := ℕ) 0 (HSMul.hSMul.{u_2, u_4, u_4} (α := A) (β := M) 1 ((D : (a : A) → M) a : M))
Tactic: rw [pow_zero, map_one_eq_zero, zero_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
a : A
zero :
  (D : (a : A) → M) 1 =
    HSMul.hSMul (α := ℕ) 0 (HSMul.hSMul.{u_2, u_4, u_4} (α := A) (β := M) 1 ((D : (a : A) → M) a : M))
zero₁ : 0 = HSMul.hSMul (α := ℕ) 0 (HSMul.hSMul.{u_2, u_4, u_4} (α := A) (β := M) 1 ((D : (a : A) → M) a : M))
⊢ (D : (a : A) → M) (HPow.hPow (β := ℕ) a 0) =
    HSMul.hSMul (α := ℕ) 0 (HSMul.hSMul (β := M) (a ^ HSub.hSub (α := ℕ) 0 1) ((D : (a : A) → M) a : M))
have zero₂ : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [pow_zero, map_one_eq_zero, zero_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
a : A
n : ℕ
ihn : (D : (a : A) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : A) → M) a : M)
⊢ (D : (a : A) → M) (a ^ (n + 1)) = (n + 1) • HSMul.hSMul (β := M) (a ^ (n + 1 - 1)) ((D : (a : A) → M) a : M)
have succ : ∀
  (ihn :
    (D : (a : A) → M) (HPow.hPow (β := ℕ) a 0) =
      HSMul.hSMul (α := ℕ) 0 (HSMul.hSMul (β := M) (a ^ HSub.hSub (α := ℕ) 0 1) ((D : (a : A) → M) a : M))),
  (D : (a : A) → M) (a ^ HAdd.hAdd (α := ℕ) 0 1) =
    HAdd.hAdd (α := ℕ) 0 1 • HSMul.hSMul (β := M) (a ^ (HAdd.hAdd (α := ℕ) 0 1 - 1)) ((D : (a : A) → M) a : M)
Tactic: rcases eq_zero_or_pos n with (rfl | hpos)
Cleared hypotheses: n, ihn
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
a : A
n : ℕ
ihn : (D : (a : A) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : A) → M) a : M)
succ :
  ∀
    (ihn :
      (D : (a : A) → M) (HPow.hPow (β := ℕ) a 0) =
        HSMul.hSMul (α := ℕ) 0 (HSMul.hSMul (β := M) (a ^ HSub.hSub (α := ℕ) 0 1) ((D : (a : A) → M) a : M))),
    (D : (a : A) → M) (a ^ HAdd.hAdd (α := ℕ) 0 1) =
      HAdd.hAdd (α := ℕ) 0 1 • HSMul.hSMul (β := M) (a ^ (HAdd.hAdd (α := ℕ) 0 1 - 1)) ((D : (a : A) → M) a : M)
⊢ (D : (a : A) → M) (a ^ (n + 1)) = (n + 1) • HSMul.hSMul (β := M) (a ^ (n + 1 - 1)) ((D : (a : A) → M) a : M)
have succ₁ : ∀ (hpos : 0 < n),
  (D : (a : A) → M) (a ^ (n + 1)) = (n + 1) • HSMul.hSMul (β := M) (a ^ (n + 1 - 1)) ((D : (a : A) → M) a : M)
Tactic: rcases eq_zero_or_pos n with (rfl | hpos)
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
a : A
n : ℕ
ihn : (D : (a : A) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : A) → M) a : M)
hpos : 0 < n
⊢ a * a ^ (n - 1) = a ^ n
have rw : a ^ (n - 1 + 1) = a ^ n
Tactic: rw [← pow_succ', Nat.sub_add_cancel hpos]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
a : A
n : ℕ
ihn : (D : (a : A) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : A) → M) a : M)
hpos : 0 < n
rw : a ^ (n - 1 + 1) = a ^ n
⊢ a * a ^ (n - 1) = a ^ n
have rw₁ : a ^ n = a ^ n
Tactic: rw [← pow_succ', Nat.sub_add_cancel hpos]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (hypothesis)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
a : A
n : ℕ
ihn : (D : (a : A) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : A) → M) a : M)
hpos : 0 < n
⊢ (D : (a : A) → M) (a ^ (n + 1)) = (n + 1) • HSMul.hSMul (β := M) (a ^ (n + 1 - 1)) ((D : (a : A) → M) a : M)
have this : a * a ^ (n - 1) = a ^ n
Tactic: have : a * a ^ (n - 1) = a ^ n := by rw [← pow_succ', Nat.sub_add_cancel hpos]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
a : A
n : ℕ
⊢ (D : (a : A) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : A) → M) a : M)
have zero : (D : (a : A) → M) (HPow.hPow (β := ℕ) a 0) =
  HSMul.hSMul (α := ℕ) 0 (HSMul.hSMul (β := M) (a ^ HSub.hSub (α := ℕ) 0 1) ((D : (a : A) → M) a : M))
Tactic: induction n with
  | zero => rw [pow_zero, map_one_eq_zero, zero_smul]
  | succ n ihn =>
    rcases eq_zero_or_pos n with (rfl | hpos)
    · simp
    · have : a * a ^ (n - 1) = a ^ n := by rw [← pow_succ', Nat.sub_add_cancel hpos]
      simp only [pow_succ', leibniz, ihn, smul_comm a n (_ : M), smul_smul a, add_smul, this,
        Nat.add_succ_sub_one, add_zero, one_nsmul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
a : A
n : ℕ
zero :
  (D : (a : A) → M) (HPow.hPow (β := ℕ) a 0) =
    HSMul.hSMul (α := ℕ) 0 (HSMul.hSMul (β := M) (a ^ HSub.hSub (α := ℕ) 0 1) ((D : (a : A) → M) a : M))
⊢ (D : (a : A) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : A) → M) a : M)
have succ : ∀ (n : ℕ) (ihn : (D : (a : A) → M) (a ^ n) = n • HSMul.hSMul (β := M) (a ^ (n - 1)) ((D : (a : A) → M) a : M)),
  (D : (a : A) → M) (a ^ (n + 1)) = (n + 1) • HSMul.hSMul (β := M) (a ^ (n + 1 - 1)) ((D : (a : A) → M) a : M)
Tactic: induction n with
  | zero => rw [pow_zero, map_one_eq_zero, zero_smul]
  | succ n ihn =>
    rcases eq_zero_or_pos n with (rfl | hpos)
    · simp
    · have : a * a ^ (n - 1) = a ^ n := by rw [← pow_succ', Nat.sub_add_cancel hpos]
      simp only [pow_succ', leibniz, ihn, smul_comm a n (_ : M), smul_smul a, add_smul, this,
        Nat.add_succ_sub_one, add_zero, one_nsmul]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
P : R[X]
x : A
⊢ (D : (a : A) → M) ((aeval x : (a : R[X]) → A) P : A) =
    HSMul.hSMul.{u_2, u_4, u_4} (α := A) (β := M)
      ((aeval x : (a : R[X]) → A) ((derivative : (a : R[X]) → R[X]) P : R[X]) : A) ((D : (a : A) → M) x : M)
have C : ∀ (a : R),
  (D : (a : A) → M) ((aeval x : (a : R[X]) → A) ((C : (a : R) → R[X]) a : R[X]) : A) =
    HSMul.hSMul.{u_2, u_4, u_4} (α := A) (β := M)
      ((aeval x : (a : R[X]) → A) ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) a) : R[X]) : A)
      ((D : (a : A) → M) x : M)
Tactic: induction P using Polynomial.induction_on
Cleared hypotheses: P
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
P : R[X]
x : A
C :
  ∀ (a : R),
    (D : (a : A) → M) ((aeval x : (a : R[X]) → A) ((Polynomial.C : (a : R) → R[X]) a : R[X]) : A) =
      HSMul.hSMul.{u_2, u_4, u_4} (α := A) (β := M)
        ((aeval x : (a : R[X]) → A) ((derivative : (a : R[X]) → R[X]) ((Polynomial.C : (a : R) → R[X]) a) : R[X]) : A)
        ((D : (a : A) → M) x : M)
⊢ (D : (a : A) → M) ((aeval x : (a : R[X]) → A) P : A) =
    HSMul.hSMul.{u_2, u_4, u_4} (α := A) (β := M)
      ((aeval x : (a : R[X]) → A) ((derivative : (a : R[X]) → R[X]) P : R[X]) : A) ((D : (a : A) → M) x : M)
have add : ∀ (p q : R[X]),
  (D : (a : A) → M) ((aeval x : (a : R[X]) → A) p : A) =
      HSMul.hSMul.{u_2, u_4, u_4} (α := A) (β := M)
        ((aeval x : (a : R[X]) → A) ((derivative : (a : R[X]) → R[X]) p : R[X]) : A) ((D : (a : A) → M) x : M) →
    (D : (a : A) → M) ((aeval x : (a : R[X]) → A) q : A) =
        HSMul.hSMul.{u_2, u_4, u_4} (α := A) (β := M)
          ((aeval x : (a : R[X]) → A) ((derivative : (a : R[X]) → R[X]) q : R[X]) : A) ((D : (a : A) → M) x : M) →
      (D : (a : A) → M) ((aeval x : (a : R[X]) → A) (p + q) : A) =
        HSMul.hSMul.{u_2, u_4, u_4} (α := A) (β := M)
          ((aeval x : (a : R[X]) → A) ((derivative : (a : R[X]) → R[X]) (p + q) : R[X]) : A) ((D : (a : A) → M) x : M)
Tactic: induction P using Polynomial.induction_on
Cleared hypotheses: P
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : AddCommMonoid M
inst_3 : Algebra R A
inst_4 : Module A M
inst_5 : Module R M
D : Derivation R A M
P : R[X]
x : A
C :
  ∀ (a : R),
    (D : (a : A) → M) ((aeval x : (a : R[X]) → A) ((Polynomial.C : (a : R) → R[X]) a : R[X]) : A) =
      HSMul.hSMul.{u_2, u_4, u_4} (α := A) (β := M)
        ((aeval x : (a : R[X]) → A) ((derivative : (a : R[X]) → R[X]) ((Polynomial.C : (a : R) → R[X]) a) : R[X]) : A)
        ((D : (a : A) → M) x : M)
add :
  ∀ (p q : R[X]),
    (D : (a : A) → M) ((aeval x : (a : R[X]) → A) p : A) =
        HSMul.hSMul.{u_2, u_4, u_4} (α := A) (β := M)
          ((aeval x : (a : R[X]) → A) ((derivative : (a : R[X]) → R[X]) p : R[X]) : A) ((D : (a : A) → M) x : M) →
      (D : (a : A) → M) ((aeval x : (a : R[X]) → A) q : A) =
          HSMul.hSMul.{u_2, u_4, u_4} (α := A) (β := M)
            ((aeval x : (a : R[X]) → A) ((derivative : (a : R[X]) → R[X]) q : R[X]) : A) ((D : (a : A) → M) x : M) →
        (D : (a : A) → M) ((aeval x : (a : R[X]) → A) (p + q) : A) =
          HSMul.hSMul.{u_2, u_4, u_4} (α := A) (β := M)
            ((aeval x : (a : R[X]) → A) ((derivative : (a : R[X]) → R[X]) (p + q) : R[X]) : A) ((D : (a : A) → M) x : M)
⊢ (D : (a : A) → M) ((aeval x : (a : R[X]) → A) P : A) =
    HSMul.hSMul.{u_2, u_4, u_4} (α := A) (β := M)
      ((aeval x : (a : R[X]) → A) ((derivative : (a : R[X]) → R[X]) P : R[X]) : A) ((D : (a : A) → M) x : M)
have monomial : ∀ (n : ℕ) (a : R),
  (D : (a : A) → M)
        ((aeval x : (a : R[X]) → A)
            (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) :
          A) =
      HSMul.hSMul.{u_2, u_4, u_4} (α := A) (β := M)
        ((aeval x : (a : R[X]) → A)
            ((derivative : (a : R[X]) → R[X])
                (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) :
              R[X]) :
          A)
        ((D : (a : A) → M) x : M) →
    (D : (a : A) → M)
        ((aeval x : (a : R[X]) → A)
            (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
          A) =
      HSMul.hSMul.{u_2, u_4, u_4} (α := A) (β := M)
        ((aeval x : (a : R[X]) → A)
            ((derivative : (a : R[X]) → R[X])
                (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
              R[X]) :
          A)
        ((D : (a : A) → M) x : M)
Tactic: induction P using Polynomial.induction_on
Cleared hypotheses: P
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : AddCommMonoid M
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Module A M
inst_7 : Module B M
inst_8 : Module R M
D_1 D1 D2 : Derivation R A M
r_1 : R
a b : A
S : Type u_5
T : Type u_6
inst_9 : Monoid S
inst_10 : DistribMulAction S M
inst_11 : SMulCommClass R S M
inst_12 : SMulCommClass S A M
inst_13 : Monoid T
inst_14 : DistribMulAction T M
inst_15 : SMulCommClass R T M
inst_16 : SMulCommClass T A M
r : S
D : Derivation R A M
⊢ Eq.{u_4 + 1} (α := M) ((r • (↑D : A →ₗ[R] M) : (a : A) → M) 1 : M) (0 : M)
have rw : HSMul.hSMul (β := M) r (((↑D : A →ₗ[R] M) : (a : A) → M) 1 : M) = 0
Tactic: rw [LinearMap.smul_apply, coeFn_coe, D.map_one_eq_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : AddCommMonoid M
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Module A M
inst_7 : Module B M
inst_8 : Module R M
D_1 D1 D2 : Derivation R A M
r_1 : R
a b : A
S : Type u_5
T : Type u_6
inst_9 : Monoid S
inst_10 : DistribMulAction S M
inst_11 : SMulCommClass R S M
inst_12 : SMulCommClass S A M
inst_13 : Monoid T
inst_14 : DistribMulAction T M
inst_15 : SMulCommClass R T M
inst_16 : SMulCommClass T A M
r : S
D : Derivation R A M
rw : HSMul.hSMul (β := M) r (((↑D : A →ₗ[R] M) : (a : A) → M) 1 : M) = 0
⊢ Eq.{u_4 + 1} (α := M) ((r • (↑D : A →ₗ[R] M) : (a : A) → M) 1 : M) (0 : M)
have rw₁ : HSMul.hSMul (β := M) r ((D : (a : A) → M) 1 : M) = 0
Tactic: rw [LinearMap.smul_apply, coeFn_coe, D.map_one_eq_zero, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : AddCommMonoid M
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Module A M
inst_7 : Module B M
inst_8 : Module R M
D_1 D1 D2 : Derivation R A M
r_1 : R
a b : A
S : Type u_5
T : Type u_6
inst_9 : Monoid S
inst_10 : DistribMulAction S M
inst_11 : SMulCommClass R S M
inst_12 : SMulCommClass S A M
inst_13 : Monoid T
inst_14 : DistribMulAction T M
inst_15 : SMulCommClass R T M
inst_16 : SMulCommClass T A M
r : S
D : Derivation R A M
rw : HSMul.hSMul (β := M) r (((↑D : A →ₗ[R] M) : (a : A) → M) 1 : M) = 0
rw₁ : HSMul.hSMul (β := M) r ((D : (a : A) → M) 1 : M) = 0
⊢ Eq.{u_4 + 1} (α := M) ((r • (↑D : A →ₗ[R] M) : (a : A) → M) 1 : M) (0 : M)
have rw₂ : HSMul.hSMul (β := M) r 0 = 0
Tactic: rw [LinearMap.smul_apply, coeFn_coe, D.map_one_eq_zero, smul_zero]