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

State before:
α : Type u_1
M✝ M : Matroid α
⊢ M.numPoints = (↑M.parallelClasses).encard
Tactic:
rw [numPoints, ← encard_univ_coe, M.parallelPointEquiv.symm.encard_univ_eq, encard_univ_coe]
State after:
no goals