∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {H : Type u_2} {inst_1 : TopologicalSpace H} {E : Type u_3}
  {inst_2 : NormedAddCommGroup E} {inst_3 : NormedSpace 𝕜 E} {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {R : Type u_4} {inst_4 : Semiring R} {inst_5 : TopologicalSpace R} {inst_6 : ChartedSpace H R}
  [self : ContMDiffRing I n R], ContMDiff (I.prod I) I n fun p => p.1 * p.2