-- 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 : B ⊗[S] B
zero :
  Eq (α := Ω[B⁄S])
    ((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])
        (((Derivation.liftKaehlerDifferential (R := S) (S := B) (M := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
                (derivationTensorProduct R S A B) :
              Ω[B⁄S] →ₗ[B] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) :
            (a : Ω[B⁄S]) → S ⊗[R] Ω[A⁄R])
          ((Derivation.tensorProductTo (D S B) : (a : B ⊗[S] B) → Ω[B⁄S]) 0)) :
      Ω[B⁄S])
    ((Derivation.tensorProductTo (D S B) : (a : B ⊗[S] B) → Ω[B⁄S]) 0 : Ω[B⁄S])
add :
  ∀ (x y : B ⊗[S] B)
    (e₁ :
      Eq.{u_4 + 1} (α := Ω[B⁄S])
        ((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])
            (((Derivation.liftKaehlerDifferential (R := S) (S := B) (M := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
                    (derivationTensorProduct R S A B) :
                  Ω[B⁄S] →ₗ[B] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) :
                (a : Ω[B⁄S]) → S ⊗[R] Ω[A⁄R])
              ((Derivation.tensorProductTo (D S B) : (a : B ⊗[S] B) → Ω[B⁄S]) x)) :
          Ω[B⁄S])
        ((Derivation.tensorProductTo (D S B) : (a : B ⊗[S] B) → Ω[B⁄S]) x : Ω[B⁄S]))
    (e₂ :
      Eq.{u_4 + 1} (α := Ω[B⁄S])
        ((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])
            (((Derivation.liftKaehlerDifferential (R := S) (S := B) (M := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
                    (derivationTensorProduct R S A B) :
                  Ω[B⁄S] →ₗ[B] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) :
                (a : Ω[B⁄S]) → S ⊗[R] Ω[A⁄R])
              ((Derivation.tensorProductTo (D S B) : (a : B ⊗[S] B) → Ω[B⁄S]) y)) :
          Ω[B⁄S])
        ((Derivation.tensorProductTo (D S B) : (a : B ⊗[S] B) → Ω[B⁄S]) y : Ω[B⁄S])),
    Eq.{u_4 + 1} (α := Ω[B⁄S])
      ((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])
          (((Derivation.liftKaehlerDifferential (R := S) (S := B) (M := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
                  (derivationTensorProduct R S A B) :
                Ω[B⁄S] →ₗ[B] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) :
              (a : Ω[B⁄S]) → S ⊗[R] Ω[A⁄R])
            ((Derivation.tensorProductTo (D S B) : (a : B ⊗[S] B) → Ω[B⁄S]) (x + y))) :
        Ω[B⁄S])
      ((Derivation.tensorProductTo (D S B) : (a : B ⊗[S] B) → Ω[B⁄S]) (x + y) : Ω[B⁄S])
tmul :
  ∀ (x y : B),
    Eq.{u_4 + 1} (α := Ω[B⁄S])
      ((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])
          (((Derivation.liftKaehlerDifferential (R := S) (S := B) (M := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
                  (derivationTensorProduct R S A B) :
                Ω[B⁄S] →ₗ[B] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) :
              (a : Ω[B⁄S]) → S ⊗[R] Ω[A⁄R])
            ((Derivation.tensorProductTo (D S B) : (a : B ⊗[S] B) → Ω[B⁄S]) (x ⊗ₜ[S] y))) :
        Ω[B⁄S])
      ((Derivation.tensorProductTo (D S B) : (a : B ⊗[S] B) → Ω[B⁄S]) (x ⊗ₜ[S] y) : Ω[B⁄S])
⊢ Eq.{u_4 + 1} (α := Ω[B⁄S])
    ((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])
        (((Derivation.liftKaehlerDifferential (R := S) (S := B) (M := TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R])
                (derivationTensorProduct R S A B) :
              Ω[B⁄S] →ₗ[B] TensorProduct.{u_1, u_2, u_3} R S Ω[A⁄R]) :
            (a : Ω[B⁄S]) → S ⊗[R] Ω[A⁄R])
          ((Derivation.tensorProductTo (D S B) : (a : B ⊗[S] B) → Ω[B⁄S]) x)) :
      Ω[B⁄S])
    ((Derivation.tensorProductTo (D S B) : (a : B ⊗[S] B) → Ω[B⁄S]) x : Ω[B⁄S])

Tactic:
induction x with
    | zero => simp
    | add x y e₁ e₂ => simp only [map_add, e₁, e₂]
    | tmul x y =>
      dsimp
      -- We use the specialized version of `map_smul` here for performance.
      simp only [Derivation.tensorProductTo_tmul, LinearMap.map_smul,
        Derivation.liftKaehlerDifferential_comp_D, map_liftBaseChange_smul]
      induction y using h.1.inductionOn
      · simp only [map_zero, smul_zero]
      · simp only [AlgHom.toLinearMap_apply, IsScalarTower.coe_toAlgHom',
          derivationTensorProduct_algebraMap, LinearMap.liftBaseChange_tmul,
          LinearMap.coe_restrictScalars, map_D, one_smul]
      · -- We use the specialized version of `map_smul` here for performance.
        simp only [Derivation.map_smul, LinearMap.map_smul, *, smul_comm x]
      · simp only [map_add, smul_add, *]

Premises used: IsScalarTower.coe_toAlgHom', LinearMap.coe_restrictScalars, smul_zero, AlgHom.toLinearMap_apply, map_zero, map_add, Derivation.liftKaehlerDifferential_comp_D, one_smul, LinearMap.liftBaseChange_tmul, LinearMap.map_smul, KaehlerDifferential.derivationTensorProduct_algebraMap, Derivation.tensorProductTo_tmul, Derivation.map_smul, TensorProduct.tmul, SMulCommClass.smul_comm, KaehlerDifferential.map_D, KaehlerDifferential.map_liftBaseChange_smul, smul_add