awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
⊢ IsCyclic (M × N) ↔ IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
have refine_1 : ∀ (h : IsCyclic (M × N)), (Nat.card M).Coprime (Nat.card N)
Tactic: refine ⟨fun h ↦ ⟨isCyclic_left_of_prod M N, isCyclic_right_of_prod M N, ?_⟩, fun ⟨hM, hN, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
refine_1 : ∀ (h : IsCyclic (M × N)), (Nat.card M).Coprime (Nat.card N)
⊢ IsCyclic (M × N) ↔ IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
have refine_2 : 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)), IsCyclic (M × N)
Tactic: refine ⟨fun h ↦ ⟨isCyclic_left_of_prod M N, isCyclic_right_of_prod M N, ?_⟩, fun ⟨hM, hN, h⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h : IsCyclic (M × N)
⊢ (Nat.card M).Coprime (Nat.card N)
have refine_1 : Infinite M → (Nat.card M).Coprime (Nat.card N)
Tactic: cases (finite_or_infinite M).symm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h : IsCyclic (M × N)
refine_1 : Infinite M → (Nat.card M).Coprime (Nat.card N)
⊢ (Nat.card M).Coprime (Nat.card N)
have refine_1₁ : Finite M → (Nat.card M).Coprime (Nat.card N)
Tactic: cases (finite_or_infinite M).symm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h : IsCyclic (M × N)
h_1 : Infinite M
⊢ (Nat.card M).Coprime (Nat.card N)
have refine_1 : Subsingleton N → (Nat.card M).Coprime (Nat.card N)
Tactic: cases subsingleton_or_nontrivial N
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h : IsCyclic (M × N)
h_1 : Infinite M
refine_1 : Subsingleton N → (Nat.card M).Coprime (Nat.card N)
⊢ (Nat.card M).Coprime (Nat.card N)
have refine_1₁ : Nontrivial N → (Nat.card M).Coprime (Nat.card N)
Tactic: cases subsingleton_or_nontrivial N
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h : IsCyclic (M × N)
h_1 : Finite M
⊢ (Nat.card M).Coprime (Nat.card N)
have refine_1 : Infinite N → (Nat.card M).Coprime (Nat.card N)
Tactic: cases (finite_or_infinite N).symm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
Goal:
M : Type u_4
N : Type u_5
inst : Group M
inst_1 : Group N
h : IsCyclic (M × N)
h_1 : Finite M
refine_1 : Infinite N → (Nat.card M).Coprime (Nat.card N)
⊢ (Nat.card M).Coprime (Nat.card N)
have refine_1₁ : Finite N → (Nat.card M).Coprime (Nat.card N)
Tactic: cases (finite_or_infinite N).symm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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 : Infinite N
⊢ (Nat.card M).Coprime (Nat.card N)
have refine_1 : Subsingleton M → (Nat.card M).Coprime (Nat.card N)
Tactic: cases subsingleton_or_nontrivial M
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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 : Infinite N
refine_1 : Subsingleton M → (Nat.card M).Coprime (Nat.card N)
⊢ (Nat.card M).Coprime (Nat.card N)
have refine_1₁ : Nontrivial M → (Nat.card M).Coprime (Nat.card N)
Tactic: cases subsingleton_or_nontrivial M
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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 : Infinite N
h_3 : Nontrivial M
⊢ (Nat.card M).Coprime (Nat.card N)
have h₁ : IsCyclic (N × M)
Tactic: rw [(MulEquiv.prodComm ..).isCyclic] at h
Cleared hypotheses: h, h_1, h_2, h_3
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
⊢ ↥f.ker ≃* M
have rw : ↥(Subgroup.prod ⊤ ⊥) ≃* M
Tactic: rw [MonoidHom.ker_snd]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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 (M × N)
have hM₁ : IsCyclic ↥f.ker
Tactic: rw [← e.isCyclic] at hM
Cleared hypotheses: e, x, x_1
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (hypothesis)
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
⊢ IsCyclic (M × N)
have h₁ : (Nat.card ↥f.ker).Coprime (Nat.card N)
Tactic: rw [← Nat.card_congr e.toEquiv] at h
Cleared hypotheses: h, hM, e, x, x_1
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Cyclic (goal)
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
⊢ IsCyclic.{u_4} (WithZero G)ˣ
have apply : Function.Injective.{u_4 + 1, u_4 + 1} (α := (WithZero G)ˣ) (β := G)
  (⇑(MulEquiv.toMonoidHom WithZero.unitsWithZeroEquiv) : (a : (WithZero G)ˣ) → G)
Tactic: apply isCyclic_of_injective (G := (WithZero G)ˣ) (WithZero.unitsWithZeroEquiv).toMonoidHom
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
i : ZMod n
k : ℕ
IH : r i ^ k = r (i * (↑k : ZMod n))
⊢ r i ^ (k + 1) = r (i * (↑(k + 1) : ZMod n))
have succ : r i ^ k * HPow.hPow (β := ℕ) (r i) 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]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
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))
⊢ r i ^ (k + 1) = r (i * (↑(k + 1) : ZMod n))
have succ₁ : r i ^ k * r i = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
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))
⊢ r i ^ (k + 1) = r (i * (↑(k + 1) : ZMod n))
have succ₂ : r (i * (↑k : ZMod n)) * r i = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
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))
⊢ r i ^ (k + 1) = r (i * (↑(k + 1) : ZMod n))
have succ₃ : r (i * (↑k : ZMod n) + i) = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
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))
⊢ r i ^ (k + 1) = r (i * (↑(k + 1) : ZMod n))
have succ₄ : r (i * (↑k : ZMod n) + i) = r (i * HAdd.hAdd (α := ZMod n) (↑k : ZMod n) (↑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]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
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))
⊢ r i ^ (k + 1) = r (i * (↑(k + 1) : ZMod n))
have succ₅ : r (i * (↑k : ZMod n) + i) = r (i * HAdd.hAdd (α := ZMod n) (↑k : ZMod n) 1)
Tactic: rw [pow_add, pow_one, IH, r_mul_r, Nat.cast_add, Nat.cast_one, r.injEq, mul_add, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
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)
⊢ r i ^ (k + 1) = r (i * (↑(k + 1) : ZMod n))
have succ₆ : i * (↑k : ZMod n) + i = i * HAdd.hAdd (α := ZMod n) (↑k : ZMod n) 1
Tactic: rw [pow_add, pow_one, IH, r_mul_r, Nat.cast_add, Nat.cast_one, r.injEq, mul_add, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
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
⊢ r i ^ (k + 1) = r (i * (↑(k + 1) : ZMod n))
have succ₇ : i * (↑k : ZMod n) + i = i * (↑k : ZMod n) + i * 1
Tactic: rw [pow_add, pow_one, IH, r_mul_r, Nat.cast_add, Nat.cast_one, r.injEq, mul_add, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
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
⊢ r i ^ (k + 1) = r (i * (↑(k + 1) : ZMod n))
have succ₈ : i * (↑k : ZMod n) + i = i * (↑k : ZMod n) + i
Tactic: rw [pow_add, pow_one, IH, r_mul_r, Nat.cast_add, Nat.cast_one, r.injEq, mul_add, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
i : ZMod n
k : ℕ
⊢ r i ^ k = r (i * (↑k : ZMod n))
have zero : HPow.hPow (β := ℕ) (r i) 0 = r (i * (↑0 : 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]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
i : ZMod n
k : ℕ
zero : HPow.hPow (β := ℕ) (r i) 0 = r (i * (↑0 : ZMod n))
⊢ r i ^ k = r (i * (↑k : ZMod n))
have succ : ∀ (k : ℕ) (IH : r i ^ k = r (i * (↑k : ZMod n))), r i ^ (k + 1) = r (i * (↑(k + 1) : 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]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
i : ZMod n
k : ℤ
⊢ r i ^ k = r (i * (↑k : ZMod n))
have ofNat : ∀ (a : ℕ), r i ^ Int.ofNat a = r (i * (↑(Int.ofNat a) : ZMod n))
Tactic: cases k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
i : ZMod n
k : ℤ
ofNat : ∀ (a : ℕ), r i ^ Int.ofNat a = r (i * (↑(Int.ofNat a) : ZMod n))
⊢ r i ^ k = r (i * (↑k : ZMod n))
have negSucc : ∀ (a : ℕ), r i ^ Int.negSucc a = r (i * (↑(Int.negSucc a) : ZMod n))
Tactic: cases k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
inst : NeZero n
⊢ Fintype.card (DihedralGroup n) = 2 * n
have rw : Fintype.card (ZMod n ⊕ ZMod n) = 2 * n
Tactic: rw [← Fintype.card_eq.mpr ⟨equivSum.symm⟩, Fintype.card_sum, ZMod.card, two_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
inst : NeZero n
rw : Fintype.card (ZMod n ⊕ ZMod n) = 2 * n
⊢ Fintype.card (DihedralGroup n) = 2 * n
have rw₁ : Fintype.card (ZMod n) + Fintype.card (ZMod n) = 2 * n
Tactic: rw [← Fintype.card_eq.mpr ⟨equivSum.symm⟩, Fintype.card_sum, ZMod.card, two_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
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
⊢ Fintype.card (DihedralGroup n) = 2 * n
have rw₂ : n + n = 2 * n
Tactic: rw [← Fintype.card_eq.mpr ⟨equivSum.symm⟩, Fintype.card_sum, ZMod.card, two_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
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
⊢ Fintype.card (DihedralGroup n) = 2 * n
have rw₃ : n + n = n + n
Tactic: rw [← Fintype.card_eq.mpr ⟨equivSum.symm⟩, Fintype.card_sum, ZMod.card, two_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
⊢ Nat.card (DihedralGroup n) = 2 * n
have zero : Nat.card (DihedralGroup 0) = HMul.hMul (α := ℕ) 2 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
zero : Nat.card (DihedralGroup 0) = HMul.hMul (α := ℕ) 2 0
⊢ Nat.card (DihedralGroup n) = 2 * n
have succ : ∀ (n : ℕ), Nat.card (DihedralGroup (n + 1)) = 2 * (n + 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
⊢ Nat.card (DihedralGroup 0) = HMul.hMul (α := ℕ) 2 0
have zero : 0 = HMul.hMul (α := ℕ) 2 0
Tactic: rw [Nat.card_eq_zero_of_infinite]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
⊢ Nat.card (DihedralGroup (n + 1)) = 2 * (n + 1)
have succ : Fintype.card (DihedralGroup (n + 1)) = 2 * (n + 1)
Tactic: rw [Nat.card_eq_fintype_card, card]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
succ : Fintype.card (DihedralGroup (n + 1)) = 2 * (n + 1)
⊢ Nat.card (DihedralGroup (n + 1)) = 2 * (n + 1)
have succ₁ : 2 * (n + 1) = 2 * (n + 1)
Tactic: rw [Nat.card_eq_fintype_card, card]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
i : ZMod n
⊢ orderOf (sr i) = 2
have hg : HPow.hPow (β := ℕ) (sr i) 2 = 1
Tactic: apply orderOf_eq_prime
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
i : ZMod n
hg : HPow.hPow (β := ℕ) (sr i) 2 = 1
⊢ orderOf (sr i) = 2
have hg1 : sr i ≠ 1
Tactic: apply orderOf_eq_prime
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
i : ZMod n
⊢ HPow.hPow (β := ℕ) (sr i) 2 = 1
have hg : sr i * sr i = 1
Tactic: rw [sq, sr_mul_self]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
i : ZMod n
hg : sr i * sr i = 1
⊢ HPow.hPow (β := ℕ) (sr i) 2 = 1
have hg₁ : Eq (α := DihedralGroup n) 1 1
Tactic: rw [sq, sr_mul_self]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
⊢ orderOf (G := DihedralGroup n) (r 1) = n
have inl : orderOf (G := DihedralGroup 0) (r 1) = 0
Tactic: rcases eq_zero_or_neZero n with (rfl | hn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
inl : orderOf (G := DihedralGroup 0) (r 1) = 0
⊢ orderOf (G := DihedralGroup n) (r 1) = n
have inr : ∀ (hn : NeZero n), orderOf (G := DihedralGroup n) (r 1) = n
Tactic: rcases eq_zero_or_neZero n with (rfl | hn)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
⊢ orderOf (G := DihedralGroup 0) (r 1) = 0
have inl : ∀ (n : ℕ), 0 < n → HPow.hPow (α := DihedralGroup 0) (r 1) n ≠ 1
Tactic: rw [orderOf_eq_zero_iff']
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
hn : 0 < n
⊢ HPow.hPow (α := DihedralGroup 0) (r 1) n ≠ 1
have inl : Ne (α := DihedralGroup 0) (r (↑n : ZMod 0)) (r 0)
Tactic: rw [r_one_pow, one_def]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
hn : 0 < n
⊢ Ne (α := DihedralGroup 0) (r (↑n : ZMod 0)) (r 0)
have inl : ¬Eq (α := ZMod 0) (↑n : ZMod 0) 0
Tactic: apply mt r.inj
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
hn : NeZero n
⊢ orderOf (G := DihedralGroup n) (r 1) = n
have inr : ¬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
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (hypothesis)
Goal:
n : ℕ
hn : NeZero n
h : orderOf (G := DihedralGroup n) (r 1) < n
⊢ False
have h1 : 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 _
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (hypothesis)
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
⊢ False
have h1₁ : Eq (α := DihedralGroup n) (r (↑(orderOf (G := DihedralGroup n) (r 1)) : ZMod n)) 1
Tactic: rw [r_one_pow] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (hypothesis)
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
⊢ False
have h2 : Eq (α := ZMod n) (↑(orderOf (G := DihedralGroup n) (r 1)) : ZMod n) 0
Tactic: injection h1 with h2
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (hypothesis)
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
⊢ False
have h2₁ : orderOf (G := DihedralGroup n) (r 1) = 0
Tactic: rw [← ZMod.val_eq_zero, ZMod.val_natCast, Nat.mod_eq_of_lt h] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
inst : NeZero n
i : ZMod n
| orderOf (r i)
have rw : orderOf (G := DihedralGroup n) (r (↑i.val : ZMod n))
Tactic: rw [← ZMod.natCast_zmod_val i]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
inst : NeZero n
i : ZMod n
⊢ orderOf (r i) = n / n.gcd i.val
have conv_lhs : orderOf (G := DihedralGroup n) (r (↑i.val : ZMod n)) = n / n.gcd i.val
Tactic: conv_lhs => rw [← ZMod.natCast_zmod_val i]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
inst : NeZero n
i : ZMod n
⊢ orderOf (G := DihedralGroup n) (r (↑i.val : ZMod n)) = n / n.gcd i.val
have rw : orderOf (HPow.hPow (α := DihedralGroup n) (r 1) i.val) = n / n.gcd i.val
Tactic: rw [← r_one_pow, orderOf_pow, orderOf_r_one]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
inst : NeZero n
i : ZMod n
rw : orderOf (HPow.hPow (α := DihedralGroup n) (r 1) i.val) = n / n.gcd i.val
⊢ orderOf (G := DihedralGroup n) (r (↑i.val : ZMod n)) = n / n.gcd i.val
have rw₁ : orderOf (G := DihedralGroup n) (r 1) / (orderOf (G := DihedralGroup n) (r 1)).gcd i.val = n / n.gcd i.val
Tactic: rw [← r_one_pow, orderOf_pow, orderOf_r_one]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
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
⊢ orderOf (G := DihedralGroup n) (r (↑i.val : ZMod n)) = n / n.gcd i.val
have rw₂ : n / n.gcd i.val = n / n.gcd i.val
Tactic: rw [← r_one_pow, orderOf_pow, orderOf_r_one]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
⊢ Monoid.exponent (DihedralGroup n) = @lcm _ Nat.instCommMonoidWithZero _ n 2
have inl : Monoid.exponent (DihedralGroup 0) = @lcm _ Nat.instCommMonoidWithZero _ 0 2
Tactic: rcases eq_zero_or_neZero n with (rfl | hn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
inl : Monoid.exponent (DihedralGroup 0) = @lcm _ Nat.instCommMonoidWithZero _ 0 2
⊢ Monoid.exponent (DihedralGroup n) = @lcm _ Nat.instCommMonoidWithZero _ n 2
have inr : ∀ (hn : NeZero n), Monoid.exponent (DihedralGroup n) = @lcm _ Nat.instCommMonoidWithZero _ n 2
Tactic: rcases eq_zero_or_neZero n with (rfl | hn)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (DihedralGroup n) = @lcm _ Nat.instCommMonoidWithZero _ n 2
have inr : Monoid.exponent (DihedralGroup n) ∣ @lcm _ Nat.instCommMonoidWithZero _ n 2
Tactic: apply Nat.dvd_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
hn : NeZero n
inr : Monoid.exponent (DihedralGroup n) ∣ @lcm _ Nat.instCommMonoidWithZero _ n 2
⊢ Monoid.exponent (DihedralGroup n) = @lcm _ Nat.instCommMonoidWithZero _ n 2
have inr₁ : @lcm _ Nat.instCommMonoidWithZero _ n 2 ∣ Monoid.exponent (DihedralGroup n)
Tactic: apply Nat.dvd_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (DihedralGroup n) ∣ @lcm _ Nat.instCommMonoidWithZero _ n 2
have inr : ∀ (g : DihedralGroup n), g ^ @lcm _ Nat.instCommMonoidWithZero _ n 2 = 1
Tactic: apply Monoid.exponent_dvd_of_forall_pow_eq_one
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
hn : NeZero n
m : ZMod n
⊢ r m ^ @lcm _ Nat.instCommMonoidWithZero _ n 2 = 1
have inr : n / n.gcd m.val ∣ @lcm _ Nat.instCommMonoidWithZero _ n 2
Tactic: rw [← orderOf_dvd_iff_pow_eq_one, orderOf_r]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Dihedral (goal)
Goal:
n : ℕ
hn : NeZero n
m : ZMod n
⊢ n / n.gcd m.val ∣ @lcm _ Nat.instCommMonoidWithZero _ n 2
have inr : n = n / n.gcd m.val * @gcd _ Nat.instCommMonoidWithZero _ n m.val
Tactic: refine Nat.dvd_trans ⟨gcd n m.val, ?_⟩ (dvd_lcm_left n 2)