α : Type u_1
β : Type ?u.10420
γ : Type u_2
δ : Type ?u.10426
ι : Sort ?u.10429
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter γ
p : α × γ × γ → Prop
h : ∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x
⊢ ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.fst, x.snd, x.snd)
α : Type u_1
β : Type ?u.10420
γ : Type u_2
δ : Type ?u.10426
ι : Sort ?u.10429
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter γ
p : α × γ × γ → Prop
⊢ (∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x) → ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.fst, x.snd, x.snd)
intro h
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.10420
γ : Type u_2
δ : Type ?u.10426
ι : Sort ?u.10429
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter γ
p : α × γ × γ → Prop
h : ∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x
t : α → Prop
ht : ∀ᶠ (x : α) in f, t x
s : γ × γ → Prop
hs : ∀ᶠ (y : γ × γ) in g ×ˢ g, s y
hst : ∀ {x : α}, t x → ∀ {y : γ × γ}, s y → p (x, y)
⊢ ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.fst, x.snd, x.snd)
α : Type u_1
β : Type ?u.10420
γ : Type u_2
δ : Type ?u.10426
ι : Sort ?u.10429
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter γ
p : α × γ × γ → Prop
h : ∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x
⊢ ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.fst, x.snd, x.snd)
obtain ⟨t, ht, s, hs, hst⟩ := eventually_prod_iff.1 h
no goals
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.10420
γ : Type u_2
δ : Type ?u.10426
ι : Sort ?u.10429
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter γ
p : α × γ × γ → Prop
h : ∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x
t : α → Prop
ht : ∀ᶠ (x : α) in f, t x
s : γ × γ → Prop
hs : ∀ᶠ (y : γ × γ) in g ×ˢ g, s y
hst : ∀ {x : α}, t x → ∀ {y : γ × γ}, s y → p (x, y)
⊢ ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.fst, x.snd, x.snd)
refine' (ht.prod_mk hs.diag_of_prod).mono fun x hx => by simp only [hst hx.1 hx.2, Prod.mk.eta]
no goals
α : Type u_1
β : Type ?u.10420
γ : Type u_2
δ : Type ?u.10426
ι : Sort ?u.10429
s✝ : Set α
t✝ : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter γ
p : α × γ × γ → Prop
h : ∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x
t : α → Prop
ht : ∀ᶠ (x : α) in f, t x
s : γ × γ → Prop
hs : ∀ᶠ (y : γ × γ) in g ×ˢ g, s y
hst : ∀ {x : α}, t x → ∀ {y : γ × γ}, s y → p (x, y)
x : α × γ
hx : t x.fst ∧ s (x.snd, x.snd)
⊢ p (x.fst, x.snd, x.snd)
simp only [hst hx.1 hx.2, Prod.mk.eta]