no goals
α : Type u_1
β : Type ?u.33213
G₀ : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : HasContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
f g : α → G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
a : α
hf : Continuous f
hg : Continuous g
h₀ : ∀ (x : α), g x ≠ 0
⊢ Continuous (f / g)
simpa only [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)