[GOAL]
R : Type u_1
A : Type u_2
inst✝ : CommSemiring R
f g : R[X]
⊢ ↑{
          toAddHom :=
            { toFun := ↑derivative,
              map_add' := (_ : ∀ (x x_1 : R[X]), ↑derivative (x + x_1) = ↑derivative x + ↑derivative x_1) },
          map_smul' := (_ : ∀ (s : R) (p : R[X]), ↑derivative (s • p) = s • ↑derivative p) }
      (f * g) =
    f •
        ↑{
              toAddHom :=
                { toFun := ↑derivative,
                  map_add' := (_ : ∀ (x x_1 : R[X]), ↑derivative (x + x_1) = ↑derivative x + ↑derivative x_1) },
              map_smul' := (_ : ∀ (s : R) (p : R[X]), ↑derivative (s • p) = s • ↑derivative p) }
          g +
      g •
        ↑{
              toAddHom :=
                { toFun := ↑derivative,
                  map_add' := (_ : ∀ (x x_1 : R[X]), ↑derivative (x + x_1) = ↑derivative x + ↑derivative x_1) },
              map_smul' := (_ : ∀ (s : R) (p : R[X]), ↑derivative (s • p) = s • ↑derivative p) }
          f
[PROOFSTEP]
simp [mul_comm, add_comm, derivative_mul]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module R[X] A
D : Derivation R R[X] A
a : R
f : R[X]
⊢ ↑C a • ↑D f = a • ↑D f
[PROOFSTEP]
have : C a • D f = D (C a * f) := by simp
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module R[X] A
D : Derivation R R[X] A
a : R
f : R[X]
⊢ ↑C a • ↑D f = ↑D (↑C a * f)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module R[X] A
D : Derivation R R[X] A
a : R
f : R[X]
this : ↑C a • ↑D f = ↑D (↑C a * f)
⊢ ↑C a • ↑D f = a • ↑D f
[PROOFSTEP]
rw [this, C_mul', D.map_smul]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module R[X] A
D₁ D₂ : Derivation R R[X] A
h : ↑D₁ X = ↑D₂ X
f : R[X]
⊢ f ∈ ↑(Algebra.adjoin R {X})
[PROOFSTEP]
simp only [adjoin_X, Algebra.coe_top, Set.mem_univ]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
a b : A
⊢ (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') (a + b) =
    (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') a +
      (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') b
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
a b : A
⊢ ↑((fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') (a + b)) X =
    ↑((fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') a +
          (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') b)
      X
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
t : R
a : A
⊢ AddHom.toFun
      { toFun := fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative',
        map_add' :=
          (_ :
            ∀ (a b : A),
              (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') (a + b) =
                (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') a +
                  (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') b) }
      (t • a) =
    ↑(RingHom.id R) t •
      AddHom.toFun
        { toFun := fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative',
          map_add' :=
            (_ :
              ∀ (a b : A),
                (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') (a + b) =
                  (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') a +
                    (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') b) }
        a
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
t : R
a : A
⊢ ↑(AddHom.toFun
          { toFun := fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative',
            map_add' :=
              (_ :
                ∀ (a b : A),
                  (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') (a + b) =
                    (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') a +
                      (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') b) }
          (t • a))
      X =
    ↑(↑(RingHom.id R) t •
          AddHom.toFun
            { toFun := fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative',
              map_add' :=
                (_ :
                  ∀ (a b : A),
                    (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') (a + b) =
                      (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') a +
                        (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') b) }
            a)
      X
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
a : A
f : R[X]
⊢ ↑(↑(mkDerivation R) a) f = ↑derivative f • a
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
a : A
⊢ ↑(↑(mkDerivation R) a) X = a
[PROOFSTEP]
simp [mkDerivation_apply]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
⊢ ↑(mkDerivation R) 1 = derivative'
[PROOFSTEP]
ext : 1
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
⊢ ↑(↑(mkDerivation R) 1) X = ↑derivative' X
[PROOFSTEP]
simp [derivative']
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
f : R[X]
⊢ ↑(↑(mkDerivation R) 1) f = ↑derivative f
[PROOFSTEP]
rw [mkDerivation_one_eq_derivative']
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
f : R[X]
⊢ ↑derivative' f = ↑derivative f
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
a : A
⊢ ↑(mkDerivationEquiv R) a = ↑(mkDerivation R) a
[PROOFSTEP]
rfl
