no goals
𝕜 : Type u_3
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
E' : Type ?u.86260
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
F' : Type ?u.86466
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace 𝕜 F'
H : Type ?u.86569
inst✝³ : TopologicalSpace H
H' : Type ?u.86575
inst✝² : TopologicalSpace H'
G : Type ?u.86581
inst✝¹ : TopologicalSpace G
G' : Type ?u.86587
inst✝ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
⊢ 𝓘(𝕜, E × F) = ModelWithCorners.prod 𝓘(𝕜, E) 𝓘(𝕜, F)
ext1 <;> simp