∀ (R : Type u_1) {S : Type u_2} (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] (M : Submonoid S)
  [inst_7 : IsLocalization M T],
  ↑(Algebra.tensorH1CotangentOfIsLocalization R T M) = LinearMap.liftBaseChange T (Algebra.H1Cotangent.map R R S T)