rw [← er_union_cl_left_eq, hX'.cl_eq_cl_of_subset_of_er_ge_er hXY hr, er_union_cl_left_eq]
case inl
α : 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.er (X ∪ Z) = M.er (Y ∪ Z)
no goals