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

State before:
α : Type u_1
M✝ M : Matroid α
inst✝ : M.Simple
⊢ M.numPoints = M.E.encard
Tactic:
simp [numPoints_eq_encard_ground_simplification]
State after:
no goals