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

case neg
n : ℕ
hn : ¬n = 0
⊢ ↑(φ n) = ↑n * ∏ p in List.toFinset (factors n), (1 - (↑p)⁻¹)
n : ℕ
⊢ ↑(φ n) = ↑n * ∏ p in List.toFinset (factors n), (1 - (↑p)⁻¹)
by_cases hn : n = 0
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ ↑(φ n) = ↑n * ∏ p in List.toFinset (factors n), (1 - (↑p)⁻¹)
case neg
n : ℕ
hn : ¬n = 0
⊢ ↑(φ n) = ↑n * ∏ p in List.toFinset (factors n), (1 - (↑p)⁻¹)
have hn' : (n : ℚ) ≠ 0 := by simp [hn]
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p in List.toFinset (factors n), ↑p ≠ 0
⊢ ↑(φ n) = ↑n * ∏ p in List.toFinset (factors n), (1 - (↑p)⁻¹)
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ ↑(φ n) = ↑n * ∏ p in List.toFinset (factors n), (1 - (↑p)⁻¹)
have hpQ : (∏ p in n.factors.toFinset, (p : ℚ)) ≠ 0 := by
  rw [← cast_prod, cast_ne_zero, ← zero_lt_iff, ← prod_factorization_eq_prod_factors]
  exact prod_pos fun p hp => pos_of_mem_factorization hp
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p in List.toFinset (factors n), ↑p ≠ 0
⊢ ∏ i in List.toFinset (factors n), ↑(i - 1) = ∏ x in List.toFinset (factors n), (1 - (↑x)⁻¹) * ↑x
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p in List.toFinset (factors n), ↑p ≠ 0
⊢ ↑(φ n) = ↑n * ∏ p in List.toFinset (factors n), (1 - (↑p)⁻¹)
simp only [totient_eq_div_factors_mul n, prod_prime_factors_dvd n, cast_mul, cast_prod,
  cast_div_charZero, mul_comm_div, mul_right_inj' hn', div_eq_iff hpQ, ← prod_mul_distrib]
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p in List.toFinset (factors n), ↑p ≠ 0
p : ℕ
hp : p ∈ List.toFinset (factors n)
⊢ ↑(p - 1) = (1 - (↑p)⁻¹) * ↑p
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p in List.toFinset (factors n), ↑p ≠ 0
⊢ ∏ i in List.toFinset (factors n), ↑(i - 1) = ∏ x in List.toFinset (factors n), (1 - (↑x)⁻¹) * ↑x
refine' prod_congr rfl fun p hp => _
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p in List.toFinset (factors n), ↑p ≠ 0
p : ℕ
hp✝ : p ∈ List.toFinset (factors n)
hp : 0 < p
⊢ ↑(p - 1) = (1 - (↑p)⁻¹) * ↑p
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p in List.toFinset (factors n), ↑p ≠ 0
p : ℕ
hp : p ∈ List.toFinset (factors n)
⊢ ↑(p - 1) = (1 - (↑p)⁻¹) * ↑p
have hp := pos_of_mem_factors (List.mem_toFinset.mp hp)
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p in List.toFinset (factors n), ↑p ≠ 0
p : ℕ
hp✝ : p ∈ List.toFinset (factors n)
hp : 0 < p
hp' : ↑p ≠ 0
⊢ ↑(p - 1) = (1 - (↑p)⁻¹) * ↑p
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p in List.toFinset (factors n), ↑p ≠ 0
p : ℕ
hp✝ : p ∈ List.toFinset (factors n)
hp : 0 < p
⊢ ↑(p - 1) = (1 - (↑p)⁻¹) * ↑p
have hp' : (p : ℚ) ≠ 0 := cast_ne_zero.mpr hp.ne.symm
no goals
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p in List.toFinset (factors n), ↑p ≠ 0
p : ℕ
hp✝ : p ∈ List.toFinset (factors n)
hp : 0 < p
hp' : ↑p ≠ 0
⊢ ↑(p - 1) = (1 - (↑p)⁻¹) * ↑p
rw [sub_mul, one_mul, mul_comm, mul_inv_cancel hp', cast_pred hp]
no goals
case pos
n : ℕ
hn : n = 0
⊢ ↑(φ n) = ↑n * ∏ p in List.toFinset (factors n), (1 - (↑p)⁻¹)
simp [hn]
no goals
n : ℕ
hn : ¬n = 0
⊢ ↑n ≠ 0
simp [hn]
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ 0 < Finsupp.prod (factorization n) fun p x => p
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ ∏ p in List.toFinset (factors n), ↑p ≠ 0
rw [← cast_prod, cast_ne_zero, ← zero_lt_iff, ← prod_factorization_eq_prod_factors]
no goals
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ 0 < Finsupp.prod (factorization n) fun p x => p
exact prod_pos fun p hp => pos_of_mem_factorization hp