case hx
n : ℕ
⊢ orderOf ?x = Fintype.card (QuaternionGroup 1)

case x
n : ℕ
⊢ QuaternionGroup 1
n : ℕ
⊢ IsCyclic (QuaternionGroup 1)
apply isCyclic_of_orderOf_eq_card
case hx
n : ℕ
⊢ orderOf ?x = 4

case x
n : ℕ
⊢ QuaternionGroup 1

case x
n : ℕ
⊢ QuaternionGroup 1

case x
n : ℕ
⊢ QuaternionGroup 1
case hx
n : ℕ
⊢ orderOf ?x = Fintype.card (QuaternionGroup 1)

case x
n : ℕ
⊢ QuaternionGroup 1
rw [card, mul_one]
no goals
case hx
n : ℕ
⊢ orderOf ?x = 4

case x
n : ℕ
⊢ QuaternionGroup 1

case x
n : ℕ
⊢ QuaternionGroup 1

case x
n : ℕ
⊢ QuaternionGroup 1
exact orderOf_xa 0