awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
Goal:
G : Type u_1
inst : Group G
inst_1 : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst_2 : Group G₁
inst_3 : Group G₂
inst_4 : IsKleinFour G₁
e : G₁ ≃ G₂
he : Eq.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) 1 : G₂) (1 : G₂)
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (1 : G₂)
hy : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) y : G₂) (1 : G₂)
hxy : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
univ₂ :
  Eq (α := Finset G₂)
    (insert (α := G₂) ((e : (a : G₁) → G₂) (x * y) : G₂)
      (insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})))
    univ
neg :
  HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂) ∉
    insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})
⊢ HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂) = (e : (a : G₁) → G₂) (x * y)

Tactic:
apply eq_of_mem_insert_of_notMem <| univ₂.symm ▸ mem_univ _

Premises used: Finset.eq_of_mem_insert_of_notMem
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
Goal:
G : Type u_1
inst : Group G
inst_1 : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst_2 : Group G₁
inst_3 : Group G₂
inst_4 : IsKleinFour G₁
e : G₁ ≃ G₂
he : Eq.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) 1 : G₂) (1 : G₂)
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (1 : G₂)
hy : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) y : G₂) (1 : G₂)
hxy : Ne.{u_3 + 1} (α := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂)
univ₂ :
  Eq (α := Finset G₂)
    (insert (α := G₂) ((e : (a : G₁) → G₂) (x * y) : G₂)
      (insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})))
    univ
⊢ HMul.hMul (α := G₂) (β := G₂) ((e : (a : G₁) → G₂) x : G₂) ((e : (a : G₁) → G₂) y : G₂) ∉
    insert (α := G₂) ((e : (a : G₁) → G₂) x : G₂) (insert (α := G₂) ((e : (a : G₁) → G₂) y : G₂) {1})

Tactic:
simpa using mul_notMem_of_exponent_two h hx hy hxy

Premises used: mul_notMem_of_exponent_two
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
Goal:
G₁ : Type u_2
G₂ : Type u_3
inst : Group G₁
inst_1 : Group G₂
inst_2 : IsKleinFour G₁
inst_3 : IsKleinFour G₂
_inst₁_1 : Fintype G₁ := Fintype.ofFinite G₁
_inst₁ : Fintype G₂ := Fintype.ofFinite G₂
⊢ Fintype.card G₁ = Fintype.card G₂

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
Goal:
G₁ : Type u_2
G₂ : Type u_3
inst : Group G₁
inst_1 : Group G₂
inst_2 : IsKleinFour G₁
inst_3 : IsKleinFour G₂
_inst₁_1 : Fintype G₁ := Fintype.ofFinite G₁
_inst₁ : Fintype G₂ := Fintype.ofFinite G₂
⊢ Eq.{u_3 + 1} (α := G₂) ((Equiv.setValue (Fintype.equivOfCardEq ⋯) 1 1 : (a : G₁) → G₂) 1 : G₂) (1 : G₂)

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
Goal:
G₁ : Type u_2
G₂ : Type u_3
inst : Group G₁
inst_1 : Group G₂
inst_2 : IsKleinFour G₁
inst_3 : IsKleinFour G₂
_inst₁_1 : Fintype G₁ := Fintype.ofFinite G₁
_inst₁ : Fintype G₂ := Fintype.ofFinite G₂
⊢ Nonempty (G₁ ≃* G₂)

Tactic:
exact ⟨mulEquiv ((Fintype.equivOfCardEq <| by simp).setValue 1 1) <| by simp⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.KleinFour
Goal:
G₁ : Type u_2
G₂ : Type u_3
inst : Group G₁
inst_1 : Group G₂
inst_2 : IsKleinFour G₁
inst_3 : IsKleinFour G₂
let let₁ let₂ let₃ : Nonempty (G₁ ≃* G₂)
⊢ Nonempty (G₁ ≃* G₂)

Tactic:
classical
  let _inst₁ := Fintype.ofFinite G₁
  let _inst₁ := Fintype.ofFinite G₂
  exact ⟨mulEquiv ((Fintype.equivOfCardEq <| by simp).setValue 1 1) <| by simp⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i j k : ZMod (2 * n)
⊢ a (i + j + k) = a (i + (j + k))

Tactic:
ring_nf
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (k - (i + j)) = xa (k - j - i)

Tactic:
ring_nf
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (j - i + k) = xa (j + k - i)

Tactic:
ring_nf
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i j k : ZMod (2 * n)
⊢ a ((↑n : ZMod (2 * n)) + k - (j - i)) = a (i + ((↑n : ZMod (2 * n)) + k - j))

Tactic:
ring_nf
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i j k : ZMod (2 * n)
⊢ xa (i + j + k) = xa (i + (j + k))

Tactic:
ring_nf
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i j k : ZMod (2 * n)
⊢ a ((↑n : ZMod (2 * n)) + k - (i + j)) = a ((↑n : ZMod (2 * n)) + (k - j) - i)

Tactic:
ring_nf
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i j k : ZMod (2 * n)
⊢ a ((↑n : ZMod (2 * n)) + j - i + k) = a ((↑n : ZMod (2 * n)) + (j + k) - i)

Tactic:
ring_nf
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i j k : ZMod (2 * n)
xa : QuaternionGroup.xa (k - (↑n : ZMod (2 * n)) - j + i) = QuaternionGroup.xa (k + (↑n : ZMod (2 * n)) - j + i)
⊢ QuaternionGroup.xa (k - ((↑n : ZMod (2 * n)) + j - i)) = QuaternionGroup.xa (i + ((↑n : ZMod (2 * n)) + k - j))

Tactic:
ring_nf
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i j k : ZMod (2 * n)
norm_cast : Eq (α := ZMod (2 * n)) (↑(2 * n) : ZMod (2 * n)) 0
⊢ HMul.hMul (α := ZMod (2 * n)) 2 (↑n : ZMod (2 * n)) = 0

Tactic:
norm_cast
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i j k : ZMod (2 * n)
⊢ Eq (α := ZMod (2 * n)) (↑(2 * n) : ZMod (2 * n)) 0

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i j k : ZMod (2 * n)
⊢ HMul.hMul (α := ZMod (2 * n)) 2 (↑n : ZMod (2 * n)) = 0

Tactic:
have : (2 * n : ZMod (2 * n)) = 0 := by norm_cast; simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i j k : ZMod (2 * n)
this : HMul.hMul (α := ZMod (2 * n)) 2 (↑n : ZMod (2 * n)) = 0
⊢ xa (k - (↑n : ZMod (2 * n)) - j + i) = xa (k + (↑n : ZMod (2 * n)) - j + i)

Tactic:
grind
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i : ZMod (2 * n)
⊢ 1 * a i = a i

Tactic:
congr_arg a (zero_add i)

Premises used: zero_add, congr_arg, QuaternionGroup.a, _private.0.QuaternionGroup.mul
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i : ZMod (2 * n)
⊢ 1 * a i = a i

Tactic:
exact congr_arg a (zero_add i)

Premises used: zero_add, congr_arg, QuaternionGroup.a
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i : ZMod (2 * n)
⊢ 1 * xa i = xa i

Tactic:
congr_arg xa (sub_zero i)

Premises used: sub_zero, congr_arg, QuaternionGroup.xa, _private.0.QuaternionGroup.mul
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i : ZMod (2 * n)
⊢ 1 * xa i = xa i

Tactic:
exact congr_arg xa (sub_zero i)

Premises used: sub_zero, congr_arg, QuaternionGroup.xa
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i : ZMod (2 * n)
⊢ a i * 1 = a i

Tactic:
congr_arg a (add_zero i)

Premises used: congr_arg, QuaternionGroup.a, add_zero, _private.0.QuaternionGroup.mul
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i : ZMod (2 * n)
⊢ a i * 1 = a i

Tactic:
exact congr_arg a (add_zero i)

Premises used: congr_arg, QuaternionGroup.a, add_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i : ZMod (2 * n)
⊢ xa i * 1 = xa i

Tactic:
congr_arg xa (add_zero i)

Premises used: congr_arg, QuaternionGroup.xa, add_zero, _private.0.QuaternionGroup.mul
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i : ZMod (2 * n)
⊢ xa i * 1 = xa i

Tactic:
exact congr_arg xa (add_zero i)

Premises used: congr_arg, QuaternionGroup.xa, add_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i : ZMod (2 * n)
⊢ (a i).inv * a i = 1

Tactic:
congr_arg a (neg_add_cancel i)

Premises used: congr_arg, QuaternionGroup.a, _private.0.QuaternionGroup.one, neg_add_cancel, _private.0.QuaternionGroup.mul
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i : ZMod (2 * n)
⊢ (a i).inv * a i = 1

Tactic:
exact congr_arg a (neg_add_cancel i)

Premises used: congr_arg, QuaternionGroup.a, neg_add_cancel
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i : ZMod (2 * n)
⊢ (xa i).inv * xa i = 1

Tactic:
congr_arg a (sub_self (n + i))

Premises used: sub_self, Nat.cast, congr_arg, QuaternionGroup.a, _private.0.QuaternionGroup.one, HAdd.hAdd, _private.0.QuaternionGroup.mul
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i : ZMod (2 * n)
⊢ (xa i).inv * xa i = 1

Tactic:
exact congr_arg a (sub_self (n + i))

Premises used: sub_self, Nat.cast, congr_arg, QuaternionGroup.a, HAdd.hAdd
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i j : ZMod (2 * n)
⊢ a i * a j = a (i + j)

Tactic:
rfl

Premises used: rfl, _private.0.QuaternionGroup.mul
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i j : ZMod (2 * n)
⊢ a i * xa j = xa (j - i)

Tactic:
rfl

Premises used: rfl, _private.0.QuaternionGroup.mul
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i j : ZMod (2 * n)
⊢ xa i * a j = xa (i + j)

Tactic:
rfl

Premises used: rfl, _private.0.QuaternionGroup.mul
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i j : ZMod (2 * n)
⊢ xa i * xa j = a ((↑n : ZMod (2 * n)) + j - i)

Tactic:
rfl

Premises used: rfl, _private.0.QuaternionGroup.mul
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
⊢ Eq (α := QuaternionGroup n) (a 0) 1

Tactic:
rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
⊢ Eq (α := QuaternionGroup n) 1 (a 0)

Tactic:
rfl

Premises used: _private.0.QuaternionGroup.one, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
x : ZMod (2 * n)
⊢ Eq (α := ZMod (2 * n) ⊕ ZMod (2 * n))
    ((fun (i : QuaternionGroup n) ↦
        (match (motive := QuaternionGroup n → ZMod (2 * n) ⊕ ZMod (2 * n)) i with
          | a j => Sum.inl j
          | xa j => Sum.inr j :
          ZMod (2 * n) ⊕ ZMod (2 * n)))
      ((fun (i : ZMod (2 * n) ⊕ ZMod (2 * n)) ↦
          (match (motive := ZMod (2 * n) ⊕ ZMod (2 * n) → QuaternionGroup n) i with
            | Sum.inl j => a j
            | Sum.inr j => xa j :
            QuaternionGroup n))
        (Sum.inl x)))
    (Sum.inl x)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
x : ZMod (2 * n)
⊢ Eq (α := ZMod (2 * n) ⊕ ZMod (2 * n))
    ((fun (i : QuaternionGroup n) ↦
        (match (motive := QuaternionGroup n → ZMod (2 * n) ⊕ ZMod (2 * n)) i with
          | a j => Sum.inl j
          | xa j => Sum.inr j :
          ZMod (2 * n) ⊕ ZMod (2 * n)))
      ((fun (i : ZMod (2 * n) ⊕ ZMod (2 * n)) ↦
          (match (motive := ZMod (2 * n) ⊕ ZMod (2 * n) → QuaternionGroup n) i with
            | Sum.inl j => a j
            | Sum.inr j => xa j :
            QuaternionGroup n))
        (Sum.inr x)))
    (Sum.inr x)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
x : ZMod (2 * n)
⊢ (fun (i : ZMod (2 * n) ⊕ ZMod (2 * n)) ↦
        (match (motive := ZMod (2 * n) ⊕ ZMod (2 * n) → QuaternionGroup n) i with
          | Sum.inl j => a j
          | Sum.inr j => xa j :
          QuaternionGroup n))
      ((fun (i : QuaternionGroup n) ↦
          (match (motive := QuaternionGroup n → ZMod (2 * n) ⊕ ZMod (2 * n)) i with
            | a j => Sum.inl j
            | xa j => Sum.inr j :
            ZMod (2 * n) ⊕ ZMod (2 * n)))
        (a x)) =
    a x

Tactic:
rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
x : ZMod (2 * n)
⊢ (fun (i : ZMod (2 * n) ⊕ ZMod (2 * n)) ↦
        (match (motive := ZMod (2 * n) ⊕ ZMod (2 * n) → QuaternionGroup n) i with
          | Sum.inl j => a j
          | Sum.inr j => xa j :
          QuaternionGroup n))
      ((fun (i : QuaternionGroup n) ↦
          (match (motive := QuaternionGroup n → ZMod (2 * n) ⊕ ZMod (2 * n)) i with
            | a j => Sum.inl j
            | xa j => Sum.inr j :
            ZMod (2 * n) ⊕ ZMod (2 * n)))
        (xa x)) =
    xa x

Tactic:
rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
k : ZMod (HMul.hMul (α := ℕ) 2 0)
⊢ (fun (x : DihedralGroup 0) ↦
        (match (motive := DihedralGroup 0 → QuaternionGroup 0) x with
          | DihedralGroup.r j => a j
          | DihedralGroup.sr j => xa j :
          QuaternionGroup 0))
      ((fun (x : QuaternionGroup 0) ↦
          (match (motive := QuaternionGroup 0 → DihedralGroup 0) x with
            | a j => DihedralGroup.r j
            | xa j => DihedralGroup.sr j :
            DihedralGroup 0))
        (a k)) =
    a k

Tactic:
rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
k : ZMod (HMul.hMul (α := ℕ) 2 0)
⊢ (fun (x : DihedralGroup 0) ↦
        (match (motive := DihedralGroup 0 → QuaternionGroup 0) x with
          | DihedralGroup.r j => a j
          | DihedralGroup.sr j => xa j :
          QuaternionGroup 0))
      ((fun (x : QuaternionGroup 0) ↦
          (match (motive := QuaternionGroup 0 → DihedralGroup 0) x with
            | a j => DihedralGroup.r j
            | xa j => DihedralGroup.sr j :
            DihedralGroup 0))
        (xa k)) =
    xa k

Tactic:
rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
k : ZMod 0
⊢ (fun (x : QuaternionGroup 0) ↦
        (match (motive := QuaternionGroup 0 → DihedralGroup 0) x with
          | a j => DihedralGroup.r j
          | xa j => DihedralGroup.sr j :
          DihedralGroup 0))
      ((fun (x : DihedralGroup 0) ↦
          (match (motive := DihedralGroup 0 → QuaternionGroup 0) x with
            | DihedralGroup.r j => a j
            | DihedralGroup.sr j => xa j :
            QuaternionGroup 0))
        (DihedralGroup.r k)) =
    DihedralGroup.r k

Tactic:
rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
k : ZMod 0
⊢ (fun (x : QuaternionGroup 0) ↦
        (match (motive := QuaternionGroup 0 → DihedralGroup 0) x with
          | a j => DihedralGroup.r j
          | xa j => DihedralGroup.sr j :
          DihedralGroup 0))
      ((fun (x : DihedralGroup 0) ↦
          (match (motive := DihedralGroup 0 → QuaternionGroup 0) x with
            | DihedralGroup.r j => a j
            | DihedralGroup.sr j => xa j :
            QuaternionGroup 0))
        (DihedralGroup.sr k)) =
    DihedralGroup.sr k

Tactic:
rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
k l : ZMod (HMul.hMul (α := ℕ) 2 0)
⊢ (match (motive := QuaternionGroup 0 → DihedralGroup 0) a k * a l with
    | a j => DihedralGroup.r j
    | xa j => DihedralGroup.sr j) =
    HMul.hMul (α := DihedralGroup 0) (β := DihedralGroup 0)
      (match (motive := QuaternionGroup 0 → DihedralGroup 0) a k with
        | a j => DihedralGroup.r j
        | xa j => DihedralGroup.sr j :
        DihedralGroup 0)
      (match (motive := QuaternionGroup 0 → DihedralGroup 0) a l with
        | a j => DihedralGroup.r j
        | xa j => DihedralGroup.sr j :
        DihedralGroup 0)

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
k l : ZMod (HMul.hMul (α := ℕ) 2 0)
⊢ (match (motive := QuaternionGroup 0 → DihedralGroup 0) a k * xa l with
    | a j => DihedralGroup.r j
    | xa j => DihedralGroup.sr j) =
    HMul.hMul (α := DihedralGroup 0) (β := DihedralGroup 0)
      (match (motive := QuaternionGroup 0 → DihedralGroup 0) a k with
        | a j => DihedralGroup.r j
        | xa j => DihedralGroup.sr j :
        DihedralGroup 0)
      (match (motive := QuaternionGroup 0 → DihedralGroup 0) xa l with
        | a j => DihedralGroup.r j
        | xa j => DihedralGroup.sr j :
        DihedralGroup 0)

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
k l : ZMod (HMul.hMul (α := ℕ) 2 0)
⊢ (match (motive := QuaternionGroup 0 → DihedralGroup 0) xa k * a l with
    | a j => DihedralGroup.r j
    | xa j => DihedralGroup.sr j) =
    HMul.hMul (α := DihedralGroup 0) (β := DihedralGroup 0)
      (match (motive := QuaternionGroup 0 → DihedralGroup 0) xa k with
        | a j => DihedralGroup.r j
        | xa j => DihedralGroup.sr j :
        DihedralGroup 0)
      (match (motive := QuaternionGroup 0 → DihedralGroup 0) a l with
        | a j => DihedralGroup.r j
        | xa j => DihedralGroup.sr j :
        DihedralGroup 0)

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
k l : ZMod (HMul.hMul (α := ℕ) 2 0)
⊢ (match (motive := QuaternionGroup 0 → DihedralGroup 0) xa k * xa l with
    | a j => DihedralGroup.r j
    | xa j => DihedralGroup.sr j) =
    HMul.hMul (α := DihedralGroup 0) (β := DihedralGroup 0)
      (match (motive := QuaternionGroup 0 → DihedralGroup 0) xa k with
        | a j => DihedralGroup.r j
        | xa j => DihedralGroup.sr j :
        DihedralGroup 0)
      (match (motive := QuaternionGroup 0 → DihedralGroup 0) xa l with
        | a j => DihedralGroup.r j
        | xa j => DihedralGroup.sr j :
        DihedralGroup 0)

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
⊢ Ne (α := QuaternionGroup n) (a 0) (xa 0)

Tactic:
simp [- a_zero]

Premises used: QuaternionGroup.a_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
inst : NeZero n
rw : n + n + (n + n) = 4 * n
⊢ Fintype.card (QuaternionGroup n) = 4 * n

Tactic:
rw [← Fintype.card_eq.mpr ⟨fintypeHelper⟩, Fintype.card_sum, ZMod.card, two_mul]

Premises used: Iff.mpr, two_mul, Fintype.card_eq, Nonempty.intro, _private.0.QuaternionGroup.fintypeHelper, ZMod.card, Fintype.card_sum
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
inst : NeZero n
⊢ n + n + (n + n) = 4 * n

Tactic:
ring
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
zero : HPow.hPow (α := QuaternionGroup n) (β := ℕ) (a 1) 0 = a 0
⊢ HPow.hPow (α := QuaternionGroup n) (β := ℕ) (a 1) 0 = a (↑0 : ZMod (2 * n))

Tactic:
rw [Nat.cast_zero]

Premises used: Nat.cast_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
⊢ HPow.hPow (α := QuaternionGroup n) (β := ℕ) (a 1) 0 = a 0

Tactic:
rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n k : ℕ
IH : HPow.hPow (α := QuaternionGroup n) (a 1) k = a (↑k : ZMod (2 * n))
succ : a (HAdd.hAdd (α := ZMod (2 * n)) (↑k : ZMod (2 * n)) 1) = a (↑(k + 1) : ZMod (2 * n))
⊢ HPow.hPow (α := QuaternionGroup n) (a 1) (k + 1) = a (↑(k + 1) : ZMod (2 * n))

Tactic:
rw [pow_succ, IH, a_mul_a]

Premises used: pow_succ, QuaternionGroup.a_mul_a
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n k : ℕ
IH : HPow.hPow (α := QuaternionGroup n) (a 1) k = a (↑k : ZMod (2 * n))
succ : HAdd.hAdd (α := ZMod (2 * n)) (↑k : ZMod (2 * n)) 1 = (↑(k + 1) : ZMod (2 * n))
⊢ a (HAdd.hAdd (α := ZMod (2 * n)) (↑k : ZMod (2 * n)) 1) = a (↑(k + 1) : ZMod (2 * n))

Tactic:
congr 1
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n k : ℕ
IH : HPow.hPow (α := QuaternionGroup n) (a 1) k = a (↑k : ZMod (2 * n))
succ succ₁ succ₂ succ₃ : Eq (α := ZMod (2 * n)) (↑(k + 1) : ZMod (2 * n)) (↑(k + 1) : ZMod (2 * n))
⊢ HAdd.hAdd (α := ZMod (2 * n)) (↑k : ZMod (2 * n)) 1 = (↑(k + 1) : ZMod (2 * n))

Tactic:
norm_cast
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n k : ℕ
zero : HPow.hPow (α := QuaternionGroup n) (β := ℕ) (a 1) 0 = a (↑0 : ZMod (2 * n))
succ :
  ∀ (k : ℕ) (IH : HPow.hPow (α := QuaternionGroup n) (a 1) k = a (↑k : ZMod (2 * n))),
    HPow.hPow (α := QuaternionGroup n) (a 1) (k + 1) = a (↑(k + 1) : ZMod (2 * n))
⊢ HPow.hPow (α := QuaternionGroup n) (a 1) k = a (↑k : ZMod (2 * n))

Tactic:
induction k with
  | zero => rw [Nat.cast_zero]; rfl
  | succ k IH =>
    rw [pow_succ, IH, a_mul_a]
    congr 1
    norm_cast

Premises used: pow_succ, QuaternionGroup.a_mul_a, Nat.cast_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
⊢ HPow.hPow (α := QuaternionGroup n) (a 1) (2 * n) = 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i : ZMod (2 * n)
⊢ HPow.hPow (β := ℕ) (xa i) 2 = a (↑n : ZMod (2 * n))

Tactic:
simp [sq]

Premises used: sq
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i : ZMod (2 * n)
⊢ HPow.hPow (β := ℕ) (xa i) 4 = a (HAdd.hAdd (α := ZMod (2 * n)) (↑n : ZMod (2 * n)) (↑n : ZMod (2 * n)))

Tactic:
simp [pow_succ, add_sub_assoc, sub_sub_cancel]

Premises used: add_sub_assoc, pow_succ, sub_sub_cancel
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i : ZMod (2 * n)
⊢ a (HAdd.hAdd (α := ZMod (2 * n)) (↑n : ZMod (2 * n)) (↑n : ZMod (2 * n))) = a (↑(2 * n) : ZMod (2 * n))

Tactic:
simp [Nat.cast_add, two_mul]

Premises used: two_mul, Nat.cast_add
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i : ZMod (2 * n)
⊢ Eq (α := QuaternionGroup n) (a (↑(2 * n) : ZMod (2 * n))) 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
i : ZMod (2 * n)
calc : HPow.hPow (β := ℕ) (xa i) 4 = a (HAdd.hAdd (α := ZMod (2 * n)) (↑n : ZMod (2 * n)) (↑n : ZMod (2 * n)))
calc₁ : a (HAdd.hAdd (α := ZMod (2 * n)) (↑n : ZMod (2 * n)) (↑n : ZMod (2 * n))) = a (↑(2 * n) : ZMod (2 * n))
calc₂ : Eq (α := QuaternionGroup n) (a (↑(2 * n) : ZMod (2 * n))) 1
⊢ HPow.hPow (β := ℕ) (xa i) 4 = 1

Tactic:
calc xa i ^ 4
      = a (n + n) := by simp [pow_succ, add_sub_assoc, sub_sub_cancel]
    _ = a ↑(2 * n) := by simp [Nat.cast_add, two_mul]
    _ = 1 := by simp

Premises used: HMul.hMul, Nat.cast, QuaternionGroup.a, HAdd.hAdd, QuaternionGroup.xa, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
inst : NeZero n
i : ZMod (2 * n)
⊢ Fact (Nat.Prime 2)

Tactic:
haveI : Fact (Nat.Prime 2) := Fact.mk Nat.prime_two
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
inst : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
hnot : ¬xa i ^ HPow.hPow (α := ℕ) (β := ℕ) 2 1 = 1
hfin : xa i ^ HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 1 1) = 1
⊢ orderOf (xa i) = HPow.hPow (α := ℕ) (β := ℕ) 2 2

Tactic:
apply orderOf_eq_prime_pow

Premises used: orderOf_eq_prime_pow
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
inst : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h : xa i ^ HPow.hPow (α := ℕ) (β := ℕ) 2 1 = 1
⊢ Eq (α := QuaternionGroup n) (a (↑n : ZMod (2 * n))) 1

Tactic:
simp only [pow_one, xa_sq] at h

Premises used: pow_one, QuaternionGroup.xa_sq
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
inst : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h : Eq (α := QuaternionGroup n) (a (↑n : ZMod (2 * n))) 1
⊢ Eq (α := ZMod (2 * n)) (↑n : ZMod (2 * n)) 0

Tactic:
injection h with h'
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
inst : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h' : Eq (α := ZMod (2 * n)) (↑n : ZMod (2 * n)) 0
⊢ ZMod.val (n := 2 * n) (↑n : ZMod (2 * n)) = ZMod.val (n := 2 * n) 0

Tactic:
apply_fun ZMod.val at h'

Premises used: ZMod.val
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
inst : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h' : ZMod.val (n := 2 * n) (↑n : ZMod (2 * n)) = ZMod.val (n := 2 * n) 0
⊢ ZMod.val (n := 2 * n) (↑n : ZMod (2 * n)) / n = ZMod.val (n := 2 * n) 0 / n

Tactic:
apply_fun (· / n) at h'

Premises used: HDiv.hDiv
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
inst : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h' : ZMod.val (n := 2 * n) (↑n : ZMod (2 * n)) / n = ZMod.val (n := 2 * n) 0 / n
⊢ False

Tactic:
simp only [ZMod.val_natCast, ZMod.val_zero, Nat.zero_div, Nat.mod_mul_left_div_self,
      Nat.div_self (NeZero.pos n), reduceCtorEq] at h'

Premises used: reduceCtorEq, Nat.mod_mul_left_div_self, Nat.zero_div, ZMod.val_zero, Nat.div_self, ZMod.val_natCast, NeZero.pos
-- Module: Mathlib.GroupTheory.SpecificGroups.Quaternion
Goal:
n : ℕ
inst : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
⊢ xa i ^ HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 1 1) = 1

Tactic:
simp