case a
α : Type u_2
α' : Type ?u.24396
β : Type u_3
β' : Type ?u.24402
γ : Type u_1
γ' : Type ?u.24408
δ : Type ?u.24411
δ' : Type ?u.24414
ε : Type ?u.24417
ε' : Type ?u.24420
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 : γ
u : Set γ
⊢ u ∈ map₂ m (f₁ ⊔ f₂) g ↔ u ∈ map₂ m f₁ g ⊔ map₂ m f₂ g
α : Type u_2
α' : Type ?u.24396
β : Type u_3
β' : Type ?u.24402
γ : Type u_1
γ' : Type ?u.24408
δ : Type ?u.24411
δ' : Type ?u.24414
ε : Type ?u.24417
ε' : Type ?u.24420
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 : γ
⊢ map₂ m (f₁ ⊔ f₂) g = map₂ m f₁ g ⊔ map₂ m f₂ g
ext u
case a.mp
α : Type u_2
α' : Type ?u.24396
β : Type u_3
β' : Type ?u.24402
γ : Type u_1
γ' : Type ?u.24408
δ : Type ?u.24411
δ' : Type ?u.24414
ε : Type ?u.24417
ε' : Type ?u.24420
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 : γ
u : Set γ
⊢ u ∈ map₂ m (f₁ ⊔ f₂) g → u ∈ map₂ m f₁ g ⊔ map₂ m f₂ g

case a.mpr
α : Type u_2
α' : Type ?u.24396
β : Type u_3
β' : Type ?u.24402
γ : Type u_1
γ' : Type ?u.24408
δ : Type ?u.24411
δ' : Type ?u.24414
ε : Type ?u.24417
ε' : Type ?u.24420
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 : γ
u : Set γ
⊢ u ∈ map₂ m f₁ g ⊔ map₂ m f₂ g → u ∈ map₂ m (f₁ ⊔ f₂) g
case a
α : Type u_2
α' : Type ?u.24396
β : Type u_3
β' : Type ?u.24402
γ : Type u_1
γ' : Type ?u.24408
δ : Type ?u.24411
δ' : Type ?u.24414
ε : Type ?u.24417
ε' : Type ?u.24420
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 : γ
u : Set γ
⊢ u ∈ map₂ m (f₁ ⊔ f₂) g ↔ u ∈ map₂ m f₁ g ⊔ map₂ m f₂ g
constructor
case a.mp.intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.24396
β : Type u_3
β' : Type ?u.24402
γ : Type u_1
γ' : Type ?u.24408
δ : Type ?u.24411
δ' : Type ?u.24414
ε : Type ?u.24417
ε' : Type ?u.24420
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 : γ
u : Set γ
s : Set α
t : Set β
h₁ : s ∈ f₁.sets
h₂ : s ∈ f₂.sets
ht : t ∈ g
hu : image2 m s t ⊆ u
⊢ u ∈ map₂ m f₁ g ⊔ map₂ m f₂ g
case a.mp
α : Type u_2
α' : Type ?u.24396
β : Type u_3
β' : Type ?u.24402
γ : Type u_1
γ' : Type ?u.24408
δ : Type ?u.24411
δ' : Type ?u.24414
ε : Type ?u.24417
ε' : Type ?u.24420
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 : γ
u : Set γ
⊢ u ∈ map₂ m (f₁ ⊔ f₂) g → u ∈ map₂ m f₁ g ⊔ map₂ m f₂ g
rintro ⟨s, t, ⟨h₁, h₂⟩, ht, hu⟩
no goals
case a.mp.intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.24396
β : Type u_3
β' : Type ?u.24402
γ : Type u_1
γ' : Type ?u.24408
δ : Type ?u.24411
δ' : Type ?u.24414
ε : Type ?u.24417
ε' : Type ?u.24420
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 : γ
u : Set γ
s : Set α
t : Set β
h₁ : s ∈ f₁.sets
h₂ : s ∈ f₂.sets
ht : t ∈ g
hu : image2 m s t ⊆ u
⊢ u ∈ map₂ m f₁ g ⊔ map₂ m f₂ g
exact ⟨mem_of_superset (image2_mem_map₂ h₁ ht) hu, mem_of_superset (image2_mem_map₂ h₂ ht) hu⟩
case a.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.24396
β : Type u_3
β' : Type ?u.24402
γ : Type u_1
γ' : Type ?u.24408
δ : Type ?u.24411
δ' : Type ?u.24414
ε : Type ?u.24417
ε' : Type ?u.24420
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 : γ
u : Set γ
s₁ : Set α
t₁ : Set β
hs₁ : s₁ ∈ f₁
ht₁ : t₁ ∈ g
hu₁ : image2 m s₁ t₁ ⊆ u
s₂ : Set α
t₂ : Set β
hs₂ : s₂ ∈ f₂
ht₂ : t₂ ∈ g
hu₂ : image2 m s₂ t₂ ⊆ u
⊢ u ∈ map₂ m (f₁ ⊔ f₂) g
case a.mpr
α : Type u_2
α' : Type ?u.24396
β : Type u_3
β' : Type ?u.24402
γ : Type u_1
γ' : Type ?u.24408
δ : Type ?u.24411
δ' : Type ?u.24414
ε : Type ?u.24417
ε' : Type ?u.24420
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 : γ
u : Set γ
⊢ u ∈ map₂ m f₁ g ⊔ map₂ m f₂ g → u ∈ map₂ m (f₁ ⊔ f₂) g
rintro ⟨⟨s₁, t₁, hs₁, ht₁, hu₁⟩, s₂, t₂, hs₂, ht₂, hu₂⟩
case a.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.24396
β : Type u_3
β' : Type ?u.24402
γ : Type u_1
γ' : Type ?u.24408
δ : Type ?u.24411
δ' : Type ?u.24414
ε : Type ?u.24417
ε' : Type ?u.24420
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 : γ
u : Set γ
s₁ : Set α
t₁ : Set β
hs₁ : s₁ ∈ f₁
ht₁ : t₁ ∈ g
hu₁ : image2 m s₁ t₁ ⊆ u
s₂ : Set α
t₂ : Set β
hs₂ : s₂ ∈ f₂
ht₂ : t₂ ∈ g
hu₂ : image2 m s₂ t₂ ⊆ u
⊢ image2 m (s₁ ∪ s₂) (t₁ ∩ t₂) ⊆ u
case a.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.24396
β : Type u_3
β' : Type ?u.24402
γ : Type u_1
γ' : Type ?u.24408
δ : Type ?u.24411
δ' : Type ?u.24414
ε : Type ?u.24417
ε' : Type ?u.24420
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 : γ
u : Set γ
s₁ : Set α
t₁ : Set β
hs₁ : s₁ ∈ f₁
ht₁ : t₁ ∈ g
hu₁ : image2 m s₁ t₁ ⊆ u
s₂ : Set α
t₂ : Set β
hs₂ : s₂ ∈ f₂
ht₂ : t₂ ∈ g
hu₂ : image2 m s₂ t₂ ⊆ u
⊢ u ∈ map₂ m (f₁ ⊔ f₂) g
refine' ⟨s₁ ∪ s₂, t₁ ∩ t₂, union_mem_sup hs₁ hs₂, inter_mem ht₁ ht₂, _⟩
case a.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.24396
β : Type u_3
β' : Type ?u.24402
γ : Type u_1
γ' : Type ?u.24408
δ : Type ?u.24411
δ' : Type ?u.24414
ε : Type ?u.24417
ε' : Type ?u.24420
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 : γ
u : Set γ
s₁ : Set α
t₁ : Set β
hs₁ : s₁ ∈ f₁
ht₁ : t₁ ∈ g
hu₁ : image2 m s₁ t₁ ⊆ u
s₂ : Set α
t₂ : Set β
hs₂ : s₂ ∈ f₂
ht₂ : t₂ ∈ g
hu₂ : image2 m s₂ t₂ ⊆ u
⊢ image2 m s₁ (t₁ ∩ t₂) ∪ image2 m s₂ (t₁ ∩ t₂) ⊆ u
case a.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.24396
β : Type u_3
β' : Type ?u.24402
γ : Type u_1
γ' : Type ?u.24408
δ : Type ?u.24411
δ' : Type ?u.24414
ε : Type ?u.24417
ε' : Type ?u.24420
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 : γ
u : Set γ
s₁ : Set α
t₁ : Set β
hs₁ : s₁ ∈ f₁
ht₁ : t₁ ∈ g
hu₁ : image2 m s₁ t₁ ⊆ u
s₂ : Set α
t₂ : Set β
hs₂ : s₂ ∈ f₂
ht₂ : t₂ ∈ g
hu₂ : image2 m s₂ t₂ ⊆ u
⊢ image2 m (s₁ ∪ s₂) (t₁ ∩ t₂) ⊆ u
rw [image2_union_left]
no goals
case a.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.24396
β : Type u_3
β' : Type ?u.24402
γ : Type u_1
γ' : Type ?u.24408
δ : Type ?u.24411
δ' : Type ?u.24414
ε : Type ?u.24417
ε' : Type ?u.24420
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 : γ
u : Set γ
s₁ : Set α
t₁ : Set β
hs₁ : s₁ ∈ f₁
ht₁ : t₁ ∈ g
hu₁ : image2 m s₁ t₁ ⊆ u
s₂ : Set α
t₂ : Set β
hs₂ : s₂ ∈ f₂
ht₂ : t₂ ∈ g
hu₂ : image2 m s₂ t₂ ⊆ u
⊢ image2 m s₁ (t₁ ∩ t₂) ∪ image2 m s₂ (t₁ ∩ t₂) ⊆ u
exact
  union_subset ((image2_subset_left <| inter_subset_left _ _).trans hu₁)
    ((image2_subset_left <| inter_subset_right _ _).trans hu₂)