Theorem: Set.sInter_distrib_inter (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:
simp_rw [inter_comm _ t, inter_distrib_sInter hs]
State after:
no goals