Theorem: Set.biInter_distrib_inter (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 [inter_comm, inter_distrib_biInter _ hu]
State after:
no goals