Theorem: Prod.frequently (Ray/Misc/Topology.lean)

State before:
A B : Type
f : Filter A
g : Filter B
p : A → Prop
q : B → Prop
⊢ (∃ᶠ (x : A × B) in f ×ˢ g, p x.1 ∧ q x.2) ↔ (∃ᶠ (a : A) in f, p a) ∧ ∃ᶠ (b : B) in g, q b
Tactic:
simp only [frequently_iff_neBot, ← prod_neBot, ← prod_inf_prod, prod_principal_principal]
State after:
A B : Type
f : Filter A
g : Filter B
p : A → Prop
q : B → Prop
⊢ (f ×ˢ g ⊓ 𝓟 {x | p x.1 ∧ q x.2}).NeBot ↔ (f ×ˢ g ⊓ 𝓟 ({a | p a} ×ˢ {b | q b})).NeBot

State before:
A B : Type
f : Filter A
g : Filter B
p : A → Prop
q : B → Prop
⊢ (f ×ˢ g ⊓ 𝓟 {x | p x.1 ∧ q x.2}).NeBot ↔ (f ×ˢ g ⊓ 𝓟 ({a | p a} ×ˢ {b | q b})).NeBot
Tactic:
rfl
State after:
no goals