case intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.21899
β : Type u_3
β' : Type ?u.21905
γ : Type u_1
γ' : Type ?u.21911
δ : Type ?u.21914
δ' : Type ?u.21917
ε : Type ?u.21920
ε' : Type ?u.21923
ζ : Type ?u.21926
ζ' : Type ?u.21929
ν : Type ?u.21932
f f' : α → β → γ
g g' : α → β → γ → δ
s s' : Set α
t t' : Set β
u u' : Set γ
v : Set δ
a✝ a' : α
b✝ b' : β
c c' : γ
d d' : δ
a : α
b : β
h1a : a ∈ s
h2a : a ∈ s'
hb : b ∈ t
⊢ f a b ∈ image2 f s t ∩ image2 f s' t
α : Type u_2
α' : Type ?u.21899
β : Type u_3
β' : Type ?u.21905
γ : Type u_1
γ' : Type ?u.21911
δ : Type ?u.21914
δ' : Type ?u.21917
ε : Type ?u.21920
ε' : Type ?u.21923
ζ : Type ?u.21926
ζ' : Type ?u.21929
ν : Type ?u.21932
f f' : α → β → γ
g g' : α → β → γ → δ
s s' : Set α
t t' : Set β
u u' : Set γ
v : Set δ
a a' : α
b b' : β
c c' : γ
d d' : δ
⊢ image2 f (s ∩ s') t ⊆ image2 f s t ∩ image2 f s' t
rintro _ ⟨a, b, ⟨h1a, h2a⟩, hb, rfl⟩
no goals
case intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.21899
β : Type u_3
β' : Type ?u.21905
γ : Type u_1
γ' : Type ?u.21911
δ : Type ?u.21914
δ' : Type ?u.21917
ε : Type ?u.21920
ε' : Type ?u.21923
ζ : Type ?u.21926
ζ' : Type ?u.21929
ν : Type ?u.21932
f f' : α → β → γ
g g' : α → β → γ → δ
s s' : Set α
t t' : Set β
u u' : Set γ
v : Set δ
a✝ a' : α
b✝ b' : β
c c' : γ
d d' : δ
a : α
b : β
h1a : a ∈ s
h2a : a ∈ s'
hb : b ∈ t
⊢ f a b ∈ image2 f s t ∩ image2 f s' t
constructor <;> exact ⟨_, _, ‹_›, ‹_›, rfl⟩