[GOAL]
n : ℕ
⊢ ∀ (a b c : DihedralGroup n), a * b * c = a * (b * c)
[PROOFSTEP]
rintro (a | a) (b | b) (c | c)
[GOAL]
case r.r.r
n : ℕ
a b c : ZMod n
⊢ r a * r b * r c = r a * (r b * r c)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case r.r.sr
n : ℕ
a b c : ZMod n
⊢ r a * r b * sr c = r a * (r b * sr c)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case r.sr.r
n : ℕ
a b c : ZMod n
⊢ r a * sr b * r c = r a * (sr b * r c)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case r.sr.sr
n : ℕ
a b c : ZMod n
⊢ r a * sr b * sr c = r a * (sr b * sr c)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case sr.r.r
n : ℕ
a b c : ZMod n
⊢ sr a * r b * r c = sr a * (r b * r c)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case sr.r.sr
n : ℕ
a b c : ZMod n
⊢ sr a * r b * sr c = sr a * (r b * sr c)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case sr.sr.r
n : ℕ
a b c : ZMod n
⊢ sr a * sr b * r c = sr a * (sr b * r c)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case sr.sr.sr
n : ℕ
a b c : ZMod n
⊢ sr a * sr b * sr c = sr a * (sr b * sr c)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case r.r.r
n : ℕ
a b c : ZMod n
⊢ r (a + b + c) = r (a + (b + c))
[PROOFSTEP]
ring_nf
[GOAL]
case r.r.sr
n : ℕ
a b c : ZMod n
⊢ sr (c - (a + b)) = sr (c - b - a)
[PROOFSTEP]
ring_nf
[GOAL]
case r.sr.r
n : ℕ
a b c : ZMod n
⊢ sr (b - a + c) = sr (b + c - a)
[PROOFSTEP]
ring_nf
[GOAL]
case r.sr.sr
n : ℕ
a b c : ZMod n
⊢ r (c - (b - a)) = r (a + (c - b))
[PROOFSTEP]
ring_nf
[GOAL]
case sr.r.r
n : ℕ
a b c : ZMod n
⊢ sr (a + b + c) = sr (a + (b + c))
[PROOFSTEP]
ring_nf
[GOAL]
case sr.r.sr
n : ℕ
a b c : ZMod n
⊢ r (c - (a + b)) = r (c - b - a)
[PROOFSTEP]
ring_nf
[GOAL]
case sr.sr.r
n : ℕ
a b c : ZMod n
⊢ r (b - a + c) = r (b + c - a)
[PROOFSTEP]
ring_nf
[GOAL]
case sr.sr.sr
n : ℕ
a b c : ZMod n
⊢ sr (c - (b - a)) = sr (a + (c - b))
[PROOFSTEP]
ring_nf
[GOAL]
n : ℕ
⊢ ∀ (a : DihedralGroup n), 1 * a = a
[PROOFSTEP]
rintro (a | a)
[GOAL]
case r
n : ℕ
a : ZMod n
⊢ 1 * r a = r a
case sr n : ℕ a : ZMod n ⊢ 1 * sr a = sr a
[PROOFSTEP]
exact congr_arg r (zero_add a)
[GOAL]
case sr
n : ℕ
a : ZMod n
⊢ 1 * sr a = sr a
[PROOFSTEP]
exact congr_arg sr (sub_zero a)
[GOAL]
n : ℕ
⊢ ∀ (a : DihedralGroup n), a * 1 = a
[PROOFSTEP]
rintro (a | a)
[GOAL]
case r
n : ℕ
a : ZMod n
⊢ r a * 1 = r a
case sr n : ℕ a : ZMod n ⊢ sr a * 1 = sr a
[PROOFSTEP]
exact congr_arg r (add_zero a)
[GOAL]
case sr
n : ℕ
a : ZMod n
⊢ sr a * 1 = sr a
[PROOFSTEP]
exact congr_arg sr (add_zero a)
[GOAL]
n : ℕ
⊢ ∀ (a : DihedralGroup n), a⁻¹ * a = 1
[PROOFSTEP]
rintro (a | a)
[GOAL]
case r
n : ℕ
a : ZMod n
⊢ (r a)⁻¹ * r a = 1
case sr n : ℕ a : ZMod n ⊢ (sr a)⁻¹ * sr a = 1
[PROOFSTEP]
exact congr_arg r (neg_add_self a)
[GOAL]
case sr
n : ℕ
a : ZMod n
⊢ (sr a)⁻¹ * sr a = 1
[PROOFSTEP]
exact congr_arg r (sub_self a)
[GOAL]
n : ℕ
⊢ Function.LeftInverse
    (fun i =>
      match i with
      | r j => Sum.inl j
      | sr j => Sum.inr j)
    fun i =>
    match i with
    | Sum.inl j => r j
    | Sum.inr j => sr j
[PROOFSTEP]
rintro (x | x)
[GOAL]
case inl
n : ℕ
x : ZMod n
⊢ (fun i =>
        match i with
        | r j => Sum.inl j
        | sr j => Sum.inr j)
      ((fun i =>
          match i with
          | Sum.inl j => r j
          | Sum.inr j => sr j)
        (Sum.inl x)) =
    Sum.inl x
[PROOFSTEP]
rfl
[GOAL]
case inr
n : ℕ
x : ZMod n
⊢ (fun i =>
        match i with
        | r j => Sum.inl j
        | sr j => Sum.inr j)
      ((fun i =>
          match i with
          | Sum.inl j => r j
          | Sum.inr j => sr j)
        (Sum.inr x)) =
    Sum.inr x
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ Function.RightInverse
    (fun i =>
      match i with
      | r j => Sum.inl j
      | sr j => Sum.inr j)
    fun i =>
    match i with
    | Sum.inl j => r j
    | Sum.inr j => sr j
[PROOFSTEP]
rintro (x | x)
[GOAL]
case r
n : ℕ
x : ZMod n
⊢ (fun i =>
        match i with
        | Sum.inl j => r j
        | Sum.inr j => sr j)
      ((fun i =>
          match i with
          | r j => Sum.inl j
          | sr j => Sum.inr j)
        (r x)) =
    r x
[PROOFSTEP]
rfl
[GOAL]
case sr
n : ℕ
x : ZMod n
⊢ (fun i =>
        match i with
        | Sum.inl j => r j
        | Sum.inr j => sr j)
      ((fun i =>
          match i with
          | r j => Sum.inl j
          | sr j => Sum.inr j)
        (sr x)) =
    sr x
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ r 0 ≠ sr 0
[PROOFSTEP]
simp_rw [ne_eq]
[GOAL]
n : ℕ
inst✝ : NeZero n
⊢ Fintype.card (DihedralGroup n) = 2 * n
[PROOFSTEP]
rw [← Fintype.card_eq.mpr ⟨fintypeHelper⟩, Fintype.card_sum, ZMod.card, two_mul]
[GOAL]
n : ℕ
⊢ Nat.card (DihedralGroup n) = 2 * n
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ Nat.card (DihedralGroup Nat.zero) = 2 * Nat.zero
[PROOFSTEP]
rw [Nat.card_eq_zero_of_infinite]
[GOAL]
case succ
n✝ : ℕ
⊢ Nat.card (DihedralGroup (Nat.succ n✝)) = 2 * Nat.succ n✝
[PROOFSTEP]
rw [Nat.card_eq_fintype_card, card]
[GOAL]
n k : ℕ
⊢ r 1 ^ k = r ↑k
[PROOFSTEP]
induction' k with k IH
[GOAL]
case zero
n : ℕ
⊢ r 1 ^ Nat.zero = r ↑Nat.zero
[PROOFSTEP]
rw [Nat.cast_zero]
[GOAL]
case zero
n : ℕ
⊢ r 1 ^ Nat.zero = r 0
[PROOFSTEP]
rfl
[GOAL]
case succ
n k : ℕ
IH : r 1 ^ k = r ↑k
⊢ r 1 ^ Nat.succ k = r ↑(Nat.succ k)
[PROOFSTEP]
rw [pow_succ, IH, r_mul_r]
[GOAL]
case succ
n k : ℕ
IH : r 1 ^ k = r ↑k
⊢ r (1 + ↑k) = r ↑(Nat.succ k)
[PROOFSTEP]
congr 1
[GOAL]
case succ.e_a
n k : ℕ
IH : r 1 ^ k = r ↑k
⊢ 1 + ↑k = ↑(Nat.succ k)
[PROOFSTEP]
norm_cast
[GOAL]
case succ.e_a
n k : ℕ
IH : r 1 ^ k = r ↑k
⊢ ↑(1 + k) = ↑(Nat.succ k)
[PROOFSTEP]
rw [Nat.one_add]
[GOAL]
n : ℕ
⊢ r 1 ^ n = 1
[PROOFSTEP]
rw [r_one_pow, one_def]
[GOAL]
n : ℕ
⊢ r ↑n = r 0
[PROOFSTEP]
congr 1
[GOAL]
case e_a
n : ℕ
⊢ ↑n = 0
[PROOFSTEP]
exact ZMod.nat_cast_self _
[GOAL]
n : ℕ
i : ZMod n
⊢ sr i * sr i = 1
[PROOFSTEP]
rw [sr_mul_sr, sub_self, one_def]
[GOAL]
n : ℕ
i : ZMod n
⊢ orderOf (sr i) = 2
[PROOFSTEP]
apply orderOf_eq_prime
[GOAL]
case hg
n : ℕ
i : ZMod n
⊢ sr i ^ 2 = 1
[PROOFSTEP]
rw [sq, sr_mul_self]
[GOAL]
case hg1
n : ℕ
i : ZMod n
⊢ sr i ≠ 1
[PROOFSTEP]
revert n
[GOAL]
case hg1
⊢ ∀ {n : ℕ} (i : ZMod n), sr i ≠ 1
[PROOFSTEP]
simp_rw [one_def, ne_eq, forall_const]
[GOAL]
n : ℕ
⊢ orderOf (r 1) = n
[PROOFSTEP]
rcases eq_zero_or_neZero n with (rfl | hn)
[GOAL]
case inl
⊢ orderOf (r 1) = 0
[PROOFSTEP]
rw [orderOf_eq_zero_iff']
[GOAL]
case inl
⊢ ∀ (n : ℕ), 0 < n → r 1 ^ n ≠ 1
[PROOFSTEP]
intro n hn
[GOAL]
case inl
n : ℕ
hn : 0 < n
⊢ r 1 ^ n ≠ 1
[PROOFSTEP]
rw [r_one_pow, one_def]
[GOAL]
case inl
n : ℕ
hn : 0 < n
⊢ r ↑n ≠ r 0
[PROOFSTEP]
apply mt r.inj
[GOAL]
case inl
n : ℕ
hn : 0 < n
⊢ ¬↑n = 0
[PROOFSTEP]
simpa using hn.ne'
[GOAL]
case inr
n : ℕ
hn : NeZero n
⊢ orderOf (r 1) = n
[PROOFSTEP]
apply (Nat.le_of_dvd (NeZero.pos n) <| orderOf_dvd_of_pow_eq_one <| @r_one_pow_n n).lt_or_eq.resolve_left
[GOAL]
case inr
n : ℕ
hn : NeZero n
⊢ ¬orderOf (r 1) < n
[PROOFSTEP]
intro h
[GOAL]
case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
⊢ False
[PROOFSTEP]
have h1 : (r 1 : DihedralGroup n) ^ orderOf (r 1) = 1 := pow_orderOf_eq_one _
[GOAL]
case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
h1 : r 1 ^ orderOf (r 1) = 1
⊢ False
[PROOFSTEP]
rw [r_one_pow] at h1 
[GOAL]
case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
h1 : r ↑(orderOf (r 1)) = 1
⊢ False
[PROOFSTEP]
injection h1 with h2
[GOAL]
case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
h2 : ↑(orderOf (r 1)) = 0
⊢ False
[PROOFSTEP]
rw [← ZMod.val_eq_zero, ZMod.val_nat_cast, Nat.mod_eq_of_lt h] at h2 
[GOAL]
case inr
n : ℕ
hn : NeZero n
h : orderOf (r 1) < n
h2 : orderOf (r 1) = 0
⊢ False
[PROOFSTEP]
exact absurd h2.symm (orderOf_pos _).ne
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod n
⊢ orderOf (r i) = n / Nat.gcd n (ZMod.val i)
[PROOFSTEP]
conv_lhs => rw [← ZMod.nat_cast_zmod_val i]
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod n
| orderOf (r i)
[PROOFSTEP]
rw [← ZMod.nat_cast_zmod_val i]
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod n
| orderOf (r i)
[PROOFSTEP]
rw [← ZMod.nat_cast_zmod_val i]
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod n
| orderOf (r i)
[PROOFSTEP]
rw [← ZMod.nat_cast_zmod_val i]
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod n
⊢ orderOf (r ↑(ZMod.val i)) = n / Nat.gcd n (ZMod.val i)
[PROOFSTEP]
rw [← r_one_pow, orderOf_pow, orderOf_r_one]
[GOAL]
n : ℕ
⊢ Monoid.exponent (DihedralGroup n) = lcm n 2
[PROOFSTEP]
rcases eq_zero_or_neZero n with (rfl | hn)
[GOAL]
case inl
⊢ Monoid.exponent (DihedralGroup 0) = lcm 0 2
[PROOFSTEP]
exact Monoid.exponent_eq_zero_of_order_zero orderOf_r_one
[GOAL]
case inr
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (DihedralGroup n) = lcm n 2
[PROOFSTEP]
apply Nat.dvd_antisymm
[GOAL]
case inr.a
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (DihedralGroup n) ∣ lcm n 2
[PROOFSTEP]
apply Monoid.exponent_dvd_of_forall_pow_eq_one
[GOAL]
case inr.a.hG
n : ℕ
hn : NeZero n
⊢ ∀ (g : DihedralGroup n), g ^ lcm n 2 = 1
[PROOFSTEP]
rintro (m | m)
[GOAL]
case inr.a.hG.r
n : ℕ
hn : NeZero n
m : ZMod n
⊢ r m ^ lcm n 2 = 1
[PROOFSTEP]
rw [← orderOf_dvd_iff_pow_eq_one, orderOf_r]
[GOAL]
case inr.a.hG.r
n : ℕ
hn : NeZero n
m : ZMod n
⊢ n / Nat.gcd n (ZMod.val m) ∣ lcm n 2
[PROOFSTEP]
refine' Nat.dvd_trans ⟨gcd n m.val, _⟩ (dvd_lcm_left n 2)
[GOAL]
case inr.a.hG.r
n : ℕ
hn : NeZero n
m : ZMod n
⊢ n = n / Nat.gcd n (ZMod.val m) * gcd n (ZMod.val m)
[PROOFSTEP]
exact (Nat.div_mul_cancel (Nat.gcd_dvd_left n m.val)).symm
[GOAL]
case inr.a.hG.sr
n : ℕ
hn : NeZero n
m : ZMod n
⊢ sr m ^ lcm n 2 = 1
[PROOFSTEP]
rw [← orderOf_dvd_iff_pow_eq_one, orderOf_sr]
[GOAL]
case inr.a.hG.sr
n : ℕ
hn : NeZero n
m : ZMod n
⊢ 2 ∣ lcm n 2
[PROOFSTEP]
exact dvd_lcm_right n 2
[GOAL]
case inr.a
n : ℕ
hn : NeZero n
⊢ lcm n 2 ∣ Monoid.exponent (DihedralGroup n)
[PROOFSTEP]
apply lcm_dvd
[GOAL]
case inr.a.hab
n : ℕ
hn : NeZero n
⊢ n ∣ Monoid.exponent (DihedralGroup n)
[PROOFSTEP]
convert Monoid.order_dvd_exponent (r (1 : ZMod n))
[GOAL]
case h.e'_3
n : ℕ
hn : NeZero n
⊢ n = orderOf (r 1)
[PROOFSTEP]
exact orderOf_r_one.symm
[GOAL]
case inr.a.hcb
n : ℕ
hn : NeZero n
⊢ 2 ∣ Monoid.exponent (DihedralGroup n)
[PROOFSTEP]
convert Monoid.order_dvd_exponent (sr (0 : ZMod n))
[GOAL]
case h.e'_3
n : ℕ
hn : NeZero n
⊢ 2 = orderOf (sr 0)
[PROOFSTEP]
exact (orderOf_sr 0).symm
[GOAL]
n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 (_ : Nat.coprime 2 n)
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h : Commute (r i, sr j).fst (r i, sr j).snd
⊢ (fun x =>
        match x with
        | Sum.inl i => { val := (sr i, r 0), property := (_ : sr (i + 0) = sr (i - 0)) }
        | Sum.inr (Sum.inl j) => { val := (r 0, sr j), property := (_ : sr (j - 0) = sr (j + 0)) }
        | Sum.inr (Sum.inr (Sum.inl k)) =>
          { val := (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)),
            property :=
              (_ :
                (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).fst * (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).snd =
                  (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).fst * (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).snd) }
        | Sum.inr (Sum.inr (Sum.inr (i, j))) => { val := (r i, r j), property := (_ : r (i + j) = r (j + i)) })
      ((fun x =>
          match x with
          | { val := (sr i, r a), property := property } => Sum.inl i
          | { val := (r a, sr j), property := property } => Sum.inr (Sum.inl j)
          | { val := (sr i, sr j), property := property } => Sum.inr (Sum.inr (Sum.inl (i + j)))
          | { val := (r i, r j), property := property } => Sum.inr (Sum.inr (Sum.inr (i, j))))
        { val := (r i, sr j), property := h }) =
    { val := (r i, sr j), property := h }
[PROOFSTEP]
simpa [sub_eq_add_neg, neg_eq_iff_add_eq_zero, hu, eq_comm (a := i) (b := 0)] using h.eq
[GOAL]
n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 (_ : Nat.coprime 2 n)
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h : Commute (sr i, r j).fst (sr i, r j).snd
⊢ (fun x =>
        match x with
        | Sum.inl i => { val := (sr i, r 0), property := (_ : sr (i + 0) = sr (i - 0)) }
        | Sum.inr (Sum.inl j) => { val := (r 0, sr j), property := (_ : sr (j - 0) = sr (j + 0)) }
        | Sum.inr (Sum.inr (Sum.inl k)) =>
          { val := (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)),
            property :=
              (_ :
                (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).fst * (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).snd =
                  (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).fst * (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).snd) }
        | Sum.inr (Sum.inr (Sum.inr (i, j))) => { val := (r i, r j), property := (_ : r (i + j) = r (j + i)) })
      ((fun x =>
          match x with
          | { val := (sr i, r a), property := property } => Sum.inl i
          | { val := (r a, sr j), property := property } => Sum.inr (Sum.inl j)
          | { val := (sr i, sr j), property := property } => Sum.inr (Sum.inr (Sum.inl (i + j)))
          | { val := (r i, r j), property := property } => Sum.inr (Sum.inr (Sum.inr (i, j))))
        { val := (sr i, r j), property := h }) =
    { val := (sr i, r j), property := h }
[PROOFSTEP]
simpa [sub_eq_add_neg, eq_neg_iff_add_eq_zero, hu, eq_comm (a := j) (b := 0)] using h.eq
[GOAL]
n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 (_ : Nat.coprime 2 n)
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h : Commute (sr i, sr j).fst (sr i, sr j).snd
⊢ (fun x =>
        match x with
        | Sum.inl i => { val := (sr i, r 0), property := (_ : sr (i + 0) = sr (i - 0)) }
        | Sum.inr (Sum.inl j) => { val := (r 0, sr j), property := (_ : sr (j - 0) = sr (j + 0)) }
        | Sum.inr (Sum.inr (Sum.inl k)) =>
          { val := (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)),
            property :=
              (_ :
                (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).fst * (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).snd =
                  (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).fst * (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).snd) }
        | Sum.inr (Sum.inr (Sum.inr (i, j))) => { val := (r i, r j), property := (_ : r (i + j) = r (j + i)) })
      ((fun x =>
          match x with
          | { val := (sr i, r a), property := property } => Sum.inl i
          | { val := (r a, sr j), property := property } => Sum.inr (Sum.inl j)
          | { val := (sr i, sr j), property := property } => Sum.inr (Sum.inr (Sum.inl (i + j)))
          | { val := (r i, r j), property := property } => Sum.inr (Sum.inr (Sum.inr (i, j))))
        { val := (sr i, sr j), property := h }) =
    { val := (sr i, sr j), property := h }
[PROOFSTEP]
replace h := r.inj h
[GOAL]
n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 (_ : Nat.coprime 2 n)
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h✝ : Commute (sr i, sr j).fst (sr i, sr j).snd
h : j - i = i - j
⊢ (fun x =>
        match x with
        | Sum.inl i => { val := (sr i, r 0), property := (_ : sr (i + 0) = sr (i - 0)) }
        | Sum.inr (Sum.inl j) => { val := (r 0, sr j), property := (_ : sr (j - 0) = sr (j + 0)) }
        | Sum.inr (Sum.inr (Sum.inl k)) =>
          { val := (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)),
            property :=
              (_ :
                (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).fst * (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).snd =
                  (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).fst * (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).snd) }
        | Sum.inr (Sum.inr (Sum.inr (i, j))) => { val := (r i, r j), property := (_ : r (i + j) = r (j + i)) })
      ((fun x =>
          match x with
          | { val := (sr i, r a), property := property } => Sum.inl i
          | { val := (r a, sr j), property := property } => Sum.inr (Sum.inl j)
          | { val := (sr i, sr j), property := property } => Sum.inr (Sum.inr (Sum.inl (i + j)))
          | { val := (r i, r j), property := property } => Sum.inr (Sum.inr (Sum.inr (i, j))))
        { val := (sr i, sr j), property := h✝ }) =
    { val := (sr i, sr j), property := h✝ }
[PROOFSTEP]
rw [← neg_sub, neg_eq_iff_add_eq_zero, hu, sub_eq_zero] at h 
[GOAL]
n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 (_ : Nat.coprime 2 n)
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h✝ : Commute (sr i, sr j).fst (sr i, sr j).snd
h : i = j
⊢ (fun x =>
        match x with
        | Sum.inl i => { val := (sr i, r 0), property := (_ : sr (i + 0) = sr (i - 0)) }
        | Sum.inr (Sum.inl j) => { val := (r 0, sr j), property := (_ : sr (j - 0) = sr (j + 0)) }
        | Sum.inr (Sum.inr (Sum.inl k)) =>
          { val := (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)),
            property :=
              (_ :
                (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).fst * (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).snd =
                  (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).fst * (sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)).snd) }
        | Sum.inr (Sum.inr (Sum.inr (i, j))) => { val := (r i, r j), property := (_ : r (i + j) = r (j + i)) })
      ((fun x =>
          match x with
          | { val := (sr i, r a), property := property } => Sum.inl i
          | { val := (r a, sr j), property := property } => Sum.inr (Sum.inl j)
          | { val := (sr i, sr j), property := property } => Sum.inr (Sum.inr (Sum.inl (i + j)))
          | { val := (r i, r j), property := property } => Sum.inr (Sum.inr (Sum.inr (i, j))))
        { val := (sr i, sr j), property := h✝ }) =
    { val := (sr i, sr j), property := h✝ }
[PROOFSTEP]
rw [Subtype.ext_iff, Prod.ext_iff, sr.injEq, sr.injEq, h, and_self, ← two_mul]
[GOAL]
n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 (_ : Nat.coprime 2 n)
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h✝ : Commute (sr i, sr j).fst (sr i, sr j).snd
h : i = j
⊢ ↑u⁻¹ * (2 * j) = j
[PROOFSTEP]
exact u.inv_mul_cancel_left j
[GOAL]
n : ℕ
hn : Odd n
⊢ Nat.card { p // Commute p.fst p.snd } = n * (n + 3)
[PROOFSTEP]
have hn' : NeZero n := ⟨hn.pos.ne'⟩
[GOAL]
n : ℕ
hn : Odd n
hn' : NeZero n
⊢ Nat.card { p // Commute p.fst p.snd } = n * (n + 3)
[PROOFSTEP]
simp_rw [Nat.card_congr (OddCommuteEquiv hn), Nat.card_sum, Nat.card_prod, Nat.card_zmod]
[GOAL]
n : ℕ
hn : Odd n
hn' : NeZero n
⊢ n + (n + (n + n * n)) = n * (n + 3)
[PROOFSTEP]
ring
[GOAL]
n : ℕ
hn : Odd n
⊢ Nat.card (ConjClasses (DihedralGroup n)) = (n + 3) / 2
[PROOFSTEP]
rw [← Nat.mul_div_mul_left _ 2 hn.pos, ← card_commute_odd hn, mul_comm, card_comm_eq_card_conjClasses_mul_card,
  nat_card, Nat.mul_div_left _ (mul_pos two_pos hn.pos)]
