no goals
α : Type u_2
β : Type u_1
γ : Type ?u.86447
ι : Sort ?u.86450
ι' : Sort ?u.86453
f : ι → α
s✝ t : Set α
s : Set (α ⊕ β)
⊢ Sum.inl '' (Sum.inl ⁻¹' s) ∪ Sum.inr '' (Sum.inr ⁻¹' s) = s
rw [image_preimage_eq_inter_range, image_preimage_eq_inter_range, ← inter_distrib_left,
  range_inl_union_range_inr, inter_univ]