awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h : IsCyclic (N × M)
h_1 : Finite M
h_2 : Infinite N
h_3 : Nontrivial M
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
(not_isCyclic_prod_of_infinite_nontrivial N M h).elim

Premises used: False.elim, not_isCyclic_prod_of_infinite_nontrivial
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h : IsCyclic (N × M)
h_1 : Finite M
h_2 : Infinite N
h_3 : Nontrivial M
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
exact (not_isCyclic_prod_of_infinite_nontrivial N M h).elim

Premises used: False.elim, not_isCyclic_prod_of_infinite_nontrivial
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h : IsCyclic (M × N)
h_1 : Finite M
h_2 : Finite N
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
apply coprime_card_of_isCyclic_prod

Premises used: coprime_card_of_isCyclic_prod
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h_1 : IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
hM : IsCyclic M
hN : IsCyclic N
h : (Nat.card M).Coprime (Nat.card N)
f : M × N →* N := MonoidHom.snd M N
rw : ↥(Subgroup.prod ⊤ ⊥) ≃* M
⊢ ↥f.ker ≃* M

Tactic:
rw [MonoidHom.ker_snd]

Premises used: MonoidHom.ker_snd
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h_1 : IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
hM : IsCyclic M
hN : IsCyclic N
h : (Nat.card M).Coprime (Nat.card N)
f : M × N →* N := MonoidHom.snd M N
⊢ ↥(Subgroup.prod ⊤ ⊥) ≃* M

Tactic:
exact ((Subgroup.prodEquiv ..).trans .prodUnique).trans Subgroup.topEquiv

Premises used: MulEquiv.trans, Subgroup.prodEquiv, Subgroup.topEquiv, MulEquiv.prodUnique
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h_1 : IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
hM : IsCyclic M
hN : IsCyclic N
h : (Nat.card M).Coprime (Nat.card N)
f : M × N →* N := MonoidHom.snd M N
e : ↥f.ker ≃* M :=
  Eq.mpr (β := ↥(Subgroup.prod ⊤ ⊥) ≃* M) ⋯
    (MulEquiv.trans (MulEquiv.trans (Subgroup.prodEquiv ⊤ ⊥) MulEquiv.prodUnique) Subgroup.topEquiv)
x : CommGroup M := IsCyclic.commGroup
x_1 : CommGroup N := IsCyclic.commGroup
⊢ IsCyclic ↥f.ker

Tactic:
rw [← e.isCyclic] at hM

Premises used: MulEquiv.isCyclic
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h_1 : IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
hM_1 : IsCyclic M
hN : IsCyclic N
h : (Nat.card M).Coprime (Nat.card N)
f : M × N →* N := MonoidHom.snd M N
hM : IsCyclic ↥f.ker
e : ↥f.ker ≃* M :=
  Eq.mpr (β := ↥(Subgroup.prod ⊤ ⊥) ≃* M) ⋯
    (MulEquiv.trans (MulEquiv.trans (Subgroup.prodEquiv ⊤ ⊥) MulEquiv.prodUnique) Subgroup.topEquiv)
x : CommGroup M := IsCyclic.commGroup
x_1 : CommGroup N := IsCyclic.commGroup
⊢ (Nat.card ↥f.ker).Coprime (Nat.card N)

Tactic:
rw [← Nat.card_congr e.toEquiv] at h

Premises used: MulEquiv.toEquiv, Nat.card_congr
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h_1 : IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
hM_1 : IsCyclic M
hN : IsCyclic N
h : (Nat.card M).Coprime (Nat.card N)
f : M × N →* N := MonoidHom.snd M N
hM : IsCyclic ↥f.ker
e : ↥f.ker ≃* M :=
  Eq.mpr (β := ↥(Subgroup.prod ⊤ ⊥) ≃* M) ⋯
    (MulEquiv.trans (MulEquiv.trans (Subgroup.prodEquiv ⊤ ⊥) MulEquiv.prodUnique) Subgroup.topEquiv)
x : CommGroup M := IsCyclic.commGroup
x_1 : CommGroup N := IsCyclic.commGroup
h₁ : (Nat.card ↥f.ker).Coprime (Nat.card N)
⊢ IsCyclic ↥f.ker

Tactic:
rw [← Nat.card_congr e.toEquiv] at h

Premises used: MulEquiv.toEquiv, Nat.card_congr
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h_1 : IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
hM_1 : IsCyclic M
hN : IsCyclic N
f : M × N →* N := MonoidHom.snd M N
h : (Nat.card ↥f.ker).Coprime (Nat.card N)
hM : IsCyclic ↥f.ker
e : ↥f.ker ≃* M :=
  Eq.mpr (β := ↥(Subgroup.prod ⊤ ⊥) ≃* M) ⋯
    (MulEquiv.trans (MulEquiv.trans (Subgroup.prodEquiv ⊤ ⊥) MulEquiv.prodUnique) Subgroup.topEquiv)
x : CommGroup M := IsCyclic.commGroup
x_1 : CommGroup N := IsCyclic.commGroup
⊢ IsCyclic (M × N)

Tactic:
isCyclic_of_coprime_card_ker f h Prod.snd_surjective

Premises used: Group.isCyclic_of_coprime_card_ker, Prod.snd_surjective
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h_1 : IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
hM_1 : IsCyclic M
hN : IsCyclic N
f : M × N →* N := MonoidHom.snd M N
h : (Nat.card ↥f.ker).Coprime (Nat.card N)
hM : IsCyclic ↥f.ker
e : ↥f.ker ≃* M :=
  Eq.mpr (β := ↥(Subgroup.prod ⊤ ⊥) ≃* M) ⋯
    (MulEquiv.trans (MulEquiv.trans (Subgroup.prodEquiv ⊤ ⊥) MulEquiv.prodUnique) Subgroup.topEquiv)
x : CommGroup M := IsCyclic.commGroup
x_1 : CommGroup N := IsCyclic.commGroup
⊢ IsCyclic (M × N)

Tactic:
exact isCyclic_of_coprime_card_ker f h Prod.snd_surjective

Premises used: Group.isCyclic_of_coprime_card_ker, Prod.snd_surjective
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
G_1 : Type u_2
G' : Type u_3
a : α
G : Type u_4
inst : Group G
inst_1 : IsCyclic G
apply :
  Function.Injective.{u_4 + 1, u_4 + 1} (α := (WithZero G)ˣ) (β := G)
    (⇑(MulEquiv.toMonoidHom WithZero.unitsWithZeroEquiv) : (a : (WithZero G)ˣ) → G)
⊢ IsCyclic.{u_4} (WithZero G)ˣ

Tactic:
apply isCyclic_of_injective (G := (WithZero G)ˣ) (WithZero.unitsWithZeroEquiv).toMonoidHom

Premises used: isCyclic_of_injective, MulEquiv.toMonoidHom, WithZero.unitsWithZeroEquiv
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
G_1 : Type u_2
G' : Type u_3
a : α
G : Type u_4
inst : Group G
inst_1 : IsCyclic G
⊢ Function.Injective.{u_4 + 1, u_4 + 1} (α := (WithZero G)ˣ) (β := G)
    (⇑(MulEquiv.toMonoidHom WithZero.unitsWithZeroEquiv) : (a : (WithZero G)ˣ) → G)

Tactic:
apply Equiv.injective

Premises used: Equiv.injective
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
a b c : ZMod n
⊢ r (a + b + c) = r (a + (b + c))

Tactic:
ring_nf
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
a b c : ZMod n
⊢ sr (c - (a + b)) = sr (c - b - a)

Tactic:
ring_nf
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
a b c : ZMod n
⊢ sr (b - a + c) = sr (b + c - a)

Tactic:
ring_nf
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
a b c : ZMod n
⊢ r (c - (b - a)) = r (a + (c - b))

Tactic:
ring_nf
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
a b c : ZMod n
⊢ sr (a + b + c) = sr (a + (b + c))

Tactic:
ring_nf
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
a b c : ZMod n
⊢ r (c - (a + b)) = r (c - b - a)

Tactic:
ring_nf
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
a b c : ZMod n
⊢ r (b - a + c) = r (b + c - a)

Tactic:
ring_nf
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
a b c : ZMod n
⊢ sr (c - (b - a)) = sr (a + (c - b))

Tactic:
ring_nf
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
a : ZMod n
⊢ 1 * r a = r a

Tactic:
congr_arg r (zero_add a)

Premises used: _private.0.DihedralGroup.mul, zero_add, congr_arg, DihedralGroup.r
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
a : ZMod n
⊢ 1 * r a = r a

Tactic:
exact congr_arg r (zero_add a)

Premises used: zero_add, congr_arg, DihedralGroup.r
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
a : ZMod n
⊢ 1 * sr a = sr a

Tactic:
congr_arg sr (sub_zero a)

Premises used: _private.0.DihedralGroup.mul, sub_zero, congr_arg, DihedralGroup.sr
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
a : ZMod n
⊢ 1 * sr a = sr a

Tactic:
exact congr_arg sr (sub_zero a)

Premises used: sub_zero, congr_arg, DihedralGroup.sr
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
a : ZMod n
⊢ r a * 1 = r a

Tactic:
congr_arg r (add_zero a)

Premises used: _private.0.DihedralGroup.mul, congr_arg, DihedralGroup.r, add_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
a : ZMod n
⊢ r a * 1 = r a

Tactic:
exact congr_arg r (add_zero a)

Premises used: congr_arg, DihedralGroup.r, add_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
a : ZMod n
⊢ sr a * 1 = sr a

Tactic:
congr_arg sr (add_zero a)

Premises used: _private.0.DihedralGroup.mul, congr_arg, DihedralGroup.sr, add_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
a : ZMod n
⊢ sr a * 1 = sr a

Tactic:
exact congr_arg sr (add_zero a)

Premises used: congr_arg, DihedralGroup.sr, add_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
a : ZMod n
⊢ (r a).inv * r a = 1

Tactic:
congr_arg r (neg_add_cancel a)

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

Tactic:
exact congr_arg r (neg_add_cancel a)

Premises used: congr_arg, DihedralGroup.r, neg_add_cancel
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
a : ZMod n
⊢ (sr a).inv * sr a = 1

Tactic:
congr_arg r (sub_self a)

Premises used: _private.0.DihedralGroup.mul, sub_self, _private.0.DihedralGroup.one, congr_arg, DihedralGroup.r
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
a : ZMod n
⊢ (sr a).inv * sr a = 1

Tactic:
exact congr_arg r (sub_self a)

Premises used: sub_self, congr_arg, DihedralGroup.r
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
i j : ZMod n
⊢ r i * r j = r (i + j)

Tactic:
rfl

Premises used: _private.0.DihedralGroup.mul, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
i j : ZMod n
⊢ r i * sr j = sr (j - i)

Tactic:
rfl

Premises used: _private.0.DihedralGroup.mul, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
i j : ZMod n
⊢ sr i * r j = sr (i + j)

Tactic:
rfl

Premises used: _private.0.DihedralGroup.mul, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
i j : ZMod n
⊢ sr i * sr j = r (j - i)

Tactic:
rfl

Premises used: _private.0.DihedralGroup.mul, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
i : ZMod n
⊢ (r i)⁻¹ = r (-i)

Tactic:
rfl

Premises used: _private.0.DihedralGroup.inv, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
i : ZMod n
⊢ (sr i)⁻¹ = sr i

Tactic:
rfl

Premises used: _private.0.DihedralGroup.inv, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
⊢ Eq (α := DihedralGroup n) (r 0) 1

Tactic:
rfl

Premises used: _private.0.DihedralGroup.one, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
⊢ Eq (α := DihedralGroup n) 1 (r 0)

Tactic:
rfl

Premises used: _private.0.DihedralGroup.one, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
i : ZMod n
⊢ HPow.hPow (β := ℕ) (r i) 0 = r (i * (↑0 : ZMod n))

Tactic:
simp only [pow_zero, Nat.cast_zero, mul_zero, r_zero]

Premises used: pow_zero, MulZeroClass.mul_zero, Nat.cast_zero, DihedralGroup.r_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
i : ZMod n
k : ℕ
IH : r i ^ k = r (i * (↑k : ZMod n))
succ : r i ^ k * HPow.hPow (β := ℕ) (r i) 1 = r (i * (↑(k + 1) : ZMod n))
succ₁ : r i ^ k * r i = r (i * (↑(k + 1) : ZMod n))
succ₂ : r (i * (↑k : ZMod n)) * r i = r (i * (↑(k + 1) : ZMod n))
succ₃ : r (i * (↑k : ZMod n) + i) = r (i * (↑(k + 1) : ZMod n))
succ₄ : r (i * (↑k : ZMod n) + i) = r (i * HAdd.hAdd (α := ZMod n) (↑k : ZMod n) (↑1 : ZMod n))
succ₅ : r (i * (↑k : ZMod n) + i) = r (i * HAdd.hAdd (α := ZMod n) (↑k : ZMod n) 1)
succ₆ : i * (↑k : ZMod n) + i = i * HAdd.hAdd (α := ZMod n) (↑k : ZMod n) 1
succ₇ : i * (↑k : ZMod n) + i = i * (↑k : ZMod n) + i * 1
succ₈ succ₉ : i * (↑k : ZMod n) + i = i * (↑k : ZMod n) + i
⊢ r i ^ (k + 1) = r (i * (↑(k + 1) : ZMod n))

Tactic:
rw [pow_add, pow_one, IH, r_mul_r, Nat.cast_add, Nat.cast_one, r.injEq, mul_add, mul_one]

Premises used: pow_add, DihedralGroup.r_mul_r, Nat.cast_add, pow_one, DihedralGroup.r.injEq, mul_add, mul_one, Nat.cast_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
i : ZMod n
k : ℕ
zero : HPow.hPow (β := ℕ) (r i) 0 = r (i * (↑0 : ZMod n))
succ : ∀ (k : ℕ) (IH : r i ^ k = r (i * (↑k : ZMod n))), r i ^ (k + 1) = r (i * (↑(k + 1) : ZMod n))
⊢ r i ^ k = r (i * (↑k : ZMod n))

Tactic:
induction k with
  | zero => simp only [pow_zero, Nat.cast_zero, mul_zero, r_zero]
  | succ k IH =>
    rw [pow_add, pow_one, IH, r_mul_r, Nat.cast_add, Nat.cast_one, r.injEq, mul_add, mul_one]

Premises used: pow_add, pow_zero, MulZeroClass.mul_zero, DihedralGroup.r_mul_r, Nat.cast_add, pow_one, DihedralGroup.r.injEq, mul_add, Nat.cast_zero, mul_one, Nat.cast_one, DihedralGroup.r_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
i : ZMod n
k : ℤ
ofNat : ∀ (a : ℕ), r i ^ Int.ofNat a = r (i * (↑(Int.ofNat a) : ZMod n))
negSucc : ∀ (a : ℕ), r i ^ Int.negSucc a = r (i * (↑(Int.negSucc a) : ZMod n))
⊢ r i ^ k = r (i * (↑k : ZMod n))

Tactic:
cases k
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
i : ZMod n
a : ℕ
⊢ r i ^ Int.ofNat a = r (i * (↑(Int.ofNat a) : ZMod n))

Tactic:
simp [r_pow, neg_mul_eq_mul_neg]

Premises used: DihedralGroup.r_pow, neg_mul_eq_mul_neg
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
i : ZMod n
a : ℕ
⊢ r i ^ Int.negSucc a = r (i * (↑(Int.negSucc a) : ZMod n))

Tactic:
simp [r_pow, neg_mul_eq_mul_neg]

Premises used: DihedralGroup.r_pow, neg_mul_eq_mul_neg
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
x : ZMod n
⊢ (fun (x : ZMod n ⊕ ZMod n) ↦
        (match (motive := ZMod n ⊕ ZMod n → DihedralGroup n) x with
          | Sum.inl j => r j
          | Sum.inr j => sr j :
          DihedralGroup n))
      ((fun (x : DihedralGroup n) ↦
          (match (motive := DihedralGroup n → ZMod n ⊕ ZMod n) x with
            | r j => Sum.inl j
            | sr j => Sum.inr j :
            ZMod n ⊕ ZMod n))
        (r x)) =
    r x

Tactic:
rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
x : ZMod n
⊢ (fun (x : ZMod n ⊕ ZMod n) ↦
        (match (motive := ZMod n ⊕ ZMod n → DihedralGroup n) x with
          | Sum.inl j => r j
          | Sum.inr j => sr j :
          DihedralGroup n))
      ((fun (x : DihedralGroup n) ↦
          (match (motive := DihedralGroup n → ZMod n ⊕ ZMod n) x with
            | r j => Sum.inl j
            | sr j => Sum.inr j :
            ZMod n ⊕ ZMod n))
        (sr x)) =
    sr x

Tactic:
rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
x : ZMod n
⊢ Eq (α := ZMod n ⊕ ZMod n)
    ((fun (x : DihedralGroup n) ↦
        (match (motive := DihedralGroup n → ZMod n ⊕ ZMod n) x with
          | r j => Sum.inl j
          | sr j => Sum.inr j :
          ZMod n ⊕ ZMod n))
      ((fun (x : ZMod n ⊕ ZMod n) ↦
          (match (motive := ZMod n ⊕ ZMod n → DihedralGroup n) x with
            | Sum.inl j => r j
            | Sum.inr j => sr j :
            DihedralGroup n))
        (Sum.inl x)))
    (Sum.inl x)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
x : ZMod n
⊢ Eq (α := ZMod n ⊕ ZMod n)
    ((fun (x : DihedralGroup n) ↦
        (match (motive := DihedralGroup n → ZMod n ⊕ ZMod n) x with
          | r j => Sum.inl j
          | sr j => Sum.inr j :
          ZMod n ⊕ ZMod n))
      ((fun (x : ZMod n ⊕ ZMod n) ↦
          (match (motive := ZMod n ⊕ ZMod n → DihedralGroup n) x with
            | Sum.inl j => r j
            | Sum.inr j => sr j :
            DihedralGroup n))
        (Sum.inr x)))
    (Sum.inr x)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
⊢ Infinite (DihedralGroup 0)

Tactic:
equivSum.symm.infinite_iff.mp inferInstance

Premises used: inferInstance, DihedralGroup.equivSum, Iff.mp, Equiv.infinite_iff, Equiv.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
by_contra : ∀ (h : Eq (α := DihedralGroup n) (r 0) (sr 0)), False
⊢ Ne (α := DihedralGroup n) (r 0) (sr 0)

Tactic:
by_contra h
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
h : Eq (α := DihedralGroup n) (r 0) (sr 0)
⊢ False

Tactic:
injection h
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
inst : NeZero n
rw : Fintype.card (ZMod n ⊕ ZMod n) = 2 * n
rw₁ : Fintype.card (ZMod n) + Fintype.card (ZMod n) = 2 * n
rw₂ : n + n = 2 * n
rw₃ rw₄ : n + n = n + n
⊢ Fintype.card (DihedralGroup n) = 2 * n

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

Premises used: Iff.mpr, two_mul, Fintype.card_eq, DihedralGroup.equivSum, Nonempty.intro, Equiv.symm, ZMod.card, Fintype.card_sum
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
zero : Nat.card (DihedralGroup 0) = HMul.hMul (α := ℕ) 2 0
succ : ∀ (n : ℕ), Nat.card (DihedralGroup (n + 1)) = 2 * (n + 1)
⊢ Nat.card (DihedralGroup n) = 2 * n

Tactic:
cases n
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
zero zero₁ : 0 = HMul.hMul (α := ℕ) 2 0
⊢ Nat.card (DihedralGroup 0) = HMul.hMul (α := ℕ) 2 0

Tactic:
rw [Nat.card_eq_zero_of_infinite]

Premises used: Nat.card_eq_zero_of_infinite
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
succ : Fintype.card (DihedralGroup (n + 1)) = 2 * (n + 1)
succ₁ succ₂ : 2 * (n + 1) = 2 * (n + 1)
⊢ Nat.card (DihedralGroup (n + 1)) = 2 * (n + 1)

Tactic:
rw [Nat.card_eq_fintype_card, card]

Premises used: DihedralGroup.card, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n k : ℕ
⊢ HPow.hPow (α := DihedralGroup n) (r 1) k = r (↑k : ZMod n)

Tactic:
simp only [r_pow, one_mul]

Premises used: DihedralGroup.r_pow, one_mul
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
k : ℤ
⊢ HPow.hPow (α := DihedralGroup n) (r 1) k = r (↑k : ZMod n)

Tactic:
simp only [r_zpow, one_mul]

Premises used: DihedralGroup.r_zpow, one_mul
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
⊢ HPow.hPow (α := DihedralGroup n) (r 1) n = 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
i : ZMod n
⊢ sr i * sr i = 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
i : ZMod n
hg : HPow.hPow (β := ℕ) (sr i) 2 = 1
hg1 : sr i ≠ 1
⊢ orderOf (sr i) = 2

Tactic:
apply orderOf_eq_prime

Premises used: orderOf_eq_prime
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
i : ZMod n
hg : sr i * sr i = 1
hg₁ hg₂ : Eq (α := DihedralGroup n) 1 1
⊢ HPow.hPow (β := ℕ) (sr i) 2 = 1

Tactic:
rw [sq, sr_mul_self]

Premises used: sq, DihedralGroup.sr_mul_self
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
i : ZMod n
⊢ sr i ≠ 1

Tactic:
simp [← r_zero]

Premises used: DihedralGroup.r_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
inl : orderOf (G := DihedralGroup 0) (r 1) = 0
inr : ∀ (hn : NeZero n), orderOf (G := DihedralGroup n) (r 1) = n
⊢ orderOf (G := DihedralGroup n) (r 1) = n

Tactic:
rcases eq_zero_or_neZero n with (rfl | hn)

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
inl : ∀ (n : ℕ), 0 < n → HPow.hPow (α := DihedralGroup 0) (r 1) n ≠ 1
⊢ orderOf (G := DihedralGroup 0) (r 1) = 0

Tactic:
rw [orderOf_eq_zero_iff']

Premises used: orderOf_eq_zero_iff'
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : 0 < n
inl : Ne (α := DihedralGroup 0) (r (↑n : ZMod 0)) (r 0)
⊢ HPow.hPow (α := DihedralGroup 0) (r 1) n ≠ 1

Tactic:
rw [r_one_pow, one_def]

Premises used: DihedralGroup.one_def, DihedralGroup.r_one_pow
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : 0 < n
inl : ¬Eq (α := ZMod 0) (↑n : ZMod 0) 0
⊢ Ne (α := DihedralGroup 0) (r (↑n : ZMod 0)) (r 0)

Tactic:
apply mt r.inj

Premises used: mt, DihedralGroup.r.inj
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : 0 < n
⊢ ¬Eq (α := ZMod 0) (↑n : ZMod 0) 0

Tactic:
simpa using hn.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
inr : ¬orderOf (G := DihedralGroup n) (r 1) < n
⊢ orderOf (G := DihedralGroup n) (r 1) = n

Tactic:
apply (Nat.le_of_dvd (NeZero.pos n) <|
      orderOf_dvd_of_pow_eq_one <| @r_one_pow_n n).lt_or_eq.resolve_left

Premises used: orderOf_dvd_of_pow_eq_one, LE.le.lt_or_eq, Or.resolve_left, NeZero.pos, DihedralGroup.r_one_pow_n, Nat.le_of_dvd
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
h : orderOf (G := DihedralGroup n) (r 1) < n
⊢ HPow.hPow (α := DihedralGroup n) (r 1) (orderOf (G := DihedralGroup n) (r 1)) = 1

Tactic:
have h1 : (r 1 : DihedralGroup n) ^ orderOf (r 1) = 1 := pow_orderOf_eq_one _
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
h : orderOf (G := DihedralGroup n) (r 1) < n
h1 : HPow.hPow (α := DihedralGroup n) (r 1) (orderOf (G := DihedralGroup n) (r 1)) = 1
⊢ Eq (α := DihedralGroup n) (r (↑(orderOf (G := DihedralGroup n) (r 1)) : ZMod n)) 1

Tactic:
rw [r_one_pow] at h1

Premises used: DihedralGroup.r_one_pow
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
h : orderOf (G := DihedralGroup n) (r 1) < n
h1 : Eq (α := DihedralGroup n) (r (↑(orderOf (G := DihedralGroup n) (r 1)) : ZMod n)) 1
⊢ Eq (α := ZMod n) (↑(orderOf (G := DihedralGroup n) (r 1)) : ZMod n) 0

Tactic:
injection h1 with h2
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
h : orderOf (G := DihedralGroup n) (r 1) < n
h2 : Eq (α := ZMod n) (↑(orderOf (G := DihedralGroup n) (r 1)) : ZMod n) 0
⊢ orderOf (G := DihedralGroup n) (r 1) = 0

Tactic:
rw [← ZMod.val_eq_zero, ZMod.val_natCast, Nat.mod_eq_of_lt h] at h2

Premises used: Nat.mod_eq_of_lt, ZMod.val_natCast, ZMod.val_eq_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
h : orderOf (G := DihedralGroup n) (r 1) < n
h2 : orderOf (G := DihedralGroup n) (r 1) = 0
⊢ False

Tactic:
absurd h2.symm (orderOf_pos _).ne

Premises used: absurd, Eq.symm, orderOf_pos, LT.lt.ne
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
hn : NeZero n
h : orderOf (G := DihedralGroup n) (r 1) < n
h2 : orderOf (G := DihedralGroup n) (r 1) = 0
⊢ False

Tactic:
exact absurd h2.symm (orderOf_pos _).ne

Premises used: absurd, Eq.symm, orderOf_pos, LT.lt.ne
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
inst : NeZero n
i : ZMod n
rw : orderOf (G := DihedralGroup n) (r (↑i.val : ZMod n))
| orderOf (r i)

Tactic:
rw [← ZMod.natCast_zmod_val i]

Premises used: ZMod.natCast_zmod_val
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
inst : NeZero n
i : ZMod n
conv_lhs : orderOf (G := DihedralGroup n) (r (↑i.val : ZMod n)) = n / n.gcd i.val
⊢ orderOf (r i) = n / n.gcd i.val

Tactic:
conv_lhs => rw [← ZMod.natCast_zmod_val i]

Premises used: ZMod.natCast_zmod_val
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
inst : NeZero n
i : ZMod n
rw : orderOf (HPow.hPow (α := DihedralGroup n) (r 1) i.val) = n / n.gcd i.val
rw₁ : orderOf (G := DihedralGroup n) (r 1) / (orderOf (G := DihedralGroup n) (r 1)).gcd i.val = n / n.gcd i.val
rw₂ rw₃ : n / n.gcd i.val = n / n.gcd i.val
⊢ orderOf (G := DihedralGroup n) (r (↑i.val : ZMod n)) = n / n.gcd i.val

Tactic:
rw [← r_one_pow, orderOf_pow, orderOf_r_one]

Premises used: DihedralGroup.orderOf_r_one, orderOf_pow, DihedralGroup.r_one_pow
-- Module: Mathlib.GroupTheory.SpecificGroups.Dihedral
Goal:
n : ℕ
inl : Monoid.exponent (DihedralGroup 0) = @lcm _ Nat.instCommMonoidWithZero _ 0 2
inr : ∀ (hn : NeZero n), Monoid.exponent (DihedralGroup n) = @lcm _ Nat.instCommMonoidWithZero _ n 2
⊢ Monoid.exponent (DihedralGroup n) = @lcm _ Nat.instCommMonoidWithZero _ n 2

Tactic:
rcases eq_zero_or_neZero n with (rfl | hn)

Premises used: eq_zero_or_neZero, rfl