α : Type u
β : Type v
X : Type ?u.93290
ι : Type u_1
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
f : Filter ι
x₀ : α
p : ι × α → Prop
⊢ (∃ ε, ε > 0 ∧ ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ {x : α}, dist x x₀ < ε → ∀ {i : ι}, pa i → p (Prod.swap (x, i))) ↔
    ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε, ε > 0 ∧ ∀ {i : ι}, pa i → ∀ {x : α}, dist x x₀ < ε → p (i, x)
α : Type u
β : Type v
X : Type ?u.93290
ι : Type u_1
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
f : Filter ι
x₀ : α
p : ι × α → Prop
⊢ (∀ᶠ (x : ι × α) in f ×ˢ 𝓝 x₀, p x) ↔
    ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε, ε > 0 ∧ ∀ {i : ι}, pa i → ∀ {x : α}, dist x x₀ < ε → p (i, x)
rw [eventually_swap_iff, Metric.eventually_nhds_prod_iff]
case mpr.intro.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.93290
ι : Type u_1
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
f : Filter ι
x₀ : α
p : ι × α → Prop
a1 : ι → Prop
a2 : ∀ᶠ (i : ι) in f, a1 i
a3 : ℝ
a4 : a3 > 0
a5 : ∀ {i : ι}, a1 i → ∀ {x : α}, dist x x₀ < a3 → p (i, x)
⊢ ∃ ε, ε > 0 ∧ ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ {x : α}, dist x x₀ < ε → ∀ {i : ι}, pa i → p (Prod.swap (x, i))
case mpr
α : Type u
β : Type v
X : Type ?u.93290
ι : Type u_1
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
f : Filter ι
x₀ : α
p : ι × α → Prop
⊢ (∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε, ε > 0 ∧ ∀ {i : ι}, pa i → ∀ {x : α}, dist x x₀ < ε → p (i, x)) →
    ∃ ε, ε > 0 ∧ ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ {x : α}, dist x x₀ < ε → ∀ {i : ι}, pa i → p (Prod.swap (x, i))
rintro ⟨a1, a2, a3, a4, a5⟩
no goals
case mpr.intro.intro.intro.intro
α : Type u
β : Type v
X : Type ?u.93290
ι : Type u_1
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
f : Filter ι
x₀ : α
p : ι × α → Prop
a1 : ι → Prop
a2 : ∀ᶠ (i : ι) in f, a1 i
a3 : ℝ
a4 : a3 > 0
a5 : ∀ {i : ι}, a1 i → ∀ {x : α}, dist x x₀ < a3 → p (i, x)
⊢ ∃ ε, ε > 0 ∧ ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ {x : α}, dist x x₀ < ε → ∀ {i : ι}, pa i → p (Prod.swap (x, i))
exact ⟨a3, a4, a1, a2, fun b1 b2 b3 => a5 b3 b1⟩