case refine'_1
𝓕 : Type ?u.504291
𝕜 : Type ?u.504294
α : Type ?u.504297
ι : Type u_1
κ : Type u_2
E : Type ?u.504306
F : Type ?u.504309
G : Type u_3
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : UniformCauchySeqOnFilter f l l'
u : Set (G × G)
hu : u ∈ 𝓤 G
⊢ ∀ᶠ (n : (ι × ι) × κ) in (l ×ˢ l) ×ˢ l', (OfNat.ofNat 1 n.snd, (fun n z => f n.fst z / f n.snd z) n.fst n.snd) ∈ u

case refine'_2
𝓕 : Type ?u.504291
𝕜 : Type ?u.504294
α : Type ?u.504297
ι : Type u_1
κ : Type u_2
E : Type ?u.504306
F : Type ?u.504309
G : Type u_3
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : TendstoUniformlyOnFilter (fun n z => f n.fst z / f n.snd z) 1 (l ×ˢ l) l'
u : Set (G × G)
hu : u ∈ 𝓤 G
⊢ ∀ᶠ (m : (ι × ι) × κ) in (l ×ˢ l) ×ˢ l', (f m.fst.fst m.snd, f m.fst.snd m.snd) ∈ u
𝓕 : Type ?u.504291
𝕜 : Type ?u.504294
α : Type ?u.504297
ι : Type u_1
κ : Type u_2
E : Type ?u.504306
F : Type ?u.504309
G : Type u_3
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : ι → κ → G
l : Filter ι
l' : Filter κ
⊢ UniformCauchySeqOnFilter f l l' ↔ TendstoUniformlyOnFilter (fun n z => f n.fst z / f n.snd z) 1 (l ×ˢ l) l'
refine' ⟨fun hf u hu => _, fun hf u hu => _⟩
case refine'_1.intro.intro
𝓕 : Type ?u.504291
𝕜 : Type ?u.504294
α : Type ?u.504297
ι : Type u_1
κ : Type u_2
E : Type ?u.504306
F : Type ?u.504309
G : Type u_3
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : UniformCauchySeqOnFilter f l l'
u : Set (G × G)
hu : u ∈ 𝓤 G
ε : ℝ
hε : 0 < ε
H : ∀ (a b : G), (a, b) ∈ {p | dist p.fst p.snd < ε} → (a, b) ∈ u
⊢ ∀ᶠ (n : (ι × ι) × κ) in (l ×ˢ l) ×ˢ l', (OfNat.ofNat 1 n.snd, (fun n z => f n.fst z / f n.snd z) n.fst n.snd) ∈ u
case refine'_1
𝓕 : Type ?u.504291
𝕜 : Type ?u.504294
α : Type ?u.504297
ι : Type u_1
κ : Type u_2
E : Type ?u.504306
F : Type ?u.504309
G : Type u_3
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : UniformCauchySeqOnFilter f l l'
u : Set (G × G)
hu : u ∈ 𝓤 G
⊢ ∀ᶠ (n : (ι × ι) × κ) in (l ×ˢ l) ×ˢ l', (OfNat.ofNat 1 n.snd, (fun n z => f n.fst z / f n.snd z) n.fst n.snd) ∈ u
obtain ⟨ε, hε, H⟩ := uniformity_basis_dist.mem_uniformity_iff.mp hu
case refine'_1.intro.intro
𝓕 : Type ?u.504291
𝕜 : Type ?u.504294
α : Type ?u.504297
ι : Type u_1
κ : Type u_2
E : Type ?u.504306
F : Type ?u.504309
G : Type u_3
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : UniformCauchySeqOnFilter f l l'
u : Set (G × G)
hu : u ∈ 𝓤 G
ε : ℝ
hε : 0 < ε
H : ∀ (a b : G), (a, b) ∈ {p | dist p.fst p.snd < ε} → (a, b) ∈ u
x : (ι × ι) × κ
hx : (f x.fst.fst x.snd, f x.fst.snd x.snd) ∈ {p | dist p.fst p.snd < ε}
⊢ (1, f x.fst.fst x.snd / f x.fst.snd x.snd) ∈ {p | dist p.fst p.snd < ε}
case refine'_1.intro.intro
𝓕 : Type ?u.504291
𝕜 : Type ?u.504294
α : Type ?u.504297
ι : Type u_1
κ : Type u_2
E : Type ?u.504306
F : Type ?u.504309
G : Type u_3
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : UniformCauchySeqOnFilter f l l'
u : Set (G × G)
hu : u ∈ 𝓤 G
ε : ℝ
hε : 0 < ε
H : ∀ (a b : G), (a, b) ∈ {p | dist p.fst p.snd < ε} → (a, b) ∈ u
⊢ ∀ᶠ (n : (ι × ι) × κ) in (l ×ˢ l) ×ˢ l', (OfNat.ofNat 1 n.snd, (fun n z => f n.fst z / f n.snd z) n.fst n.snd) ∈ u
refine'
  (hf { p : G × G | dist p.fst p.snd < ε } <| dist_mem_uniformity hε).mono fun x hx =>
    H 1 (f x.fst.fst x.snd / f x.fst.snd x.snd) _
no goals
case refine'_1.intro.intro
𝓕 : Type ?u.504291
𝕜 : Type ?u.504294
α : Type ?u.504297
ι : Type u_1
κ : Type u_2
E : Type ?u.504306
F : Type ?u.504309
G : Type u_3
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : UniformCauchySeqOnFilter f l l'
u : Set (G × G)
hu : u ∈ 𝓤 G
ε : ℝ
hε : 0 < ε
H : ∀ (a b : G), (a, b) ∈ {p | dist p.fst p.snd < ε} → (a, b) ∈ u
x : (ι × ι) × κ
hx : (f x.fst.fst x.snd, f x.fst.snd x.snd) ∈ {p | dist p.fst p.snd < ε}
⊢ (1, f x.fst.fst x.snd / f x.fst.snd x.snd) ∈ {p | dist p.fst p.snd < ε}
simpa [dist_eq_norm_div, norm_div_rev] using hx
case refine'_2.intro.intro
𝓕 : Type ?u.504291
𝕜 : Type ?u.504294
α : Type ?u.504297
ι : Type u_1
κ : Type u_2
E : Type ?u.504306
F : Type ?u.504309
G : Type u_3
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : TendstoUniformlyOnFilter (fun n z => f n.fst z / f n.snd z) 1 (l ×ˢ l) l'
u : Set (G × G)
hu : u ∈ 𝓤 G
ε : ℝ
hε : 0 < ε
H : ∀ (a b : G), (a, b) ∈ {p | dist p.fst p.snd < ε} → (a, b) ∈ u
⊢ ∀ᶠ (m : (ι × ι) × κ) in (l ×ˢ l) ×ˢ l', (f m.fst.fst m.snd, f m.fst.snd m.snd) ∈ u
case refine'_2
𝓕 : Type ?u.504291
𝕜 : Type ?u.504294
α : Type ?u.504297
ι : Type u_1
κ : Type u_2
E : Type ?u.504306
F : Type ?u.504309
G : Type u_3
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : TendstoUniformlyOnFilter (fun n z => f n.fst z / f n.snd z) 1 (l ×ˢ l) l'
u : Set (G × G)
hu : u ∈ 𝓤 G
⊢ ∀ᶠ (m : (ι × ι) × κ) in (l ×ˢ l) ×ˢ l', (f m.fst.fst m.snd, f m.fst.snd m.snd) ∈ u
obtain ⟨ε, hε, H⟩ := uniformity_basis_dist.mem_uniformity_iff.mp hu
case refine'_2.intro.intro
𝓕 : Type ?u.504291
𝕜 : Type ?u.504294
α : Type ?u.504297
ι : Type u_1
κ : Type u_2
E : Type ?u.504306
F : Type ?u.504309
G : Type u_3
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : TendstoUniformlyOnFilter (fun n z => f n.fst z / f n.snd z) 1 (l ×ˢ l) l'
u : Set (G × G)
hu : u ∈ 𝓤 G
ε : ℝ
hε : 0 < ε
H : ∀ (a b : G), (a, b) ∈ {p | dist p.fst p.snd < ε} → (a, b) ∈ u
x : (ι × ι) × κ
hx : (OfNat.ofNat 1 x.snd, (fun n z => f n.fst z / f n.snd z) x.fst x.snd) ∈ {p | dist p.fst p.snd < ε}
⊢ (f x.fst.fst x.snd, f x.fst.snd x.snd) ∈ {p | dist p.fst p.snd < ε}
case refine'_2.intro.intro
𝓕 : Type ?u.504291
𝕜 : Type ?u.504294
α : Type ?u.504297
ι : Type u_1
κ : Type u_2
E : Type ?u.504306
F : Type ?u.504309
G : Type u_3
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : TendstoUniformlyOnFilter (fun n z => f n.fst z / f n.snd z) 1 (l ×ˢ l) l'
u : Set (G × G)
hu : u ∈ 𝓤 G
ε : ℝ
hε : 0 < ε
H : ∀ (a b : G), (a, b) ∈ {p | dist p.fst p.snd < ε} → (a, b) ∈ u
⊢ ∀ᶠ (m : (ι × ι) × κ) in (l ×ˢ l) ×ˢ l', (f m.fst.fst m.snd, f m.fst.snd m.snd) ∈ u
refine'
  (hf { p : G × G | dist p.fst p.snd < ε } <| dist_mem_uniformity hε).mono fun x hx =>
    H (f x.fst.fst x.snd) (f x.fst.snd x.snd) _
no goals
case refine'_2.intro.intro
𝓕 : Type ?u.504291
𝕜 : Type ?u.504294
α : Type ?u.504297
ι : Type u_1
κ : Type u_2
E : Type ?u.504306
F : Type ?u.504309
G : Type u_3
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : TendstoUniformlyOnFilter (fun n z => f n.fst z / f n.snd z) 1 (l ×ˢ l) l'
u : Set (G × G)
hu : u ∈ 𝓤 G
ε : ℝ
hε : 0 < ε
H : ∀ (a b : G), (a, b) ∈ {p | dist p.fst p.snd < ε} → (a, b) ∈ u
x : (ι × ι) × κ
hx : (OfNat.ofNat 1 x.snd, (fun n z => f n.fst z / f n.snd z) x.fst x.snd) ∈ {p | dist p.fst p.snd < ε}
⊢ (f x.fst.fst x.snd, f x.fst.snd x.snd) ∈ {p | dist p.fst p.snd < ε}
simpa [dist_eq_norm_div, norm_div_rev] using hx