rw [← er_lt_top_iff] at *
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hY : M.rFin Y
⊢ M.rFin (X ∪ Y)
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.er X < ⊤
hY : M.er Y < ⊤
⊢ M.er (X ∪ Y) < ⊤