[GOAL]
α : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSpace M
x : tsze R M
⊢ nhds x = Filter.prod (nhds (fst x)) (nhds (snd x))
[PROOFSTEP]
cases x
[GOAL]
case mk
α : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSpace M
fst✝ : R
snd✝ : M
⊢ nhds (fst✝, snd✝) = Filter.prod (nhds (fst (fst✝, snd✝))) (nhds (snd (fst✝, snd✝)))
[PROOFSTEP]
exact nhds_prod_eq
