case a
α : Type u_4
α' : Type ?u.34074
β : Type u_5
β' : Type ?u.34080
γ : Type u_3
γ' : Type ?u.34086
δ : Type u_2
δ' : Type ?u.34092
ε : Type u_1
ε' : Type ?u.34098
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 : α → β → δ
w : Set ε
⊢ w ∈ map₂ m (map₂ n f g) h ↔ w ∈ map₃ (fun a b c => m (n a b) c) f g h
α : Type u_4
α' : Type ?u.34074
β : Type u_5
β' : Type ?u.34080
γ : Type u_3
γ' : Type ?u.34086
δ : Type u_2
δ' : Type ?u.34092
ε : Type u_1
ε' : Type ?u.34098
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 : α → β → δ
⊢ map₂ m (map₂ n f g) h = map₃ (fun a b c => m (n a b) c) f g h
ext w
case a.mp
α : Type u_4
α' : Type ?u.34074
β : Type u_5
β' : Type ?u.34080
γ : Type u_3
γ' : Type ?u.34086
δ : Type u_2
δ' : Type ?u.34092
ε : Type u_1
ε' : Type ?u.34098
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 : α → β → δ
w : Set ε
⊢ w ∈ map₂ m (map₂ n f g) h → w ∈ map₃ (fun a b c => m (n a b) c) f g h

case a.mpr
α : Type u_4
α' : Type ?u.34074
β : Type u_5
β' : Type ?u.34080
γ : Type u_3
γ' : Type ?u.34086
δ : Type u_2
δ' : Type ?u.34092
ε : Type u_1
ε' : Type ?u.34098
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 : α → β → δ
w : Set ε
⊢ w ∈ map₃ (fun a b c => m (n a b) c) f g h → w ∈ map₂ m (map₂ n f g) h
case a
α : Type u_4
α' : Type ?u.34074
β : Type u_5
β' : Type ?u.34080
γ : Type u_3
γ' : Type ?u.34086
δ : Type u_2
δ' : Type ?u.34092
ε : Type u_1
ε' : Type ?u.34098
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 : α → β → δ
w : Set ε
⊢ w ∈ map₂ m (map₂ n f g) h ↔ w ∈ map₃ (fun a b c => m (n a b) c) f g h
constructor
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_4
α' : Type ?u.34074
β : Type u_5
β' : Type ?u.34080
γ : Type u_3
γ' : Type ?u.34086
δ : Type u_2
δ' : Type ?u.34092
ε : Type u_1
ε' : Type ?u.34098
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 : α → β → δ
w : Set ε
s : Set δ
t : Set γ
u : Set α
v : Set β
hu : u ∈ f
hv : v ∈ g
hs : image2 n u v ⊆ s
ht : t ∈ h
hw : image2 m s t ⊆ w
⊢ w ∈ map₃ (fun a b c => m (n a b) c) f g h
case a.mp
α : Type u_4
α' : Type ?u.34074
β : Type u_5
β' : Type ?u.34080
γ : Type u_3
γ' : Type ?u.34086
δ : Type u_2
δ' : Type ?u.34092
ε : Type u_1
ε' : Type ?u.34098
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 : α → β → δ
w : Set ε
⊢ w ∈ map₂ m (map₂ n f g) h → w ∈ map₃ (fun a b c => m (n a b) c) f g h
rintro ⟨s, t, ⟨u, v, hu, hv, hs⟩, ht, hw⟩
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_4
α' : Type ?u.34074
β : Type u_5
β' : Type ?u.34080
γ : Type u_3
γ' : Type ?u.34086
δ : Type u_2
δ' : Type ?u.34092
ε : Type u_1
ε' : Type ?u.34098
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 : α → β → δ
w : Set ε
s : Set δ
t : Set γ
u : Set α
v : Set β
hu : u ∈ f
hv : v ∈ g
hs : image2 n u v ⊆ s
ht : t ∈ h
hw : image2 m s t ⊆ w
⊢ image3 (fun a b c => m (n a b) c) u v t ⊆ w
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_4
α' : Type ?u.34074
β : Type u_5
β' : Type ?u.34080
γ : Type u_3
γ' : Type ?u.34086
δ : Type u_2
δ' : Type ?u.34092
ε : Type u_1
ε' : Type ?u.34098
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 : α → β → δ
w : Set ε
s : Set δ
t : Set γ
u : Set α
v : Set β
hu : u ∈ f
hv : v ∈ g
hs : image2 n u v ⊆ s
ht : t ∈ h
hw : image2 m s t ⊆ w
⊢ w ∈ map₃ (fun a b c => m (n a b) c) f g h
refine' ⟨u, v, t, hu, hv, ht, _⟩
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_4
α' : Type ?u.34074
β : Type u_5
β' : Type ?u.34080
γ : Type u_3
γ' : Type ?u.34086
δ : Type u_2
δ' : Type ?u.34092
ε : Type u_1
ε' : Type ?u.34098
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 : α → β → δ
w : Set ε
s : Set δ
t : Set γ
u : Set α
v : Set β
hu : u ∈ f
hv : v ∈ g
hs : image2 n u v ⊆ s
ht : t ∈ h
hw : image2 m s t ⊆ w
⊢ image2 m (image2 (fun a b => n a b) u v) t ⊆ w
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_4
α' : Type ?u.34074
β : Type u_5
β' : Type ?u.34080
γ : Type u_3
γ' : Type ?u.34086
δ : Type u_2
δ' : Type ?u.34092
ε : Type u_1
ε' : Type ?u.34098
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 : α → β → δ
w : Set ε
s : Set δ
t : Set γ
u : Set α
v : Set β
hu : u ∈ f
hv : v ∈ g
hs : image2 n u v ⊆ s
ht : t ∈ h
hw : image2 m s t ⊆ w
⊢ image3 (fun a b c => m (n a b) c) u v t ⊆ w
rw [← image2_image2_left]
no goals
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_4
α' : Type ?u.34074
β : Type u_5
β' : Type ?u.34080
γ : Type u_3
γ' : Type ?u.34086
δ : Type u_2
δ' : Type ?u.34092
ε : Type u_1
ε' : Type ?u.34098
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 : α → β → δ
w : Set ε
s : Set δ
t : Set γ
u : Set α
v : Set β
hu : u ∈ f
hv : v ∈ g
hs : image2 n u v ⊆ s
ht : t ∈ h
hw : image2 m s t ⊆ w
⊢ image2 m (image2 (fun a b => n a b) u v) t ⊆ w
exact (image2_subset_right hs).trans hw
case a.mpr.intro.intro.intro.intro.intro.intro
α : Type u_4
α' : Type ?u.34074
β : Type u_5
β' : Type ?u.34080
γ : Type u_3
γ' : Type ?u.34086
δ : Type u_2
δ' : Type ?u.34092
ε : Type u_1
ε' : Type ?u.34098
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 : α → β → δ
w : Set ε
s : Set α
t : Set β
u : Set γ
hs : s ∈ f
ht : t ∈ g
hu : u ∈ h
hw : image3 (fun a b c => m (n a b) c) s t u ⊆ w
⊢ w ∈ map₂ m (map₂ n f g) h
case a.mpr
α : Type u_4
α' : Type ?u.34074
β : Type u_5
β' : Type ?u.34080
γ : Type u_3
γ' : Type ?u.34086
δ : Type u_2
δ' : Type ?u.34092
ε : Type u_1
ε' : Type ?u.34098
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 : α → β → δ
w : Set ε
⊢ w ∈ map₃ (fun a b c => m (n a b) c) f g h → w ∈ map₂ m (map₂ n f g) h
rintro ⟨s, t, u, hs, ht, hu, hw⟩
no goals
case a.mpr.intro.intro.intro.intro.intro.intro
α : Type u_4
α' : Type ?u.34074
β : Type u_5
β' : Type ?u.34080
γ : Type u_3
γ' : Type ?u.34086
δ : Type u_2
δ' : Type ?u.34092
ε : Type u_1
ε' : Type ?u.34098
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 : α → β → δ
w : Set ε
s : Set α
t : Set β
u : Set γ
hs : s ∈ f
ht : t ∈ g
hu : u ∈ h
hw : image3 (fun a b c => m (n a b) c) s t u ⊆ w
⊢ w ∈ map₂ m (map₂ n f g) h
exact ⟨_, u, image2_mem_map₂ hs ht, hu, by rwa [image2_image2_left]⟩
no goals
α : Type u_4
α' : Type ?u.34074
β : Type u_5
β' : Type ?u.34080
γ : Type u_3
γ' : Type ?u.34086
δ : Type u_2
δ' : Type ?u.34092
ε : Type u_1
ε' : Type ?u.34098
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 : α → β → δ
w : Set ε
s : Set α
t : Set β
u : Set γ
hs : s ∈ f
ht : t ∈ g
hu : u ∈ h
hw : image3 (fun a b c => m (n a b) c) s t u ⊆ w
⊢ image2 m (image2 n s t) u ⊆ w
rwa [image2_image2_left]