-- 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:
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
⊢ #(filter (fun a => orderOf a = d) univ) = φ d

Tactic:
have ha : orderOf a = d := (mem_filter.1 ha').2

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
⊢ #(filter (fun a => orderOf a = d) univ) = φ d

Proof state:
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

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

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
⊢ #(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
m : ℕ
hm : m ∣ d ∧ m < d
⊢ a ^ (d / m) ∈ filter (fun a => orderOf a = m) univ

Tactic:
simp only [mem_filter, mem_univ, orderOf_pow a, ha, true_and,
  Nat.gcd_eq_right (div_dvd_of_dvd hm.1), Nat.div_div_self hm.1 hd0]

Result:
no goals

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
⊢ #(filter (fun a => orderOf a = d) univ) = φ d

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_filter, mem_range, mem_properDivisors] at hm
  refine IH m hm.2 (hm.1.trans hd) (Finset.card_pos.2 ⟨a ^ (d / m), ?_⟩)
  simp only [mem_filter, mem_univ, orderOf_pow a, ha, true_and,
    Nat.gcd_eq_right (div_dvd_of_dvd hm.1), Nat.div_div_self hm.1 hd0]

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
⊢ #(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
⊢ ∑ m ∈ d.properDivisors, #(filter (fun a => orderOf a = m) univ) = ∑ m ∈ d.properDivisors, φ m

Tactic:
refine Finset.sum_congr rfl fun m 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.properDivisors
⊢ #(filter (fun a => orderOf a = m) univ) = φ m

Proof state:
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

Tactic:
cases Fintype.card_ne_zero (eq_zero_of_zero_dvd hd)

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 : ℕ
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

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

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
⊢ a ^ (d / m) ∈ filter (fun a => orderOf a = m) univ