case inl

⊢ Finset.sum (divisors 0) φ = 0

case inr
n : ℕ
hn : n > 0
⊢ Finset.sum (divisors n) φ = n
n : ℕ
⊢ Finset.sum (divisors n) φ = n
rcases n.eq_zero_or_pos with (rfl | hn)
case inr
n : ℕ
hn : n > 0
⊢ ∑ d in divisors n, φ (n / d) = n
case inr
n : ℕ
hn : n > 0
⊢ Finset.sum (divisors n) φ = n
rw [← sum_div_divisors n φ]
case inr
n : ℕ
hn : n > 0
this : n = ∑ d in divisors n, Finset.card (filter (fun k => gcd n k = d) (range n))
⊢ ∑ d in divisors n, φ (n / d) = n
case inr
n : ℕ
hn : n > 0
⊢ ∑ d in divisors n, φ (n / d) = n
have : n = ∑ d : ℕ in n.divisors, (filter (fun k : ℕ => n.gcd k = d) (range n)).card := by
  nth_rw 1 [← card_range n]
  refine' card_eq_sum_card_fiberwise fun x _ => mem_divisors.2 ⟨_, hn.ne'⟩
  apply gcd_dvd_left
case inr
n : ℕ
hn : n > 0
this : n = ∑ d in divisors n, Finset.card (filter (fun k => gcd n k = d) (range n))
⊢ ∑ d in divisors n, φ (n / d) = ∑ d in divisors n, Finset.card (filter (fun k => gcd n k = d) (range n))
case inr
n : ℕ
hn : n > 0
this : n = ∑ d in divisors n, Finset.card (filter (fun k => gcd n k = d) (range n))
⊢ ∑ d in divisors n, φ (n / d) = n
nth_rw 3 [this]
no goals
case inr
n : ℕ
hn : n > 0
this : n = ∑ d in divisors n, Finset.card (filter (fun k => gcd n k = d) (range n))
⊢ ∑ d in divisors n, φ (n / d) = ∑ d in divisors n, Finset.card (filter (fun k => gcd n k = d) (range n))
exact sum_congr rfl fun x hx => totient_div_of_dvd (dvd_of_mem_divisors hx)
no goals
case inl

⊢ Finset.sum (divisors 0) φ = 0
simp
n : ℕ
hn : n > 0
⊢ Finset.card (range n) = ∑ d in divisors n, Finset.card (filter (fun k => gcd n k = d) (range n))
n : ℕ
hn : n > 0
⊢ n = ∑ d in divisors n, Finset.card (filter (fun k => gcd n k = d) (range n))
nth_rw 1 [← card_range n]
n : ℕ
hn : n > 0
x : ℕ
x✝ : x ∈ range n
⊢ gcd n x ∣ n
n : ℕ
hn : n > 0
⊢ Finset.card (range n) = ∑ d in divisors n, Finset.card (filter (fun k => gcd n k = d) (range n))
refine' card_eq_sum_card_fiberwise fun x _ => mem_divisors.2 ⟨_, hn.ne'⟩
no goals
n : ℕ
hn : n > 0
x : ℕ
x✝ : x ∈ range n
⊢ gcd n x ∣ n
apply gcd_dvd_left