simp [Nonloop.lineContractPointEquiv, cl_singleton_eq he,
  diff_singleton_eq_self (fun heP ↦ (hP.subset_ground heP).2 rfl)]
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
no goals