∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {R' : Type u'}
  {S' : Type v'} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S'] {P' : Algebra.Extension 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'' : Algebra.Extension 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'']
  {P : Algebra.Extension R S} (f : P.Hom P') (g : P'.Hom P'') (x : P.H1Cotangent),
  (Algebra.Extension.H1Cotangent.map (g.comp f)) x =
    (Algebra.Extension.H1Cotangent.map g) ((Algebra.Extension.H1Cotangent.map f) x)