case h
α : Type u_2
α' : Type ?u.13084
β : Type u_3
β' : Type ?u.13090
γ : Type u_1
γ' : Type ?u.13096
δ : Type ?u.13099
δ' : Type ?u.13102
ε : Type ?u.13105
ε' : Type ?u.13108
ζ : Type ?u.13111
ζ' : Type ?u.13114
ν : Type ?u.13117
f f' : α → β → γ
g g' : α → β → γ → δ
s s' : Set α
t t' : Set β
u u' : Set γ
v : Set δ
a a' : α
b b' : β
c✝ c' : γ
d d' : δ
c : γ
⊢ c ∈ image2 f (s ∪ s') t ↔ c ∈ image2 f s t ∪ image2 f s' t
α : Type u_2
α' : Type ?u.13084
β : Type u_3
β' : Type ?u.13090
γ : Type u_1
γ' : Type ?u.13096
δ : Type ?u.13099
δ' : Type ?u.13102
ε : Type ?u.13105
ε' : Type ?u.13108
ζ : Type ?u.13111
ζ' : Type ?u.13114
ν : Type ?u.13117
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
ext c
case h.mp
α : Type u_2
α' : Type ?u.13084
β : Type u_3
β' : Type ?u.13090
γ : Type u_1
γ' : Type ?u.13096
δ : Type ?u.13099
δ' : Type ?u.13102
ε : Type ?u.13105
ε' : Type ?u.13108
ζ : Type ?u.13111
ζ' : Type ?u.13114
ν : Type ?u.13117
f f' : α → β → γ
g g' : α → β → γ → δ
s s' : Set α
t t' : Set β
u u' : Set γ
v : Set δ
a a' : α
b b' : β
c✝ c' : γ
d d' : δ
c : γ
⊢ c ∈ image2 f (s ∪ s') t → c ∈ image2 f s t ∪ image2 f s' t

case h.mpr
α : Type u_2
α' : Type ?u.13084
β : Type u_3
β' : Type ?u.13090
γ : Type u_1
γ' : Type ?u.13096
δ : Type ?u.13099
δ' : Type ?u.13102
ε : Type ?u.13105
ε' : Type ?u.13108
ζ : Type ?u.13111
ζ' : Type ?u.13114
ν : Type ?u.13117
f f' : α → β → γ
g g' : α → β → γ → δ
s s' : Set α
t t' : Set β
u u' : Set γ
v : Set δ
a a' : α
b b' : β
c✝ c' : γ
d d' : δ
c : γ
⊢ c ∈ image2 f s t ∪ image2 f s' t → c ∈ image2 f (s ∪ s') t
case h
α : Type u_2
α' : Type ?u.13084
β : Type u_3
β' : Type ?u.13090
γ : Type u_1
γ' : Type ?u.13096
δ : Type ?u.13099
δ' : Type ?u.13102
ε : Type ?u.13105
ε' : Type ?u.13108
ζ : Type ?u.13111
ζ' : Type ?u.13114
ν : Type ?u.13117
f f' : α → β → γ
g g' : α → β → γ → δ
s s' : Set α
t t' : Set β
u u' : Set γ
v : Set δ
a a' : α
b b' : β
c✝ c' : γ
d d' : δ
c : γ
⊢ c ∈ image2 f (s ∪ s') t ↔ c ∈ image2 f s t ∪ image2 f s' t
constructor
no goals
case h.mp
α : Type u_2
α' : Type ?u.13084
β : Type u_3
β' : Type ?u.13090
γ : Type u_1
γ' : Type ?u.13096
δ : Type ?u.13099
δ' : Type ?u.13102
ε : Type ?u.13105
ε' : Type ?u.13108
ζ : Type ?u.13111
ζ' : Type ?u.13114
ν : Type ?u.13117
f f' : α → β → γ
g g' : α → β → γ → δ
s s' : Set α
t t' : Set β
u u' : Set γ
v : Set δ
a a' : α
b b' : β
c✝ c' : γ
d d' : δ
c : γ
⊢ c ∈ image2 f (s ∪ s') t → c ∈ image2 f s t ∪ image2 f s' t
rintro ⟨a, b, ha | ha, hb, rfl⟩ <;> [left; right] <;> exact ⟨_, _, ‹_›, ‹_›, rfl⟩
no goals
case h.mpr
α : Type u_2
α' : Type ?u.13084
β : Type u_3
β' : Type ?u.13090
γ : Type u_1
γ' : Type ?u.13096
δ : Type ?u.13099
δ' : Type ?u.13102
ε : Type ?u.13105
ε' : Type ?u.13108
ζ : Type ?u.13111
ζ' : Type ?u.13114
ν : Type ?u.13117
f f' : α → β → γ
g g' : α → β → γ → δ
s s' : Set α
t t' : Set β
u u' : Set γ
v : Set δ
a a' : α
b b' : β
c✝ c' : γ
d d' : δ
c : γ
⊢ c ∈ image2 f s t ∪ image2 f s' t → c ∈ image2 f (s ∪ s') t
rintro (⟨_, _, _, _, rfl⟩ | ⟨_, _, _, _, rfl⟩) <;> refine' ⟨_, _, _, ‹_›, rfl⟩ <;>
  simp [mem_union, *]