case intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.22358
β : Type u_3
β' : Type ?u.22364
γ : Type u_1
γ' : Type ?u.22370
δ : Type ?u.22373
δ' : Type ?u.22376
ε : Type ?u.22379
ε' : Type ?u.22382
ζ : Type ?u.22385
ζ' : Type ?u.22388
ν : Type ?u.22391
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 : β
ha : a ∈ s
h1b : b ∈ t
h2b : b ∈ t'
⊢ f a b ∈ image2 f s t ∩ image2 f s t'
α : Type u_2
α' : Type ?u.22358
β : Type u_3
β' : Type ?u.22364
γ : Type u_1
γ' : Type ?u.22370
δ : Type ?u.22373
δ' : Type ?u.22376
ε : Type ?u.22379
ε' : Type ?u.22382
ζ : Type ?u.22385
ζ' : Type ?u.22388
ν : Type ?u.22391
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 (t ∩ t') ⊆ image2 f s t ∩ image2 f s t'
rintro _ ⟨a, b, ha, ⟨h1b, h2b⟩, rfl⟩
no goals
case intro.intro.intro.intro.intro
α : Type u_2
α' : Type ?u.22358
β : Type u_3
β' : Type ?u.22364
γ : Type u_1
γ' : Type ?u.22370
δ : Type ?u.22373
δ' : Type ?u.22376
ε : Type ?u.22379
ε' : Type ?u.22382
ζ : Type ?u.22385
ζ' : Type ?u.22388
ν : Type ?u.22391
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 : β
ha : a ∈ s
h1b : b ∈ t
h2b : b ∈ t'
⊢ f a b ∈ image2 f s t ∩ image2 f s t'
constructor <;> exact ⟨_, _, ‹_›, ‹_›, rfl⟩