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

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