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

Tactic:
exact mem_erase_of_ne_of_mem hm₂ hm₁

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
hm₂ : m ∉ c.divisors.erase d
this : m = d
⊢ #(filter (fun a => orderOf a = m) univ) = 0

Tactic:
simp [this, h0]

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

Tactic:
have hc0 : 0 < c := Fintype.card_pos_iff.2 ⟨1⟩

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

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

Tactic:
simp [card_orderOf_eq_totient_aux₁ hn hmc h1]

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.erase d, φ m

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

Tactic:
apply card_orderOf_eq_totient_aux₁ hn hd

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

Tactic:
have hmc : m ∣ c := by
  simp only [mem_erase, mem_divisors] at hm
  tauto

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.erase d
hmc : m ∣ c
⊢ #(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 = ∅
m : ℕ
hm₁ : m ∈ c.divisors
hm₂ : m ∉ c.divisors.erase d
⊢ m = d

Tactic:
contrapose! 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 ≠ d
⊢ m ∈ c.divisors.erase 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 = ∅
m : ℕ
hm₁ : m ∈ c.divisors
hm₂ : m ∉ c.divisors.erase d
⊢ #(filter (fun a => orderOf a = m) univ) = 0

Tactic:
have : m = d := by
  contrapose! hm₂
  exact mem_erase_of_ne_of_mem 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
this : m = d
⊢ #(filter (fun a => orderOf a = m) univ) = 0

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

Tactic:
simp [h1]

Result:
no goals