refine tsum_congr (fun ⟨P,hP⟩ ↦ ?_)
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
case h.e'_2
α : Type u_1
M : Matroid α
inst✝ : M.Simple
e : α
he : e ∈ M.E
x✝ : { P // (M ／ e).Point P }
P : Set α
hP : (M ／ e).Point P
⊢ (↑(⋯.lineContractPointEquiv ⟨P, hP⟩) \ {e}).encard = (↑((M ／ e).parallelPointEquiv.symm ⟨P, hP⟩)).encard