-- 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 : S
y : Ω[P.Ring⁄R]
rw :
  Eq (α := P'.CotangentSpace)
    ((LinearMap.liftBaseChange S
            ((↑P.Ring :
                  {S_1 M : Type w'} →
                    {M₂ : Type (max v' w')} →
                      [inst_10 : Semiring P.Ring] →
                        [inst_11 : Semiring S_1] →
                          [inst_12 : AddCommMonoid M] →
                            [inst_13 : AddCommMonoid M₂] →
                              [inst_14 : Module P.Ring M] →
                                [inst_15 : Module P.Ring M₂] →
                                  [inst_16 : Module S_1 M] →
                                    [inst_17 : Module S_1 M₂] →
                                      [LinearMap.CompatibleSMul M M₂ P.Ring S_1] →
                                        (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
                (S := P'.Ring)
                ((TensorProduct.mk P'.Ring S' Ω[P'.Ring⁄R'] :
                    (a : S') → Ω[P'.Ring⁄R'] →ₗ[P'.Ring] S' ⊗[P'.Ring] Ω[P'.Ring⁄R'])
                  1) ∘ₗ
              KaehlerDifferential.map R R' P.Ring P'.Ring) :
          (a : P.CotangentSpace) → P'.CotangentSpace)
        (x ⊗ₜ[P.Ring] y) :
      P'.CotangentSpace)
    ((algebraMap S S' : (a : S) → S') x ⊗ₜ[P'.Ring]
        (KaehlerDifferential.map R R' P.Ring P'.Ring : (a : Ω[P.Ring⁄R]) → Ω[P'.Ring⁄R']) y :
      TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
rw₁ :
  HSMul.hSMul (β := P'.CotangentSpace) x
      (((↑P.Ring :
                  {S_1 M : Type w'} →
                    {M₂ : Type (max v' w')} →
                      [inst_10 : Semiring P.Ring] →
                        [inst_11 : Semiring S_1] →
                          [inst_12 : AddCommMonoid M] →
                            [inst_13 : AddCommMonoid M₂] →
                              [inst_14 : Module P.Ring M] →
                                [inst_15 : Module P.Ring M₂] →
                                  [inst_16 : Module S_1 M] →
                                    [inst_17 : Module S_1 M₂] →
                                      [LinearMap.CompatibleSMul M M₂ P.Ring S_1] →
                                        (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
                (S := P'.Ring)
                ((TensorProduct.mk P'.Ring S' Ω[P'.Ring⁄R'] :
                    (a : S') → Ω[P'.Ring⁄R'] →ₗ[P'.Ring] S' ⊗[P'.Ring] Ω[P'.Ring⁄R'])
                  1) ∘ₗ
              KaehlerDifferential.map R R' P.Ring P'.Ring :
            (a : Ω[P.Ring⁄R]) → P'.CotangentSpace)
          y :
        P'.CotangentSpace) =
    (algebraMap S S' : (a : S) → S') x ⊗ₜ[P'.Ring]
      (KaehlerDifferential.map R R' P.Ring P'.Ring : (a : Ω[P.Ring⁄R]) → Ω[P'.Ring⁄R']) y
rw₂ :
  HSMul.hSMul (β := P'.CotangentSpace) x
      (Function.comp (β := Ω[P'.Ring⁄R'])
        (⇑((↑P.Ring :
                {S_1 M : Type w'} →
                  {M₂ : Type (max v' w')} →
                    [inst_10 : Semiring P.Ring] →
                      [inst_11 : Semiring S_1] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module P.Ring M] →
                              [inst_15 : Module P.Ring M₂] →
                                [inst_16 : Module S_1 M] →
                                  [inst_17 : Module S_1 M₂] →
                                    [LinearMap.CompatibleSMul M M₂ P.Ring S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
              (S := P'.Ring)
              ((TensorProduct.mk P'.Ring S' Ω[P'.Ring⁄R'] :
                  (a : S') → Ω[P'.Ring⁄R'] →ₗ[P'.Ring] S' ⊗[P'.Ring] Ω[P'.Ring⁄R'])
                1)) :
          (a : Ω[P'.Ring⁄R']) → P'.CotangentSpace)
        (⇑(KaehlerDifferential.map R R' P.Ring P'.Ring) : (a : Ω[P.Ring⁄R]) → Ω[P'.Ring⁄R']) y) =
    (algebraMap S S' : (a : S) → S') x ⊗ₜ[P'.Ring]
      (KaehlerDifferential.map R R' P.Ring P'.Ring : (a : Ω[P.Ring⁄R]) → Ω[P'.Ring⁄R']) y
rw₃ :
  HSMul.hSMul (β := P'.CotangentSpace) x
      (((↑P.Ring :
                {S_1 M : Type w'} →
                  {M₂ : Type (max v' w')} →
                    [inst_10 : Semiring P.Ring] →
                      [inst_11 : Semiring S_1] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module P.Ring M] →
                              [inst_15 : Module P.Ring M₂] →
                                [inst_16 : Module S_1 M] →
                                  [inst_17 : Module S_1 M₂] →
                                    [LinearMap.CompatibleSMul M M₂ P.Ring S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
              (S := P'.Ring)
              ((TensorProduct.mk P'.Ring S' Ω[P'.Ring⁄R'] :
                  (a : S') → Ω[P'.Ring⁄R'] →ₗ[P'.Ring] S' ⊗[P'.Ring] Ω[P'.Ring⁄R'])
                1) :
            (a : Ω[P'.Ring⁄R']) → P'.CotangentSpace)
          ((KaehlerDifferential.map R R' P.Ring P'.Ring : (a : Ω[P.Ring⁄R]) → Ω[P'.Ring⁄R']) y) :
        P'.CotangentSpace) =
    (algebraMap S S' : (a : S) → S') x ⊗ₜ[P'.Ring]
      (KaehlerDifferential.map R R' P.Ring P'.Ring : (a : Ω[P.Ring⁄R]) → Ω[P'.Ring⁄R']) y
rw₄ :
  HSMul.hSMul (β := P'.CotangentSpace) x
      (((TensorProduct.mk P'.Ring S' Ω[P'.Ring⁄R'] : (a : S') → Ω[P'.Ring⁄R'] →ₗ[P'.Ring] S' ⊗[P'.Ring] Ω[P'.Ring⁄R'])
              1 :
            (a : Ω[P'.Ring⁄R']) → S' ⊗[P'.Ring] Ω[P'.Ring⁄R'])
          ((KaehlerDifferential.map R R' P.Ring P'.Ring : (a : Ω[P.Ring⁄R]) → Ω[P'.Ring⁄R']) y) :
        TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R']) =
    (algebraMap S S' : (a : S) → S') x ⊗ₜ[P'.Ring]
      (KaehlerDifferential.map R R' P.Ring P'.Ring : (a : Ω[P.Ring⁄R]) → Ω[P'.Ring⁄R']) y
rw₅ :
  HSMul.hSMul (β := P'.CotangentSpace) x
      (1 ⊗ₜ[P'.Ring] (KaehlerDifferential.map R R' P.Ring P'.Ring : (a : Ω[P.Ring⁄R]) → Ω[P'.Ring⁄R']) y :
        TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R']) =
    (algebraMap S S' : (a : S) → S') x ⊗ₜ[P'.Ring]
      (KaehlerDifferential.map R R' P.Ring P'.Ring : (a : Ω[P.Ring⁄R]) → Ω[P'.Ring⁄R']) y
rw₆ :
  Eq (α := P'.CotangentSpace)
    (HSMul.hSMul (β := S') x 1 ⊗ₜ[P'.Ring]
        (KaehlerDifferential.map R R' P.Ring P'.Ring : (a : Ω[P.Ring⁄R]) → Ω[P'.Ring⁄R']) y :
      TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
    ((algebraMap S S' : (a : S) → S') x ⊗ₜ[P'.Ring]
        (KaehlerDifferential.map R R' P.Ring P'.Ring : (a : Ω[P.Ring⁄R]) → Ω[P'.Ring⁄R']) y :
      TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
⊢ Eq (α := P'.CotangentSpace)
    ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace) (x ⊗ₜ[P.Ring] y) : P'.CotangentSpace)
    ((algebraMap S S' : (a : S) → S') x ⊗ₜ[P'.Ring]
        (KaehlerDifferential.map R R' P.Ring P'.Ring : (a : Ω[P.Ring⁄R]) → Ω[P'.Ring⁄R']) y :
      TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
have rw₇ : Eq (α := P'.CotangentSpace)
  (HMul.hMul (α := S') (β := S') ((algebraMap S S' : (a : S) → S') x : S') (1 : S') ⊗ₜ[P'.Ring]
      (KaehlerDifferential.map R R' P.Ring P'.Ring : (a : Ω[P.Ring⁄R]) → Ω[P'.Ring⁄R']) y :
    TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
  ((algebraMap S S' : (a : S) → S') x ⊗ₜ[P'.Ring]
      (KaehlerDifferential.map R R' P.Ring P'.Ring : (a : Ω[P.Ring⁄R]) → Ω[P'.Ring⁄R']) y :
    TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
Tactic: rw [CotangentSpace.map, LinearMap.liftBaseChange_tmul, LinearMap.coe_comp, Function.comp_apply,
    LinearMap.restrictScalars_apply, mk_apply, smul_tmul', Algebra.smul_def, mul_one]