case a
α : Type u_2
α' : Type ?u.30077
β : Type u_1
β' : Type ?u.30083
γ : Type ?u.30086
γ' : Type ?u.30089
δ : Type ?u.30092
δ' : Type ?u.30095
ε : Type ?u.30098
ε' : Type ?u.30101
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 : γ
h : NeBot g
u : Set α
⊢ u ∈ map₂ (fun x x_1 => x) f g ↔ u ∈ f
α : Type u_2
α' : Type ?u.30077
β : Type u_1
β' : Type ?u.30083
γ : Type ?u.30086
γ' : Type ?u.30089
δ : Type ?u.30092
δ' : Type ?u.30095
ε : Type ?u.30098
ε' : Type ?u.30101
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 : γ
h : NeBot g
⊢ map₂ (fun x x_1 => x) f g = f
ext u
case a
α : Type u_2
α' : Type ?u.30077
β : Type u_1
β' : Type ?u.30083
γ : Type ?u.30086
γ' : Type ?u.30089
δ : Type ?u.30092
δ' : Type ?u.30095
ε : Type ?u.30098
ε' : Type ?u.30101
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 : γ
h : NeBot g
u : Set α
⊢ u ∈ map₂ (fun x x_1 => x) f g → u ∈ f
case a
α : Type u_2
α' : Type ?u.30077
β : Type u_1
β' : Type ?u.30083
γ : Type ?u.30086
γ' : Type ?u.30089
δ : Type ?u.30092
δ' : Type ?u.30095
ε : Type ?u.30098
ε' : Type ?u.30101
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 : γ
h : NeBot g
u : Set α
⊢ u ∈ map₂ (fun x x_1 => x) f g ↔ u ∈ f
refine' ⟨_, fun hu => ⟨_, _, hu, univ_mem, (image2_left <| h.nonempty_of_mem univ_mem).subset⟩⟩
case a.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.30077
β : Type u_1
β' : Type ?u.30083
γ : Type ?u.30086
γ' : Type ?u.30089
δ : Type ?u.30092
δ' : Type ?u.30095
ε : Type ?u.30098
ε' : Type ?u.30101
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 : γ
h : NeBot g
u s : Set α
t : Set β
hs : s ∈ f
ht : t ∈ g
hu : image2 (fun x x_1 => x) s t ⊆ u
⊢ u ∈ f
case a
α : Type u_2
α' : Type ?u.30077
β : Type u_1
β' : Type ?u.30083
γ : Type ?u.30086
γ' : Type ?u.30089
δ : Type ?u.30092
δ' : Type ?u.30095
ε : Type ?u.30098
ε' : Type ?u.30101
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 : γ
h : NeBot g
u : Set α
⊢ u ∈ map₂ (fun x x_1 => x) f g → u ∈ f
rintro ⟨s, t, hs, ht, hu⟩
case a.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.30077
β : Type u_1
β' : Type ?u.30083
γ : Type ?u.30086
γ' : Type ?u.30089
δ : Type ?u.30092
δ' : Type ?u.30095
ε : Type ?u.30098
ε' : Type ?u.30101
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 : γ
h : NeBot g
u s : Set α
t : Set β
hs : s ∈ f
ht : t ∈ g
hu : s ⊆ u
⊢ u ∈ f
case a.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.30077
β : Type u_1
β' : Type ?u.30083
γ : Type ?u.30086
γ' : Type ?u.30089
δ : Type ?u.30092
δ' : Type ?u.30095
ε : Type ?u.30098
ε' : Type ?u.30101
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 : γ
h : NeBot g
u s : Set α
t : Set β
hs : s ∈ f
ht : t ∈ g
hu : image2 (fun x x_1 => x) s t ⊆ u
⊢ u ∈ f
rw [image2_left (h.nonempty_of_mem ht)] at hu
no goals
case a.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.30077
β : Type u_1
β' : Type ?u.30083
γ : Type ?u.30086
γ' : Type ?u.30089
δ : Type ?u.30092
δ' : Type ?u.30095
ε : Type ?u.30098
ε' : Type ?u.30101
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 : γ
h : NeBot g
u s : Set α
t : Set β
hs : s ∈ f
ht : t ∈ g
hu : s ⊆ u
⊢ u ∈ f
exact mem_of_superset hs hu