no goals
α : Type u_2
β : Type u_1
γ : Type ?u.226389
ι : Sort ?u.226392
ι' : Sort ?u.226395
ι₂ : Sort ?u.226398
κ : ι → Sort ?u.226403
κ₁ : ι → Sort ?u.226408
κ₂ : ι → Sort ?u.226413
κ' : ι' → Sort ?u.226418
f : α → β
s : Set (Set β)
⊢ f ⁻¹' ⋂₀ s = ⋂ (t : Set β) (_ : t ∈ s), f ⁻¹' t
rw [sInter_eq_biInter, preimage_iInter₂]