-- Module: Mathlib.RingTheory.Kaehler.TensorProduct
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : Algebra S B
inst_9 : IsScalarTower R A B
inst_10 : IsScalarTower R S B
h : Algebra.IsPushout R S A B
x n₁ n₂ : B
h_1 :
  HSMul.hSMul (β := Ω[B⁄S]) x
      ((LinearMap.liftBaseChange S
              ((↑R :
                  {S M : Type u_3} →
                    {M₂ : Type u_4} →
                      [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₂)
                (map R S A B)) :
            (a : S ⊗[R] Ω[A⁄R]) → Ω[B⁄S])
          ((derivationTensorProduct R S A B : (a : B) → S ⊗[R] Ω[A⁄R]) n₁) :
        Ω[B⁄S]) =
    HSMul.hSMul (β := Ω[B⁄S]) x ((D S B : (a : B) → Ω[B⁄S]) n₁ : Ω[B⁄S])
h_2 :
  HSMul.hSMul (β := Ω[B⁄S]) x
      ((LinearMap.liftBaseChange S
              ((↑R :
                  {S M : Type u_3} →
                    {M₂ : Type u_4} →
                      [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₂)
                (map R S A B)) :
            (a : S ⊗[R] Ω[A⁄R]) → Ω[B⁄S])
          ((derivationTensorProduct R S A B : (a : B) → S ⊗[R] Ω[A⁄R]) n₂) :
        Ω[B⁄S]) =
    HSMul.hSMul (β := Ω[B⁄S]) x ((D S B : (a : B) → Ω[B⁄S]) n₂ : Ω[B⁄S])
⊢ HSMul.hSMul (β := Ω[B⁄S]) x
      ((LinearMap.liftBaseChange S
              ((↑R :
                  {S M : Type u_3} →
                    {M₂ : Type u_4} →
                      [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₂)
                (map R S A B)) :
            (a : S ⊗[R] Ω[A⁄R]) → Ω[B⁄S])
          ((derivationTensorProduct R S A B : (a : B) → S ⊗[R] Ω[A⁄R]) (n₁ + n₂)) :
        Ω[B⁄S]) =
    HSMul.hSMul (β := Ω[B⁄S]) x ((D S B : (a : B) → Ω[B⁄S]) (n₁ + n₂) : Ω[B⁄S])

Tactic:
simp only [map_add, smul_add, *]

Premises used: map_add, smul_add