exact not_rFin_of_er_ge hX' (M.er_mono (subset_union_of_subset_left hXY _))
case inr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z✝ R : Set α
n : ℕ∞
e f : α
Z : Set α
hXY : X ⊆ Y
hr : M.er Y ≤ M.er X
hX' : ¬M.rFin X
⊢ ¬M.rFin (Y ∪ Z)
no goals