have h1 : ∀ᶠ i in p, ∀ x ∈ s, ‖F i x‖ ≤ mf + 1 := by
  simp_rw [Metric.tendstoUniformlyOn_iff, dist_eq_norm] at hF
  filter_upwards [hF 1 zero_lt_one] with i hF x hx
  have : ‖F i x‖ ≤ ‖f x - F i x‖ + ‖f x‖ := by
    simpa [← norm_neg (F i x - f x)] using norm_add_le (F i x - f x) (f x)
  linarith [hF x hx, hf x hx]
𝕜 : 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 : ∀ x ∈ s, ‖f x‖ ≤ mf
hg : ∀ x ∈ s, ‖g x‖ ≤ mg
⊢ TendstoUniformlyOn (F * G) (f * g) p s
𝕜 : 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 : ∀ x ∈ s, ‖f x‖ ≤ mf
hg : ∀ x ∈ s, ‖g x‖ ≤ mg
h1 : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf + 1
⊢ TendstoUniformlyOn (F * G) (f * g) p s