rw [er_union_eq_of_subset_of_er_le_er _ hX hXX', union_comm,
  er_union_eq_of_subset_of_er_le_er _ hY hYY', union_comm]
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : X ⊆ X'
hY : Y ⊆ Y'
hXX' : M.er X' ≤ M.er X
hYY' : M.er Y' ≤ M.er Y
⊢ M.er (X ∪ Y) = M.er (X' ∪ Y')
no goals