Theorem: xmp_1_2_11 (AlgebraI/Subgroups.lean)

State before:
n : ℕ+
⊢ AddSubgroup.index (ex1232 ↑↑n) = ↑n
Tactic:
simp [ex1232, AddSubgroup.index, Nat.card_congr (Int.quotientZMultiplesNatEquivZMod n).toEquiv,
  Nat.card_eq_fintype_card, ZMod.card]
State after:
no goals