[GOAL]
n : ℕ
⊢ ∀ (a b c : QuaternionGroup n), a * b * c = a * (b * c)
[PROOFSTEP]
rintro (i | i) (j | j) (k | k)
[GOAL]
case a.a.a
n : ℕ
i j k : ZMod (2 * n)
⊢ a i * a j * a k = a i * (a j * a k)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case a.a.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ a i * a j * xa k = a i * (a j * xa k)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case a.xa.a
n : ℕ
i j k : ZMod (2 * n)
⊢ a i * xa j * a k = a i * (xa j * a k)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case a.xa.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ a i * xa j * xa k = a i * (xa j * xa k)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case xa.a.a
n : ℕ
i j k : ZMod (2 * n)
⊢ xa i * a j * a k = xa i * (a j * a k)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case xa.a.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ xa i * a j * xa k = xa i * (a j * xa k)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case xa.xa.a
n : ℕ
i j k : ZMod (2 * n)
⊢ xa i * xa j * a k = xa i * (xa j * a k)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case xa.xa.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ xa i * xa j * xa k = xa i * (xa j * xa k)
[PROOFSTEP]
simp only [(· * ·), mul]
[GOAL]
case a.a.a
n : ℕ
i j k : ZMod (2 * n)
⊢ a (i + j + k) = a (i + (j + k))
[PROOFSTEP]
ring_nf
[GOAL]
case a.a.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (k - (i + j)) = xa (k - j - i)
[PROOFSTEP]
ring_nf
[GOAL]
case a.xa.a
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (j - i + k) = xa (j + k - i)
[PROOFSTEP]
ring_nf
[GOAL]
case a.xa.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ a (↑n + k - (j - i)) = a (i + (↑n + k - j))
[PROOFSTEP]
ring_nf
[GOAL]
case xa.a.a
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (i + j + k) = xa (i + (j + k))
[PROOFSTEP]
ring_nf
[GOAL]
case xa.a.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ a (↑n + k - (i + j)) = a (↑n + (k - j) - i)
[PROOFSTEP]
ring_nf
[GOAL]
case xa.xa.a
n : ℕ
i j k : ZMod (2 * n)
⊢ a (↑n + j - i + k) = a (↑n + (j + k) - i)
[PROOFSTEP]
ring_nf
[GOAL]
case xa.xa.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (k - (↑n + j - i)) = xa (i + (↑n + k - j))
[PROOFSTEP]
ring_nf
[GOAL]
case xa.xa.xa
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (k + (-↑n - j) + i) = xa (k + (↑n - j) + i)
[PROOFSTEP]
congr
[GOAL]
case xa.xa.xa.e_a.e_a.e_a.e_a
n : ℕ
i j k : ZMod (2 * n)
⊢ -↑n = ↑n
[PROOFSTEP]
calc
  -(n : ZMod (2 * n)) = 0 - n := by rw [zero_sub]
  _ = 2 * n - n := by norm_cast; simp
  _ = n := by ring
[GOAL]
n : ℕ
i j k : ZMod (2 * n)
⊢ -↑n = 0 - ↑n
[PROOFSTEP]
rw [zero_sub]
[GOAL]
n : ℕ
i j k : ZMod (2 * n)
⊢ 0 - ↑n = 2 * ↑n - ↑n
[PROOFSTEP]
norm_cast
[GOAL]
n : ℕ
i j k : ZMod (2 * n)
⊢ ↑(Int.subNatNat 0 n) = ↑(Int.subNatNat (2 * n) n)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
i j k : ZMod (2 * n)
⊢ 2 * ↑n - ↑n = ↑n
[PROOFSTEP]
ring
[GOAL]
n : ℕ
⊢ ∀ (a : QuaternionGroup n), 1 * a = a
[PROOFSTEP]
rintro (i | i)
[GOAL]
case a
n : ℕ
i : ZMod (2 * n)
⊢ 1 * a i = a i
[PROOFSTEP]
exact congr_arg a (zero_add i)
[GOAL]
case xa
n : ℕ
i : ZMod (2 * n)
⊢ 1 * xa i = xa i
[PROOFSTEP]
exact congr_arg xa (sub_zero i)
[GOAL]
n : ℕ
⊢ ∀ (a : QuaternionGroup n), a * 1 = a
[PROOFSTEP]
rintro (i | i)
[GOAL]
case a
n : ℕ
i : ZMod (2 * n)
⊢ a i * 1 = a i
[PROOFSTEP]
exact congr_arg a (add_zero i)
[GOAL]
case xa
n : ℕ
i : ZMod (2 * n)
⊢ xa i * 1 = xa i
[PROOFSTEP]
exact congr_arg xa (add_zero i)
[GOAL]
n : ℕ
⊢ ∀ (a : QuaternionGroup n), a⁻¹ * a = 1
[PROOFSTEP]
rintro (i | i)
[GOAL]
case a
n : ℕ
i : ZMod (2 * n)
⊢ (a i)⁻¹ * a i = 1
[PROOFSTEP]
exact congr_arg a (neg_add_self i)
[GOAL]
case xa
n : ℕ
i : ZMod (2 * n)
⊢ (xa i)⁻¹ * xa i = 1
[PROOFSTEP]
exact congr_arg a (sub_self (n + i))
[GOAL]
n : ℕ
⊢ Function.LeftInverse
    (fun i =>
      match i with
      | a j => Sum.inl j
      | xa j => Sum.inr j)
    fun i =>
    match i with
    | Sum.inl j => a j
    | Sum.inr j => xa j
[PROOFSTEP]
rintro (x | x)
[GOAL]
case inl
n : ℕ
x : ZMod (2 * n)
⊢ (fun i =>
        match i with
        | a j => Sum.inl j
        | xa j => Sum.inr j)
      ((fun i =>
          match i with
          | Sum.inl j => a j
          | Sum.inr j => xa j)
        (Sum.inl x)) =
    Sum.inl x
[PROOFSTEP]
rfl
[GOAL]
case inr
n : ℕ
x : ZMod (2 * n)
⊢ (fun i =>
        match i with
        | a j => Sum.inl j
        | xa j => Sum.inr j)
      ((fun i =>
          match i with
          | Sum.inl j => a j
          | Sum.inr j => xa j)
        (Sum.inr x)) =
    Sum.inr x
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ Function.RightInverse
    (fun i =>
      match i with
      | a j => Sum.inl j
      | xa j => Sum.inr j)
    fun i =>
    match i with
    | Sum.inl j => a j
    | Sum.inr j => xa j
[PROOFSTEP]
rintro (x | x)
[GOAL]
case a
n : ℕ
x : ZMod (2 * n)
⊢ (fun i =>
        match i with
        | Sum.inl j => a j
        | Sum.inr j => xa j)
      ((fun i =>
          match i with
          | a j => Sum.inl j
          | xa j => Sum.inr j)
        (a x)) =
    a x
[PROOFSTEP]
rfl
[GOAL]
case xa
n : ℕ
x : ZMod (2 * n)
⊢ (fun i =>
        match i with
        | Sum.inl j => a j
        | Sum.inr j => xa j)
      ((fun i =>
          match i with
          | a j => Sum.inl j
          | xa j => Sum.inr j)
        (xa x)) =
    xa x
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ Function.LeftInverse
    (fun i =>
      match i with
      | DihedralGroup.r j => a j
      | DihedralGroup.sr j => xa j)
    fun i =>
    match i with
    | a j => DihedralGroup.r j
    | xa j => DihedralGroup.sr j
[PROOFSTEP]
rintro (k | k)
[GOAL]
case a
n : ℕ
k : ZMod (2 * 0)
⊢ (fun i =>
        match i with
        | DihedralGroup.r j => a j
        | DihedralGroup.sr j => xa j)
      ((fun i =>
          match i with
          | a j => DihedralGroup.r j
          | xa j => DihedralGroup.sr j)
        (a k)) =
    a k
[PROOFSTEP]
rfl
[GOAL]
case xa
n : ℕ
k : ZMod (2 * 0)
⊢ (fun i =>
        match i with
        | DihedralGroup.r j => a j
        | DihedralGroup.sr j => xa j)
      ((fun i =>
          match i with
          | a j => DihedralGroup.r j
          | xa j => DihedralGroup.sr j)
        (xa k)) =
    xa k
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ Function.RightInverse
    (fun i =>
      match i with
      | DihedralGroup.r j => a j
      | DihedralGroup.sr j => xa j)
    fun i =>
    match i with
    | a j => DihedralGroup.r j
    | xa j => DihedralGroup.sr j
[PROOFSTEP]
rintro (k | k)
[GOAL]
case r
n : ℕ
k : ZMod 0
⊢ (fun i =>
        match i with
        | a j => DihedralGroup.r j
        | xa j => DihedralGroup.sr j)
      ((fun i =>
          match i with
          | DihedralGroup.r j => a j
          | DihedralGroup.sr j => xa j)
        (DihedralGroup.r k)) =
    DihedralGroup.r k
[PROOFSTEP]
rfl
[GOAL]
case sr
n : ℕ
k : ZMod 0
⊢ (fun i =>
        match i with
        | a j => DihedralGroup.r j
        | xa j => DihedralGroup.sr j)
      ((fun i =>
          match i with
          | DihedralGroup.r j => a j
          | DihedralGroup.sr j => xa j)
        (DihedralGroup.sr k)) =
    DihedralGroup.sr k
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ ∀ (x y : QuaternionGroup 0),
    Equiv.toFun
        {
          toFun := fun i =>
            match i with
            | a j => DihedralGroup.r j
            | xa j => DihedralGroup.sr j,
          invFun := fun i =>
            match i with
            | DihedralGroup.r j => a j
            | DihedralGroup.sr j => xa j,
          left_inv :=
            (_ :
              ∀ (x : QuaternionGroup 0),
                (fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    ((fun i =>
                        match i with
                        | a j => DihedralGroup.r j
                        | xa j => DihedralGroup.sr j)
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DihedralGroup 0),
                (fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    ((fun i =>
                        match i with
                        | DihedralGroup.r j => a j
                        | DihedralGroup.sr j => xa j)
                      x) =
                  x) }
        (x * y) =
      Equiv.toFun
          {
            toFun := fun i =>
              match i with
              | a j => DihedralGroup.r j
              | xa j => DihedralGroup.sr j,
            invFun := fun i =>
              match i with
              | DihedralGroup.r j => a j
              | DihedralGroup.sr j => xa j,
            left_inv :=
              (_ :
                ∀ (x : QuaternionGroup 0),
                  (fun i =>
                        match i with
                        | DihedralGroup.r j => a j
                        | DihedralGroup.sr j => xa j)
                      ((fun i =>
                          match i with
                          | a j => DihedralGroup.r j
                          | xa j => DihedralGroup.sr j)
                        x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : DihedralGroup 0),
                  (fun i =>
                        match i with
                        | a j => DihedralGroup.r j
                        | xa j => DihedralGroup.sr j)
                      ((fun i =>
                          match i with
                          | DihedralGroup.r j => a j
                          | DihedralGroup.sr j => xa j)
                        x) =
                    x) }
          x *
        Equiv.toFun
          {
            toFun := fun i =>
              match i with
              | a j => DihedralGroup.r j
              | xa j => DihedralGroup.sr j,
            invFun := fun i =>
              match i with
              | DihedralGroup.r j => a j
              | DihedralGroup.sr j => xa j,
            left_inv :=
              (_ :
                ∀ (x : QuaternionGroup 0),
                  (fun i =>
                        match i with
                        | DihedralGroup.r j => a j
                        | DihedralGroup.sr j => xa j)
                      ((fun i =>
                          match i with
                          | a j => DihedralGroup.r j
                          | xa j => DihedralGroup.sr j)
                        x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : DihedralGroup 0),
                  (fun i =>
                        match i with
                        | a j => DihedralGroup.r j
                        | xa j => DihedralGroup.sr j)
                      ((fun i =>
                          match i with
                          | DihedralGroup.r j => a j
                          | DihedralGroup.sr j => xa j)
                        x) =
                    x) }
          y
[PROOFSTEP]
rintro (k | k) (l | l)
[GOAL]
case a.a
n : ℕ
k l : ZMod (2 * 0)
⊢ Equiv.toFun
      {
        toFun := fun i =>
          match i with
          | a j => DihedralGroup.r j
          | xa j => DihedralGroup.sr j,
        invFun := fun i =>
          match i with
          | DihedralGroup.r j => a j
          | DihedralGroup.sr j => xa j,
        left_inv :=
          (_ :
            ∀ (x : QuaternionGroup 0),
              (fun i =>
                    match i with
                    | DihedralGroup.r j => a j
                    | DihedralGroup.sr j => xa j)
                  ((fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    x) =
                x),
        right_inv :=
          (_ :
            ∀ (x : DihedralGroup 0),
              (fun i =>
                    match i with
                    | a j => DihedralGroup.r j
                    | xa j => DihedralGroup.sr j)
                  ((fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    x) =
                x) }
      (a k * a l) =
    Equiv.toFun
        {
          toFun := fun i =>
            match i with
            | a j => DihedralGroup.r j
            | xa j => DihedralGroup.sr j,
          invFun := fun i =>
            match i with
            | DihedralGroup.r j => a j
            | DihedralGroup.sr j => xa j,
          left_inv :=
            (_ :
              ∀ (x : QuaternionGroup 0),
                (fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    ((fun i =>
                        match i with
                        | a j => DihedralGroup.r j
                        | xa j => DihedralGroup.sr j)
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DihedralGroup 0),
                (fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    ((fun i =>
                        match i with
                        | DihedralGroup.r j => a j
                        | DihedralGroup.sr j => xa j)
                      x) =
                  x) }
        (a k) *
      Equiv.toFun
        {
          toFun := fun i =>
            match i with
            | a j => DihedralGroup.r j
            | xa j => DihedralGroup.sr j,
          invFun := fun i =>
            match i with
            | DihedralGroup.r j => a j
            | DihedralGroup.sr j => xa j,
          left_inv :=
            (_ :
              ∀ (x : QuaternionGroup 0),
                (fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    ((fun i =>
                        match i with
                        | a j => DihedralGroup.r j
                        | xa j => DihedralGroup.sr j)
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DihedralGroup 0),
                (fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    ((fun i =>
                        match i with
                        | DihedralGroup.r j => a j
                        | DihedralGroup.sr j => xa j)
                      x) =
                  x) }
        (a l)
[PROOFSTEP]
simp
[GOAL]
case a.xa
n : ℕ
k l : ZMod (2 * 0)
⊢ Equiv.toFun
      {
        toFun := fun i =>
          match i with
          | a j => DihedralGroup.r j
          | xa j => DihedralGroup.sr j,
        invFun := fun i =>
          match i with
          | DihedralGroup.r j => a j
          | DihedralGroup.sr j => xa j,
        left_inv :=
          (_ :
            ∀ (x : QuaternionGroup 0),
              (fun i =>
                    match i with
                    | DihedralGroup.r j => a j
                    | DihedralGroup.sr j => xa j)
                  ((fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    x) =
                x),
        right_inv :=
          (_ :
            ∀ (x : DihedralGroup 0),
              (fun i =>
                    match i with
                    | a j => DihedralGroup.r j
                    | xa j => DihedralGroup.sr j)
                  ((fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    x) =
                x) }
      (a k * xa l) =
    Equiv.toFun
        {
          toFun := fun i =>
            match i with
            | a j => DihedralGroup.r j
            | xa j => DihedralGroup.sr j,
          invFun := fun i =>
            match i with
            | DihedralGroup.r j => a j
            | DihedralGroup.sr j => xa j,
          left_inv :=
            (_ :
              ∀ (x : QuaternionGroup 0),
                (fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    ((fun i =>
                        match i with
                        | a j => DihedralGroup.r j
                        | xa j => DihedralGroup.sr j)
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DihedralGroup 0),
                (fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    ((fun i =>
                        match i with
                        | DihedralGroup.r j => a j
                        | DihedralGroup.sr j => xa j)
                      x) =
                  x) }
        (a k) *
      Equiv.toFun
        {
          toFun := fun i =>
            match i with
            | a j => DihedralGroup.r j
            | xa j => DihedralGroup.sr j,
          invFun := fun i =>
            match i with
            | DihedralGroup.r j => a j
            | DihedralGroup.sr j => xa j,
          left_inv :=
            (_ :
              ∀ (x : QuaternionGroup 0),
                (fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    ((fun i =>
                        match i with
                        | a j => DihedralGroup.r j
                        | xa j => DihedralGroup.sr j)
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DihedralGroup 0),
                (fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    ((fun i =>
                        match i with
                        | DihedralGroup.r j => a j
                        | DihedralGroup.sr j => xa j)
                      x) =
                  x) }
        (xa l)
[PROOFSTEP]
simp
[GOAL]
case xa.a
n : ℕ
k l : ZMod (2 * 0)
⊢ Equiv.toFun
      {
        toFun := fun i =>
          match i with
          | a j => DihedralGroup.r j
          | xa j => DihedralGroup.sr j,
        invFun := fun i =>
          match i with
          | DihedralGroup.r j => a j
          | DihedralGroup.sr j => xa j,
        left_inv :=
          (_ :
            ∀ (x : QuaternionGroup 0),
              (fun i =>
                    match i with
                    | DihedralGroup.r j => a j
                    | DihedralGroup.sr j => xa j)
                  ((fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    x) =
                x),
        right_inv :=
          (_ :
            ∀ (x : DihedralGroup 0),
              (fun i =>
                    match i with
                    | a j => DihedralGroup.r j
                    | xa j => DihedralGroup.sr j)
                  ((fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    x) =
                x) }
      (xa k * a l) =
    Equiv.toFun
        {
          toFun := fun i =>
            match i with
            | a j => DihedralGroup.r j
            | xa j => DihedralGroup.sr j,
          invFun := fun i =>
            match i with
            | DihedralGroup.r j => a j
            | DihedralGroup.sr j => xa j,
          left_inv :=
            (_ :
              ∀ (x : QuaternionGroup 0),
                (fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    ((fun i =>
                        match i with
                        | a j => DihedralGroup.r j
                        | xa j => DihedralGroup.sr j)
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DihedralGroup 0),
                (fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    ((fun i =>
                        match i with
                        | DihedralGroup.r j => a j
                        | DihedralGroup.sr j => xa j)
                      x) =
                  x) }
        (xa k) *
      Equiv.toFun
        {
          toFun := fun i =>
            match i with
            | a j => DihedralGroup.r j
            | xa j => DihedralGroup.sr j,
          invFun := fun i =>
            match i with
            | DihedralGroup.r j => a j
            | DihedralGroup.sr j => xa j,
          left_inv :=
            (_ :
              ∀ (x : QuaternionGroup 0),
                (fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    ((fun i =>
                        match i with
                        | a j => DihedralGroup.r j
                        | xa j => DihedralGroup.sr j)
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DihedralGroup 0),
                (fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    ((fun i =>
                        match i with
                        | DihedralGroup.r j => a j
                        | DihedralGroup.sr j => xa j)
                      x) =
                  x) }
        (a l)
[PROOFSTEP]
simp
[GOAL]
case xa.xa
n : ℕ
k l : ZMod (2 * 0)
⊢ Equiv.toFun
      {
        toFun := fun i =>
          match i with
          | a j => DihedralGroup.r j
          | xa j => DihedralGroup.sr j,
        invFun := fun i =>
          match i with
          | DihedralGroup.r j => a j
          | DihedralGroup.sr j => xa j,
        left_inv :=
          (_ :
            ∀ (x : QuaternionGroup 0),
              (fun i =>
                    match i with
                    | DihedralGroup.r j => a j
                    | DihedralGroup.sr j => xa j)
                  ((fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    x) =
                x),
        right_inv :=
          (_ :
            ∀ (x : DihedralGroup 0),
              (fun i =>
                    match i with
                    | a j => DihedralGroup.r j
                    | xa j => DihedralGroup.sr j)
                  ((fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    x) =
                x) }
      (xa k * xa l) =
    Equiv.toFun
        {
          toFun := fun i =>
            match i with
            | a j => DihedralGroup.r j
            | xa j => DihedralGroup.sr j,
          invFun := fun i =>
            match i with
            | DihedralGroup.r j => a j
            | DihedralGroup.sr j => xa j,
          left_inv :=
            (_ :
              ∀ (x : QuaternionGroup 0),
                (fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    ((fun i =>
                        match i with
                        | a j => DihedralGroup.r j
                        | xa j => DihedralGroup.sr j)
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DihedralGroup 0),
                (fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    ((fun i =>
                        match i with
                        | DihedralGroup.r j => a j
                        | DihedralGroup.sr j => xa j)
                      x) =
                  x) }
        (xa k) *
      Equiv.toFun
        {
          toFun := fun i =>
            match i with
            | a j => DihedralGroup.r j
            | xa j => DihedralGroup.sr j,
          invFun := fun i =>
            match i with
            | DihedralGroup.r j => a j
            | DihedralGroup.sr j => xa j,
          left_inv :=
            (_ :
              ∀ (x : QuaternionGroup 0),
                (fun i =>
                      match i with
                      | DihedralGroup.r j => a j
                      | DihedralGroup.sr j => xa j)
                    ((fun i =>
                        match i with
                        | a j => DihedralGroup.r j
                        | xa j => DihedralGroup.sr j)
                      x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : DihedralGroup 0),
                (fun i =>
                      match i with
                      | a j => DihedralGroup.r j
                      | xa j => DihedralGroup.sr j)
                    ((fun i =>
                        match i with
                        | DihedralGroup.r j => a j
                        | DihedralGroup.sr j => xa j)
                      x) =
                  x) }
        (xa l)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ a 0 ≠ xa 0
[PROOFSTEP]
revert n
[GOAL]
⊢ ∀ {n : ℕ}, a 0 ≠ xa 0
[PROOFSTEP]
simp
[GOAL]
n : ℕ
inst✝ : NeZero n
⊢ Fintype.card (QuaternionGroup n) = 4 * n
[PROOFSTEP]
rw [← Fintype.card_eq.mpr ⟨fintypeHelper⟩, Fintype.card_sum, ZMod.card, two_mul]
[GOAL]
n : ℕ
inst✝ : NeZero n
⊢ n + n + (n + n) = 4 * n
[PROOFSTEP]
ring
[GOAL]
n k : ℕ
⊢ a 1 ^ k = a ↑k
[PROOFSTEP]
induction' k with k IH
[GOAL]
case zero
n : ℕ
⊢ a 1 ^ Nat.zero = a ↑Nat.zero
[PROOFSTEP]
rw [Nat.cast_zero]
[GOAL]
case zero
n : ℕ
⊢ a 1 ^ Nat.zero = a 0
[PROOFSTEP]
rfl
[GOAL]
case succ
n k : ℕ
IH : a 1 ^ k = a ↑k
⊢ a 1 ^ Nat.succ k = a ↑(Nat.succ k)
[PROOFSTEP]
rw [pow_succ, IH, a_mul_a]
[GOAL]
case succ
n k : ℕ
IH : a 1 ^ k = a ↑k
⊢ a (1 + ↑k) = a ↑(Nat.succ k)
[PROOFSTEP]
congr 1
[GOAL]
case succ.e_a
n k : ℕ
IH : a 1 ^ k = a ↑k
⊢ 1 + ↑k = ↑(Nat.succ k)
[PROOFSTEP]
norm_cast
[GOAL]
case succ.e_a
n k : ℕ
IH : a 1 ^ k = a ↑k
⊢ ↑(1 + k) = ↑(Nat.succ k)
[PROOFSTEP]
rw [Nat.one_add]
[GOAL]
n : ℕ
⊢ a 1 ^ (2 * n) = 1
[PROOFSTEP]
rw [a_one_pow, one_def]
[GOAL]
n : ℕ
⊢ a ↑(2 * n) = a 0
[PROOFSTEP]
congr 1
[GOAL]
case e_a
n : ℕ
⊢ ↑(2 * n) = 0
[PROOFSTEP]
exact ZMod.nat_cast_self _
[GOAL]
n : ℕ
i : ZMod (2 * n)
⊢ xa i ^ 2 = a ↑n
[PROOFSTEP]
simp [sq]
[GOAL]
n : ℕ
i : ZMod (2 * n)
⊢ xa i ^ 4 = 1
[PROOFSTEP]
rw [pow_succ, pow_succ, sq, xa_mul_xa, xa_mul_a, xa_mul_xa, add_sub_cancel, add_sub_assoc, add_sub_cancel']
[GOAL]
n : ℕ
i : ZMod (2 * n)
⊢ a (↑n + ↑n) = 1
[PROOFSTEP]
norm_cast
[GOAL]
n : ℕ
i : ZMod (2 * n)
⊢ a ↑(n + n) = 1
[PROOFSTEP]
rw [← two_mul]
[GOAL]
n : ℕ
i : ZMod (2 * n)
⊢ a ↑(2 * n) = 1
[PROOFSTEP]
simp [one_def]
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
⊢ orderOf (xa i) = 4
[PROOFSTEP]
change _ = 2 ^ 2
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
⊢ orderOf (xa i) = 2 ^ 2
[PROOFSTEP]
haveI : Fact (Nat.Prime 2) := Fact.mk Nat.prime_two
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
⊢ orderOf (xa i) = 2 ^ 2
[PROOFSTEP]
apply orderOf_eq_prime_pow
[GOAL]
case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
⊢ ¬xa i ^ 2 ^ 1 = 1
[PROOFSTEP]
intro h
[GOAL]
case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h : xa i ^ 2 ^ 1 = 1
⊢ False
[PROOFSTEP]
simp only [pow_one, xa_sq] at h 
[GOAL]
case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h : a ↑n = 1
⊢ False
[PROOFSTEP]
injection h with h'
[GOAL]
case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h' : ↑n = 0
⊢ False
[PROOFSTEP]
apply_fun ZMod.val at h' 
[GOAL]
case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h' : ZMod.val ↑n = ZMod.val 0
⊢ False
[PROOFSTEP]
apply_fun (· / n) at h' 
[GOAL]
case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h' : ZMod.val ↑n / n = ZMod.val 0 / n
⊢ False
[PROOFSTEP]
simp only [ZMod.val_nat_cast, ZMod.val_zero, Nat.zero_div, Nat.mod_mul_left_div_self, Nat.div_self (NeZero.pos n)] at h' 
[GOAL]
case hfin
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
⊢ xa i ^ 2 ^ (1 + 1) = 1
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
⊢ IsCyclic (QuaternionGroup 1)
[PROOFSTEP]
apply isCyclic_of_orderOf_eq_card
[GOAL]
case hx
n : ℕ
⊢ orderOf ?x = Fintype.card (QuaternionGroup 1)
case x n : ℕ ⊢ QuaternionGroup 1
[PROOFSTEP]
rw [card, mul_one]
[GOAL]
case hx
n : ℕ
⊢ orderOf ?x = 4
case x
n : ℕ
⊢ QuaternionGroup 1
case x
n : ℕ
⊢ QuaternionGroup 1
case x n : ℕ ⊢ QuaternionGroup 1
[PROOFSTEP]
exact orderOf_xa 0
[GOAL]
n : ℕ
⊢ orderOf (a 1) = 2 * n
[PROOFSTEP]
cases' eq_zero_or_neZero n with hn hn
[GOAL]
case inl
n : ℕ
hn : n = 0
⊢ orderOf (a 1) = 2 * n
[PROOFSTEP]
subst hn
[GOAL]
case inl
⊢ orderOf (a 1) = 2 * 0
[PROOFSTEP]
simp_rw [mul_zero, orderOf_eq_zero_iff']
[GOAL]
case inl
⊢ ∀ (n : ℕ), 0 < n → QuaternionGroup.a 1 ^ n ≠ 1
[PROOFSTEP]
intro n h
[GOAL]
case inl
n : ℕ
h : 0 < n
⊢ a 1 ^ n ≠ 1
[PROOFSTEP]
rw [one_def, a_one_pow]
[GOAL]
case inl
n : ℕ
h : 0 < n
⊢ a ↑n ≠ a 0
[PROOFSTEP]
apply mt a.inj
[GOAL]
case inl
n : ℕ
h : 0 < n
⊢ ¬↑n = 0
[PROOFSTEP]
haveI : CharZero (ZMod (2 * 0)) := ZMod.charZero
[GOAL]
case inl
n : ℕ
h : 0 < n
this : CharZero (ZMod (2 * 0))
⊢ ¬↑n = 0
[PROOFSTEP]
simpa using h.ne'
[GOAL]
case inr
n : ℕ
hn : NeZero n
⊢ orderOf (a 1) = 2 * n
[PROOFSTEP]
apply (Nat.le_of_dvd (NeZero.pos _) (orderOf_dvd_of_pow_eq_one (@a_one_pow_n n))).lt_or_eq.resolve_left
[GOAL]
case inr
n : ℕ
hn : NeZero n
⊢ ¬orderOf (a 1) < 2 * n
[PROOFSTEP]
intro h
[GOAL]
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
⊢ False
[PROOFSTEP]
have h1 : (a 1 : QuaternionGroup n) ^ orderOf (a 1) = 1 := pow_orderOf_eq_one _
[GOAL]
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h1 : a 1 ^ orderOf (a 1) = 1
⊢ False
[PROOFSTEP]
rw [a_one_pow] at h1 
[GOAL]
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h1 : a ↑(orderOf (a 1)) = 1
⊢ False
[PROOFSTEP]
injection h1 with h2
[GOAL]
case inr
n : ℕ
hn : NeZero n
h : orderOf (a 1) < 2 * n
h2 : ↑(orderOf (a 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 (a 1) < 2 * n
h2 : orderOf (a 1) = 0
⊢ False
[PROOFSTEP]
exact absurd h2.symm (orderOf_pos _).ne
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
⊢ orderOf (a i) = 2 * n / Nat.gcd (2 * n) (ZMod.val i)
[PROOFSTEP]
conv_lhs => rw [← ZMod.nat_cast_zmod_val i]
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
| orderOf (a i)
[PROOFSTEP]
rw [← ZMod.nat_cast_zmod_val i]
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
| orderOf (a i)
[PROOFSTEP]
rw [← ZMod.nat_cast_zmod_val i]
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
| orderOf (a i)
[PROOFSTEP]
rw [← ZMod.nat_cast_zmod_val i]
[GOAL]
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
⊢ orderOf (a ↑(ZMod.val i)) = 2 * n / Nat.gcd (2 * n) (ZMod.val i)
[PROOFSTEP]
rw [← a_one_pow, orderOf_pow, orderOf_a_one]
[GOAL]
n : ℕ
⊢ Monoid.exponent (QuaternionGroup n) = 2 * lcm n 2
[PROOFSTEP]
rw [← normalize_eq 2, ← lcm_mul_left, normalize_eq]
[GOAL]
n : ℕ
⊢ Monoid.exponent (QuaternionGroup n) = lcm (2 * n) (2 * 2)
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
⊢ Monoid.exponent (QuaternionGroup n) = lcm (2 * n) 4
[PROOFSTEP]
cases' eq_zero_or_neZero n with hn hn
[GOAL]
case inl
n : ℕ
hn : n = 0
⊢ Monoid.exponent (QuaternionGroup n) = lcm (2 * n) 4
[PROOFSTEP]
subst hn
[GOAL]
case inl
⊢ Monoid.exponent (QuaternionGroup 0) = lcm (2 * 0) 4
[PROOFSTEP]
simp only [lcm_zero_left, mul_zero]
[GOAL]
case inl
⊢ Monoid.exponent (QuaternionGroup 0) = 0
[PROOFSTEP]
exact Monoid.exponent_eq_zero_of_order_zero orderOf_a_one
[GOAL]
case inr
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (QuaternionGroup n) = lcm (2 * n) 4
[PROOFSTEP]
apply Nat.dvd_antisymm
[GOAL]
case inr.a
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (QuaternionGroup n) ∣ lcm (2 * n) 4
[PROOFSTEP]
apply Monoid.exponent_dvd_of_forall_pow_eq_one
[GOAL]
case inr.a.hG
n : ℕ
hn : NeZero n
⊢ ∀ (g : QuaternionGroup n), g ^ lcm (2 * n) 4 = 1
[PROOFSTEP]
rintro (m | m)
[GOAL]
case inr.a.hG.a
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ a m ^ lcm (2 * n) 4 = 1
[PROOFSTEP]
rw [← orderOf_dvd_iff_pow_eq_one, orderOf_a]
[GOAL]
case inr.a.hG.a
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ 2 * n / Nat.gcd (2 * n) (ZMod.val m) ∣ lcm (2 * n) 4
[PROOFSTEP]
refine' Nat.dvd_trans ⟨gcd (2 * n) m.val, _⟩ (dvd_lcm_left (2 * n) 4)
[GOAL]
case inr.a.hG.a
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ 2 * n = 2 * n / Nat.gcd (2 * n) (ZMod.val m) * gcd (2 * n) (ZMod.val m)
[PROOFSTEP]
exact (Nat.div_mul_cancel (Nat.gcd_dvd_left (2 * n) m.val)).symm
[GOAL]
case inr.a.hG.xa
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ xa m ^ lcm (2 * n) 4 = 1
[PROOFSTEP]
rw [← orderOf_dvd_iff_pow_eq_one, orderOf_xa]
[GOAL]
case inr.a.hG.xa
n : ℕ
hn : NeZero n
m : ZMod (2 * n)
⊢ 4 ∣ lcm (2 * n) 4
[PROOFSTEP]
exact dvd_lcm_right (2 * n) 4
[GOAL]
case inr.a
n : ℕ
hn : NeZero n
⊢ lcm (2 * n) 4 ∣ Monoid.exponent (QuaternionGroup n)
[PROOFSTEP]
apply lcm_dvd
[GOAL]
case inr.a.hab
n : ℕ
hn : NeZero n
⊢ 2 * n ∣ Monoid.exponent (QuaternionGroup n)
[PROOFSTEP]
convert Monoid.order_dvd_exponent (a 1)
[GOAL]
case h.e'_3
n : ℕ
hn : NeZero n
⊢ 2 * n = orderOf (a 1)
[PROOFSTEP]
exact orderOf_a_one.symm
[GOAL]
case inr.a.hcb
n : ℕ
hn : NeZero n
⊢ 4 ∣ Monoid.exponent (QuaternionGroup n)
[PROOFSTEP]
convert Monoid.order_dvd_exponent (xa (0 : ZMod (2 * n)))
[GOAL]
case h.e'_3
n : ℕ
hn : NeZero n
⊢ 4 = orderOf (xa 0)
[PROOFSTEP]
exact (orderOf_xa 0).symm
