exact (hY.indep.subset hss).not_dep hXc.dep
case inr.intro.inl
α : Type u_1
M✝ : Matroid α
E I H B X✝ : Set α
e f : α
M : Matroid α
X : Set α
hXc : M.Circuit X
Y : Set α
hY : M.Base Y
hne : X ≠ Y
hss : X ⊆ Y
⊢ False
no goals