-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem card_orderOf_eq_totient_aux₁ {d : ℕ} (hd : d ∣ Fintype.card α)
    (hpos : 0 < #{a : α | orderOf a = d}) : #{a : α | orderOf a = d} = φ d

Proof state:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #(filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
IH :
  ∀ m < d,
    m ∣ Fintype.card α → 0 < #(filter (fun a => orderOf a = m) univ) → #(filter (fun a => orderOf a = m) univ) = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #(filter (fun a => orderOf a = d) univ)
hd0 : d ≠ 0
a : α
ha' : a ∈ filter (fun a => orderOf a = d) univ
ha : orderOf a = d
m : ℕ
hm : m ∈ d.properDivisors
⊢ #(filter (fun a => orderOf a = m) univ) = φ m

Tactic:
simp only [mem_filter, mem_range, mem_properDivisors] at hm

Result:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #(filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
IH :
  ∀ m < d,
    m ∣ Fintype.card α → 0 < #(filter (fun a => orderOf a = m) univ) → #(filter (fun a => orderOf a = m) univ) = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #(filter (fun a => orderOf a = d) univ)
hd0 : d ≠ 0
a : α
ha' : a ∈ filter (fun a => orderOf a = d) univ
ha : orderOf a = d
m : ℕ
hm : m ∣ d ∧ m < d
⊢ #(filter (fun a => orderOf a = m) univ) = φ m

Proof state:
case H
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #(filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
IH :
  ∀ m < d,
    m ∣ Fintype.card α → 0 < #(filter (fun a => orderOf a = m) univ) → #(filter (fun a => orderOf a = m) univ) = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #(filter (fun a => orderOf a = d) univ)
⊢ #(filter (fun a => orderOf a = d) univ) = φ d

Tactic:
rcases Decidable.eq_or_ne d 0 with (rfl | hd0)

Result:
case H.inl
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #(filter (fun a => a ^ n = 1) univ) ≤ n
IH :
  ∀ m < 0,
    m ∣ Fintype.card α → 0 < #(filter (fun a => orderOf a = m) univ) → #(filter (fun a => orderOf a = m) univ) = φ m
hd : 0 ∣ Fintype.card α
hpos : 0 < #(filter (fun a => orderOf a = 0) univ)
⊢ #(filter (fun a => orderOf a = 0) univ) = φ 0

case H.inr
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #(filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
IH :
  ∀ m < d,
    m ∣ Fintype.card α → 0 < #(filter (fun a => orderOf a = m) univ) → #(filter (fun a => orderOf a = m) univ) = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #(filter (fun a => orderOf a = d) univ)
hd0 : d ≠ 0
⊢ #(filter (fun a => orderOf a = d) univ) = φ d

Proof state:
case H.inr.intro
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #(filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
IH :
  ∀ m < d,
    m ∣ Fintype.card α → 0 < #(filter (fun a => orderOf a = m) univ) → #(filter (fun a => orderOf a = m) univ) = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #(filter (fun a => orderOf a = d) univ)
hd0 : d ≠ 0
a : α
ha' : a ∈ filter (fun a => orderOf a = d) univ
ha : orderOf a = d
h1 : ∑ m ∈ d.properDivisors, #(filter (fun a => orderOf a = m) univ) = ∑ m ∈ d.properDivisors, φ m
⊢ #(filter (fun a => orderOf a = d) univ) = φ d

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]

Result:
case H.inr.intro
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #(filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
IH :
  ∀ m < d,
    m ∣ Fintype.card α → 0 < #(filter (fun a => orderOf a = m) univ) → #(filter (fun a => orderOf a = m) univ) = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #(filter (fun a => orderOf a = d) univ)
hd0 : d ≠ 0
a : α
ha' : a ∈ filter (fun a => orderOf a = d) univ
ha : orderOf a = d
h1 : ∑ m ∈ d.properDivisors, #(filter (fun a => orderOf a = m) univ) = ∑ m ∈ d.properDivisors, φ m
h2 : ∑ m ∈ d.divisors, #(filter (fun a => orderOf a = m) univ) = ∑ m ∈ d.divisors, φ m
⊢ #(filter (fun a => orderOf a = d) univ) = φ d

Proof state:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #(filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
IH :
  ∀ m < d,
    m ∣ Fintype.card α → 0 < #(filter (fun a => orderOf a = m) univ) → #(filter (fun a => orderOf a = m) univ) = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #(filter (fun a => orderOf a = d) univ)
hd0 : d ≠ 0
a : α
ha' : a ∈ filter (fun a => orderOf a = d) univ
ha : orderOf a = d
h1 : ∑ m ∈ d.properDivisors, #(filter (fun a => orderOf a = m) univ) = ∑ m ∈ d.properDivisors, φ m
⊢ ∑ m ∈ d.divisors, #(filter (fun a => orderOf a = m) univ) = ∑ 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]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #(filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
hpos : 0 < #(filter (fun a => orderOf a = d) univ)
⊢ #(filter (fun a => orderOf a = d) univ) = φ d

Tactic:
induction' d using Nat.strongRec' with d IH

Result:
case H
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #(filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
IH :
  ∀ m < d,
    m ∣ Fintype.card α → 0 < #(filter (fun a => orderOf a = m) univ) → #(filter (fun a => orderOf a = m) univ) = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #(filter (fun a => orderOf a = d) univ)
⊢ #(filter (fun a => orderOf a = d) univ) = φ d

Proof state:
case H.inr.intro
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #(filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
IH :
  ∀ m < d,
    m ∣ Fintype.card α → 0 < #(filter (fun a => orderOf a = m) univ) → #(filter (fun a => orderOf a = m) univ) = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #(filter (fun a => orderOf a = d) univ)
hd0 : d ≠ 0
a : α
ha' : a ∈ filter (fun a => orderOf a = d) univ
ha : orderOf a = d
h1 : ∑ m ∈ d.properDivisors, #(filter (fun a => orderOf a = m) univ) = ∑ m ∈ d.properDivisors, φ m
h2 : ∑ m ∈ d.divisors, #(filter (fun a => orderOf a = m) univ) = ∑ m ∈ d.divisors, φ m
⊢ #(filter (fun a => orderOf a = d) univ) = φ d

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

Result:
no goals