rw [numPoints_eq_encard_parallelClasses, M.simplification_equiv.encard_eq]
α : Type u_1
M✝ M : Matroid α
⊢ M.numPoints = M.simplification.E.encard
α : Type u_1
M✝ M : Matroid α
⊢ (↑M.parallelClasses).encard = M.simplification.E.encard