-- 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
x : T
x_1 : P.Cotangent
⊢ Eq (α := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
    (((((AlgebraTensorModule.curry
                    (sorry ∘ₗ
                      (↑(LinearEquiv.restrictScalars R (P.tensorCotangentOfFlat T)) :
                        T ⊗[R] P.Cotangent →ₗ[R] P.baseChange.Cotangent)) :
                  T →ₗ[R] P.Cotangent →ₗ[R] CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) :
                (a : T) → P.Cotangent →ₗ[R] P.baseChange.CotangentSpace)
              x :
            P.Cotangent →ₗ[R] CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) :
          (a : P.Cotangent) → P.baseChange.CotangentSpace)
        x_1 :
      CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
    (((((AlgebraTensorModule.curry
                    ((↑(LinearEquiv.restrictScalars R (P.tensorCotangentSpace T)) :
                        T ⊗[R] P.CotangentSpace →ₗ[R] P.baseChange.CotangentSpace) ∘ₗ
                      LinearMap.lTensor T
                        ((↑R :
                            {S : Type u_2} →
                              {M : Type u} →
                                {M₂ : Type (max u u_2)} →
                                  [inst : Semiring R] →
                                    [inst_6 : Semiring S] →
                                      [inst_7 : AddCommMonoid M] →
                                        [inst_8 : AddCommMonoid M₂] →
                                          [inst_9 : Module R M] →
                                            [inst_10 : Module R M₂] →
                                              [inst_11 : Module S M] →
                                                [inst_12 : Module S M₂] →
                                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                          P.cotangentComplex)) :
                  T →ₗ[R] P.Cotangent →ₗ[R] CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) :
                (a : T) → P.Cotangent →ₗ[R] P.baseChange.CotangentSpace)
              x :
            P.Cotangent →ₗ[R] CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) :
          (a : P.Cotangent) → P.baseChange.CotangentSpace)
        x_1 :
      CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
have hc₄ : (sorry () : (a : P.baseChange.Cotangent) → P.baseChange.CotangentSpace)
    (HSMul.hSMul (β := Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) x
      ((Cotangent.map (toBaseChange T) : (a : P.Cotangent) → P.baseChange.Cotangent) x_1 :
        Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)) =
  HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) x
    ((cotangentComplex P.baseChange : (a : P.baseChange.Cotangent) → P.baseChange.CotangentSpace)
        ((Cotangent.map (toBaseChange T) : (a : P.Cotangent) → P.baseChange.Cotangent) x_1) :
      CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
Tactic: simp [CotangentSpace.map_cotangentComplex]