rw [h.er_eq, er_cl_eq, he.er_eq]
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
he : M.Nonloop e
h : M.cl {e} ⋖[M] L
⊢ M.er L = 2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
he : M.Nonloop e
h : M.cl {e} ⋖[M] L
⊢ 1 + 1 = 2