Theorem: Matroid.er_union_eq_of_subsets_of_ers_le (Matroid/Rank.lean)

State before:
α : 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')
Tactic:
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]
State after:
no goals