no goals
α : Type u_2
β : Type u_1
γ : Type ?u.226621
ι : Sort ?u.226624
ι' : Sort ?u.226627
ι₂ : Sort ?u.226630
κ : ι → Sort ?u.226635
κ₁ : ι → Sort ?u.226640
κ₂ : ι → Sort ?u.226645
κ' : ι' → Sort ?u.226650
f : α → β
s : Set β
⊢ (⋃ (y : β) (_ : y ∈ s), f ⁻¹' {y}) = f ⁻¹' s
rw [← preimage_iUnion₂, biUnion_of_singleton]