-- 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'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
f g : P.Hom P'
this_1 : Algebra.{w, v'} P.Ring S' :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S))
this_2 : IsScalarTower.{w, v, v'} P.Ring S S'
this_3 : Algebra.{w, w'} P.Ring P'.Ring := (AlgHom.toRingHom f.toAlgHom).toAlgebra
this_4 : IsScalarTower.{w, w', v'} P.Ring P'.Ring S'
this : IsScalarTower.{u, w, v'} R P.Ring S'
x y : P.Ring
⊢ Cotangent.val
      ((((↑R :
                  {S M M₂ : Type w'} →
                    [inst : Semiring R] →
                      [inst_24 : Semiring S] →
                        [inst_25 : AddCommMonoid M] →
                          [inst_26 : AddCommMonoid M₂] →
                            [inst_27 : Module R M] →
                              [inst_28 : Module R M₂] →
                                [inst_29 : Module S M] →
                                  [inst_30 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                Cotangent.mk ∘ₗ
              f.subToKer g :
            LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring P'.Cotangent) :
          (a : P.Ring) → P'.Cotangent)
        (x * y)) =
    (HSMul.hSMul (β := P'.Cotangent) x
          ((((↑R :
                        {S M M₂ : Type w'} →
                          [inst : Semiring R] →
                            [inst_24 : Semiring S] →
                              [inst_25 : AddCommMonoid M] →
                                [inst_26 : AddCommMonoid M₂] →
                                  [inst_27 : Module R M] →
                                    [inst_28 : Module R M₂] →
                                      [inst_29 : Module S M] →
                                        [inst_30 : Module S M₂] →
                                          [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                      Cotangent.mk ∘ₗ
                    f.subToKer g :
                  LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring P'.Cotangent) :
                (a : P.Ring) → P'.Cotangent)
              y :
            P'.Cotangent) +
        HSMul.hSMul (β := P'.Cotangent) y
          ((((↑R :
                        {S M M₂ : Type w'} →
                          [inst : Semiring R] →
                            [inst_24 : Semiring S] →
                              [inst_25 : AddCommMonoid M] →
                                [inst_26 : AddCommMonoid M₂] →
                                  [inst_27 : Module R M] →
                                    [inst_28 : Module R M₂] →
                                      [inst_29 : Module S M] →
                                        [inst_30 : Module S M₂] →
                                          [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                      Cotangent.mk ∘ₗ
                    f.subToKer g :
                  LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring P'.Cotangent) :
                (a : P.Ring) → P'.Cotangent)
              x :
            P'.Cotangent)).val
have refine_2 : (↑(((f.subToKer g : LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring ↥P'.ker) : (a : P.Ring) → ↥P'.ker) (x * y)) :
      P'.Ring) -
    (↑(HSMul.hSMul (β := ↥P'.ker) (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') x))
            (((f.subToKer g : LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring ↥P'.ker) : (a : P.Ring) → ↥P'.ker) y :
              ↥P'.ker) +
          HSMul.hSMul (β := ↥P'.ker) (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') y))
            (((f.subToKer g : LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring ↥P'.ker) : (a : P.Ring) → ↥P'.ker) x :
              ↥P'.ker)) :
      P'.Ring) ∈
  HPow.hPow (β := ℕ) P'.ker 2
Tactic: simp only [LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply,
      Cotangent.val_mk, Cotangent.val_add, Cotangent.val_smul''', ← map_smul, ← map_add,
      Ideal.toCotangent_eq]