no goals
α : Type u_2
β : Type u_1
γ : Type ?u.218372
ι : Sort u_3
ι' : Sort ?u.218378
ι₂ : Sort ?u.218381
κ : ι → Sort ?u.218386
κ₁ : ι → Sort ?u.218391
κ₂ : ι → Sort ?u.218396
κ' : ι' → Sort ?u.218401
f : α → β
s : ι → Set β
⊢ ∀ (x : α), (x ∈ f ⁻¹' ⋃ (i : ι), s i) ↔ x ∈ ⋃ (i : ι), f ⁻¹' s i
simp [preimage]