no goals
α : Type u_2
β : Type u_1
γ : Type ?u.224545
ι : Sort ?u.224548
ι' : Sort ?u.224551
ι₂ : Sort ?u.224554
κ : ι → Sort ?u.224559
κ₁ : ι → Sort ?u.224564
κ₂ : ι → Sort ?u.224569
κ' : ι' → Sort ?u.224574
f : α → β
s : Set (Set β)
⊢ f ⁻¹' ⋃₀ s = ⋃ (t : Set β) (_ : t ∈ s), f ⁻¹' t
rw [sUnion_eq_biUnion, preimage_iUnion₂]