no goals
α : Type u_1
β : Type ?u.4103
G₀ : Type u_2
inst✝³ : DivInvMonoid G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : ContinuousMul G₀
f : α → G₀
s : Set α
l : Filter α
inst✝ : TopologicalSpace α
hf : ContinuousOn f s
y : G₀
⊢ ContinuousOn (fun x => f x / y) s
simpa only [div_eq_mul_inv] using hf.mul continuousOn_const