-- Mathlib/Data/Nat/Totient.lean
theorem totient_eq_mul_prod_factors (n : ℕ) :
    (φ n : ℚ) = n * ∏ p ∈ n.primeFactors, (1 - (p : ℚ)⁻¹)

Proof state:
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0
⊢ ↑(φ n) = ↑n * ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)

Tactic:
simp only [totient_eq_div_primeFactors_mul n, prod_primeFactors_dvd n, cast_mul, cast_prod,
  cast_div_charZero, mul_comm_div, mul_right_inj' hn', div_eq_iff hpQ, ← prod_mul_distrib]

Result:
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0
⊢ ∏ i ∈ n.primeFactors, ↑(i - 1) = ∏ x ∈ n.primeFactors, (1 - (↑x)⁻¹) * ↑x

Proof state:
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ 0 < n.factorization.prod fun p x => p

Tactic:
exact prod_pos fun p hp => pos_of_mem_primeFactors hp

Result:
no goals

Proof state:
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : 0 < p
⊢ ↑(p - 1) = (1 - (↑p)⁻¹) * ↑p

Tactic:
have hp' : (p : ℚ) ≠ 0 := cast_ne_zero.mpr hp.ne.symm

Result:
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : 0 < p
hp' : ↑p ≠ 0
⊢ ↑(p - 1) = (1 - (↑p)⁻¹) * ↑p

Proof state:
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0
p : ℕ
hp : p ∈ n.primeFactors
⊢ ↑(p - 1) = (1 - (↑p)⁻¹) * ↑p

Tactic:
have hp := pos_of_mem_primeFactorsList (List.mem_toFinset.mp hp)

Result:
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : 0 < p
⊢ ↑(p - 1) = (1 - (↑p)⁻¹) * ↑p

Proof state:
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : 0 < p
hp' : ↑p ≠ 0
⊢ ↑(p - 1) = (1 - (↑p)⁻¹) * ↑p

Tactic:
rw [sub_mul, one_mul, mul_comm, mul_inv_cancel₀ hp', cast_pred hp]

Result:
no goals

Proof state:
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0
⊢ ∏ i ∈ n.primeFactors, ↑(i - 1) = ∏ x ∈ n.primeFactors, (1 - (↑x)⁻¹) * ↑x

Tactic:
refine prod_congr rfl fun p hp => ?_

Result:
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0
p : ℕ
hp : p ∈ n.primeFactors
⊢ ↑(p - 1) = (1 - (↑p)⁻¹) * ↑p

Proof state:
case neg
n : ℕ
hn : ¬n = 0
⊢ ↑(φ n) = ↑n * ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)

Tactic:
have hn' : (n : ℚ) ≠ 0 := by simp [hn]

Result:
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ ↑(φ n) = ↑n * ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)

Proof state:
n : ℕ
⊢ ↑(φ n) = ↑n * ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)

Tactic:
by_cases hn : n = 0

Result:
case pos
n : ℕ
hn : n = 0
⊢ ↑(φ n) = ↑n * ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)

case neg
n : ℕ
hn : ¬n = 0
⊢ ↑(φ n) = ↑n * ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)

Proof state:
case pos
n : ℕ
hn : n = 0
⊢ ↑(φ n) = ↑n * ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)

Tactic:
simp [hn]

Result:
no goals

Proof state:
n : ℕ
hn : ¬n = 0
⊢ ↑n ≠ 0

Tactic:
simp [hn]

Result:
no goals

Proof state:
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ ↑(φ n) = ↑n * ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)

Tactic:
have hpQ : (∏ p ∈ n.primeFactors, (p : ℚ)) ≠ 0 := by
  rw [← cast_prod, cast_ne_zero, ← zero_lt_iff, prod_primeFactors_prod_factorization]
  exact prod_pos fun p hp => pos_of_mem_primeFactors hp

Result:
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0
⊢ ↑(φ n) = ↑n * ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)

Proof state:
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ ∏ p ∈ n.primeFactors, ↑p ≠ 0

Tactic:
rw [← cast_prod, cast_ne_zero, ← zero_lt_iff, prod_primeFactors_prod_factorization]

Result:
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ 0 < n.factorization.prod fun p x => p