Theorem: Set.inter_distrib_biInter (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 [biInter_eq_iInter, inter_iInter, biInter_eq_iInter]
State after:
no goals