rw [← he.er_eq]
case refine_2
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
hX : autoParam (X ⊆ M.E) _auto✝
x✝ : ∃ e ∈ X, M.Nonloop e ∧ X ⊆ M.cl {e}
e : α
heX : e ∈ X
he : M.Nonloop e
hXe : X ⊆ M.cl {e}
⊢ M.er X = 1
case refine_2
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
hX : autoParam (X ⊆ M.E) _auto✝
x✝ : ∃ e ∈ X, M.Nonloop e ∧ X ⊆ M.cl {e}
e : α
heX : e ∈ X
he : M.Nonloop e
hXe : X ⊆ M.cl {e}
⊢ M.er X = M.er {e}