case h
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Sort ?u.244602
ι' : Sort ?u.244605
ι₂ : Sort ?u.244608
κ : ι → Sort ?u.244613
κ₁ : ι → Sort ?u.244618
κ₂ : ι → Sort ?u.244623
κ' : ι' → Sort ?u.244628
f : α → β → γ
s : Set α
t : Set β
y : γ
⊢ (y ∈ ⋃ (a : α) (_ : a ∈ s), f a '' t) ↔ y ∈ image2 f s t
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Sort ?u.244602
ι' : Sort ?u.244605
ι₂ : Sort ?u.244608
κ : ι → Sort ?u.244613
κ₁ : ι → Sort ?u.244618
κ₂ : ι → Sort ?u.244623
κ' : ι' → Sort ?u.244628
f : α → β → γ
s : Set α
t : Set β
⊢ (⋃ (a : α) (_ : a ∈ s), f a '' t) = image2 f s t
ext y
no goals
case h
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Sort ?u.244602
ι' : Sort ?u.244605
ι₂ : Sort ?u.244608
κ : ι → Sort ?u.244613
κ₁ : ι → Sort ?u.244618
κ₂ : ι → Sort ?u.244623
κ' : ι' → Sort ?u.244628
f : α → β → γ
s : Set α
t : Set β
y : γ
⊢ (y ∈ ⋃ (a : α) (_ : a ∈ s), f a '' t) ↔ y ∈ image2 f s t
constructor <;> simp only [mem_iUnion] <;> rintro ⟨a, ha, x, hx, ax⟩ <;> exact ⟨a, x, ha, hx, ax⟩