case pos
n : ℕ
hn : n = 0
⊢ φ n * ∏ p in List.toFinset (factors n), p = n * ∏ p in List.toFinset (factors n), (p - 1)

case neg
n : ℕ
hn : ¬n = 0
⊢ φ n * ∏ p in List.toFinset (factors n), p = n * ∏ p in List.toFinset (factors n), (p - 1)
n : ℕ
⊢ φ n * ∏ p in List.toFinset (factors n), p = n * ∏ p in List.toFinset (factors n), (p - 1)
by_cases hn : n = 0
case neg
n : ℕ
hn : ¬n = 0
⊢ (Finsupp.prod (factorization n) fun p k => p ^ (k - 1) * (p - 1)) * ∏ p in List.toFinset (factors n), p =
    n * ∏ p in List.toFinset (factors n), (p - 1)
case neg
n : ℕ
hn : ¬n = 0
⊢ φ n * ∏ p in List.toFinset (factors n), p = n * ∏ p in List.toFinset (factors n), (p - 1)
rw [totient_eq_prod_factorization hn]
case neg
n : ℕ
hn : ¬n = 0
⊢ (Finsupp.prod (factorization n) fun p k => p ^ (k - 1) * (p - 1)) * ∏ p in List.toFinset (factors n), p =
    (Finsupp.prod (factorization n) fun x x_1 => x ^ x_1) * ∏ p in List.toFinset (factors n), (p - 1)
case neg
n : ℕ
hn : ¬n = 0
⊢ (Finsupp.prod (factorization n) fun p k => p ^ (k - 1) * (p - 1)) * ∏ p in List.toFinset (factors n), p =
    n * ∏ p in List.toFinset (factors n), (p - 1)
nth_rw 3 [← factorization_prod_pow_eq_self hn]
case neg
n : ℕ
hn : ¬n = 0
⊢ (Finsupp.prod (factorization n) fun a b => a ^ (b - 1) * (a - 1) * a) =
    Finsupp.prod (factorization n) fun a b => a ^ b * (a - 1)
case neg
n : ℕ
hn : ¬n = 0
⊢ (Finsupp.prod (factorization n) fun p k => p ^ (k - 1) * (p - 1)) * ∏ p in List.toFinset (factors n), p =
    (Finsupp.prod (factorization n) fun x x_1 => x ^ x_1) * ∏ p in List.toFinset (factors n), (p - 1)
simp only [← prod_factorization_eq_prod_factors, ← Finsupp.prod_mul]
case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : p ∈ (factorization n).support
⊢ p ^ (↑(factorization n) p - 1) * (p - 1) * p = p ^ ↑(factorization n) p * (p - 1)
case neg
n : ℕ
hn : ¬n = 0
⊢ (Finsupp.prod (factorization n) fun a b => a ^ (b - 1) * (a - 1) * a) =
    Finsupp.prod (factorization n) fun a b => a ^ b * (a - 1)
refine' Finsupp.prod_congr (M := ℕ) (N := ℕ) fun p hp => _
case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : 0 < ↑(factorization n) p
⊢ p ^ (↑(factorization n) p - 1) * (p - 1) * p = p ^ ↑(factorization n) p * (p - 1)
case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : p ∈ (factorization n).support
⊢ p ^ (↑(factorization n) p - 1) * (p - 1) * p = p ^ ↑(factorization n) p * (p - 1)
rw [Finsupp.mem_support_iff, ← zero_lt_iff] at hp
no goals
case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : 0 < ↑(factorization n) p
⊢ p ^ (↑(factorization n) p - 1) * (p - 1) * p = p ^ ↑(factorization n) p * (p - 1)
rw [mul_comm, ← mul_assoc, ← pow_succ', Nat.sub_one, Nat.succ_pred_eq_of_pos hp]
no goals
case pos
n : ℕ
hn : n = 0
⊢ φ n * ∏ p in List.toFinset (factors n), p = n * ∏ p in List.toFinset (factors n), (p - 1)
simp [hn]