convert ENat.tsum_comp_eq_tsum_of_equiv (M ／ e).parallelPointEquiv.symm (g := fun x ↦ x.1.encard)
  using 1
case h.e'_3
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
⊢ ∑' (L : { L // M.Line L ∧ e ∈ L }), (↑L \ {e}).encard = ∑' (t : ↑↑(M ／ e).parallelClasses), (↑t).encard
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