-- Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.Flat R T
t : T
x : ↥P.ker
simp :
  HSMul.hSMul (β := Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((LinearEquiv.restrictScalars T (LinearEquiv.symm cotangentEquivCotangentKer) :
            (a : P.baseChange.ker.Cotangent) → P.baseChange.Cotangent)
          (((Ideal.toCotangent (ker P.baseChange) :
                LinearMap (R := TensorProduct.{u_1, u_3, u} R T P.Ring)
                  (RingHom.id (TensorProduct.{u_1, u_3, u} R T P.Ring))
                  (↥(ker P.baseChange : Ideal (Ring (R := T) (S := T ⊗[R] S) P.baseChange)))
                  (Ideal.Cotangent (R := TensorProduct.{u_1, u_3, u} R T P.Ring)
                    (ker P.baseChange : Ideal (Ring (R := T) (S := T ⊗[R] S) P.baseChange)))) :
              (a : ↥P.baseChange.ker) → P.baseChange.ker.Cotangent)
            (((LinearEquiv.ofEq
                    (Ideal.map (F := P.Ring →+* TensorProduct.{u_1, u_3, u} R T P.Ring)
                      (AlgHom.toRingHom TensorProduct.includeRight) P.ker)
                    (ker P.baseChange) ⋯ :
                  ↥(Ideal.map (F := P.Ring →+* TensorProduct.{u_1, u_3, u} R T P.Ring)
                        (AlgHom.toRingHom TensorProduct.includeRight) P.ker) ≃ₗ[TensorProduct.{u_1, u_3, u} R T P.Ring]
                    ↥(ker P.baseChange : Ideal (Ring (R := T) (S := T ⊗[R] S) P.baseChange))) :
                (a : ↥(Ideal.map TensorProduct.includeRight.toRingHom P.ker)) → ↥P.baseChange.ker)
              (Subtype.mk (p := fun (x : TensorProduct.{u_1, u_3, u} R T P.Ring) ↦
                Membership.mem (γ := Ideal (TensorProduct.{u_1, u_3, u} R T P.Ring))
                  (Ideal.map (F := P.Ring →+* TensorProduct.{u_1, u_3, u} R T P.Ring)
                    (AlgHom.toRingHom TensorProduct.includeRight) P.ker)
                  x)
                (1 ⊗ₜ[R] (↑x : P.Ring)) ⋯))) :
        Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) =
    HSMul.hSMul (β := Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((Cotangent.mk : (a : ↥P.baseChange.ker) → P.baseChange.Cotangent)
          (Subtype.mk (p := fun (x : Ring (R := T) (S := T ⊗[R] S) P.baseChange) ↦
            Membership.mem (γ := Ideal (Ring (R := T) (S := T ⊗[R] S) P.baseChange)) (ker P.baseChange) x)
            ((Hom.toRingHom (toBaseChange T) : (a : P.Ring) → P.baseChange.Ring) (↑x : P.Ring)) ⋯) :
        Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
⊢ (P.tensorCotangentOfFlat T : (a : T ⊗[R] P.Cotangent) → P.baseChange.Cotangent)
      (t ⊗ₜ[R] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) x) =
    HSMul.hSMul (β := Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((Cotangent.map (toBaseChange T) : (a : P.Cotangent) → P.baseChange.Cotangent)
          ((Cotangent.mk : (a : ↥P.ker) → P.Cotangent) x) :
        Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)

Tactic:
simp only [tensorCotangentOfFlat, LinearEquiv.trans_apply, AlgebraTensorModule.congr_tmul,
    LinearEquiv.refl_apply, LinearEquiv.restrictScalars_apply, cotangentEquivCotangentKer_apply,
    Cotangent.val_mk, Ideal.tensorCotangentEquiv_tmul, map_smul, Cotangent.map_mk,
    Hom.toAlgHom_apply, Ideal.Cotangent.equivOfEq_toCotangent]

Premises used: Ideal.tensorCotangentEquiv_tmul, LinearEquiv.restrictScalars_apply, Algebra.Extension.Cotangent.val_mk, LinearEquiv.trans_apply, LinearEquiv.refl_apply, Algebra.Extension.tensorCotangentOfFlat, Ideal.Cotangent.equivOfEq_toCotangent, Algebra.Extension.Cotangent.map_mk, Algebra.Extension.cotangentEquivCotangentKer_apply, Algebra.Extension.Hom.toAlgHom_apply, map_smul, TensorProduct.AlgebraTensorModule.congr_tmul