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

State before:
α : Type u_1
ι : Type u_2
s : ι → Set α
u : Set ι
hu : u.Nonempty
t : Set α
⊢ t ∪ ⋃ i ∈ u, s i = ⋃ i ∈ u, t ∪ s i
Tactic:
have := hu.coe_sort
State after:
α : Type u_1
ι : Type u_2
s : ι → Set α
u : Set ι
hu : u.Nonempty
t : Set α
this : Nonempty ↑u
⊢ t ∪ ⋃ i ∈ u, s i = ⋃ i ∈ u, t ∪ s i

State before:
α : Type u_1
ι : Type u_2
s : ι → Set α
u : Set ι
hu : u.Nonempty
t : Set α
this : Nonempty ↑u
⊢ t ∪ ⋃ i ∈ u, s i = ⋃ i ∈ u, t ∪ s i
Tactic:
rw [biUnion_eq_iUnion, union_iUnion, biUnion_eq_iUnion]
State after:
no goals