no goals
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalRing R
inst✝ : TopologicalAddGroup M
hmul : Tendsto (fun p => p.fst • p.snd) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto (fun a => a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (fun m => a • m) (𝓝 0) (𝓝 0)
⊢ Continuous fun p => p.fst • p.snd
refine continuous_of_continuousAt_zero₂ (AddMonoidHom.smul : R →+ M →+ M) ?_ ?_ ?_ <;>
  simpa [ContinuousAt, nhds_prod_eq]