α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
⊢ card (filter (fun a => orderOf a = d) univ) = φ d
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
⊢ card (filter (fun a => orderOf a = d) univ) = φ d
let c := Fintype.card α
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
⊢ card (filter (fun a => orderOf a = d) univ) = φ d
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
⊢ card (filter (fun a => orderOf a = d) univ) = φ d
have hc0 : 0 < c := Fintype.card_pos_iff.2 ⟨1⟩
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
⊢ 0 < card (filter (fun a => orderOf a = d) univ)
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
⊢ card (filter (fun a => orderOf a = d) univ) = φ d
apply card_orderOf_eq_totient_aux₁ hn hd
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : ¬0 < card (filter (fun a => orderOf a = d) univ)
⊢ False
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
⊢ 0 < card (filter (fun a => orderOf a = d) univ)
by_contra h0
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : ¬0 < card (filter (fun a => orderOf a = d) univ)
⊢ False
simp only [not_lt, _root_.le_zero_iff, card_eq_zero] at h0
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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
apply lt_irrefl c
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 = ∅
⊢ Fintype.card α = card (filter (fun x => x ^ Fintype.card α = 1) univ)
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 in divisors c, card (filter (fun a => orderOf a = m) univ)
simp only [← filter_dvd_eq_divisors hc0.ne', sum_card_orderOf_eq_card_pow_eq_one hc0.ne']
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 ^ Fintype.card α = 1) univ
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 = ∅
⊢ Fintype.card α = card (filter (fun x => x ^ Fintype.card α = 1) univ)
apply congr_arg card
no goals
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 ^ Fintype.card α = 1) univ
simp
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 in erase (divisors c) d, card (filter (fun a => orderOf a = m) univ) =
    ∑ m in divisors c, card (filter (fun a => orderOf a = m) univ)
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 in divisors c, card (filter (fun a => orderOf a = m) univ) =
    ∑ m in erase (divisors c) d, card (filter (fun a => orderOf a = m) univ)
rw [eq_comm]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 ∈ divisors c
hm₂ : ¬m ∈ erase (divisors c) d
⊢ card (filter (fun a => orderOf a = m) univ) = 0
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 in erase (divisors c) d, card (filter (fun a => orderOf a = m) univ) =
    ∑ m in divisors c, card (filter (fun a => orderOf a = m) univ)
refine' sum_subset (erase_subset _ _) fun m hm₁ hm₂ => _
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 ∈ divisors c
hm₂ : ¬m ∈ erase (divisors c) d
this : m = d
⊢ card (filter (fun a => orderOf a = m) univ) = 0
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 ∈ divisors c
hm₂ : ¬m ∈ erase (divisors c) d
⊢ card (filter (fun a => orderOf a = m) univ) = 0
have : m = d := by
  contrapose! hm₂
  exact mem_erase_of_ne_of_mem hm₂ hm₁
no goals
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 ∈ divisors c
hm₂ : ¬m ∈ erase (divisors c) d
this : m = d
⊢ card (filter (fun a => orderOf a = m) univ) = 0
simp [this, h0]
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 ∈ divisors c
hm₂ : m ≠ d
⊢ m ∈ erase (divisors (Fintype.card α)) d
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 ∈ divisors c
hm₂ : ¬m ∈ erase (divisors c) d
⊢ m = d
contrapose! hm₂
no goals
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 ∈ divisors c
hm₂ : m ≠ d
⊢ m ∈ erase (divisors (Fintype.card α)) d
exact mem_erase_of_ne_of_mem hm₂ hm₁
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 ∈ erase (divisors c) d
⊢ card (filter (fun a => orderOf a = m) univ) ≤ φ m
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 in erase (divisors c) d, card (filter (fun a => orderOf a = m) univ) ≤ ∑ m in erase (divisors c) d, φ m
refine' sum_le_sum fun m hm => _
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 ∈ erase (divisors c) d
hmc : m ∣ c
⊢ card (filter (fun a => orderOf a = m) univ) ≤ φ m
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 ∈ erase (divisors c) d
⊢ card (filter (fun a => orderOf a = m) univ) ≤ φ m
have hmc : m ∣ c := by
  simp only [mem_erase, mem_divisors] at hm
  tauto
case inl
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 ∈ erase (divisors c) d
hmc : m ∣ c
h1 : card (filter (fun a => orderOf a = m) univ) = 0
⊢ card (filter (fun a => orderOf a = m) univ) ≤ φ m

case inr
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 ∈ erase (divisors c) d
hmc : m ∣ c
h1 : card (filter (fun a => orderOf a = m) univ) > 0
⊢ card (filter (fun a => orderOf a = m) univ) ≤ φ m
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 ∈ erase (divisors c) d
hmc : m ∣ c
⊢ card (filter (fun a => orderOf a = m) univ) ≤ φ m
rcases (filter (fun a : α => orderOf a = m) univ).card.eq_zero_or_pos with (h1 | h1)
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 ∣ Fintype.card α ∧ Fintype.card α ≠ 0
⊢ m ∣ c
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 ∈ erase (divisors c) d
⊢ m ∣ c
simp only [mem_erase, mem_divisors] at hm
no goals
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 ∣ Fintype.card α ∧ Fintype.card α ≠ 0
⊢ m ∣ c
tauto
no goals
case inl
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 ∈ erase (divisors c) d
hmc : m ∣ c
h1 : card (filter (fun a => orderOf a = m) univ) = 0
⊢ card (filter (fun a => orderOf a = m) univ) ≤ φ m
simp [h1]
no goals
case inr
α : Type u
a : α
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → card (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 ∈ erase (divisors c) d
hmc : m ∣ c
h1 : card (filter (fun a => orderOf a = m) univ) > 0
⊢ card (filter (fun a => orderOf a = m) univ) ≤ φ m
simp [card_orderOf_eq_totient_aux₁ hn hmc h1]