-- 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'
inst_10 : IsScalarTower R S S'
f g : P.Hom P'
x : P.CotangentSpace
h :
  Eq (α := P'.CotangentSpace)
    ((CotangentSpace.map f - CotangentSpace.map g : (a : P.CotangentSpace) → P'.CotangentSpace) 0)
    (((↑S :
              {S_1 : Type v'} →
                {M : Type w'} →
                  {M₂ : Type (max v' w')} →
                    [inst : Semiring S] →
                      [inst_11 : Semiring S_1] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] →
                                [inst_16 : Module S_1 M] →
                                  [inst_17 : Module S_1 M₂] →
                                    [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            P'.cotangentComplex ∘ₗ
          f.sub g :
        (a : P.CotangentSpace) → P'.CotangentSpace)
      0)
h₁ :
  ∀ (x y : TensorProduct.{w, v, w} P.Ring S Ω[P.Ring⁄R]),
    Eq (α := P'.CotangentSpace)
        ((CotangentSpace.map f - CotangentSpace.map g : (a : P.CotangentSpace) → P'.CotangentSpace) x :
          P'.CotangentSpace)
        (((↑S :
                    {S_1 : Type v'} →
                      {M : Type w'} →
                        {M₂ : Type (max v' w')} →
                          [inst : Semiring S] →
                            [inst_11 : Semiring S_1] →
                              [inst_12 : AddCommMonoid M] →
                                [inst_13 : AddCommMonoid M₂] →
                                  [inst_14 : Module S M] →
                                    [inst_15 : Module S M₂] →
                                      [inst_16 : Module S_1 M] →
                                        [inst_17 : Module S_1 M₂] →
                                          [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                  P'.cotangentComplex ∘ₗ
                f.sub g :
              (a : P.CotangentSpace) → P'.CotangentSpace)
            x :
          P'.CotangentSpace) →
      Eq (α := P'.CotangentSpace)
          ((CotangentSpace.map f - CotangentSpace.map g : (a : P.CotangentSpace) → P'.CotangentSpace) y :
            P'.CotangentSpace)
          (((↑S :
                      {S_1 : Type v'} →
                        {M : Type w'} →
                          {M₂ : Type (max v' w')} →
                            [inst : Semiring S] →
                              [inst_11 : Semiring S_1] →
                                [inst_12 : AddCommMonoid M] →
                                  [inst_13 : AddCommMonoid M₂] →
                                    [inst_14 : Module S M] →
                                      [inst_15 : Module S M₂] →
                                        [inst_16 : Module S_1 M] →
                                          [inst_17 : Module S_1 M₂] →
                                            [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                    P'.cotangentComplex ∘ₗ
                  f.sub g :
                (a : P.CotangentSpace) → P'.CotangentSpace)
              y :
            P'.CotangentSpace) →
        Eq (α := P'.CotangentSpace)
          ((CotangentSpace.map f - CotangentSpace.map g : (a : P.CotangentSpace) → P'.CotangentSpace) (x + y) :
            P'.CotangentSpace)
          (((↑S :
                      {S_1 : Type v'} →
                        {M : Type w'} →
                          {M₂ : Type (max v' w')} →
                            [inst : Semiring S] →
                              [inst_11 : Semiring S_1] →
                                [inst_12 : AddCommMonoid M] →
                                  [inst_13 : AddCommMonoid M₂] →
                                    [inst_14 : Module S M] →
                                      [inst_15 : Module S M₂] →
                                        [inst_16 : Module S_1 M] →
                                          [inst_17 : Module S_1 M₂] →
                                            [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                    P'.cotangentComplex ∘ₗ
                  f.sub g :
                (a : P.CotangentSpace) → P'.CotangentSpace)
              (x + y) :
            P'.CotangentSpace)
h₂ :
  ∀ (x : S) (y : Ω[P.Ring⁄R]),
    Eq (α := P'.CotangentSpace)
      ((CotangentSpace.map f - CotangentSpace.map g : (a : P.CotangentSpace) → P'.CotangentSpace) (x ⊗ₜ[P.Ring] y) :
        P'.CotangentSpace)
      (((↑S :
                  {S_1 : Type v'} →
                    {M : Type w'} →
                      {M₂ : Type (max v' w')} →
                        [inst : Semiring S] →
                          [inst_11 : Semiring S_1] →
                            [inst_12 : AddCommMonoid M] →
                              [inst_13 : AddCommMonoid M₂] →
                                [inst_14 : Module S M] →
                                  [inst_15 : Module S M₂] →
                                    [inst_16 : Module S_1 M] →
                                      [inst_17 : Module S_1 M₂] →
                                        [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                P'.cotangentComplex ∘ₗ
              f.sub g :
            (a : P.CotangentSpace) → P'.CotangentSpace)
          (x ⊗ₜ[P.Ring] y) :
        P'.CotangentSpace)
⊢ Eq (α := P'.CotangentSpace)
    ((CotangentSpace.map f - CotangentSpace.map g : (a : P.CotangentSpace) → P'.CotangentSpace) x : P'.CotangentSpace)
    (((↑S :
                {S_1 : Type v'} →
                  {M : Type w'} →
                    {M₂ : Type (max v' w')} →
                      [inst : Semiring S] →
                        [inst_11 : Semiring S_1] →
                          [inst_12 : AddCommMonoid M] →
                            [inst_13 : AddCommMonoid M₂] →
                              [inst_14 : Module S M] →
                                [inst_15 : Module S M₂] →
                                  [inst_16 : Module S_1 M] →
                                    [inst_17 : Module S_1 M₂] →
                                      [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
              P'.cotangentComplex ∘ₗ
            f.sub g :
          (a : P.CotangentSpace) → P'.CotangentSpace)
        x :
      P'.CotangentSpace)

Tactic:
induction x using TensorProduct.induction_on with
  | zero =>
    simp only [map_zero]
  | add =>
    simp only [map_add, LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply, *]
  | tmul x y =>
    obtain ⟨y, rfl⟩ := KaehlerDifferential.tensorProductTo_surjective _ _ y
    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', LinearMap.sub_apply,
        map_tmul, Hom.toAlgHom_apply, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
        Function.comp_apply, Hom.sub_tmul, LinearMap.map_smul_of_tower, cotangentComplex_mk,
        Hom.subToKer_apply_coe, map_sub, ← algebraMap_eq_smul_one, tmul_sub, smul_sub]

Premises used: map_sub, TensorProduct.tmul_sub, Algebra.Extension.CotangentSpace.map_tmul, LinearMap.coe_restrictScalars, TensorProduct.tmul_smul, TensorProduct.tmul_zero, map_zero, map_add, Algebra.algebraMap_eq_smul_one, smul_sub, TensorProduct.smul_tmul', LinearMap.coe_comp, Algebra.Extension.Hom.subToKer_apply_coe, Derivation.tensorProductTo_tmul, TensorProduct.tmul_add, LinearMap.sub_apply, Function.comp_apply, Algebra.Extension.Hom.sub_tmul, TensorProduct.tmul, LinearMap.map_smul_of_tower, rfl, Algebra.Extension.Hom.toAlgHom_apply, Algebra.Extension.cotangentComplex_mk