n : ℕ
⊢ 0 < ∏ p in List.toFinset (factors n), p
n : ℕ
⊢ φ n = (n / ∏ p in List.toFinset (factors n), p) * ∏ p in List.toFinset (factors n), (p - 1)
rw [← mul_div_left n.totient, totient_mul_prod_factors, mul_comm,
  Nat.mul_div_assoc _ (prod_prime_factors_dvd n), mul_comm]
n : ℕ
this : 0 < ∏ i in (factorization n).support, i
⊢ 0 < ∏ p in List.toFinset (factors n), p
n : ℕ
⊢ 0 < ∏ p in List.toFinset (factors n), p
have := prod_pos (fun p => pos_of_mem_factorization (n := n))
no goals
n : ℕ
this : 0 < ∏ i in (factorization n).support, i
⊢ 0 < ∏ p in List.toFinset (factors n), p
simpa [prod_factorization_eq_prod_factors] using this