rw [← er_lt_top_iff, ← M.relRank_add_er_eq, relRank]
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hX : (M ／ C).rFin X
hC : M.rFin C
⊢ M.rFin (X ∪ C)
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hX : (M ／ C).rFin X
hC : M.rFin C
⊢ (M ／ C).er X + M.er C < ⊤