case a
α : Type u_2
α' : Type ?u.25458
β : Type u_3
β' : Type ?u.25464
γ : Type u_1
γ' : Type ?u.25470
δ : Type ?u.25473
δ' : Type ?u.25476
ε : Type ?u.25479
ε' : Type ?u.25482
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₁ ⊔ g₂) ↔ u ∈ map₂ m f g₁ ⊔ map₂ m f g₂
α : Type u_2
α' : Type ?u.25458
β : Type u_3
β' : Type ?u.25464
γ : Type u_1
γ' : Type ?u.25470
δ : Type ?u.25473
δ' : Type ?u.25476
ε : Type ?u.25479
ε' : Type ?u.25482
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 (g₁ ⊔ g₂) = map₂ m f g₁ ⊔ map₂ m f g₂
ext u
case a.mp
α : Type u_2
α' : Type ?u.25458
β : Type u_3
β' : Type ?u.25464
γ : Type u_1
γ' : Type ?u.25470
δ : Type ?u.25473
δ' : Type ?u.25476
ε : Type ?u.25479
ε' : Type ?u.25482
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₁ ⊔ g₂) → u ∈ map₂ m f g₁ ⊔ map₂ m f g₂

case a.mpr
α : Type u_2
α' : Type ?u.25458
β : Type u_3
β' : Type ?u.25464
γ : Type u_1
γ' : Type ?u.25470
δ : Type ?u.25473
δ' : Type ?u.25476
ε : Type ?u.25479
ε' : Type ?u.25482
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 (g₁ ⊔ g₂)
case a
α : Type u_2
α' : Type ?u.25458
β : Type u_3
β' : Type ?u.25464
γ : Type u_1
γ' : Type ?u.25470
δ : Type ?u.25473
δ' : Type ?u.25476
ε : Type ?u.25479
ε' : Type ?u.25482
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₁ ⊔ g₂) ↔ u ∈ map₂ m f g₁ ⊔ map₂ m f g₂
constructor
case a.mp.intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.25458
β : Type u_3
β' : Type ?u.25464
γ : Type u_1
γ' : Type ?u.25470
δ : Type ?u.25473
δ' : Type ?u.25476
ε : Type ?u.25479
ε' : Type ?u.25482
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
hu : image2 m s t ⊆ u
h₁ : t ∈ g₁.sets
h₂ : t ∈ g₂.sets
⊢ u ∈ map₂ m f g₁ ⊔ map₂ m f g₂
case a.mp
α : Type u_2
α' : Type ?u.25458
β : Type u_3
β' : Type ?u.25464
γ : Type u_1
γ' : Type ?u.25470
δ : Type ?u.25473
δ' : Type ?u.25476
ε : Type ?u.25479
ε' : Type ?u.25482
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₁ ⊔ g₂) → u ∈ map₂ m f g₁ ⊔ map₂ m f g₂
rintro ⟨s, t, hs, ⟨h₁, h₂⟩, hu⟩
no goals
case a.mp.intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.25458
β : Type u_3
β' : Type ?u.25464
γ : Type u_1
γ' : Type ?u.25470
δ : Type ?u.25473
δ' : Type ?u.25476
ε : Type ?u.25479
ε' : Type ?u.25482
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
hu : image2 m s t ⊆ u
h₁ : t ∈ g₁.sets
h₂ : t ∈ g₂.sets
⊢ u ∈ map₂ m f g₁ ⊔ map₂ m f g₂
exact ⟨mem_of_superset (image2_mem_map₂ hs h₁) hu, mem_of_superset (image2_mem_map₂ hs h₂) hu⟩
case a.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.25458
β : Type u_3
β' : Type ?u.25464
γ : Type u_1
γ' : Type ?u.25470
δ : Type ?u.25473
δ' : Type ?u.25476
ε : Type ?u.25479
ε' : Type ?u.25482
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 (g₁ ⊔ g₂)
case a.mpr
α : Type u_2
α' : Type ?u.25458
β : Type u_3
β' : Type ?u.25464
γ : Type u_1
γ' : Type ?u.25470
δ : Type ?u.25473
δ' : Type ?u.25476
ε : Type ?u.25479
ε' : Type ?u.25482
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 (g₁ ⊔ 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.25458
β : Type u_3
β' : Type ?u.25464
γ : Type u_1
γ' : Type ?u.25470
δ : Type ?u.25473
δ' : Type ?u.25476
ε : Type ?u.25479
ε' : Type ?u.25482
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.25458
β : Type u_3
β' : Type ?u.25464
γ : Type u_1
γ' : Type ?u.25470
δ : Type ?u.25473
δ' : Type ?u.25476
ε : Type ?u.25479
ε' : Type ?u.25482
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 (g₁ ⊔ g₂)
refine' ⟨s₁ ∩ s₂, t₁ ∪ t₂, inter_mem hs₁ hs₂, union_mem_sup ht₁ ht₂, _⟩
case a.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.25458
β : Type u_3
β' : Type ?u.25464
γ : Type u_1
γ' : Type ?u.25470
δ : Type ?u.25473
δ' : Type ?u.25476
ε : Type ?u.25479
ε' : Type ?u.25482
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₁ ∪ image2 m (s₁ ∩ s₂) t₂ ⊆ u
case a.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.25458
β : Type u_3
β' : Type ?u.25464
γ : Type u_1
γ' : Type ?u.25470
δ : Type ?u.25473
δ' : Type ?u.25476
ε : Type ?u.25479
ε' : Type ?u.25482
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_right]
no goals
case a.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.25458
β : Type u_3
β' : Type ?u.25464
γ : Type u_1
γ' : Type ?u.25470
δ : Type ?u.25473
δ' : Type ?u.25476
ε : Type ?u.25479
ε' : Type ?u.25482
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₁ ∪ image2 m (s₁ ∩ s₂) t₂ ⊆ u
exact
  union_subset ((image2_subset_right <| inter_subset_left _ _).trans hu₁)
    ((image2_subset_right <| inter_subset_right _ _).trans hu₂)