by_cases h : g x = 0
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
h : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
hf✝ : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg
h1 : ∀ x ∈ s, ‖g x‖ ≤ Mg
hF✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖f x - F n x‖ < ε
hG✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖g x - G n x‖ < ε
ε : ℝ
hε : ε > 0
i : ι
hf : ∀ x ∈ s, ‖F i x‖ ≤ Mf
hF : ∀ x ∈ s, ‖f x - F i x‖ < ε / (2 * Mg)
hG : ∀ x ∈ s, ‖g x - G i x‖ < ε / (2 * Mf)
x : α
hx : x ∈ s
⊢ ‖f x - F i x‖ * ‖g x‖ < ε / 2
case pos
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
h✝ : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
hf✝ : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg
h1 : ∀ x ∈ s, ‖g x‖ ≤ Mg
hF✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖f x - F n x‖ < ε
hG✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖g x - G n x‖ < ε
ε : ℝ
hε : ε > 0
i : ι
hf : ∀ x ∈ s, ‖F i x‖ ≤ Mf
hF : ∀ x ∈ s, ‖f x - F i x‖ < ε / (2 * Mg)
hG : ∀ x ∈ s, ‖g x - G i x‖ < ε / (2 * Mf)
x : α
hx : x ∈ s
h : g x = 0
⊢ ‖f x - F i x‖ * ‖g x‖ < ε / 2

case neg
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
h✝ : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
hf✝ : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg
h1 : ∀ x ∈ s, ‖g x‖ ≤ Mg
hF✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖f x - F n x‖ < ε
hG✝ : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖g x - G n x‖ < ε
ε : ℝ
hε : ε > 0
i : ι
hf : ∀ x ∈ s, ‖F i x‖ ≤ Mf
hF : ∀ x ∈ s, ‖f x - F i x‖ < ε / (2 * Mg)
hG : ∀ x ∈ s, ‖g x - G i x‖ < ε / (2 * Mf)
x : α
hx : x ∈ s
h : ¬g x = 0
⊢ ‖f x - F i x‖ * ‖g x‖ < ε / 2