∀ (R : Type u_3) (S : Type u_1) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (S' : Type u_2)
  [inst_3 : CommRing S'] [inst_4 : Algebra R S'] (e : S ≃ₐ[R] S'),
  IsScalarTower S S' (Algebra.Generators.self R S').toExtension.Cotangent