Theorem: Set.biUnion_distrib_union (Matroid/ForMathlib/Set.lean)

State before:
α : Type u_1
ι : Type u_2
s : ι → Set α
u : Set ι
hu : u.Nonempty
t : Set α
⊢ (⋃ i ∈ u, s i) ∪ t = ⋃ i ∈ u, s i ∪ t
Tactic:
simp_rw [union_comm, union_distrib_biUnion _ hu]
State after:
no goals