[GOAL]
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1✝ D2✝ : Derivation R A M
r : R
a b : A
D1 D2 : Derivation R A M
h : (fun D => D.toFun) D1 = (fun D => D.toFun) D2
⊢ D1 = D2
[PROOFSTEP]
cases D1
[GOAL]
case mk
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2✝ : Derivation R A M
r : R
a b : A
D2 : Derivation R A M
toLinearMap✝ : A →ₗ[R] M
map_one_eq_zero'✝ : ↑toLinearMap✝ 1 = 0
leibniz'✝ : ∀ (a b : A), ↑toLinearMap✝ (a * b) = a • ↑toLinearMap✝ b + b • ↑toLinearMap✝ a
h :
  (fun D => D.toFun) { toLinearMap := toLinearMap✝, map_one_eq_zero' := map_one_eq_zero'✝, leibniz' := leibniz'✝ } =
    (fun D => D.toFun) D2
⊢ { toLinearMap := toLinearMap✝, map_one_eq_zero' := map_one_eq_zero'✝, leibniz' := leibniz'✝ } = D2
[PROOFSTEP]
cases D2
[GOAL]
case mk.mk
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
toLinearMap✝¹ : A →ₗ[R] M
map_one_eq_zero'✝¹ : ↑toLinearMap✝¹ 1 = 0
leibniz'✝¹ : ∀ (a b : A), ↑toLinearMap✝¹ (a * b) = a • ↑toLinearMap✝¹ b + b • ↑toLinearMap✝¹ a
toLinearMap✝ : A →ₗ[R] M
map_one_eq_zero'✝ : ↑toLinearMap✝ 1 = 0
leibniz'✝ : ∀ (a b : A), ↑toLinearMap✝ (a * b) = a • ↑toLinearMap✝ b + b • ↑toLinearMap✝ a
h :
  (fun D => D.toFun) { toLinearMap := toLinearMap✝¹, map_one_eq_zero' := map_one_eq_zero'✝¹, leibniz' := leibniz'✝¹ } =
    (fun D => D.toFun) { toLinearMap := toLinearMap✝, map_one_eq_zero' := map_one_eq_zero'✝, leibniz' := leibniz'✝ }
⊢ { toLinearMap := toLinearMap✝¹, map_one_eq_zero' := map_one_eq_zero'✝¹, leibniz' := leibniz'✝¹ } =
    { toLinearMap := toLinearMap✝, map_one_eq_zero' := map_one_eq_zero'✝, leibniz' := leibniz'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toLinearMap
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
toLinearMap✝¹ : A →ₗ[R] M
map_one_eq_zero'✝¹ : ↑toLinearMap✝¹ 1 = 0
leibniz'✝¹ : ∀ (a b : A), ↑toLinearMap✝¹ (a * b) = a • ↑toLinearMap✝¹ b + b • ↑toLinearMap✝¹ a
toLinearMap✝ : A →ₗ[R] M
map_one_eq_zero'✝ : ↑toLinearMap✝ 1 = 0
leibniz'✝ : ∀ (a b : A), ↑toLinearMap✝ (a * b) = a • ↑toLinearMap✝ b + b • ↑toLinearMap✝ a
h :
  (fun D => D.toFun) { toLinearMap := toLinearMap✝¹, map_one_eq_zero' := map_one_eq_zero'✝¹, leibniz' := leibniz'✝¹ } =
    (fun D => D.toFun) { toLinearMap := toLinearMap✝, map_one_eq_zero' := map_one_eq_zero'✝, leibniz' := leibniz'✝ }
⊢ toLinearMap✝¹ = toLinearMap✝
[PROOFSTEP]
exact FunLike.coe_injective h
[GOAL]
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
⊢ ↑D (↑(algebraMap R A) r) = 0
[PROOFSTEP]
rw [← mul_one r, RingHom.map_mul, RingHom.map_one, ← smul_def, map_smul, map_one_eq_zero, smul_zero]
[GOAL]
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
n : ℕ
⊢ ↑D ↑n = 0
[PROOFSTEP]
rw [← nsmul_one, D.map_smul_of_tower n, map_one_eq_zero, smul_zero]
[GOAL]
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
n : ℕ
⊢ ↑D (a ^ n) = n • a ^ (n - 1) • ↑D a
[PROOFSTEP]
induction' n with n ihn
[GOAL]
case zero
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
⊢ ↑D (a ^ Nat.zero) = Nat.zero • a ^ (Nat.zero - 1) • ↑D a
[PROOFSTEP]
rw [Nat.zero_eq, pow_zero, map_one_eq_zero, zero_smul]
[GOAL]
case succ
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
n : ℕ
ihn : ↑D (a ^ n) = n • a ^ (n - 1) • ↑D a
⊢ ↑D (a ^ Nat.succ n) = Nat.succ n • a ^ (Nat.succ n - 1) • ↑D a
[PROOFSTEP]
rcases(zero_le n).eq_or_lt with (rfl | hpos)
[GOAL]
case succ.inl
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
ihn : ↑D (a ^ 0) = 0 • a ^ (0 - 1) • ↑D a
⊢ ↑D (a ^ Nat.succ 0) = Nat.succ 0 • a ^ (Nat.succ 0 - 1) • ↑D a
[PROOFSTEP]
erw [pow_one, one_smul, pow_zero, one_smul]
[GOAL]
case succ.inr
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
n : ℕ
ihn : ↑D (a ^ n) = n • a ^ (n - 1) • ↑D a
hpos : 0 < n
⊢ ↑D (a ^ Nat.succ n) = Nat.succ n • a ^ (Nat.succ n - 1) • ↑D a
[PROOFSTEP]
have : a * a ^ (n - 1) = a ^ n := by rw [← pow_succ, Nat.sub_add_cancel hpos]
[GOAL]
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
n : ℕ
ihn : ↑D (a ^ n) = n • a ^ (n - 1) • ↑D a
hpos : 0 < n
⊢ a * a ^ (n - 1) = a ^ n
[PROOFSTEP]
rw [← pow_succ, Nat.sub_add_cancel hpos]
[GOAL]
case succ.inr
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
n : ℕ
ihn : ↑D (a ^ n) = n • a ^ (n - 1) • ↑D a
hpos : 0 < n
this : a * a ^ (n - 1) = a ^ n
⊢ ↑D (a ^ Nat.succ n) = Nat.succ n • a ^ (Nat.succ n - 1) • ↑D a
[PROOFSTEP]
simp only [pow_succ, leibniz, ihn, smul_comm a n (_ : M), smul_smul a, add_smul, this, Nat.succ_eq_add_one,
  Nat.add_succ_sub_one, add_zero, one_nsmul]
[GOAL]
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
s : Set A
h : Set.EqOn (↑D1) (↑D2) s
x✝ : A
hx✝ : x✝ ∈ ↑(adjoin R s)
x y : A
hx : ↑D1 x = ↑D2 x
hy : ↑D1 y = ↑D2 y
⊢ ↑D1 (x + y) = ↑D2 (x + y)
[PROOFSTEP]
simp only [map_add, *]
[GOAL]
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
s : Set A
h : Set.EqOn (↑D1) (↑D2) s
x✝ : A
hx✝ : x✝ ∈ ↑(adjoin R s)
x y : A
hx : ↑D1 x = ↑D2 x
hy : ↑D1 y = ↑D2 y
⊢ ↑D1 (x * y) = ↑D2 (x * y)
[PROOFSTEP]
simp only [leibniz, *]
[GOAL]
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a✝ b✝ a b : A
⊢ ↑0 (a * b) = a • ↑0 b + b • ↑0 a
[PROOFSTEP]
simp only [add_zero, LinearMap.zero_apply, smul_zero]
[GOAL]
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1✝ D2✝ : Derivation R A M
r : R
a b : A
D1 D2 : Derivation R A M
⊢ ↑(↑D1 + ↑D2) 1 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module A M
inst✝ : Module R M
D D1✝ D2✝ : Derivation R A M
r : R
a✝ b✝ : A
D1 D2 : Derivation R A M
a b : A
⊢ ↑(↑D1 + ↑D2) (a * b) = a • ↑(↑D1 + ↑D2) b + b • ↑(↑D1 + ↑D2) a
[PROOFSTEP]
simp only [leibniz, LinearMap.add_apply, coeFn_coe, smul_add, add_add_add_comm]
[GOAL]
R : Type u_1
inst✝¹³ : CommSemiring R
A : Type u_2
inst✝¹² : CommSemiring A
inst✝¹¹ : Algebra R A
M : Type u_3
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module A M
inst✝⁸ : Module R M
D✝ D1 D2 : Derivation R A M
r✝ : R
a b : A
S : Type u_4
T : Type u_5
inst✝⁷ : Monoid S
inst✝⁶ : DistribMulAction S M
inst✝⁵ : SMulCommClass R S M
inst✝⁴ : SMulCommClass S A M
inst✝³ : Monoid T
inst✝² : DistribMulAction T M
inst✝¹ : SMulCommClass R T M
inst✝ : SMulCommClass T A M
r : S
D : Derivation R A M
⊢ ↑(r • ↑D) 1 = 0
[PROOFSTEP]
rw [LinearMap.smul_apply, coeFn_coe, D.map_one_eq_zero, smul_zero]
[GOAL]
R : Type u_1
inst✝¹³ : CommSemiring R
A : Type u_2
inst✝¹² : CommSemiring A
inst✝¹¹ : Algebra R A
M : Type u_3
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module A M
inst✝⁸ : Module R M
D✝ D1 D2 : Derivation R A M
r✝ : R
a✝ b✝ : A
S : Type u_4
T : Type u_5
inst✝⁷ : Monoid S
inst✝⁶ : DistribMulAction S M
inst✝⁵ : SMulCommClass R S M
inst✝⁴ : SMulCommClass S A M
inst✝³ : Monoid T
inst✝² : DistribMulAction T M
inst✝¹ : SMulCommClass R T M
inst✝ : SMulCommClass T A M
r : S
D : Derivation R A M
a b : A
⊢ ↑(r • ↑D) (a * b) = a • ↑(r • ↑D) b + b • ↑(r • ↑D) a
[PROOFSTEP]
simp only [LinearMap.smul_apply, coeFn_coe, leibniz, smul_add, smul_comm r (_ : A) (_ : M)]
[GOAL]
R : Type u_1
inst✝¹⁰ : CommSemiring R
A : Type u_2
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r : R
a b : A
N : Type u_4
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
D : Derivation R A M
⊢ ↑(LinearMap.comp (↑R f) ↑D) 1 = 0
[PROOFSTEP]
simp only [LinearMap.comp_apply, coeFn_coe, map_one_eq_zero, map_zero]
[GOAL]
R : Type u_1
inst✝¹⁰ : CommSemiring R
A : Type u_2
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r : R
a✝ b✝ : A
N : Type u_4
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
D : Derivation R A M
a b : A
⊢ ↑(LinearMap.comp (↑R f) ↑D) (a * b) = a • ↑(LinearMap.comp (↑R f) ↑D) b + b • ↑(LinearMap.comp (↑R f) ↑D) a
[PROOFSTEP]
simp only [coeFn_coe, LinearMap.comp_apply, LinearMap.map_add, leibniz, LinearMap.coe_restrictScalars,
  LinearMap.map_smul]
[GOAL]
R : Type u_1
inst✝¹⁰ : CommSemiring R
A : Type u_2
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
N : Type u_4
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
D₁ D₂ : Derivation R A M
⊢ (fun D =>
        { toLinearMap := LinearMap.comp (↑R f) ↑D, map_one_eq_zero' := (_ : ↑(↑R f) (↑D 1) = 0),
          leibniz' := (_ : ∀ (a b : A), ↑(↑R f) (↑D (a * b)) = a • ↑f (↑D b) + b • ↑f (↑D a)) })
      (D₁ + D₂) =
    (fun D =>
          { toLinearMap := LinearMap.comp (↑R f) ↑D, map_one_eq_zero' := (_ : ↑(↑R f) (↑D 1) = 0),
            leibniz' := (_ : ∀ (a b : A), ↑(↑R f) (↑D (a * b)) = a • ↑f (↑D b) + b • ↑f (↑D a)) })
        D₁ +
      (fun D =>
          { toLinearMap := LinearMap.comp (↑R f) ↑D, map_one_eq_zero' := (_ : ↑(↑R f) (↑D 1) = 0),
            leibniz' := (_ : ∀ (a b : A), ↑(↑R f) (↑D (a * b)) = a • ↑f (↑D b) + b • ↑f (↑D a)) })
        D₂
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u_1
inst✝¹⁰ : CommSemiring R
A : Type u_2
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
N : Type u_4
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
D₁ D₂ : Derivation R A M
a✝ : A
⊢ ↑((fun D =>
            { toLinearMap := LinearMap.comp (↑R f) ↑D, map_one_eq_zero' := (_ : ↑(↑R f) (↑D 1) = 0),
              leibniz' := (_ : ∀ (a b : A), ↑(↑R f) (↑D (a * b)) = a • ↑f (↑D b) + b • ↑f (↑D a)) })
          (D₁ + D₂))
      a✝ =
    ↑((fun D =>
              { toLinearMap := LinearMap.comp (↑R f) ↑D, map_one_eq_zero' := (_ : ↑(↑R f) (↑D 1) = 0),
                leibniz' := (_ : ∀ (a b : A), ↑(↑R f) (↑D (a * b)) = a • ↑f (↑D b) + b • ↑f (↑D a)) })
            D₁ +
          (fun D =>
              { toLinearMap := LinearMap.comp (↑R f) ↑D, map_one_eq_zero' := (_ : ↑(↑R f) (↑D 1) = 0),
                leibniz' := (_ : ∀ (a b : A), ↑(↑R f) (↑D (a * b)) = a • ↑f (↑D b) + b • ↑f (↑D a)) })
            D₂)
      a✝
[PROOFSTEP]
exact LinearMap.map_add _ _ _
[GOAL]
R : Type u_1
inst✝¹⁰ : CommSemiring R
A : Type u_2
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r✝ : R
a b : A
N : Type u_4
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
r : R
D : Derivation R A M
⊢ AddHom.toFun
      {
        toFun := fun D =>
          { toLinearMap := LinearMap.comp (↑R f) ↑D, map_one_eq_zero' := (_ : ↑(↑R f) (↑D 1) = 0),
            leibniz' := (_ : ∀ (a b : A), ↑(↑R f) (↑D (a * b)) = a • ↑f (↑D b) + b • ↑f (↑D a)) },
        map_add' :=
          (_ :
            ∀ (D₁ D₂ : Derivation R A M),
              (fun D =>
                    { toLinearMap := LinearMap.comp (↑R f) ↑D, map_one_eq_zero' := (_ : ↑(↑R f) (↑D 1) = 0),
                      leibniz' := (_ : ∀ (a b : A), ↑(↑R f) (↑D (a * b)) = a • ↑f (↑D b) + b • ↑f (↑D a)) })
                  (D₁ + D₂) =
                (fun D =>
                      { toLinearMap := LinearMap.comp (↑R f) ↑D, map_one_eq_zero' := (_ : ↑(↑R f) (↑D 1) = 0),
                        leibniz' := (_ : ∀ (a b : A), ↑(↑R f) (↑D (a * b)) = a • ↑f (↑D b) + b • ↑f (↑D a)) })
                    D₁ +
                  (fun D =>
                      { toLinearMap := LinearMap.comp (↑R f) ↑D, map_one_eq_zero' := (_ : ↑(↑R f) (↑D 1) = 0),
                        leibniz' := (_ : ∀ (a b : A), ↑(↑R f) (↑D (a * b)) = a • ↑f (↑D b) + b • ↑f (↑D a)) })
                    D₂) }
      (r • D) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        {
          toFun := fun D =>
            { toLinearMap := LinearMap.comp (↑R f) ↑D, map_one_eq_zero' := (_ : ↑(↑R f) (↑D 1) = 0),
              leibniz' := (_ : ∀ (a b : A), ↑(↑R f) (↑D (a * b)) = a • ↑f (↑D b) + b • ↑f (↑D a)) },
          map_add' :=
            (_ :
              ∀ (D₁ D₂ : Derivation R A M),
                (fun D =>
                      { toLinearMap := LinearMap.comp (↑R f) ↑D, map_one_eq_zero' := (_ : ↑(↑R f) (↑D 1) = 0),
                        leibniz' := (_ : ∀ (a b : A), ↑(↑R f) (↑D (a * b)) = a • ↑f (↑D b) + b • ↑f (↑D a)) })
                    (D₁ + D₂) =
                  (fun D =>
                        { toLinearMap := LinearMap.comp (↑R f) ↑D, map_one_eq_zero' := (_ : ↑(↑R f) (↑D 1) = 0),
                          leibniz' := (_ : ∀ (a b : A), ↑(↑R f) (↑D (a * b)) = a • ↑f (↑D b) + b • ↑f (↑D a)) })
                      D₁ +
                    (fun D =>
                        { toLinearMap := LinearMap.comp (↑R f) ↑D, map_one_eq_zero' := (_ : ↑(↑R f) (↑D 1) = 0),
                          leibniz' := (_ : ∀ (a b : A), ↑(↑R f) (↑D (a * b)) = a • ↑f (↑D b) + b • ↑f (↑D a)) })
                      D₂) }
        D
[PROOFSTEP]
dsimp
[GOAL]
R : Type u_1
inst✝¹⁰ : CommSemiring R
A : Type u_2
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r✝ : R
a b : A
N : Type u_4
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
r : R
D : Derivation R A M
⊢ { toLinearMap := LinearMap.comp (↑R f) (r • ↑D), map_one_eq_zero' := (_ : ↑f (r • ↑D 1) = 0),
      leibniz' := (_ : ∀ (a b : A), ↑f (r • ↑D (a * b)) = a • ↑f (r • ↑D b) + b • ↑f (r • ↑D a)) } =
    r •
      { toLinearMap := LinearMap.comp (↑R f) ↑D, map_one_eq_zero' := (_ : ↑f (↑D 1) = 0),
        leibniz' := (_ : ∀ (a b : A), ↑f (↑D (a * b)) = a • ↑f (↑D b) + b • ↑f (↑D a)) }
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u_1
inst✝¹⁰ : CommSemiring R
A : Type u_2
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r✝ : R
a b : A
N : Type u_4
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
r : R
D : Derivation R A M
a✝ : A
⊢ ↑{ toLinearMap := LinearMap.comp (↑R f) (r • ↑D), map_one_eq_zero' := (_ : ↑f (r • ↑D 1) = 0),
          leibniz' := (_ : ∀ (a b : A), ↑f (r • ↑D (a * b)) = a • ↑f (r • ↑D b) + b • ↑f (r • ↑D a)) }
      a✝ =
    ↑(r •
          { toLinearMap := LinearMap.comp (↑R f) ↑D, map_one_eq_zero' := (_ : ↑f (↑D 1) = 0),
            leibniz' := (_ : ∀ (a b : A), ↑f (↑D (a * b)) = a • ↑f (↑D b) + b • ↑f (↑D a)) })
      a✝
[PROOFSTEP]
exact LinearMap.map_smul (f : M →ₗ[R] N) _ _
[GOAL]
R : Type u_1
inst✝¹⁰ : CommSemiring R
A : Type u_2
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
N : Type u_4
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
f₁ f₂ : M →ₗ[A] N
⊢ (fun f => LinearMap.compDer f) (f₁ + f₂) = (fun f => LinearMap.compDer f) f₁ + (fun f => LinearMap.compDer f) f₂
[PROOFSTEP]
ext
[GOAL]
case h.H
R : Type u_1
inst✝¹⁰ : CommSemiring R
A : Type u_2
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
N : Type u_4
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
f₁ f₂ : M →ₗ[A] N
x✝ : Derivation R A M
a✝ : A
⊢ ↑(↑((fun f => LinearMap.compDer f) (f₁ + f₂)) x✝) a✝ =
    ↑(↑((fun f => LinearMap.compDer f) f₁ + (fun f => LinearMap.compDer f) f₂) x✝) a✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝¹⁰ : CommSemiring R
A : Type u_2
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r✝ : R
a b : A
N : Type u_4
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
r : A
D : M →ₗ[A] N
⊢ AddHom.toFun
      { toFun := fun f => LinearMap.compDer f,
        map_add' :=
          (_ :
            ∀ (f₁ f₂ : M →ₗ[A] N),
              (fun f => LinearMap.compDer f) (f₁ + f₂) =
                (fun f => LinearMap.compDer f) f₁ + (fun f => LinearMap.compDer f) f₂) }
      (r • D) =
    ↑(RingHom.id A) r •
      AddHom.toFun
        { toFun := fun f => LinearMap.compDer f,
          map_add' :=
            (_ :
              ∀ (f₁ f₂ : M →ₗ[A] N),
                (fun f => LinearMap.compDer f) (f₁ + f₂) =
                  (fun f => LinearMap.compDer f) f₁ + (fun f => LinearMap.compDer f) f₂) }
        D
[PROOFSTEP]
ext
[GOAL]
case h.H
R : Type u_1
inst✝¹⁰ : CommSemiring R
A : Type u_2
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r✝ : R
a b : A
N : Type u_4
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
r : A
D : M →ₗ[A] N
x✝ : Derivation R A M
a✝ : A
⊢ ↑(↑(AddHom.toFun
              { toFun := fun f => LinearMap.compDer f,
                map_add' :=
                  (_ :
                    ∀ (f₁ f₂ : M →ₗ[A] N),
                      (fun f => LinearMap.compDer f) (f₁ + f₂) =
                        (fun f => LinearMap.compDer f) f₁ + (fun f => LinearMap.compDer f) f₂) }
              (r • D))
          x✝)
      a✝ =
    ↑(↑(↑(RingHom.id A) r •
              AddHom.toFun
                { toFun := fun f => LinearMap.compDer f,
                  map_add' :=
                    (_ :
                      ∀ (f₁ f₂ : M →ₗ[A] N),
                        (fun f => LinearMap.compDer f) (f₁ + f₂) =
                          (fun f => LinearMap.compDer f) f₁ + (fun f => LinearMap.compDer f) f₂) }
                D)
          x✝)
      a✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝¹⁰ : CommSemiring R
A : Type u_2
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r : R
a b : A
N : Type u_4
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
src✝ : Derivation R A M →ₗ[R] Derivation R A N := LinearMap.compDer ↑e
D : Derivation R A M
⊢ ↑(LinearMap.compDer ↑(LinearEquiv.symm e))
      (AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : Derivation R A M),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        D) =
    D
[PROOFSTEP]
ext a
[GOAL]
case H
R : Type u_1
inst✝¹⁰ : CommSemiring R
A : Type u_2
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r : R
a✝ b : A
N : Type u_4
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
src✝ : Derivation R A M →ₗ[R] Derivation R A N := LinearMap.compDer ↑e
D : Derivation R A M
a : A
⊢ ↑(↑(LinearMap.compDer ↑(LinearEquiv.symm e))
          (AddHom.toFun
            { toAddHom := src✝.toAddHom,
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : Derivation R A M),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
            D))
      a =
    ↑D a
[PROOFSTEP]
exact e.symm_apply_apply (D a)
[GOAL]
R : Type u_1
inst✝¹⁰ : CommSemiring R
A : Type u_2
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r : R
a b : A
N : Type u_4
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
src✝ : Derivation R A M →ₗ[R] Derivation R A N := LinearMap.compDer ↑e
D : Derivation R A N
⊢ AddHom.toFun
      { toAddHom := src✝.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : R) (x : Derivation R A M),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      (↑(LinearMap.compDer ↑(LinearEquiv.symm e)) D) =
    D
[PROOFSTEP]
ext a
[GOAL]
case H
R : Type u_1
inst✝¹⁰ : CommSemiring R
A : Type u_2
inst✝⁹ : CommSemiring A
inst✝⁸ : Algebra R A
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r : R
a✝ b : A
N : Type u_4
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
src✝ : Derivation R A M →ₗ[R] Derivation R A N := LinearMap.compDer ↑e
D : Derivation R A N
a : A
⊢ ↑(AddHom.toFun
          { toAddHom := src✝.toAddHom,
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : Derivation R A M),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
          (↑(LinearMap.compDer ↑(LinearEquiv.symm e)) D))
      a =
    ↑D a
[PROOFSTEP]
exact e.apply_symm_apply (D a)
[GOAL]
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCancelCommMonoid M
inst✝¹ : Module R M
inst✝ : Module A M
D : A →ₗ[R] M
h : ∀ (a b : A), ↑D (a * b) = a • ↑D b + b • ↑D a
⊢ ?m.473416 D h + ↑D 1 = ?m.473416 D h
[PROOFSTEP]
simpa only [one_smul, one_mul] using (h 1 1).symm
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a b : A
n : ℤ
⊢ ↑D ↑n = 0
[PROOFSTEP]
rw [← zsmul_one, D.map_smul_of_tower n, map_one_eq_zero, smul_zero]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a✝ b✝ a b : A
h : a * b = 1
⊢ ↑D a = -a ^ 2 • ↑D b
[PROOFSTEP]
rw [neg_smul]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a✝ b✝ a b : A
h : a * b = 1
⊢ ↑D a = -(a ^ 2 • ↑D b)
[PROOFSTEP]
refine' eq_neg_of_add_eq_zero_left _
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a✝ b✝ a b : A
h : a * b = 1
⊢ ↑D a + a ^ 2 • ↑D b = 0
[PROOFSTEP]
calc
  D a + a ^ 2 • D b = a • b • D a + a • a • D b := by simp only [smul_smul, h, one_smul, sq]
  _ = a • D (a * b) := by rw [leibniz, smul_add, add_comm]
  _ = 0 := by rw [h, map_one_eq_zero, smul_zero]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a✝ b✝ a b : A
h : a * b = 1
⊢ ↑D a + a ^ 2 • ↑D b = a • b • ↑D a + a • a • ↑D b
[PROOFSTEP]
simp only [smul_smul, h, one_smul, sq]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a✝ b✝ a b : A
h : a * b = 1
⊢ a • b • ↑D a + a • a • ↑D b = a • ↑D (a * b)
[PROOFSTEP]
rw [leibniz, smul_add, add_comm]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D D1 D2 : Derivation R A M
r : R
a✝ b✝ a b : A
h : a * b = 1
⊢ a • ↑D (a * b) = 0
[PROOFSTEP]
rw [h, map_one_eq_zero, smul_zero]
[GOAL]
R : Type u_1
inst✝⁸ : CommRing R
A : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module A M
inst✝³ : Module R M
D✝ D1 D2 : Derivation R A M
r : R
a✝ b : A
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
⊢ ↑D a⁻¹ = -a⁻¹ ^ 2 • ↑D a
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
R : Type u_1
inst✝⁸ : CommRing R
A : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module A M
inst✝³ : Module R M
D✝ D1 D2 : Derivation R A M
r : R
a b : A
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
⊢ ↑D 0⁻¹ = -0⁻¹ ^ 2 • ↑D 0
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u_1
inst✝⁸ : CommRing R
A : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module A M
inst✝³ : Module R M
D✝ D1 D2 : Derivation R A M
r : R
a✝ b : A
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
ha : a ≠ 0
⊢ ↑D a⁻¹ = -a⁻¹ ^ 2 • ↑D a
[PROOFSTEP]
exact D.leibniz_of_mul_eq_one (inv_mul_cancel ha)
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D✝ D1 D2 : Derivation R A M
r : R
a✝ b✝ : A
D : Derivation R A M
a b : A
⊢ ↑(-↑D) (a * b) = a • ↑(-↑D) b + b • ↑(-↑D) a
[PROOFSTEP]
simp only [LinearMap.neg_apply, smul_neg, neg_add_rev, leibniz, coeFn_coe, add_comm]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D D1✝ D2✝ : Derivation R A M
r : R
a✝ b✝ : A
D1 D2 : Derivation R A M
a b : A
⊢ ↑(↑D1 - ↑D2) (a * b) = a • ↑(↑D1 - ↑D2) b + b • ↑(↑D1 - ↑D2) a
[PROOFSTEP]
simp only [LinearMap.sub_apply, leibniz, coeFn_coe, smul_sub, add_sub_add_comm]
