Distinguish spaces in Lean by counting homs from π₁ to ZMod p

To show two CW-model spaces (e.g. closed surfaces with π₁ = PresentedGroup {r}) are not homotopy equivalent, count Nat.card (π₁ →* Multiplicative (ZMod p)). Pieces: (PresentedGroup rels →* G) ≃ {f : α → G // ∀ r ∈ rels, FreeGroup.lift f r = 1} (toGroup / PresentedGroup.ext); MulEquiv.monoidHomCongrLeftEquiv to transport along π₁ isos; FundamentalGroup.fundamentalGroupMulEquivOfPathConnected to make the count base-point free; Equiv.subtypeUnivEquiv + Nat.card_fun when every f kills the relators (commutators in a CommGroup), Fintype.card_subtype_lt with one bad f for a strict bound. ZMod 2 and ZMod 3 already separate all Σ_g and N_g. Small decide tricks that worked: generalize f i = x; revert x; decide for a statement over Multiplicative (ZMod 2), and revert z; decide for surjectivity onto it.