Theorem: ex_1_2_10_ii (AlgebraI/Subgroups.lean)

State before:
⊢ Nat.card { x // orderOf x = 2 } = 9
Tactic:
rw [Nat.card_eq_fintype_card]
State after:
⊢ Fintype.card { x // orderOf x = 2 } = 9

State before:
⊢ Fintype.card { x // orderOf x = 2 } = 9
Tactic:
simp_rw [ex_1_2_10_ii_aux_1]
State after:
⊢ Fintype.card { x // x ≠ 1 ∧ x ^ 2 = 1 } = 9

State before:
⊢ Fintype.card { x // x ≠ 1 ∧ x ^ 2 = 1 } = 9
Tactic:
decide
State after:
no goals