case inl
n : ℕ
hn : n = 0
⊢ orderOf (a 1) = 2 * n

case inr
n : ℕ
hn : NeZero n
⊢ orderOf (a 1) = 2 * n
n : ℕ
⊢ orderOf (a 1) = 2 * n
cases' eq_zero_or_neZero n with hn hn
case inr
n : ℕ
hn : NeZero n
⊢ ¬orderOf (a 1) < 2 * n
case inr
n : ℕ
hn : NeZero n
⊢ orderOf (a 1) = 2 * n
apply (Nat.le_of_dvd
  (NeZero.pos _) (orderOf_dvd_of_pow_eq_one (@a_one_pow_n n))).lt_or_eq.resolve_left
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
⊢ False
case inr
n : ℕ
hn : NeZero n
⊢ ¬orderOf (a 1) < 2 * n
intro h
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h1 : a 1 ^ orderOf (a 1) = 1
⊢ False
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
⊢ False
have h1 : (a 1 : QuaternionGroup n) ^ orderOf (a 1) = 1 := pow_orderOf_eq_one _
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h1 : a ↑(orderOf (a 1)) = 1
⊢ False
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h1 : a 1 ^ orderOf (a 1) = 1
⊢ False
rw [a_one_pow] at h1
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h2 : ↑(orderOf (a 1)) = 0
⊢ False
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h1 : a ↑(orderOf (a 1)) = 1
⊢ False
injection h1 with h2
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h2 : orderOf (a 1) = 0
⊢ False
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h2 : ↑(orderOf (a 1)) = 0
⊢ False
rw [← ZMod.val_eq_zero, ZMod.val_nat_cast, Nat.mod_eq_of_lt h] at h2
no goals
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h2 : orderOf (a 1) = 0
⊢ False
exact absurd h2.symm (orderOf_pos _).ne
case inl

⊢ orderOf (a 1) = 2 * 0
case inl
n : ℕ
hn : n = 0
⊢ orderOf (a 1) = 2 * n
subst hn
case inl

⊢ ∀ (n : ℕ), 0 < n → QuaternionGroup.a 1 ^ n ≠ 1
case inl

⊢ orderOf (a 1) = 2 * 0
simp_rw [MulZeroClass.mul_zero, orderOf_eq_zero_iff']
case inl
n : ℕ
h : 0 < n
⊢ a 1 ^ n ≠ 1
case inl

⊢ ∀ (n : ℕ), 0 < n → QuaternionGroup.a 1 ^ n ≠ 1
intro n h
case inl
n : ℕ
h : 0 < n
⊢ a ↑n ≠ a 0
case inl
n : ℕ
h : 0 < n
⊢ a 1 ^ n ≠ 1
rw [one_def, a_one_pow]
case inl
n : ℕ
h : 0 < n
⊢ ¬↑n = 0
case inl
n : ℕ
h : 0 < n
⊢ a ↑n ≠ a 0
apply mt a.inj
case inl
n : ℕ
h : 0 < n
this : CharZero (ZMod (2 * 0))
⊢ ¬↑n = 0
case inl
n : ℕ
h : 0 < n
⊢ ¬↑n = 0
haveI : CharZero (ZMod (2 * 0)) := ZMod.charZero
no goals
case inl
n : ℕ
h : 0 < n
this : CharZero (ZMod (2 * 0))
⊢ ¬↑n = 0
simpa using h.ne'