theorem contMDiff_prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F' : Type u_5} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {G' : Type u_9} [TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_11} [TopologicalSpace M'] [ChartedSpace H' M'] {N' : Type u_13} [TopologicalSpace N'] [ChartedSpace G' N'] {n : WithTop ℕ∞} {f : M → M' × N'} : ContMDiff I (I'.prod J') n f ↔ (ContMDiff I I' n fun (x : M) => (f x).1) ∧ ContMDiff I J' n fun (x : M) => (f x).2

theorem contMDiffAt_prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F' : Type u_5} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {G' : Type u_9} [TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_11} [TopologicalSpace M'] [ChartedSpace H' M'] {N' : Type u_13} [TopologicalSpace N'] [ChartedSpace G' N'] {n : WithTop ℕ∞} {f : M → M' × N'} {x : M} : ContMDiffAt I (I'.prod J') n f x ↔ ContMDiffAt I I' n (fun (x : M) => (f x).1) x ∧ ContMDiffAt I J' n (fun (x : M) => (f x).2) x

theorem smooth_prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F' : Type u_5} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {G' : Type u_9} [TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_11} [TopologicalSpace M'] [ChartedSpace H' M'] {N' : Type u_13} [TopologicalSpace N'] [ChartedSpace G' N'] {f : M → M' × N'} : ContMDiff I (I'.prod J') (↑⊤) f ↔ (ContMDiff I I' ↑⊤ fun (x : M) => (f x).1) ∧ ContMDiff I J' ↑⊤ fun (x : M) => (f x).2

theorem smoothAt_prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F' : Type u_5} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {H : Type u_6} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_7} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {G' : Type u_9} [TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {M : Type u_10} [TopologicalSpace M] [ChartedSpace H M] {M' : Type u_11} [TopologicalSpace M'] [ChartedSpace H' M'] {N' : Type u_13} [TopologicalSpace N'] [ChartedSpace G' N'] {f : M → M' × N'} {x : M} : ContMDiffAt I (I'.prod J') (↑⊤) f x ↔ ContMDiffAt I I' (↑⊤) (fun (x : M) => (f x).1) x ∧ ContMDiffAt I J' (↑⊤) (fun (x : M) => (f x).2) x