simp_rw [biInter_distrib_inter _ hA,
  cl_biInter_eq_biInter_cl_of_biUnion_indep hA (I := fun i ↦ (X i) ∩ I) (hI.subset (by simp)),
  subset_iInter_iff]
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
Xs Ys : Set (Set α)
ι : Type u_3
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.Basis (X i ∩ I) (X i)
⊢ ⋂ i ∈ A, X i ⊆ M.cl ((⋂ i ∈ A, X i) ∩ I)
α : Type u_1
ι✝ : Type u_2
M : Matroid α
F I J X✝ Y B C R : Set α
e f x y : α
Xs Ys : Set (Set α)
ι : Type u_3
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.Basis (X i ∩ I) (X i)
⊢ ∀ i ∈ A, ⋂ i ∈ A, X i ⊆ M.cl (X i ∩ I)