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

State before:
α : Type u_1
ι : Type u_2
s : Set (Set α)
hs : s.Nonempty
t : Set α
⊢ t ∪ ⋃₀ s = ⋃ x ∈ s, t ∪ x
Tactic:
rw [sUnion_eq_biUnion, union_distrib_biUnion _ hs]
State after:
no goals