Theorem: TendstoUniformlyOn.div_of_compact (RMT4/hurwitz.lean)

State before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝¹ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
inst✝ : TopologicalSpace α
hF : TendstoUniformlyOn F f p K
hG : TendstoUniformlyOn G g p K
hf : ContinuousOn f K
hg : ContinuousOn g K
hgK : ∀ z ∈ K, g z ≠ 0
hK : IsCompact K
⊢ TendstoUniformlyOn (F / G) (f / g) p K
Tactic:
simpa [div_eq_mul_inv] using hF.mul_of_compact (hG.inv_of_compact hg hK hgK) hf (hg.inv₀ hgK) hK
State after:
no goals