case a
α : Type u_1
α' : Type ?u.3075
β : Type u_2
β' : Type ?u.3081
γ : Type u_3
γ' : Type ?u.3087
δ : Type ?u.3090
δ' : Type ?u.3093
ε : Type ?u.3096
ε' : Type ?u.3099
m✝ : α → β → γ
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ s ∈ map (fun p => m p.fst p.snd) (f ×ˢ g) ↔ s ∈ map₂ m f g
α : Type u_1
α' : Type ?u.3075
β : Type u_2
β' : Type ?u.3081
γ : Type u_3
γ' : Type ?u.3087
δ : Type ?u.3090
δ' : Type ?u.3093
ε : Type ?u.3096
ε' : Type ?u.3099
m✝ : α → β → γ
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → β → γ
f : Filter α
g : Filter β
⊢ map (fun p => m p.fst p.snd) (f ×ˢ g) = map₂ m f g
ext s
no goals
case a
α : Type u_1
α' : Type ?u.3075
β : Type u_2
β' : Type ?u.3081
γ : Type u_3
γ' : Type ?u.3087
δ : Type ?u.3090
δ' : Type ?u.3093
ε : Type ?u.3096
ε' : Type ?u.3099
m✝ : α → β → γ
f✝ f₁ f₂ : Filter α
g✝ g₁ g₂ : Filter β
h h₁ h₂ : Filter γ
s✝ s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b : β
c : γ
m : α → β → γ
f : Filter α
g : Filter β
s : Set γ
⊢ s ∈ map (fun p => m p.fst p.snd) (f ×ˢ g) ↔ s ∈ map₂ m f g
simp [mem_prod_iff, prod_subset_iff]