case mk
α : Type ?u.7776
S : Type ?u.7779
R : Type u_1
M : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSpace M
fst✝ : R
snd✝ : M
⊢ nhds (fst✝, snd✝) = Filter.prod (nhds (fst (fst✝, snd✝))) (nhds (snd (fst✝, snd✝)))
α : Type ?u.7776
S : Type ?u.7779
R : Type u_1
M : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSpace M
x : tsze R M
⊢ nhds x = Filter.prod (nhds (fst x)) (nhds (snd x))
cases x
no goals
case mk
α : Type ?u.7776
S : Type ?u.7779
R : Type u_1
M : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalSpace M
fst✝ : R
snd✝ : M
⊢ nhds (fst✝, snd✝) = Filter.prod (nhds (fst (fst✝, snd✝))) (nhds (snd (fst✝, snd✝)))
exact nhds_prod_eq