no goals
α : Type ?u.27268
β : Type ?u.27271
γ : Type ?u.27274
δ : Type ?u.27277
ι : Sort ?u.27280
s✝ : Set α
t : Set β
f : Filter α
g : Filter β
α₁ : Type u
α₂ : Type v
β₁ : Type w
β₂ : Type x
f₁ : Filter α₁
f₂ : Filter α₂
m₁ : α₁ → β₁
m₂ : α₂ → β₂
s : Set (β₁ × β₂)
hs : (fun p => (m₁ p.fst, m₂ p.snd)) ⁻¹' s ∈ f₁ ×ˢ f₂
s₁ : Set α₁
hs₁ : s₁ ∈ f₁
s₂ : Set α₂
hs₂ : s₂ ∈ f₂
h : s₁ ×ˢ s₂ ⊆ (fun p => (m₁ p.fst, m₂ p.snd)) ⁻¹' s
⊢ (m₁ '' s₁) ×ˢ (m₂ '' s₂) ⊆ s
rwa [prod_image_image_eq, image_subset_iff]