-- 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 : ι'
erw :
  Eq.{v' + 1} (α := S')
    ((aeval P'.val : (a : MvPolynomial ι' R') → S')
        ((pderiv j : (a : MvPolynomial ι' R') → MvPolynomial ι' R')
            ((Extension.Hom.toAlgHom f.toExtensionHom :
                (a :
                    { Ring := P.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                        algebra₂ := P.instRing, isScalarTower := ⋯, σ := P.σ, algebraMap_σ := ⋯ }.Ring) →
                  { Ring := P'.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                      algebra₂ := P'.instRing, isScalarTower := ⋯, σ := P'.σ, algebraMap_σ := ⋯ }.Ring)
              (X i)) :
          MvPolynomial ι' R') :
      S')
    ((aeval P'.val : (a : MvPolynomial ι' R') → S')
        ((pderiv j : (a : MvPolynomial ι' R') → MvPolynomial ι' R') (f.val i) : MvPolynomial ι' R') :
      S')
⊢ 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')
              (1 ⊗ₜ[Extension.Ring (R := R')
                  { Ring := P'.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                    algebra₂ := P'.instRing, isScalarTower := ⋯, σ := P'.σ, algebraMap_σ := ⋯ }]
                (D R'
                      (Extension.Ring (R := R')
                        { Ring := P'.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                          algebra₂ := P'.instRing, isScalarTower := ⋯, σ := P'.σ, algebraMap_σ := ⋯ }) :
                    (a :
                        { Ring := P'.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                            algebra₂ := P'.instRing, isScalarTower := ⋯, σ := P'.σ, algebraMap_σ := ⋯ }.Ring) →
                      Ω[{ Ring := P'.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                            algebra₂ := P'.instRing, isScalarTower := ⋯, σ := P'.σ, algebraMap_σ := ⋯ }.Ring⁄R'])
                  ((Extension.Hom.toAlgHom f.toExtensionHom :
                      (a :
                          { Ring := P.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                              algebra₂ := P.instRing, isScalarTower := ⋯, σ := P.σ, algebraMap_σ := ⋯ }.Ring) →
                        { Ring := P'.Ring, commRing := AddMonoidAlgebra.commRing, algebra₁ := AddMonoidAlgebra.algebra,
                            algebra₂ := P'.instRing, isScalarTower := ⋯, σ := P'.σ, algebraMap_σ := ⋯ }.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')
have erw₁ : Eq.{v' + 1} (α := S')
  ((aeval P'.val : (a : MvPolynomial ι' R') → S')
      ((pderiv j : (a : MvPolynomial ι' R') → MvPolynomial ι' R') (f.val i) : MvPolynomial ι' R') :
    S')
  ((aeval P'.val : (a : MvPolynomial ι' R') → S')
      ((pderiv j : (a : MvPolynomial ι' R') → MvPolynomial ι' R') (f.val i) : MvPolynomial ι' R') :
    S')
Tactic: erw [cotangentSpaceBasis_repr_one_tmul, Hom.toAlgHom_X]