-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
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 g : P.Hom P'
x y : P.Ring
this_1 : Algebra.{w, v'} P.Ring S' :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S))
this :
  HSub.hSub (α := P'.Ring) (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring)
          (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') x)) *
        HSub.hSub (α := P'.Ring) (β := P'.Ring)
          (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring)
          (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring) +
      HSub.hSub (α := P'.Ring)
          (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring)
          (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') y)) *
        HSub.hSub (α := P'.Ring) (β := P'.Ring)
          (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring)
          (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring) ∈
    HPow.hPow (β := ℕ) P'.ker 2
h :
  HSub.hSub (α := P'.Ring) (β := P'.Ring)
        (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (x * y) : P'.Ring)
        (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (x * y) : P'.Ring) -
      (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') x) *
          HSub.hSub (α := P'.Ring) (β := P'.Ring)
            (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring)
            (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring) +
        P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') y) *
          HSub.hSub (α := P'.Ring) (β := P'.Ring)
            (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring)
            (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring)) =
    HSub.hSub (α := P'.Ring) (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring)
          (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') x)) *
        HSub.hSub (α := P'.Ring) (β := P'.Ring)
          (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring)
          (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring) +
      HSub.hSub (α := P'.Ring)
          (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring)
          (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') y)) *
        HSub.hSub (α := P'.Ring) (β := P'.Ring)
          (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring)
          (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring)
⊢ HSub.hSub (α := P'.Ring) (β := P'.Ring)
        (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (x * y) : P'.Ring)
        (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) (x * y) : P'.Ring) -
      (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') x) *
          HSub.hSub (α := P'.Ring) (β := P'.Ring)
            (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring)
            (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y : P'.Ring) +
        P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') y) *
          HSub.hSub (α := P'.Ring) (β := P'.Ring)
            (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring)
            (((g.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) x : P'.Ring)) ∈
    HPow.hPow (β := ℕ) P'.ker 2

Tactic:
convert! this using 1