simpa using (hXfin.inter_right Y).finite_of_basis hIi
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
hXfin : M.rFin X
hYfin : M.rFin Y
hXE : autoParam (X ⊆ M.E) _auto✝
hYE : autoParam (Y ⊆ M.E) _auto✝
hr : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y)
Ii : Set α
hIi : M.Basis Ii (X ∩ Y)
⊢ Ii.encard ≠ ⊤
no goals