no goals
α : Type u_1
β : Type u_2
γ : Type ?u.226879
ι : Sort ?u.226882
ι' : Sort ?u.226885
ι₂ : Sort ?u.226888
κ : ι → Sort ?u.226893
κ₁ : ι → Sort ?u.226898
κ₂ : ι → Sort ?u.226903
κ' : ι' → Sort ?u.226908
f : α → β
⊢ (⋃ (y : β) (_ : y ∈ range f), f ⁻¹' {y}) = univ
rw [biUnion_preimage_singleton, preimage_range]