-- 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
ι : Type w
P : Generators R S ι
R' : Type u'
S' : Type v'
ι' : Type w'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Generators 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 : P.Hom P'
i : ι
j : ι'
⊢ Eq.{v' + 1} (α := S')
    ((((P'.cotangentSpaceBasis.repr :
                (a :
                    { Ring := P'.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                        algebra₂ := P'.instRing, isScalarTower := ⋯, σ := P'.σ, algebraMap_σ := ⋯ }.CotangentSpace) →
                  ι' →₀ S')
              ((CotangentSpace.map f.toExtensionHom :
                  (a :
                      { Ring := P.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                          algebra₂ := P.instRing, isScalarTower := ⋯, σ := P.σ, algebraMap_σ := ⋯ }.CotangentSpace) →
                    { Ring := P'.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                        algebra₂ := P'.instRing, isScalarTower := ⋯, σ := P'.σ, algebraMap_σ := ⋯ }.CotangentSpace)
                (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) (X i))) :
            ι' →₀ S') :
          (a : ι') → S')
        j :
      S')
    ((aeval P'.val : (a : MvPolynomial ι' R') → S')
        ((pderiv j : (a : MvPolynomial ι' R') → MvPolynomial ι' R') (f.val i) : MvPolynomial ι' R') :
      S')
have rw : Eq.{v' + 1} (α := S')
  ((((P'.cotangentSpaceBasis.repr :
              (a :
                  { Ring := P'.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                      algebra₂ := P'.instRing, isScalarTower := sorry, σ := P'.σ, algebraMap_σ := sorry }.CotangentSpace) →
                ι' →₀ S')
            (1 ⊗ₜ[Extension.Ring (R := R')
                { Ring := P'.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                  algebra₂ := P'.instRing, isScalarTower := sorry, σ := P'.σ, algebraMap_σ := sorry }]
              (D R'
                    (Extension.Ring (R := R')
                      { Ring := P'.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                        algebra₂ := P'.instRing, isScalarTower := sorry, σ := P'.σ, algebraMap_σ := sorry }) :
                  (a :
                      { Ring := P'.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                          algebra₂ := P'.instRing, isScalarTower := sorry, σ := P'.σ, algebraMap_σ := sorry }.Ring) →
                    Ω[{ Ring := P'.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                          algebra₂ := P'.instRing, isScalarTower := sorry, σ := P'.σ, algebraMap_σ := sorry }.Ring⁄R'])
                ((Extension.Hom.toAlgHom f.toExtensionHom :
                    (a :
                        { Ring := P.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                            algebra₂ := P.instRing, isScalarTower := sorry, σ := P.σ, algebraMap_σ := sorry }.Ring) →
                      { Ring := P'.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                          algebra₂ := P'.instRing, isScalarTower := sorry, σ := P'.σ, algebraMap_σ := sorry }.Ring)
                  (X i))) :
          ι' →₀ S') :
        (a : ι') → S')
      j :
    S')
  ((aeval P'.val : (a : MvPolynomial ι' R') → S')
      ((pderiv j : (a : MvPolynomial ι' R') → MvPolynomial ι' R') (f.val i) : MvPolynomial ι' R') :
    S')
Tactic: rw [CotangentSpace.map_tmul, map_one]