case a
α : Type u_1
α' : Type ?u.29406
β : Type u_2
β' : Type ?u.29412
γ : Type u_3
γ' : Type ?u.29418
δ : Type ?u.29421
δ' : Type ?u.29424
ε : Type ?u.29427
ε' : Type ?u.29430
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 β
u : Set γ
⊢ u ∈ map₂ m f g ↔ u ∈ map₂ (fun a b => m b a) g f
α : Type u_1
α' : Type ?u.29406
β : Type u_2
β' : Type ?u.29412
γ : Type u_3
γ' : Type ?u.29418
δ : Type ?u.29421
δ' : Type ?u.29424
ε : Type ?u.29427
ε' : Type ?u.29430
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₂ m f g = map₂ (fun a b => m b a) g f
ext u
no goals
case a
α : Type u_1
α' : Type ?u.29406
β : Type u_2
β' : Type ?u.29412
γ : Type u_3
γ' : Type ?u.29418
δ : Type ?u.29421
δ' : Type ?u.29424
ε : Type ?u.29427
ε' : Type ?u.29430
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 β
u : Set γ
⊢ u ∈ map₂ m f g ↔ u ∈ map₂ (fun a b => m b a) g f
constructor <;> rintro ⟨s, t, hs, ht, hu⟩ <;> refine' ⟨t, s, ht, hs, by rwa [image2_swap]⟩
no goals
α : Type u_1
α' : Type ?u.29406
β : Type u_2
β' : Type ?u.29412
γ : Type u_3
γ' : Type ?u.29418
δ : Type ?u.29421
δ' : Type ?u.29424
ε : Type ?u.29427
ε' : Type ?u.29430
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 β
u : Set γ
s : Set β
t : Set α
hs : s ∈ g
ht : t ∈ f
hu : image2 (fun a b => m b a) s t ⊆ u
⊢ image2 m t s ⊆ u
rwa [image2_swap]