-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
x : S
y : P.Ring ⊗[R] P.Ring
h :
  Eq (α := P''.CotangentSpace)
    ((CotangentSpace.map (g.comp f) : (a : P.CotangentSpace) → P''.CotangentSpace)
        (x ⊗ₜ[P.Ring] (Derivation.tensorProductTo (D R P.Ring) : (a : P.Ring ⊗[R] P.Ring) → Ω[P.Ring⁄R]) 0) :
      P''.CotangentSpace)
    (((↑S :
                {S_1 : Type v'} →
                  {M : Type (max v' w')} →
                    {M₂ : Type (max v'' w'')} →
                      [inst : Semiring S] →
                        [inst_23 : Semiring S_1] →
                          [inst_24 : AddCommMonoid M] →
                            [inst_25 : AddCommMonoid M₂] →
                              [inst_26 : Module S M] →
                                [inst_27 : Module S M₂] →
                                  [inst_28 : Module S_1 M] →
                                    [inst_29 : Module S_1 M₂] →
                                      [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
              (CotangentSpace.map g) ∘ₗ
            CotangentSpace.map f :
          (a : P.CotangentSpace) → P''.CotangentSpace)
        (x ⊗ₜ[P.Ring] (Derivation.tensorProductTo (D R P.Ring) : (a : P.Ring ⊗[R] P.Ring) → Ω[P.Ring⁄R]) 0) :
      P''.CotangentSpace)
h₁ :
  ∀ (x_1 y : P.Ring ⊗[R] P.Ring),
    Eq (α := P''.CotangentSpace)
        ((CotangentSpace.map (g.comp f) : (a : P.CotangentSpace) → P''.CotangentSpace)
            (x ⊗ₜ[P.Ring] (Derivation.tensorProductTo (D R P.Ring) : (a : P.Ring ⊗[R] P.Ring) → Ω[P.Ring⁄R]) x_1) :
          P''.CotangentSpace)
        (((↑S :
                    {S_1 : Type v'} →
                      {M : Type (max v' w')} →
                        {M₂ : Type (max v'' w'')} →
                          [inst : Semiring S] →
                            [inst_23 : Semiring S_1] →
                              [inst_24 : AddCommMonoid M] →
                                [inst_25 : AddCommMonoid M₂] →
                                  [inst_26 : Module S M] →
                                    [inst_27 : Module S M₂] →
                                      [inst_28 : Module S_1 M] →
                                        [inst_29 : Module S_1 M₂] →
                                          [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                  (CotangentSpace.map g) ∘ₗ
                CotangentSpace.map f :
              (a : P.CotangentSpace) → P''.CotangentSpace)
            (x ⊗ₜ[P.Ring] (Derivation.tensorProductTo (D R P.Ring) : (a : P.Ring ⊗[R] P.Ring) → Ω[P.Ring⁄R]) x_1) :
          P''.CotangentSpace) →
      Eq (α := P''.CotangentSpace)
          ((CotangentSpace.map (g.comp f) : (a : P.CotangentSpace) → P''.CotangentSpace)
              (x ⊗ₜ[P.Ring] (Derivation.tensorProductTo (D R P.Ring) : (a : P.Ring ⊗[R] P.Ring) → Ω[P.Ring⁄R]) y) :
            P''.CotangentSpace)
          (((↑S :
                      {S_1 : Type v'} →
                        {M : Type (max v' w')} →
                          {M₂ : Type (max v'' w'')} →
                            [inst : Semiring S] →
                              [inst_23 : Semiring S_1] →
                                [inst_24 : AddCommMonoid M] →
                                  [inst_25 : AddCommMonoid M₂] →
                                    [inst_26 : Module S M] →
                                      [inst_27 : Module S M₂] →
                                        [inst_28 : Module S_1 M] →
                                          [inst_29 : Module S_1 M₂] →
                                            [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                    (CotangentSpace.map g) ∘ₗ
                  CotangentSpace.map f :
                (a : P.CotangentSpace) → P''.CotangentSpace)
              (x ⊗ₜ[P.Ring] (Derivation.tensorProductTo (D R P.Ring) : (a : P.Ring ⊗[R] P.Ring) → Ω[P.Ring⁄R]) y) :
            P''.CotangentSpace) →
        Eq (α := P''.CotangentSpace)
          ((CotangentSpace.map (g.comp f) : (a : P.CotangentSpace) → P''.CotangentSpace)
              (x ⊗ₜ[P.Ring]
                (Derivation.tensorProductTo (D R P.Ring) : (a : P.Ring ⊗[R] P.Ring) → Ω[P.Ring⁄R]) (x_1 + y)) :
            P''.CotangentSpace)
          (((↑S :
                      {S_1 : Type v'} →
                        {M : Type (max v' w')} →
                          {M₂ : Type (max v'' w'')} →
                            [inst : Semiring S] →
                              [inst_23 : Semiring S_1] →
                                [inst_24 : AddCommMonoid M] →
                                  [inst_25 : AddCommMonoid M₂] →
                                    [inst_26 : Module S M] →
                                      [inst_27 : Module S M₂] →
                                        [inst_28 : Module S_1 M] →
                                          [inst_29 : Module S_1 M₂] →
                                            [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                    (CotangentSpace.map g) ∘ₗ
                  CotangentSpace.map f :
                (a : P.CotangentSpace) → P''.CotangentSpace)
              (x ⊗ₜ[P.Ring]
                (Derivation.tensorProductTo (D R P.Ring) : (a : P.Ring ⊗[R] P.Ring) → Ω[P.Ring⁄R]) (x_1 + y)) :
            P''.CotangentSpace)
h₂ :
  ∀ (x_1 y : P.Ring),
    Eq (α := P''.CotangentSpace)
      ((CotangentSpace.map (g.comp f) : (a : P.CotangentSpace) → P''.CotangentSpace)
          (x ⊗ₜ[P.Ring]
            (Derivation.tensorProductTo (D R P.Ring) : (a : P.Ring ⊗[R] P.Ring) → Ω[P.Ring⁄R]) (x_1 ⊗ₜ[R] y)) :
        P''.CotangentSpace)
      (((↑S :
                  {S_1 : Type v'} →
                    {M : Type (max v' w')} →
                      {M₂ : Type (max v'' w'')} →
                        [inst : Semiring S] →
                          [inst_23 : Semiring S_1] →
                            [inst_24 : AddCommMonoid M] →
                              [inst_25 : AddCommMonoid M₂] →
                                [inst_26 : Module S M] →
                                  [inst_27 : Module S M₂] →
                                    [inst_28 : Module S_1 M] →
                                      [inst_29 : Module S_1 M₂] →
                                        [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                (CotangentSpace.map g) ∘ₗ
              CotangentSpace.map f :
            (a : P.CotangentSpace) → P''.CotangentSpace)
          (x ⊗ₜ[P.Ring]
            (Derivation.tensorProductTo (D R P.Ring) : (a : P.Ring ⊗[R] P.Ring) → Ω[P.Ring⁄R]) (x_1 ⊗ₜ[R] y)) :
        P''.CotangentSpace)
⊢ Eq (α := P''.CotangentSpace)
    ((CotangentSpace.map (g.comp f) : (a : P.CotangentSpace) → P''.CotangentSpace)
        (x ⊗ₜ[P.Ring] (Derivation.tensorProductTo (D R P.Ring) : (a : P.Ring ⊗[R] P.Ring) → Ω[P.Ring⁄R]) y) :
      P''.CotangentSpace)
    (((↑S :
                {S_1 : Type v'} →
                  {M : Type (max v' w')} →
                    {M₂ : Type (max v'' w'')} →
                      [inst : Semiring S] →
                        [inst_23 : Semiring S_1] →
                          [inst_24 : AddCommMonoid M] →
                            [inst_25 : AddCommMonoid M₂] →
                              [inst_26 : Module S M] →
                                [inst_27 : Module S M₂] →
                                  [inst_28 : Module S_1 M] →
                                    [inst_29 : Module S_1 M₂] →
                                      [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
              (CotangentSpace.map g) ∘ₗ
            CotangentSpace.map f :
          (a : P.CotangentSpace) → P''.CotangentSpace)
        (x ⊗ₜ[P.Ring] (Derivation.tensorProductTo (D R P.Ring) : (a : P.Ring ⊗[R] P.Ring) → Ω[P.Ring⁄R]) y) :
      P''.CotangentSpace)

Tactic:
induction y with
    | zero => simp only [map_zero, tmul_zero]
    | add => simp only [map_add, tmul_add, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
      Function.comp_apply, *]
    | tmul => simp only [Derivation.tensorProductTo_tmul, tmul_smul, smul_tmul', map_tmul,
        Hom.toAlgHom_apply, Hom.comp_toRingHom, RingHom.coe_comp, Function.comp_apply,
        LinearMap.coe_comp, LinearMap.coe_restrictScalars,
        ← IsScalarTower.algebraMap_apply S S' S'']

Premises used: Algebra.Extension.CotangentSpace.map_tmul, LinearMap.coe_restrictScalars, TensorProduct.tmul_smul, TensorProduct.tmul_zero, map_zero, map_add, TensorProduct.smul_tmul', LinearMap.coe_comp, RingHom.coe_comp, Derivation.tensorProductTo_tmul, TensorProduct.tmul_add, Function.comp_apply, TensorProduct.tmul, IsScalarTower.algebraMap_apply, Algebra.Extension.Hom.comp_toRingHom, Algebra.Extension.Hom.toAlgHom_apply