no goals
α : Type u_1
β : Type ?u.182387
γ : Type ?u.182390
ι : Sort u_2
ι' : Sort ?u.182396
ι₂ : Sort ?u.182399
κ : ι → Sort u_3
κ₁ : ι → Sort ?u.182409
κ₂ : ι → Sort ?u.182414
κ' : ι' → Sort ?u.182419
s : (i : ι) → κ i → Set α
t : Set α
⊢ (⋂ (i : ι) (j : κ i), s i j) ∪ t = ⋂ (i : ι) (j : κ i), s i j ∪ t
simp_rw [union_distrib_iInter_right]