-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem card_orderOf_eq_totient_aux₂ {d : ℕ} (hd : d ∣ Fintype.card α) :
    #{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 : ℕ
hd : d ∣ Fintype.card α
⊢ #(filter (fun a => orderOf a = d) univ) = φ d

Tactic:
let c := Fintype.card α

Result:
α : 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 α
c : ℕ := Fintype.card α
⊢ #(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 : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
⊢ univ = filter (fun x => x ^ c = 1) univ

Tactic:
simp [c]

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 α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
m : ℕ
hm : m ∈ c.divisors.erase d
hmc : m ∣ c
⊢ #(filter (fun a => orderOf a = m) univ) ≤ φ m

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

Result:
case inl
α : 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 α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
m : ℕ
hm : m ∈ c.divisors.erase d
hmc : m ∣ c
h1 : #(filter (fun a => orderOf a = m) univ) = 0
⊢ #(filter (fun a => orderOf a = m) univ) ≤ φ m

case inr
α : 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 α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
m : ℕ
hm : m ∈ c.divisors.erase d
hmc : m ∣ c
h1 : #(filter (fun a => orderOf a = m) univ) > 0
⊢ #(filter (fun a => orderOf a = m) univ) ≤ φ m

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 α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
⊢ c = ∑ m ∈ c.divisors, #(filter (fun a => orderOf a = m) univ)

Tactic:
simp only [sum_card_orderOf_eq_card_pow_eq_one hc0.ne']

Result:
α : 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 α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
⊢ c = #(filter (fun x => x ^ c = 1) univ)

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 α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : ¬0 < #(filter (fun a => orderOf a = d) univ)
⊢ False

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

Result:
α : 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 α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
⊢ False

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 α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
⊢ ∑ m ∈ c.divisors, #(filter (fun a => orderOf a = m) univ) =
    ∑ m ∈ c.divisors.erase d, #(filter (fun a => orderOf a = m) univ)

Tactic:
rw [eq_comm]

Result:
α : 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 α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
⊢ ∑ m ∈ c.divisors.erase d, #(filter (fun a => orderOf a = m) univ) =
    ∑ m ∈ c.divisors, #(filter (fun a => orderOf a = m) univ)

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 α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
m : ℕ
hm : m ∈ c.divisors.erase d
⊢ m ∣ c

Tactic:
simp only [mem_erase, mem_divisors] 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 : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
m : ℕ
hm : m ≠ d ∧ m ∣ c ∧ c ≠ 0
⊢ m ∣ c

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 α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
⊢ c = #(filter (fun x => x ^ c = 1) univ)

Tactic:
apply congr_arg card

Result:
α : 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 α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
⊢ univ = filter (fun x => x ^ c = 1) univ

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 α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
⊢ False

Tactic:
apply lt_irrefl c

Result:
α : 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 α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
⊢ c < c

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 α
c : ℕ := Fintype.card α
hc0 : 0 < c
⊢ 0 < #(filter (fun a => orderOf a = d) univ)

Tactic:
by_contra h0

Result:
α : 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 α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : ¬0 < #(filter (fun a => orderOf a = d) univ)
⊢ False

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 α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
m : ℕ
hm : m ≠ d ∧ m ∣ c ∧ c ≠ 0
⊢ m ∣ c

Tactic:
tauto

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 α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
⊢ ∑ m ∈ c.divisors.erase d, #(filter (fun a => orderOf a = m) univ) =
    ∑ m ∈ c.divisors, #(filter (fun a => orderOf a = m) univ)

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

Result:
α : 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 α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : filter (fun a => orderOf a = d) univ = ∅
m : ℕ
hm₁ : m ∈ c.divisors
hm₂ : m ∉ c.divisors.erase d
⊢ #(filter (fun a => orderOf a = m) univ) = 0