case h
α : Type u_1
β : Type u_2
γ : Type ?u.195273
ι : Sort u_3
ι' : Sort ?u.195279
ι₂ : Sort ?u.195282
κ : ι → Sort ?u.195287
κ₁ : ι → Sort ?u.195292
κ₂ : ι → Sort ?u.195297
κ' : ι' → Sort ?u.195302
f : α → β
s : ι → Set α
x : β
⊢ (x ∈ f '' ⋃ (i : ι), s i) ↔ x ∈ ⋃ (i : ι), f '' s i
α : Type u_1
β : Type u_2
γ : Type ?u.195273
ι : Sort u_3
ι' : Sort ?u.195279
ι₂ : Sort ?u.195282
κ : ι → Sort ?u.195287
κ₁ : ι → Sort ?u.195292
κ₂ : ι → Sort ?u.195297
κ' : ι' → Sort ?u.195302
f : α → β
s : ι → Set α
⊢ (f '' ⋃ (i : ι), s i) = ⋃ (i : ι), f '' s i
ext1 x
case h
α : Type u_1
β : Type u_2
γ : Type ?u.195273
ι : Sort u_3
ι' : Sort ?u.195279
ι₂ : Sort ?u.195282
κ : ι → Sort ?u.195287
κ₁ : ι → Sort ?u.195292
κ₂ : ι → Sort ?u.195297
κ' : ι' → Sort ?u.195302
f : α → β
s : ι → Set α
x : β
⊢ (∃ x_1 x_2, x_1 ∈ s x_2 ∧ f x_1 = x) ↔ ∃ i x_1, x_1 ∈ s i ∧ f x_1 = x
case h
α : Type u_1
β : Type u_2
γ : Type ?u.195273
ι : Sort u_3
ι' : Sort ?u.195279
ι₂ : Sort ?u.195282
κ : ι → Sort ?u.195287
κ₁ : ι → Sort ?u.195292
κ₂ : ι → Sort ?u.195297
κ' : ι' → Sort ?u.195302
f : α → β
s : ι → Set α
x : β
⊢ (x ∈ f '' ⋃ (i : ι), s i) ↔ x ∈ ⋃ (i : ι), f '' s i
simp only [mem_image, mem_iUnion, ← exists_and_right, ← exists_and_left]
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.195273
ι : Sort u_3
ι' : Sort ?u.195279
ι₂ : Sort ?u.195282
κ : ι → Sort ?u.195287
κ₁ : ι → Sort ?u.195292
κ₂ : ι → Sort ?u.195297
κ' : ι' → Sort ?u.195302
f : α → β
s : ι → Set α
x : β
⊢ (∃ x_1 x_2, x_1 ∈ s x_2 ∧ f x_1 = x) ↔ ∃ i x_1, x_1 ∈ s i ∧ f x_1 = x
rw [exists_swap]