awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Derivation.Basic
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)
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)
⊢ (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)

Tactic:
induction P using Polynomial.induction_on
-- Module: Mathlib.RingTheory.Derivation.Basic
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
x : A
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:
simp
-- Module: Mathlib.RingTheory.Derivation.Basic
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
x : A
p q : R[X]
h :
  (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)
h_1 :
  (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:
simp [add_smul, *]

Premises used: add_smul
-- Module: Mathlib.RingTheory.Derivation.Basic
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
x : A
n : ℕ
a : R
h :
  (D : (a : A) → M)
      ((aeval x : (a : R[X]) → A) (HMul.hMul (α := R[X]) ((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]) ((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]) ((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]) ((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:
simp [mul_smul, ← Nat.cast_smul_eq_nsmul A]

Premises used: Nat.cast_smul_eq_nsmul, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Derivation.Basic
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
D1 D2 : Derivation R A M
s : Set A
h : Set.EqOn.{u_2, u_4} (β := M) (⇑D1 : (a : A) → M) (⇑D2 : (a : A) → M) s
x_1 : A
hx_1 : x_1 ∈ (↑(adjoin R s) : Set A)
x y : A
h_1 : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
h_2 : Membership.mem (γ := Subalgebra R A) (adjoin R s) y
hx : Eq.{u_4 + 1} (α := M) ((D1 : (a : A) → M) x : M) ((D2 : (a : A) → M) x : M)
hy : Eq.{u_4 + 1} (α := M) ((D1 : (a : A) → M) y : M) ((D2 : (a : A) → M) y : M)
⊢ Eq.{u_4 + 1} (α := M) ((D1 : (a : A) → M) (x + y) : M) ((D2 : (a : A) → M) (x + y) : M)

Tactic:
simp only [map_add, *]

Premises used: map_add
-- Module: Mathlib.RingTheory.Derivation.Basic
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
D1 D2 : Derivation R A M
s : Set A
h : Set.EqOn.{u_2, u_4} (β := M) (⇑D1 : (a : A) → M) (⇑D2 : (a : A) → M) s
x_1 : A
hx_1 : x_1 ∈ (↑(adjoin R s) : Set A)
x y : A
h_1 : Membership.mem (γ := Subalgebra R A) (adjoin R s) x
h_2 : Membership.mem (γ := Subalgebra R A) (adjoin R s) y
hx : Eq.{u_4 + 1} (α := M) ((D1 : (a : A) → M) x : M) ((D2 : (a : A) → M) x : M)
hy : Eq.{u_4 + 1} (α := M) ((D1 : (a : A) → M) y : M) ((D2 : (a : A) → M) y : M)
⊢ Eq.{u_4 + 1} (α := M) ((D1 : (a : A) → M) (x * y) : M) ((D2 : (a : A) → M) (x * y) : M)

Tactic:
simp only [leibniz, *]

Premises used: Derivation.leibniz
-- Module: Mathlib.RingTheory.Derivation.Basic
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
D1 D2 : Derivation R A M
s : Set A
hs : Eq (α := Subalgebra R A) (adjoin R s) ⊤
h : Set.EqOn.{u_2, u_4} (β := M) (⇑D1 : (a : A) → M) (⇑D2 : (a : A) → M) s
⊢ D1 = D2

Tactic:
ext fun _ => eqOn_adjoin h <| hs.symm ▸ trivial

Premises used: Derivation.ext, trivial, Eq.rec, Derivation.eqOn_adjoin, Eq.symm
-- Module: Mathlib.RingTheory.Derivation.Basic
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 D1 D2 : Derivation R A M
r : R
a_1 b_1 a b : A
⊢ (0 : (a : A) → M) (a * b) =
    HSMul.hSMul (β := M) a ((0 : (a : A) → M) b : M) + HSMul.hSMul (β := M) b ((0 : (a : A) → M) a : M)

Tactic:
simp only [add_zero, LinearMap.zero_apply, smul_zero]

Premises used: LinearMap.zero_apply, smul_zero, add_zero
-- Module: Mathlib.RingTheory.Derivation.Basic
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
⊢ Eq (α := (a : A) → M) (⇑0 : (a : A) → M) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
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
⊢ Eq (α := A →ₗ[R] M) (↑0 : A →ₗ[R] M) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
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
a : A
⊢ Eq.{u_4 + 1} (α := M) ((0 : (a : A) → M) a : M) (0 : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
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 D1_1 D2_1 : Derivation R A M
r : R
a b : A
D1 D2 : Derivation R A M
⊢ Eq.{u_4 + 1} (α := M) (((↑D1 : A →ₗ[R] M) + (↑D2 : A →ₗ[R] M) : (a : A) → M) 1 : M) (0 : M)

Tactic:
simp
-- Module: Mathlib.RingTheory.Derivation.Basic
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 D1_1 D2_1 : Derivation R A M
r : R
a_1 b_1 : A
D1 D2 : Derivation R A M
a b : A
⊢ ((↑D1 : A →ₗ[R] M) + (↑D2 : A →ₗ[R] M) : (a : A) → M) (a * b) =
    HSMul.hSMul (β := M) a (((↑D1 : A →ₗ[R] M) + (↑D2 : A →ₗ[R] M) : (a : A) → M) b : M) +
      HSMul.hSMul (β := M) b (((↑D1 : A →ₗ[R] M) + (↑D2 : A →ₗ[R] M) : (a : A) → M) a : M)

Tactic:
simp only [leibniz, LinearMap.add_apply, coeFn_coe, smul_add, add_add_add_comm]

Premises used: LinearMap.add_apply, Derivation.leibniz, Derivation.coeFn_coe, add_add_add_comm, smul_add
-- Module: Mathlib.RingTheory.Derivation.Basic
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
D1 D2 : Derivation R A M
⊢ (⇑(D1 + D2) : (a : A) → M) = HAdd.hAdd (α := (a : A) → M) (⇑D1 : (a : A) → M) (⇑D2 : (a : A) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
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
D1 D2 : Derivation R A M
⊢ (↑(D1 + D2) : A →ₗ[R] M) = (↑D1 : A →ₗ[R] M) + (↑D2 : A →ₗ[R] M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
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
D1 D2 : Derivation R A M
a : A
⊢ (D1 + D2 : (a : A) → M) a = HAdd.hAdd (α := M) (β := M) ((D1 : (a : A) → M) a : M) ((D2 : (a : A) → M) a : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
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
rw₂ : HSMul.hSMul (β := M) r 0 = 0
rw₃ rw₄ : Eq.{u_4 + 1} (α := M) 0 0
⊢ Eq.{u_4 + 1} (α := M) ((r • (↑D : A →ₗ[R] M) : (a : A) → M) 1 : M) (0 : M)

Tactic:
rw [LinearMap.smul_apply, coeFn_coe, D.map_one_eq_zero, smul_zero]

Premises used: LinearMap.smul_apply, Derivation.map_one_eq_zero, smul_zero, Derivation.coeFn_coe
-- Module: Mathlib.RingTheory.Derivation.Basic
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_1 b_1 : 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
a b : A
⊢ (r • (↑D : A →ₗ[R] M) : (a : A) → M) (a * b) =
    HSMul.hSMul (β := M) a ((r • (↑D : A →ₗ[R] M) : (a : A) → M) b : M) +
      HSMul.hSMul (β := M) b ((r • (↑D : A →ₗ[R] M) : (a : A) → M) a : M)

Tactic:
simp only [LinearMap.smul_apply, coeFn_coe, leibniz, smul_add,
        smul_comm r (_ : A) (_ : M)]

Premises used: LinearMap.smul_apply, Derivation.leibniz, Derivation.coeFn_coe, SMulCommClass.smul_comm, smul_add
-- Module: Mathlib.RingTheory.Derivation.Basic
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
S : Type u_5
inst_6 : Monoid S
inst_7 : DistribMulAction S M
inst_8 : SMulCommClass R S M
inst_9 : SMulCommClass S A M
r : S
D : Derivation R A M
⊢ (⇑(r • D) : (a : A) → M) = HSMul.hSMul (β := (a : A) → M) r (⇑D : (a : A) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
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
S : Type u_5
inst_6 : Monoid S
inst_7 : DistribMulAction S M
inst_8 : SMulCommClass R S M
inst_9 : SMulCommClass S A M
r : S
D : Derivation R A M
⊢ (↑(r • D) : A →ₗ[R] M) = r • (↑D : A →ₗ[R] M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
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
a : A
S : Type u_5
inst_6 : Monoid S
inst_7 : DistribMulAction S M
inst_8 : SMulCommClass R S M
inst_9 : SMulCommClass S A M
r : S
D : Derivation R A M
⊢ (r • D : (a : A) → M) a = HSMul.hSMul (β := M) r ((D : (a : A) → M) a : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
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
⊢ Eq (α := A → M) ((coeFnAddMonoidHom : (a : Derivation R A M) → A → M) D : A → M) ((⇑D : (a : A) → M) : (a : A) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Derivation.Basic
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 D1 D2 : Derivation R A M
r : 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
inst_17 : SMul S T
inst_18 : IsScalarTower S T M
⊢ IsScalarTower S T (Derivation R A M)

Tactic:
⟨fun _ _ _ => ext fun _ => smul_assoc _ _ _⟩

Premises used: Derivation.toLinearMap, Derivation.ext, smul_assoc, IsScalarTower.mk, DFunLike.coe
-- Module: Mathlib.RingTheory.Derivation.Basic
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 D1 D2 : Derivation R A M
r : 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
inst_17 : SMulCommClass S T M
⊢ SMulCommClass S T (Derivation R A M)

Tactic:
⟨fun _ _ _ => ext fun _ => smul_comm _ _ _⟩

Premises used: Derivation.toLinearMap, Derivation.ext, SMulCommClass.smul_comm, SMulCommClass.mk, DFunLike.coe
-- Module: Mathlib.RingTheory.Derivation.Basic
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 : R
a b : A
N : Type u_5
inst_9 : AddCommMonoid N
inst_10 : Module A N
inst_11 : Module R N
inst_12 : IsScalarTower R A M
inst_13 : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
D : Derivation R A M
⊢ Eq.{u_5 + 1} (α := N)
    (((↑R :
                {S : Type u_2} →
                  {M : Type u_4} →
                    {M₂ : Type u_5} →
                      [inst : Semiring R] →
                        [inst_14 : Semiring S] →
                          [inst_15 : AddCommMonoid M] →
                            [inst_16 : AddCommMonoid M₂] →
                              [inst_17 : Module R M] →
                                [inst_18 : Module R M₂] →
                                  [inst_19 : Module S M] →
                                    [inst_20 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              f ∘ₗ
            (↑D : A →ₗ[R] M) :
          (a : A) → N)
        1 :
      N)
    (0 : N)

Tactic:
simp only [LinearMap.comp_apply, coeFn_coe, map_one_eq_zero, map_zero]

Premises used: Derivation.map_one_eq_zero, LinearMap.comp_apply, map_zero, Derivation.coeFn_coe
-- Module: Mathlib.RingTheory.Derivation.Basic
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
N : Type u_5
inst_9 : AddCommMonoid N
inst_10 : Module A N
inst_11 : Module R N
inst_12 : IsScalarTower R A M
inst_13 : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
r : A
D : Derivation R A M
a_1 : A
H :
  (f : (a : M) → N) (HSMul.hSMul (β := M) r ((D : (a : A) → M) a_1 : M)) =
    HSMul.hSMul (β := N) r ((f : (a : M) → N) ((D : (a : A) → M) a_1 : M) : N)
⊢ Eq.{u_5 + 1} (α := N)
    ((let __LinearMap : A →ₗ[R] N :=
            (↑R :
                  {S : Type u_2} →
                    {M : Type u_4} →
                      {M₂ : Type u_5} →
                        [inst : Semiring R] →
                          [inst_14 : Semiring S] →
                            [inst_15 : AddCommMonoid M] →
                              [inst_16 : AddCommMonoid M₂] →
                                [inst_17 : Module R M] →
                                  [inst_18 : Module R M₂] →
                                    [inst_19 : Module S M] →
                                      [inst_20 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                f ∘ₗ
              (↑(r • D) : A →ₗ[R] M);
          { toLinearMap := __LinearMap, map_one_eq_zero' := ⋯, leibniz' := ⋯ } :
          (a : A) → N)
        a_1 :
      N)
    ((HSMul.hSMul (α := A) (β := Derivation R A N) ((RingHom.id A : (a : A) → A) r : A)
            (let __LinearMap : A →ₗ[R] N :=
              (↑R :
                    {S : Type u_2} →
                      {M : Type u_4} →
                        {M₂ : Type u_5} →
                          [inst : Semiring R] →
                            [inst_14 : Semiring S] →
                              [inst_15 : AddCommMonoid M] →
                                [inst_16 : AddCommMonoid M₂] →
                                  [inst_17 : Module R M] →
                                    [inst_18 : Module R M₂] →
                                      [inst_19 : Module S M] →
                                        [inst_20 : Module S M₂] →
                                          [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  f ∘ₗ
                (↑D : A →ₗ[R] M);
            { toLinearMap := __LinearMap, map_one_eq_zero' := ⋯, leibniz' := ⋯ : Derivation R A N }) :
          (a : A) → N)
        a_1 :
      N)

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Derivation.Basic
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
N : Type u_5
inst_9 : AddCommMonoid N
inst_10 : Module A N
inst_11 : Module R N
inst_12 : IsScalarTower R A M
inst_13 : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
r : A
D : Derivation R A M
a_1 : A
⊢ (f : (a : M) → N) (HSMul.hSMul (β := M) r ((D : (a : A) → M) a_1 : M)) =
    HSMul.hSMul (β := N) r ((f : (a : M) → N) ((D : (a : A) → M) a_1 : M) : N)

Tactic:
simp only [_root_.map_smul]

Premises used: map_smul
-- Module: Mathlib.RingTheory.Derivation.Basic
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 : Type u_5
inst_6 : AddCommMonoid N
inst_7 : Module A N
inst_8 : Module R N
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R A N
f : M →ₗ[A] N
⊢ Eq (α := A →ₗ[R] N)
    (↑(((f.compDer : Derivation R A M →ₗ[A] Derivation R A N) : (a : Derivation R A M) → Derivation R A N) D) :
      A →ₗ[R] N)
    ((↑R :
          {S : Type u_2} →
            {M : Type u_4} →
              {M₂ : Type u_5} →
                [inst : Semiring R] →
                  [inst_11 : Semiring S] →
                    [inst_12 : AddCommMonoid M] →
                      [inst_13 : AddCommMonoid M₂] →
                        [inst_14 : Module R M] →
                          [inst_15 : Module R M₂] →
                            [inst_16 : Module S M] →
                              [inst_17 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        f ∘ₗ
      (↑D : A →ₗ[R] M))

Tactic:
rfl

Premises used: rfl