-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
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'
f : P.Hom P'
x : ↥P.ker
rw :
  Eq (α := P'.CotangentSpace)
    ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace)
        (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (↑x : P.Ring)) :
      P'.CotangentSpace)
    ((P'.cotangentComplex : (a : P'.Cotangent) → P'.CotangentSpace)
        ((Cotangent.map f : (a : P.Cotangent) → P'.Cotangent) ((Cotangent.mk : (a : ↥P.ker) → P.Cotangent) x)) :
      P'.CotangentSpace)
rw₁ :
  Eq (α := P'.CotangentSpace)
    ((algebraMap S S' : (a : S) → S') 1 ⊗ₜ[P'.Ring]
        (D R' P'.Ring : (a : P'.Ring) → Ω[P'.Ring⁄R'])
          (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) :
      TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
    ((P'.cotangentComplex : (a : P'.Cotangent) → P'.CotangentSpace)
        ((Cotangent.map f : (a : P.Cotangent) → P'.Cotangent) ((Cotangent.mk : (a : ↥P.ker) → P.Cotangent) x)) :
      P'.CotangentSpace)
rw₂ :
  Eq (α := P'.CotangentSpace)
    (1 ⊗ₜ[P'.Ring]
        (D R' P'.Ring : (a : P'.Ring) → Ω[P'.Ring⁄R'])
          (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) :
      TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
    ((P'.cotangentComplex : (a : P'.Cotangent) → P'.CotangentSpace)
        ((Cotangent.map f : (a : P.Cotangent) → P'.Cotangent) ((Cotangent.mk : (a : ↥P.ker) → P.Cotangent) x)) :
      P'.CotangentSpace)
rw₃ :
  Eq (α := P'.CotangentSpace)
    (1 ⊗ₜ[P'.Ring]
        (D R' P'.Ring : (a : P'.Ring) → Ω[P'.Ring⁄R'])
          (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) :
      TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
    ((P'.cotangentComplex : (a : P'.Cotangent) → P'.CotangentSpace)
        ((Cotangent.mk : (a : ↥P'.ker) → P'.Cotangent)
          (Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
            (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) ⋯)) :
      P'.CotangentSpace)
⊢ Eq (α := P'.CotangentSpace)
    ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace)
        ((P.cotangentComplex : (a : P.Cotangent) → P.CotangentSpace) ((Cotangent.mk : (a : ↥P.ker) → P.Cotangent) x)) :
      P'.CotangentSpace)
    ((P'.cotangentComplex : (a : P'.Cotangent) → P'.CotangentSpace)
        ((Cotangent.map f : (a : P.Cotangent) → P'.Cotangent) ((Cotangent.mk : (a : ↥P.ker) → P.Cotangent) x)) :
      P'.CotangentSpace)
have rw₄ : Eq (α := P'.CotangentSpace)
  (1 ⊗ₜ[P'.Ring]
      (D R' P'.Ring : (a : P'.Ring) → Ω[P'.Ring⁄R'])
        (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) :
    TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
  (1 ⊗ₜ[P'.Ring]
      (D R' P'.Ring : (a : P'.Ring) → Ω[P'.Ring⁄R'])
        (↑(Subtype.mk (p := fun (x : P'.Ring) ↦ x ∈ P'.ker)
              (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (↑x : P.Ring)) sorry) :
          P'.Ring) :
    TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
Tactic: rw [cotangentComplex_mk, map_tmul, map_one, Cotangent.map_mk, cotangentComplex_mk]