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

State before:
α : Type u_1
ι : Type u_2
s : Set (Set α)
hs : s.Nonempty
t : Set α
⊢ t ∩ ⋂₀ s = ⋂ x ∈ s, t ∩ x
Tactic:
rw [sInter_eq_biInter, inter_distrib_biInter _ hs]
State after:
no goals