rw [mem_iInter₂] at he
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : e ∈ ⋂ J ∈ Js, M.cl J
he' : e ∉ M.cl (⋂₀ Js)
⊢ False
α : Type u_1
ι : Type u_2
M : Matroid α
F I J X Y B C R : Set α
e✝ f x y : α
Js : Set (Set α)
hI : M.Indep I
hne : Js.Nonempty
hIs : ∀ J ∈ Js, J ⊆ I
hiX : ⋂₀ Js ⊆ I
hiI : M.Indep (⋂₀ Js)
e : α
he : ∀ i ∈ Js, e ∈ M.cl i
he' : e ∉ M.cl (⋂₀ Js)
⊢ False