case pos =>
  set Mf := |mf| + 1
  set Mg := |mg| + 1
  have hMf : 0 < Mf := by positivity
  have hMg : 0 < Mg := by positivity
  replace hf : ∀ᶠ i in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf := by
    filter_upwards [hf] with i hF x hx using (hF x hx).trans ((le_abs_self mf).trans (lt_add_one _).le)
  replace hg : ∀ᶠ i in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg := by
    filter_upwards [hg] with i hG x hx using (hG x hx).trans ((le_abs_self mg).trans (lt_add_one _).le)
  have h1 : ∀ x ∈ s, ‖g x‖ ≤ Mg := by
    intro x hx
    refine le_of_tendsto ((continuous_norm.tendsto (g x)).comp (hG.tendsto_at hx)) ?_
    filter_upwards [hg] with i hg using hg x hx
  simp_rw [Metric.tendstoUniformlyOn_iff, dist_eq_norm] at hF hG ⊢
  intro ε hε
  filter_upwards [hf, hF (ε / (2 * Mg)) (by positivity), hG (ε / (2 * Mf)) (by positivity)] with i hf hF hG x hx
  have h2 : ‖(f x - F i x) * g x‖ < ε / 2 := by
    rw [norm_mul]
    by_cases h : g x = 0
    case pos => simp [h, half_pos hε]
    case neg =>
      convert mul_lt_mul (hF x hx) (h1 x hx) (norm_pos_iff.mpr h) (by positivity) using 1
      simp only [div_mul, mul_div_cancel, hMg.ne.symm, Ne.def, not_false_iff]
  have h3 : ‖F i x * (g x - G i x)‖ < ε / 2 := by
    rw [norm_mul]
    by_cases h : F i x = 0
    case pos => simp [h, half_pos hε]
    case neg =>
      convert mul_lt_mul' (hf x hx) (hG x hx) (norm_nonneg _) hMf using 1
      field_simp [hMf.ne.symm]; ring
  simp_rw [Pi.mul_apply, lxyab]
  exact (norm_add_le _ _).trans_lt (add_halves' ε ▸ add_lt_add h2 h3)
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg
h : NeBot p
⊢ TendstoUniformlyOn (F * G) (f * g) p s
no goals