rw [← ENat.tsum_comp_eq_tsum_of_equiv (toNonloop he).lineContractPointEquiv]
case h.e'_2
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ ∑' (L : { L // M.Line L ∧ e ∈ L }), (↑L \ {e}).encard =
    ∑' (x : { P // (M ／ e).Point P }), (↑((M ／ e).parallelPointEquiv.symm x)).encard
case h.e'_2
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ ∑' (x : { P // (M ／ e).Point P }), (↑(⋯.lineContractPointEquiv x) \ {e}).encard =
    ∑' (x : { P // (M ／ e).Point P }), (↑((M ／ e).parallelPointEquiv.symm x)).encard