tauto
case h
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X✝ Y B C R : Set α
e✝ f x y : α
I E X : Set α
hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E)
e : α
⊢ (e ∈ E → e ∉ I) ∧ e ∈ E ∨ e ∈ E ∧ e ∈ I ∧ e ∈ X ↔ (e ∈ X ∨ e ∈ E ∧ e ∉ I) ∧ e ∈ E
no goals