exact hne (hX.eq_of_subset_base hY hss)
case inl.inl
α : Type u_1
M✝ : Matroid α
E I H B X✝ : Set α
e f : α
M : Matroid α
X : Set α
hX : M.Base X
Y : Set α
hY : M.Base Y
hne : X ≠ Y
hss : X ⊆ Y
⊢ False
no goals