case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.41440
β : Type u_4
β' : Type u_6
γ : Type u_5
γ' : Type u_7
δ : Type u_3
δ' : Type ?u.41458
ε : Type u_1
ε' : Type ?u.41464
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 : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
t₂ : Set γ'
u₁ : Set α
v : Set β
hu₁ : u₁ ∈ f
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
w : Set γ
hu₂ : u₂ ∈ f
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ s ∈ map₂ m f (map₂ n g h)
α : Type u_2
α' : Type ?u.41440
β : Type u_4
β' : Type u_6
γ : Type u_5
γ' : Type u_7
δ : Type u_3
δ' : Type ?u.41458
ε : Type u_1
ε' : Type ?u.41464
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 : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
⊢ map₂ m f (map₂ n g h) ≤ map₂ n' (map₂ m₁ f g) (map₂ m₂ f h)
rintro s ⟨t₁, t₂, ⟨u₁, v, hu₁, hv, ht₁⟩, ⟨u₂, w, hu₂, hw, ht₂⟩, hs⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.41440
β : Type u_4
β' : Type u_6
γ : Type u_5
γ' : Type u_7
δ : Type u_3
δ' : Type ?u.41458
ε : Type u_1
ε' : Type ?u.41464
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 : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
t₂ : Set γ'
u₁ : Set α
v : Set β
hu₁ : u₁ ∈ f
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
w : Set γ
hu₂ : u₂ ∈ f
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ image2 m (u₁ ∩ u₂) (image2 n v w) ⊆ s
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.41440
β : Type u_4
β' : Type u_6
γ : Type u_5
γ' : Type u_7
δ : Type u_3
δ' : Type ?u.41458
ε : Type u_1
ε' : Type ?u.41464
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 : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
t₂ : Set γ'
u₁ : Set α
v : Set β
hu₁ : u₁ ∈ f
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
w : Set γ
hu₂ : u₂ ∈ f
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ s ∈ map₂ m f (map₂ n g h)
refine' ⟨u₁ ∩ u₂, _, inter_mem hu₁ hu₂, image2_mem_map₂ hv hw, _⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_2
α' : Type ?u.41440
β : Type u_4
β' : Type u_6
γ : Type u_5
γ' : Type u_7
δ : Type u_3
δ' : Type ?u.41458
ε : Type u_1
ε' : Type ?u.41464
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 : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
t₂ : Set γ'
u₁ : Set α
v : Set β
hu₁ : u₁ ∈ f
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
w : Set γ
hu₂ : u₂ ∈ f
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ image2 (fun a b => m₁ a b) (u₁ ∩ u₂) v ⊆ t₁

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_2
α' : Type ?u.41440
β : Type u_4
β' : Type u_6
γ : Type u_5
γ' : Type u_7
δ : Type u_3
δ' : Type ?u.41458
ε : Type u_1
ε' : Type ?u.41464
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 : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
t₂ : Set γ'
u₁ : Set α
v : Set β
hu₁ : u₁ ∈ f
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
w : Set γ
hu₂ : u₂ ∈ f
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ image2 (fun a c => m₂ a c) (u₁ ∩ u₂) w ⊆ t₂
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.41440
β : Type u_4
β' : Type u_6
γ : Type u_5
γ' : Type u_7
δ : Type u_3
δ' : Type ?u.41458
ε : Type u_1
ε' : Type ?u.41464
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 : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
t₂ : Set γ'
u₁ : Set α
v : Set β
hu₁ : u₁ ∈ f
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
w : Set γ
hu₂ : u₂ ∈ f
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ image2 m (u₁ ∩ u₂) (image2 n v w) ⊆ s
refine' (image2_distrib_subset_left h_distrib).trans ((image2_subset _ _).trans hs)
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_2
α' : Type ?u.41440
β : Type u_4
β' : Type u_6
γ : Type u_5
γ' : Type u_7
δ : Type u_3
δ' : Type ?u.41458
ε : Type u_1
ε' : Type ?u.41464
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 : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
t₂ : Set γ'
u₁ : Set α
v : Set β
hu₁ : u₁ ∈ f
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
w : Set γ
hu₂ : u₂ ∈ f
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ image2 (fun a b => m₁ a b) (u₁ ∩ u₂) v ⊆ t₁
exact (image2_subset_right <| inter_subset_left _ _).trans ht₁
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_2
α' : Type ?u.41440
β : Type u_4
β' : Type u_6
γ : Type u_5
γ' : Type u_7
δ : Type u_3
δ' : Type ?u.41458
ε : Type u_1
ε' : Type ?u.41464
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 : α → δ → ε
n : β → γ → δ
m₁ : α → β → β'
m₂ : α → γ → γ'
n' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)
s : Set ε
t₁ : Set β'
t₂ : Set γ'
u₁ : Set α
v : Set β
hu₁ : u₁ ∈ f
hv : v ∈ g
ht₁ : image2 m₁ u₁ v ⊆ t₁
hs : image2 n' t₁ t₂ ⊆ s
u₂ : Set α
w : Set γ
hu₂ : u₂ ∈ f
hw : w ∈ h
ht₂ : image2 m₂ u₂ w ⊆ t₂
⊢ image2 (fun a c => m₂ a c) (u₁ ∩ u₂) w ⊆ t₂
exact (image2_subset_right <| inter_subset_right _ _).trans ht₂