-- Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
theorem exponent : Monoid.exponent (DihedralGroup n) = lcm n 2

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

Tactic:
rintro (m | m)

Result:
case inr.a.a.r
n : ℕ
hn : NeZero n
m : ZMod n
⊢ r m ^ lcm n 2 = 1

case inr.a.a.sr
n : ℕ
hn : NeZero n
m : ZMod n
⊢ sr m ^ lcm n 2 = 1

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

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

Result:
no goals

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

Tactic:
exact orderOf_r_one.symm

Result:
no goals

Proof state:
case inl

⊢ Monoid.exponent (DihedralGroup 0) = lcm 0 2

Tactic:
exact Monoid.exponent_eq_zero_of_order_zero orderOf_r_one

Result:
no goals

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

Tactic:
apply lcm_dvd

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

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

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

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

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

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

Tactic:
exact (orderOf_sr 0).symm

Result:
no goals

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

Tactic:
convert Monoid.order_dvd_exponent (r (1 : ZMod n))

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

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

Tactic:
apply Monoid.exponent_dvd_of_forall_pow_eq_one

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

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

Tactic:
convert Monoid.order_dvd_exponent (sr (0 : ZMod n))

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

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

Tactic:
rcases eq_zero_or_neZero n with (rfl | hn)

Result:
case inl

⊢ Monoid.exponent (DihedralGroup 0) = lcm 0 2

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

Proof state:
case inr.a.a.sr
n : ℕ
hn : NeZero n
m : ZMod n
⊢ sr m ^ lcm n 2 = 1

Tactic:
rw [← orderOf_dvd_iff_pow_eq_one, orderOf_sr]

Result:
case inr.a.a.sr
n : ℕ
hn : NeZero n
m : ZMod n
⊢ 2 ∣ lcm n 2

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

Tactic:
apply Nat.dvd_antisymm

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

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

Proof state:
case inr.a.a.sr
n : ℕ
hn : NeZero n
m : ZMod n
⊢ 2 ∣ lcm n 2

Tactic:
exact dvd_lcm_right n 2

Result:
no goals

Proof state:
case inr.a.a.r
n : ℕ
hn : NeZero n
m : ZMod n
⊢ r m ^ lcm n 2 = 1

Tactic:
rw [← orderOf_dvd_iff_pow_eq_one, orderOf_r]

Result:
case inr.a.a.r
n : ℕ
hn : NeZero n
m : ZMod n
⊢ n / n.gcd m.val ∣ lcm n 2