-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
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
⊢ (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)
have 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) sorry :
                ↥(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)) sorry))) :
      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)) sorry) :
      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]