-- Mathlib/GroupTheory/SpecificGroups/Quaternion.lean
theorem exponent : Monoid.exponent (QuaternionGroup n) = 2 * lcm n 2

Proof state:
case h.e'_3
n : ℕ
hn : NeZero n
⊢ 2 * n = orderOf (a 1)

Tactic:
exact orderOf_a_one.symm

Result:
no goals

Proof state:
n : ℕ
⊢ Monoid.exponent (QuaternionGroup n) = 2 * lcm n 2

Tactic:
rw [← normalize_eq 2, ← lcm_mul_left, normalize_eq]

Result:
n : ℕ
⊢ Monoid.exponent (QuaternionGroup n) = lcm (2 * n) (2 * 2)

Proof state:
case inr.a.a.xa
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ xa m ^ lcm (2 * n) 4 = 1

Tactic:
rw [← orderOf_dvd_iff_pow_eq_one, orderOf_xa]

Result:
case inr.a.a.xa
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ 4 ∣ lcm (2 * n) 4

Proof state:
case inr.a.a
n : ℕ
hn : NeZero n
⊢ ∀ (g : QuaternionGroup n), g ^ lcm (2 * n) 4 = 1

Tactic:
rintro (m | m)

Result:
case inr.a.a.a
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ a m ^ lcm (2 * n) 4 = 1

case inr.a.a.xa
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ xa m ^ lcm (2 * n) 4 = 1

Proof state:
case inr
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (QuaternionGroup n) = lcm (2 * n) 4

Tactic:
apply Nat.dvd_antisymm

Result:
case inr.a
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (QuaternionGroup n) ∣ lcm (2 * n) 4

case inr.a
n : ℕ
hn : NeZero n
⊢ lcm (2 * n) 4 ∣ Monoid.exponent (QuaternionGroup n)

Proof state:
n : ℕ
⊢ Monoid.exponent (QuaternionGroup n) = lcm (2 * n) (2 * 2)

Tactic:
norm_num

Result:
n : ℕ
⊢ Monoid.exponent (QuaternionGroup n) = lcm (2 * n) 4

Proof state:
case inr.a.hcb
n : ℕ
hn : NeZero n
⊢ 4 ∣ Monoid.exponent (QuaternionGroup n)

Tactic:
convert Monoid.order_dvd_exponent (xa (0 : ZMod (2 * n)))

Result:
case h.e'_3
n : ℕ
hn : NeZero n
⊢ 4 = orderOf (xa 0)

Proof state:
case inl

⊢ Monoid.exponent (QuaternionGroup 0) = 0

Tactic:
exact Monoid.exponent_eq_zero_of_order_zero orderOf_a_one

Result:
no goals

Proof state:
case inr.a.a.a
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ a m ^ lcm (2 * n) 4 = 1

Tactic:
rw [← orderOf_dvd_iff_pow_eq_one, orderOf_a]

Result:
case inr.a.a.a
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ 2 * n / (2 * n).gcd m.val ∣ lcm (2 * n) 4

Proof state:
n : ℕ
⊢ Monoid.exponent (QuaternionGroup n) = lcm (2 * n) 4

Tactic:
rcases eq_zero_or_neZero n with hn | hn

Result:
case inl
n : ℕ
hn : n = 0
⊢ Monoid.exponent (QuaternionGroup n) = lcm (2 * n) 4

case inr
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (QuaternionGroup n) = lcm (2 * n) 4

Proof state:
case inr.a
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (QuaternionGroup n) ∣ lcm (2 * n) 4

Tactic:
apply Monoid.exponent_dvd_of_forall_pow_eq_one

Result:
case inr.a.a
n : ℕ
hn : NeZero n
⊢ ∀ (g : QuaternionGroup n), g ^ lcm (2 * n) 4 = 1

Proof state:
case inr.a.a.a
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ 2 * n = 2 * n / (2 * n).gcd m.val * gcd (2 * n) m.val

Tactic:
exact (Nat.div_mul_cancel (Nat.gcd_dvd_left (2 * n) m.val)).symm

Result:
no goals

Proof state:
case h.e'_3
n : ℕ
hn : NeZero n
⊢ 4 = orderOf (xa 0)

Tactic:
exact (orderOf_xa 0).symm

Result:
no goals

Proof state:
case inl

⊢ Monoid.exponent (QuaternionGroup 0) = lcm (2 * 0) 4

Tactic:
simp only [lcm_zero_left, mul_zero]

Result:
case inl

⊢ Monoid.exponent (QuaternionGroup 0) = 0

Proof state:
case inr.a.a.xa
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ 4 ∣ lcm (2 * n) 4

Tactic:
exact dvd_lcm_right (2 * n) 4

Result:
no goals

Proof state:
case inl
n : ℕ
hn : n = 0
⊢ Monoid.exponent (QuaternionGroup n) = lcm (2 * n) 4

Tactic:
subst hn

Result:
case inl

⊢ Monoid.exponent (QuaternionGroup 0) = lcm (2 * 0) 4

Proof state:
case inr.a.a.a
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ 2 * n / (2 * n).gcd m.val ∣ lcm (2 * n) 4

Tactic:
refine Nat.dvd_trans ⟨gcd (2 * n) m.val, ?_⟩ (dvd_lcm_left (2 * n) 4)

Result:
case inr.a.a.a
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ 2 * n = 2 * n / (2 * n).gcd m.val * gcd (2 * n) m.val

Proof state:
case inr.a
n : ℕ
hn : NeZero n
⊢ lcm (2 * n) 4 ∣ Monoid.exponent (QuaternionGroup n)

Tactic:
apply lcm_dvd

Result:
case inr.a.hab
n : ℕ
hn : NeZero n
⊢ 2 * n ∣ Monoid.exponent (QuaternionGroup n)

case inr.a.hcb
n : ℕ
hn : NeZero n
⊢ 4 ∣ Monoid.exponent (QuaternionGroup n)

Proof state:
case inr.a.hab
n : ℕ
hn : NeZero n
⊢ 2 * n ∣ Monoid.exponent (QuaternionGroup n)

Tactic:
convert Monoid.order_dvd_exponent (a 1)

Result:
case h.e'_3
n : ℕ
hn : NeZero n
⊢ 2 * n = orderOf (a 1)