case h
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Sort ?u.246068
ι' : Sort ?u.246071
ι₂ : Sort ?u.246074
κ : ι → Sort ?u.246079
κ₁ : ι → Sort ?u.246084
κ₂ : ι → Sort ?u.246089
κ' : ι' → Sort ?u.246094
f : α → β → γ
s : Set α
t : Set β
y : γ
⊢ (y ∈ ⋃ (b : β) (_ : b ∈ t), (fun a => f a b) '' s) ↔ y ∈ image2 f s t
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Sort ?u.246068
ι' : Sort ?u.246071
ι₂ : Sort ?u.246074
κ : ι → Sort ?u.246079
κ₁ : ι → Sort ?u.246084
κ₂ : ι → Sort ?u.246089
κ' : ι' → Sort ?u.246094
f : α → β → γ
s : Set α
t : Set β
⊢ (⋃ (b : β) (_ : b ∈ t), (fun a => f a b) '' s) = image2 f s t
ext y
case h.mp.intro.intro.intro.intro
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Sort ?u.246068
ι' : Sort ?u.246071
ι₂ : Sort ?u.246074
κ : ι → Sort ?u.246079
κ₁ : ι → Sort ?u.246084
κ₂ : ι → Sort ?u.246089
κ' : ι' → Sort ?u.246094
f : α → β → γ
s : Set α
t : Set β
y : γ
a : β
b : a ∈ t
c : α
d : c ∈ s
e : (fun a_1 => f a_1 a) c = y
⊢ y ∈ image2 f s t

case h.mpr.intro.intro.intro.intro
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Sort ?u.246068
ι' : Sort ?u.246071
ι₂ : Sort ?u.246074
κ : ι → Sort ?u.246079
κ₁ : ι → Sort ?u.246084
κ₂ : ι → Sort ?u.246089
κ' : ι' → Sort ?u.246094
f : α → β → γ
s : Set α
t : Set β
y : γ
a : α
b : β
c : a ∈ s
d : b ∈ t
e : f a b = y
⊢ ∃ i i_1, y ∈ (fun a => f a i) '' s
case h
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Sort ?u.246068
ι' : Sort ?u.246071
ι₂ : Sort ?u.246074
κ : ι → Sort ?u.246079
κ₁ : ι → Sort ?u.246084
κ₂ : ι → Sort ?u.246089
κ' : ι' → Sort ?u.246094
f : α → β → γ
s : Set α
t : Set β
y : γ
⊢ (y ∈ ⋃ (b : β) (_ : b ∈ t), (fun a => f a b) '' s) ↔ y ∈ image2 f s t
constructor <;> simp only [mem_iUnion] <;> rintro ⟨a, b, c, d, e⟩
case h.mpr.intro.intro.intro.intro
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Sort ?u.246068
ι' : Sort ?u.246071
ι₂ : Sort ?u.246074
κ : ι → Sort ?u.246079
κ₁ : ι → Sort ?u.246084
κ₂ : ι → Sort ?u.246089
κ' : ι' → Sort ?u.246094
f : α → β → γ
s : Set α
t : Set β
y : γ
a : α
b : β
c : a ∈ s
d : b ∈ t
e : f a b = y
⊢ ∃ i i_1, y ∈ (fun a => f a i) '' s
case h.mp.intro.intro.intro.intro
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Sort ?u.246068
ι' : Sort ?u.246071
ι₂ : Sort ?u.246074
κ : ι → Sort ?u.246079
κ₁ : ι → Sort ?u.246084
κ₂ : ι → Sort ?u.246089
κ' : ι' → Sort ?u.246094
f : α → β → γ
s : Set α
t : Set β
y : γ
a : β
b : a ∈ t
c : α
d : c ∈ s
e : (fun a_1 => f a_1 a) c = y
⊢ y ∈ image2 f s t

case h.mpr.intro.intro.intro.intro
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Sort ?u.246068
ι' : Sort ?u.246071
ι₂ : Sort ?u.246074
κ : ι → Sort ?u.246079
κ₁ : ι → Sort ?u.246084
κ₂ : ι → Sort ?u.246089
κ' : ι' → Sort ?u.246094
f : α → β → γ
s : Set α
t : Set β
y : γ
a : α
b : β
c : a ∈ s
d : b ∈ t
e : f a b = y
⊢ ∃ i i_1, y ∈ (fun a => f a i) '' s
exact ⟨c, a, d, b, e⟩
no goals
case h.mpr.intro.intro.intro.intro
α : Type u_3
β : Type u_2
γ : Type u_1
ι : Sort ?u.246068
ι' : Sort ?u.246071
ι₂ : Sort ?u.246074
κ : ι → Sort ?u.246079
κ₁ : ι → Sort ?u.246084
κ₂ : ι → Sort ?u.246089
κ' : ι' → Sort ?u.246094
f : α → β → γ
s : Set α
t : Set β
y : γ
a : α
b : β
c : a ∈ s
d : b ∈ t
e : f a b = y
⊢ ∃ i i_1, y ∈ (fun a => f a i) '' s
exact ⟨b, d, a, c, e⟩