-- Mathlib/Analysis/Normed/Group/Continuity.lean
theorem SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one {f : ι → κ → G}
    {l : Filter ι} {l' : Filter κ} :
    UniformCauchySeqOnFilter f l l' ↔
      TendstoUniformlyOnFilter (fun n : ι × ι => fun z => f n.fst z / f n.snd z) 1 (l ×ˢ l) l'

Proof state:
case refine_1.intro.intro
ι : Type u_3
κ : Type u_4
G : Type u_7
inst✝ : SeminormedGroup G
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.1 p.2 < ε} → (a, b) ∈ u
x : (ι × ι) × κ
hx : (f x.1.1 x.2, f x.1.2 x.2) ∈ {p | dist p.1 p.2 < ε}
⊢ (1, f x.1.1 x.2 / f x.1.2 x.2) ∈ {p | dist p.1 p.2 < ε}

Tactic:
simpa [dist_eq_norm_div, norm_div_rev] using hx

Result:
no goals

Proof state:
case refine_2.intro.intro
ι : Type u_3
κ : Type u_4
G : Type u_7
inst✝ : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : TendstoUniformlyOnFilter (fun n z => f n.1 z / f n.2 z) 1 (l ×ˢ l) l'
u : Set (G × G)
hu : u ∈ 𝓤 G
ε : ℝ
hε : 0 < ε
H : ∀ (a b : G), (a, b) ∈ {p | dist p.1 p.2 < ε} → (a, b) ∈ u
x : (ι × ι) × κ
hx : (1 x.2, (fun n z => f n.1 z / f n.2 z) x.1 x.2) ∈ {p | dist p.1 p.2 < ε}
⊢ (f x.1.1 x.2, f x.1.2 x.2) ∈ {p | dist p.1 p.2 < ε}

Tactic:
simpa [dist_eq_norm_div, norm_div_rev] using hx

Result:
no goals

Proof state:
ι : Type u_3
κ : Type u_4
G : Type u_7
inst✝ : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
⊢ UniformCauchySeqOnFilter f l l' ↔ TendstoUniformlyOnFilter (fun n z => f n.1 z / f n.2 z) 1 (l ×ˢ l) l'

Tactic:
refine ⟨fun hf u hu => ?_, fun hf u hu => ?_⟩

Result:
case refine_1
ι : Type u_3
κ : Type u_4
G : Type u_7
inst✝ : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : UniformCauchySeqOnFilter f l l'
u : Set (G × G)
hu : u ∈ 𝓤 G
⊢ ∀ᶠ (n : (ι × ι) × κ) in (l ×ˢ l) ×ˢ l', (1 n.2, (fun n z => f n.1 z / f n.2 z) n.1 n.2) ∈ u

case refine_2
ι : Type u_3
κ : Type u_4
G : Type u_7
inst✝ : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : TendstoUniformlyOnFilter (fun n z => f n.1 z / f n.2 z) 1 (l ×ˢ l) l'
u : Set (G × G)
hu : u ∈ 𝓤 G
⊢ ∀ᶠ (m : (ι × ι) × κ) in (l ×ˢ l) ×ˢ l', (f m.1.1 m.2, f m.1.2 m.2) ∈ u

Proof state:
case refine_1.intro.intro
ι : Type u_3
κ : Type u_4
G : Type u_7
inst✝ : SeminormedGroup G
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.1 p.2 < ε} → (a, b) ∈ u
⊢ ∀ᶠ (n : (ι × ι) × κ) in (l ×ˢ l) ×ˢ l', (1 n.2, (fun n z => f n.1 z / f n.2 z) n.1 n.2) ∈ u

Tactic:
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) ?_

Result:
case refine_1.intro.intro
ι : Type u_3
κ : Type u_4
G : Type u_7
inst✝ : SeminormedGroup G
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.1 p.2 < ε} → (a, b) ∈ u
x : (ι × ι) × κ
hx : (f x.1.1 x.2, f x.1.2 x.2) ∈ {p | dist p.1 p.2 < ε}
⊢ (1, f x.1.1 x.2 / f x.1.2 x.2) ∈ {p | dist p.1 p.2 < ε}

Proof state:
case refine_2
ι : Type u_3
κ : Type u_4
G : Type u_7
inst✝ : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : TendstoUniformlyOnFilter (fun n z => f n.1 z / f n.2 z) 1 (l ×ˢ l) l'
u : Set (G × G)
hu : u ∈ 𝓤 G
⊢ ∀ᶠ (m : (ι × ι) × κ) in (l ×ˢ l) ×ˢ l', (f m.1.1 m.2, f m.1.2 m.2) ∈ u

Tactic:
obtain ⟨ε, hε, H⟩ := uniformity_basis_dist.mem_uniformity_iff.mp hu

Result:
case refine_2.intro.intro
ι : Type u_3
κ : Type u_4
G : Type u_7
inst✝ : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : TendstoUniformlyOnFilter (fun n z => f n.1 z / f n.2 z) 1 (l ×ˢ l) l'
u : Set (G × G)
hu : u ∈ 𝓤 G
ε : ℝ
hε : 0 < ε
H : ∀ (a b : G), (a, b) ∈ {p | dist p.1 p.2 < ε} → (a, b) ∈ u
⊢ ∀ᶠ (m : (ι × ι) × κ) in (l ×ˢ l) ×ˢ l', (f m.1.1 m.2, f m.1.2 m.2) ∈ u

Proof state:
case refine_1
ι : Type u_3
κ : Type u_4
G : Type u_7
inst✝ : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : UniformCauchySeqOnFilter f l l'
u : Set (G × G)
hu : u ∈ 𝓤 G
⊢ ∀ᶠ (n : (ι × ι) × κ) in (l ×ˢ l) ×ˢ l', (1 n.2, (fun n z => f n.1 z / f n.2 z) n.1 n.2) ∈ u

Tactic:
obtain ⟨ε, hε, H⟩ := uniformity_basis_dist.mem_uniformity_iff.mp hu

Result:
case refine_1.intro.intro
ι : Type u_3
κ : Type u_4
G : Type u_7
inst✝ : SeminormedGroup G
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.1 p.2 < ε} → (a, b) ∈ u
⊢ ∀ᶠ (n : (ι × ι) × κ) in (l ×ˢ l) ×ˢ l', (1 n.2, (fun n z => f n.1 z / f n.2 z) n.1 n.2) ∈ u

Proof state:
case refine_2.intro.intro
ι : Type u_3
κ : Type u_4
G : Type u_7
inst✝ : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : TendstoUniformlyOnFilter (fun n z => f n.1 z / f n.2 z) 1 (l ×ˢ l) l'
u : Set (G × G)
hu : u ∈ 𝓤 G
ε : ℝ
hε : 0 < ε
H : ∀ (a b : G), (a, b) ∈ {p | dist p.1 p.2 < ε} → (a, b) ∈ u
⊢ ∀ᶠ (m : (ι × ι) × κ) in (l ×ˢ l) ×ˢ l', (f m.1.1 m.2, f m.1.2 m.2) ∈ u

Tactic:
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) ?_

Result:
case refine_2.intro.intro
ι : Type u_3
κ : Type u_4
G : Type u_7
inst✝ : SeminormedGroup G
f : ι → κ → G
l : Filter ι
l' : Filter κ
hf : TendstoUniformlyOnFilter (fun n z => f n.1 z / f n.2 z) 1 (l ×ˢ l) l'
u : Set (G × G)
hu : u ∈ 𝓤 G
ε : ℝ
hε : 0 < ε
H : ∀ (a b : G), (a, b) ∈ {p | dist p.1 p.2 < ε} → (a, b) ∈ u
x : (ι × ι) × κ
hx : (1 x.2, (fun n z => f n.1 z / f n.2 z) x.1 x.2) ∈ {p | dist p.1 p.2 < ε}
⊢ (f x.1.1 x.2, f x.1.2 x.2) ∈ {p | dist p.1 p.2 < ε}