awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
IH :
  ∀ m < 0,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : 0 ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = 0}
⊢ card.{u_1} (α := α) {a : α | orderOf a = 0} = φ 0

Tactic:
cases Fintype.card_ne_zero (eq_zero_of_zero_dvd hd)

Premises used: Fintype.card_ne_zero, eq_zero_of_zero_dvd
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
H :
  ∀ (a : α) (ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a),
    card.{u_1} (α := α) {a : α | orderOf a = d} = φ d
⊢ card.{u_1} (α := α) {a : α | orderOf a = d} = φ d

Tactic:
rcases Finset.card_pos.1 hpos with ⟨a, ha'⟩

Premises used: Iff.mp, Finset.card_pos
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
⊢ orderOf a = d

Tactic:
have ha : orderOf a = d := (mem_filter.1 ha').2
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
ha : orderOf a = d
⊢ Eq (α := ℕ) (∑ m ∈ d.properDivisors, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ d.properDivisors, φ m)

Tactic:
Finset.sum_congr rfl fun m hm => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
ha : orderOf a = d
refine : ∀ (m : ℕ) (hm : m ∈ d.properDivisors), card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
⊢ Eq (α := ℕ) (∑ m ∈ d.properDivisors, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ d.properDivisors, φ m)

Tactic:
refine Finset.sum_congr rfl fun m hm => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
ha : orderOf a = d
m : ℕ
hm : m ∈ d.properDivisors
⊢ m ∣ d ∧ m < d

Tactic:
simp only [mem_properDivisors] at hm

Premises used: Nat.mem_properDivisors
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
ha : orderOf a = d
m : ℕ
hm : m ∣ d ∧ m < d
⊢ card.{u_1} (α := α) {a : α | orderOf a = m} = φ m

Tactic:
IH m hm.2 (hm.1.trans hd) (Finset.card_pos.2 ⟨a ^ (d / m), ?_⟩)

Premises used: Iff.mpr, HDiv.hDiv, HPow.hPow, And.right, And.left, Exists.intro, Finset.card_pos, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
ha : orderOf a = d
m : ℕ
hm : m ∣ d ∧ m < d
refine : Membership.mem (γ := Finset α) {a : α | orderOf a = m} (a ^ (d / m))
⊢ card.{u_1} (α := α) {a : α | orderOf a = m} = φ m

Tactic:
refine IH m hm.2 (hm.1.trans hd) (Finset.card_pos.2 ⟨a ^ (d / m), ?_⟩)

Premises used: Iff.mpr, HDiv.hDiv, HPow.hPow, And.right, And.left, Exists.intro, Finset.card_pos, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
ha : orderOf a = d
m : ℕ
hm : m ∣ d ∧ m < d
rw : orderOf (a ^ (d / m)) = m
rw₁ : orderOf a / (orderOf a).gcd (d / m) = m
rw₂ : d / d.gcd (d / m) = m
rw₃ : d / (d / m) = m
rw₄ rw₅ : m = m
⊢ Membership.mem (γ := Finset α) {a : α | orderOf a = m} (a ^ (d / m))

Tactic:
rw [mem_filter_univ, orderOf_pow a, ha, Nat.gcd_eq_right (div_dvd_of_dvd hm.1),
      Nat.div_div_self hm.1 hd0]

Premises used: Finset.mem_filter_univ, orderOf_pow, And.left, Nat.div_dvd_of_dvd, Nat.div_div_self, Nat.gcd_eq_right
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
ha : orderOf a = d
⊢ Eq (α := ℕ) (∑ m ∈ d.properDivisors, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ d.properDivisors, φ m)

Tactic:
have h1 :
    (∑ m ∈ d.properDivisors, #{a : α | orderOf a = m}) =
      ∑ m ∈ d.properDivisors, φ m := by
    refine Finset.sum_congr rfl fun m hm => ?_
    simp only [mem_properDivisors] at hm
    refine IH m hm.2 (hm.1.trans hd) (Finset.card_pos.2 ⟨a ^ (d / m), ?_⟩)
    rw [mem_filter_univ, orderOf_pow a, ha, Nat.gcd_eq_right (div_dvd_of_dvd hm.1),
      Nat.div_div_self hm.1 hd0]
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
ha : orderOf a = d
h1 : Eq (α := ℕ) (∑ m ∈ d.properDivisors, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ d.properDivisors, φ m)
rw : card.{u_1} (α := α) {x : α | x ^ d = 1} = ∑ m ∈ d.divisors, φ m
rw₁ : card.{u_1} (α := α) {x : α | x ^ d = 1} = d
rw₂ : card.{u_1} (α := α) {x : α | x ^ orderOf a = 1} = orderOf a
rw₃ rw₄ : orderOf a = orderOf a
⊢ Eq (α := ℕ) (∑ m ∈ d.divisors, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ d.divisors, φ m)

Tactic:
rw [sum_card_orderOf_eq_card_pow_eq_one hd0, sum_totient,
      ← ha, card_pow_eq_one_eq_orderOf_aux hn a]

Premises used: _private.0.card_pow_eq_one_eq_orderOf_aux, Nat.sum_totient, sum_card_orderOf_eq_card_pow_eq_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
ha : orderOf a = d
h1 : Eq (α := ℕ) (∑ m ∈ d.properDivisors, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ d.properDivisors, φ m)
⊢ Eq (α := ℕ) (∑ m ∈ d.divisors, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ d.divisors, φ m)

Tactic:
have h2 :
    (∑ m ∈ d.divisors, #{a : α | orderOf a = m}) =
      ∑ m ∈ d.divisors, φ m := by
    rw [sum_card_orderOf_eq_card_pow_eq_one hd0, sum_totient,
      ← ha, card_pow_eq_one_eq_orderOf_aux hn a]
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
IH :
  ∀ m < d,
    ∀ (hd : m ∣ Fintype.card α) (hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = m}),
      card.{u_1} (α := α) {a : α | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : Membership.mem (γ := Finset α) {a : α | orderOf a = d} a
ha : orderOf a = d
h1 : Eq (α := ℕ) (∑ m ∈ d.properDivisors, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ d.properDivisors, φ m)
h2 : Eq (α := ℕ) (∑ m ∈ d.divisors, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ d.divisors, φ m)
⊢ card.{u_1} (α := α) {a : α | orderOf a = d} = φ d

Tactic:
simpa [← cons_self_properDivisors hd0, ← h1] using h2

Premises used: Nat.cons_self_properDivisors
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
⊢ 0 < c

Tactic:
have hc0 : 0 < c := Fintype.card_pos_iff.2 ⟨1⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
apply : 0 < card.{u_1} (α := α) {a : α | orderOf a = d}
⊢ card.{u_1} (α := α) {a : α | orderOf a = d} = φ d

Tactic:
apply card_orderOf_eq_totient_aux₁ hn hd

Premises used: _private.0.card_orderOf_eq_totient_aux₁
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
by_contra : ∀ (h0 : ¬0 < card.{u_1} (α := α) {a : α | orderOf a = d}), False
⊢ 0 < card.{u_1} (α := α) {a : α | orderOf a = d}

Tactic:
by_contra h0
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : ¬0 < card.{u_1} (α := α) {a : α | orderOf a = d}
⊢ Eq.{u_1 + 1} (α := Finset α) {a : α | orderOf a = d} ∅

Tactic:
simp_rw [not_lt, Nat.le_zero, Finset.card_eq_zero] at h0

Premises used: Nat.le_zero, not_lt, Finset.card_eq_zero
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : Eq.{u_1 + 1} (α := Finset α) {a : α | orderOf a = d} ∅
apply : c < c
⊢ False

Tactic:
apply lt_irrefl c

Premises used: lt_irrefl
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : Eq.{u_1 + 1} (α := Finset α) {a : α | orderOf a = d} ∅
simp : c = card.{u_1} (α := α) {x : α | x ^ c = 1}
⊢ c = ∑ m ∈ c.divisors, card.{u_1} (α := α) {a : α | orderOf a = m}

Tactic:
simp only [sum_card_orderOf_eq_card_pow_eq_one hc0.ne']

Premises used: LT.lt.ne', sum_card_orderOf_eq_card_pow_eq_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : Eq.{u_1 + 1} (α := Finset α) {a : α | orderOf a = d} ∅
apply : Eq.{u_1 + 1} (α := Finset α) univ {x : α | x ^ c = 1}
⊢ c = card.{u_1} (α := α) {x : α | x ^ c = 1}

Tactic:
apply congr_arg card

Premises used: congr_arg, Finset.card
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : Eq.{u_1 + 1} (α := Finset α) {a : α | orderOf a = d} ∅
⊢ Eq.{u_1 + 1} (α := Finset α) univ {x : α | x ^ c = 1}

Tactic:
simp [c]
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : Eq.{u_1 + 1} (α := Finset α) {a : α | orderOf a = d} ∅
rw :
  Eq (α := ℕ) (∑ m ∈ c.divisors.erase d, card.{u_1} (α := α) {a : α | orderOf a = m})
    (∑ m ∈ c.divisors, card.{u_1} (α := α) {a : α | orderOf a = m})
⊢ Eq (α := ℕ) (∑ m ∈ c.divisors, card.{u_1} (α := α) {a : α | orderOf a = m})
    (∑ m ∈ c.divisors.erase d, card.{u_1} (α := α) {a : α | orderOf a = m})

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : Eq.{u_1 + 1} (α := Finset α) {a : α | orderOf a = d} ∅
⊢ Eq (α := ℕ) (∑ m ∈ c.divisors.erase d, card.{u_1} (α := α) {a : α | orderOf a = m})
    (∑ m ∈ c.divisors, card.{u_1} (α := α) {a : α | orderOf a = m})

Tactic:
sum_subset (erase_subset _ _) fun m hm₁ hm₂ => ?_

Premises used: Finset.sum_subset, Finset.erase_subset
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : Eq.{u_1 + 1} (α := Finset α) {a : α | orderOf a = d} ∅
refine :
  ∀ (m : ℕ) (hm₁ : m ∈ c.divisors) (hm₂ : m ∉ c.divisors.erase d), card.{u_1} (α := α) {a : α | orderOf a = m} = 0
⊢ Eq (α := ℕ) (∑ m ∈ c.divisors.erase d, card.{u_1} (α := α) {a : α | orderOf a = m})
    (∑ m ∈ c.divisors, card.{u_1} (α := α) {a : α | orderOf a = m})

Tactic:
refine sum_subset (erase_subset _ _) fun m hm₁ hm₂ => ?_

Premises used: Finset.sum_subset, Finset.erase_subset
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : Eq.{u_1 + 1} (α := Finset α) {a : α | orderOf a = d} ∅
m : ℕ
hm₁ : m ∈ c.divisors
hm₂ : m ∉ c.divisors.erase d
contrapose! : ∀ (hm₂ : m ≠ d), m ∈ c.divisors.erase d
⊢ m = d

Tactic:
contrapose! hm₂
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : Eq.{u_1 + 1} (α := Finset α) {a : α | orderOf a = d} ∅
m : ℕ
hm₁ : m ∈ c.divisors
hm₂ : m ≠ d
⊢ m ∈ c.divisors.erase d

Tactic:
mem_erase_of_ne_of_mem hm₂ hm₁

Premises used: Finset.mem_erase_of_ne_of_mem
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : Eq.{u_1 + 1} (α := Finset α) {a : α | orderOf a = d} ∅
m : ℕ
hm₁ : m ∈ c.divisors
hm₂ : m ≠ d
⊢ m ∈ c.divisors.erase d

Tactic:
exact mem_erase_of_ne_of_mem hm₂ hm₁

Premises used: Finset.mem_erase_of_ne_of_mem
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : Eq.{u_1 + 1} (α := Finset α) {a : α | orderOf a = d} ∅
m : ℕ
hm₁ : m ∈ c.divisors
hm₂ : m ∉ c.divisors.erase d
⊢ m = d

Tactic:
have : m = d := by
        contrapose! hm₂
        exact mem_erase_of_ne_of_mem hm₂ hm₁
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : Eq.{u_1 + 1} (α := Finset α) {a : α | orderOf a = d} ∅
m : ℕ
hm₁ : m ∈ c.divisors
hm₂ : m ∉ c.divisors.erase d
this : m = d
⊢ card.{u_1} (α := α) {a : α | orderOf a = m} = 0

Tactic:
simp [this, h0]
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : Eq.{u_1 + 1} (α := Finset α) {a : α | orderOf a = d} ∅
h : ∀ (m : ℕ) (hm : m ∈ c.divisors.erase d), card.{u_1} (α := α) {a : α | orderOf a = m} ≤ φ m
⊢ LE.le (α := ℕ) (∑ m ∈ c.divisors.erase d, card.{u_1} (α := α) {a : α | orderOf a = m}) (∑ m ∈ c.divisors.erase d, φ m)

Tactic:
gcongr with m hm
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : Eq.{u_1 + 1} (α := Finset α) {a : α | orderOf a = d} ∅
m : ℕ
hm : m ∈ c.divisors.erase d
⊢ m ≠ d ∧ m ∣ c ∧ c ≠ 0

Tactic:
simp only [mem_erase, mem_divisors] at hm

Premises used: Nat.mem_divisors, Finset.mem_erase
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : Eq.{u_1 + 1} (α := Finset α) {a : α | orderOf a = d} ∅
m : ℕ
hm : m ≠ d ∧ m ∣ c ∧ c ≠ 0
tauto tauto₁ tauto₂ : m ≠ d → m ∣ c → c ≠ 0 → m ∣ c
⊢ m ∣ c

Tactic:
tauto
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : Eq.{u_1 + 1} (α := Finset α) {a : α | orderOf a = d} ∅
m : ℕ
hm : m ∈ c.divisors.erase d
⊢ m ∣ c

Tactic:
have hmc : m ∣ c := by
        simp only [mem_erase, mem_divisors] at hm
        tauto
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : Eq.{u_1 + 1} (α := Finset α) {a : α | orderOf a = d} ∅
m : ℕ
hm : m ∈ c.divisors.erase d
hmc : m ∣ c
h : ∀ (h1 : card.{u_1} (α := α) {a : α | orderOf a = m} = 0), card.{u_1} (α := α) {a : α | orderOf a = m} ≤ φ m
h₁ : ∀ (h1 : card.{u_1} (α := α) {a : α | orderOf a = m} > 0), card.{u_1} (α := α) {a : α | orderOf a = m} ≤ φ m
⊢ card.{u_1} (α := α) {a : α | orderOf a = m} ≤ φ m

Tactic:
obtain h1 | h1 := (#{a : α | orderOf a = m}).eq_zero_or_pos

Premises used: Finset.univ, orderOf, Finset.card, Finset.filter, Eq, Nat.eq_zero_or_pos
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : Eq.{u_1 + 1} (α := Finset α) {a : α | orderOf a = d} ∅
m : ℕ
hm : m ∈ c.divisors.erase d
hmc : m ∣ c
h1 : card.{u_1} (α := α) {a : α | orderOf a = m} = 0
⊢ card.{u_1} (α := α) {a : α | orderOf a = m} ≤ φ m

Tactic:
simp [h1]
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : Eq.{u_1 + 1} (α := Finset α) {a : α | orderOf a = d} ∅
m : ℕ
hm : m ∈ c.divisors.erase d
hmc : m ∣ c
h1 : card.{u_1} (α := α) {a : α | orderOf a = m} > 0
⊢ card.{u_1} (α := α) {a : α | orderOf a = m} ≤ φ m

Tactic:
simp [card_orderOf_eq_totient_aux₁ hn hmc h1]

Premises used: _private.0.card_orderOf_eq_totient_aux₁
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : Eq.{u_1 + 1} (α := Finset α) {a : α | orderOf a = d} ∅
⊢ LT.lt (α := ℕ) (∑ m ∈ c.divisors.erase d, φ m) (∑ m ∈ c.divisors, φ m)

Tactic:
sum_erase_lt_of_pos (mem_divisors.2 ⟨hd, hc0.ne'⟩) (totient_pos.2 (pos_of_dvd_of_pos hd hc0))

Premises used: Iff.mpr, Nat.mem_divisors, LT.lt.ne', And.intro, Nat.pos_of_dvd_of_pos, Nat.totient_pos, Finset.sum_erase_lt_of_pos
-- Module: Mathlib.GroupTheory.SpecificGroups.Cyclic
Goal:
α : Type u_1
inst : Group α
inst_1 : DecidableEq α
inst_2 : Fintype α
hn : ∀ (n : ℕ), 0 < n → card.{u_1} (α := α) {a : α | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : Eq.{u_1 + 1} (α := Finset α) {a : α | orderOf a = d} ∅
⊢ ∑ m ∈ c.divisors, φ m = c

Tactic:
sum_totient _

Premises used: Nat.sum_totient