𝕜 : Type u_5
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
E' : Type ?u.88570
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
F' : Type ?u.88776
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace 𝕜 F'
H : Type u_3
inst✝³ : TopologicalSpace H
H' : Type ?u.88885
inst✝² : TopologicalSpace H'
G : Type u_4
inst✝¹ : TopologicalSpace G
G' : Type ?u.88897
inst✝ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
⊢ (prod I J).toLocalEquiv.target = I.target ×ˢ J.target
𝕜 : Type u_5
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
E' : Type ?u.88570
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
F' : Type ?u.88776
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace 𝕜 F'
H : Type u_3
inst✝³ : TopologicalSpace H
H' : Type ?u.88885
inst✝² : TopologicalSpace H'
G : Type u_4
inst✝¹ : TopologicalSpace G
G' : Type ?u.88897
inst✝ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
⊢ range ↑(prod I J) = range ↑I ×ˢ range ↑J
simp_rw [← ModelWithCorners.target_eq]
no goals
𝕜 : Type u_5
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
E' : Type ?u.88570
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
F' : Type ?u.88776
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace 𝕜 F'
H : Type u_3
inst✝³ : TopologicalSpace H
H' : Type ?u.88885
inst✝² : TopologicalSpace H'
G : Type u_4
inst✝¹ : TopologicalSpace G
G' : Type ?u.88897
inst✝ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
⊢ (prod I J).toLocalEquiv.target = I.target ×ˢ J.target
rfl