case intro.intro.intro.intro
α : Type u_1
β : Type ?u.9533
γ : Type ?u.9536
δ : Type ?u.9539
ι : Sort ?u.9542
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g : Filter β
f : Filter α
p : α × α → Prop
h : ∀ᶠ (i : α × α) in f ×ˢ f, p i
t : α → Prop
ht : ∀ᶠ (x : α) in f, t x
s : α → Prop
hs : ∀ᶠ (y : α) in f, s y
hst : ∀ {x : α}, t x → ∀ {y : α}, s y → p (x, y)
⊢ ∀ᶠ (i : α) in f, p (i, i)
α : Type u_1
β : Type ?u.9533
γ : Type ?u.9536
δ : Type ?u.9539
ι : Sort ?u.9542
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
p : α × α → Prop
h : ∀ᶠ (i : α × α) in f ×ˢ f, p i
⊢ ∀ᶠ (i : α) in f, p (i, i)
obtain ⟨t, ht, s, hs, hst⟩ := eventually_prod_iff.1 h
no goals
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.9533
γ : Type ?u.9536
δ : Type ?u.9539
ι : Sort ?u.9542
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g : Filter β
f : Filter α
p : α × α → Prop
h : ∀ᶠ (i : α × α) in f ×ˢ f, p i
t : α → Prop
ht : ∀ᶠ (x : α) in f, t x
s : α → Prop
hs : ∀ᶠ (y : α) in f, s y
hst : ∀ {x : α}, t x → ∀ {y : α}, s y → p (x, y)
⊢ ∀ᶠ (i : α) in f, p (i, i)
apply (ht.and hs).mono fun x hx => hst hx.1 hx.2