Theorem: Matroid.numPoints_eq_encard_ground_simplification (Matroid/Old/Kung.lean)

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