α✝ : Type u
β : Type v
X : Type ?u.91426
ι✝ : Type ?u.91429
inst✝¹ : PseudoMetricSpace α✝
x y z : α✝
δ ε ε₁ ε₂ : ℝ
s : Set α✝
ι : Type u_1
α : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : α × ι → Prop
⊢ (∃ i, (0 < i.fst ∧ i.snd ∈ f) ∧ ∀ ⦃x : α × ι⦄, x ∈ ball x₀ i.fst ×ˢ id i.snd → p x) ↔
    ∃ ε, ε > 0 ∧ ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ {x : α}, dist x x₀ < ε → ∀ {i : ι}, pa i → p (x, i)
α✝ : Type u
β : Type v
X : Type ?u.91426
ι✝ : Type ?u.91429
inst✝¹ : PseudoMetricSpace α✝
x y z : α✝
δ ε ε₁ ε₂ : ℝ
s : Set α✝
ι : Type u_1
α : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : α × ι → Prop
⊢ (∀ᶠ (x : α × ι) in 𝓝 x₀ ×ˢ f, p x) ↔
    ∃ ε, ε > 0 ∧ ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ {x : α}, dist x x₀ < ε → ∀ {i : ι}, pa i → p (x, i)
refine (nhds_basis_ball.prod f.basis_sets).eventually_iff.trans ?_
α✝ : Type u
β : Type v
X : Type ?u.91426
ι✝ : Type ?u.91429
inst✝¹ : PseudoMetricSpace α✝
x y z : α✝
δ ε ε₁ ε₂ : ℝ
s : Set α✝
ι : Type u_1
α : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : α × ι → Prop
⊢ (∃ a, 0 < a ∧ ∃ x, x ∈ f ∧ ∀ (x_1 : α), dist x_1 x₀ < a → ∀ (y : ι), y ∈ x → p (x_1, y)) ↔
    ∃ ε, ε > 0 ∧ ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ {x : α}, dist x x₀ < ε → ∀ {i : ι}, pa i → p (x, i)
α✝ : Type u
β : Type v
X : Type ?u.91426
ι✝ : Type ?u.91429
inst✝¹ : PseudoMetricSpace α✝
x y z : α✝
δ ε ε₁ ε₂ : ℝ
s : Set α✝
ι : Type u_1
α : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : α × ι → Prop
⊢ (∃ i, (0 < i.fst ∧ i.snd ∈ f) ∧ ∀ ⦃x : α × ι⦄, x ∈ ball x₀ i.fst ×ˢ id i.snd → p x) ↔
    ∃ ε, ε > 0 ∧ ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ {x : α}, dist x x₀ < ε → ∀ {i : ι}, pa i → p (x, i)
simp only [Prod.exists, forall_prod_set, id, mem_ball, and_assoc, exists_and_left, and_imp]
no goals
α✝ : Type u
β : Type v
X : Type ?u.91426
ι✝ : Type ?u.91429
inst✝¹ : PseudoMetricSpace α✝
x y z : α✝
δ ε ε₁ ε₂ : ℝ
s : Set α✝
ι : Type u_1
α : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : α × ι → Prop
⊢ (∃ a, 0 < a ∧ ∃ x, x ∈ f ∧ ∀ (x_1 : α), dist x_1 x₀ < a → ∀ (y : ι), y ∈ x → p (x_1, y)) ↔
    ∃ ε, ε > 0 ∧ ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ {x : α}, dist x x₀ < ε → ∀ {i : ι}, pa i → p (x, i)
rfl