awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
zero : Odd (φ 0) ↔ Eq (α := ℕ) 0 1 ∨ Eq (α := ℕ) 0 2
succ : Odd (φ (HAdd.hAdd (α := ℕ) 0 1)) ↔ HAdd.hAdd (α := ℕ) 0 1 = 1 ∨ HAdd.hAdd (α := ℕ) 0 1 = 2
succ₁ : Odd (φ (HAdd.hAdd (α := ℕ) 0 1 + 1)) ↔ HAdd.hAdd (α := ℕ) 0 1 + 1 = 1 ∨ HAdd.hAdd (α := ℕ) 0 1 + 1 = 2
succ₂ : ∀ (n : ℕ), Odd (φ (n + 1 + 1 + 1)) ↔ n + 1 + 1 + 1 = 1 ∨ n + 1 + 1 + 1 = 2
⊢ Odd (φ n) ↔ n = 1 ∨ n = 2

Tactic:
rcases n with _ | _ | _ | _
-- Module: Mathlib.Data.Nat.Totient
Goal:
⊢ Odd (φ 0) ↔ Eq (α := ℕ) 0 1 ∨ Eq (α := ℕ) 0 2

Tactic:
simp [Nat.totient_even]

Premises used: Nat.totient_even
-- Module: Mathlib.Data.Nat.Totient
Goal:
⊢ Odd (φ (HAdd.hAdd (α := ℕ) 0 1)) ↔ HAdd.hAdd (α := ℕ) 0 1 = 1 ∨ HAdd.hAdd (α := ℕ) 0 1 = 2

Tactic:
simp [Nat.totient_even]

Premises used: Nat.totient_even
-- Module: Mathlib.Data.Nat.Totient
Goal:
⊢ Odd (φ (HAdd.hAdd (α := ℕ) 0 1 + 1)) ↔ HAdd.hAdd (α := ℕ) 0 1 + 1 = 1 ∨ HAdd.hAdd (α := ℕ) 0 1 + 1 = 2

Tactic:
simp [Nat.totient_even]

Premises used: Nat.totient_even
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
⊢ Odd (φ (n + 1 + 1 + 1)) ↔ n + 1 + 1 + 1 = 1 ∨ n + 1 + 1 + 1 = 2

Tactic:
simp [Nat.totient_even]

Premises used: Nat.totient_even
-- Module: Mathlib.Data.Nat.Totient
Goal:
⊢ φ 0 = 1 ↔ Eq (α := ℕ) 0 1 ∨ Eq (α := ℕ) 0 2

Tactic:
simp
-- Module: Mathlib.Data.Nat.Totient
Goal:
⊢ φ 1 = 1 ↔ Eq (α := ℕ) 1 1 ∨ Eq (α := ℕ) 1 2

Tactic:
simp
-- Module: Mathlib.Data.Nat.Totient
Goal:
⊢ φ 2 = 1 ↔ Eq (α := ℕ) 2 1 ∨ Eq (α := ℕ) 2 2

Tactic:
simp
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
⊢ 3 ≤ n + 3

Tactic:
have : 3 ≤ n + 3 := le_add_self
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
this : 3 ≤ n + 3
simp : φ (n + 3) = 1 ↔ n + 3 = 2
⊢ φ (n + 3) = 1 ↔ n + 3 = 1 ∨ n + 3 = 2

Tactic:
simp only [succ_succ_ne_one, false_or]

Premises used: false_or, Nat.succ_succ_ne_one
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
this : 3 ≤ n + 3
⊢ φ (n + 3) = 1 ↔ n + 3 = 2

Tactic:
exact ⟨fun h => not_even_one.elim <| h ▸ totient_even this, by rintro ⟨⟩⟩
-- Module: Mathlib.Data.Nat.Totient
Goal:
a : ℕ
han : 0 < a
ha : φ a ≤ 1
inl : ∀ (han : LT.lt (α := ℕ) 0 1) (ha : φ 1 ≤ 1), Dvd.dvd (α := ℕ) 1 2
inr : ∀ (han : LT.lt (α := ℕ) 0 2) (ha : φ 2 ≤ 1), Dvd.dvd (α := ℕ) 2 2
⊢ a ∣ 2

Tactic:
rcases totient_eq_one_iff.mp <| le_antisymm ha <| totient_pos.2 han with rfl | rfl

Premises used: Iff.mpr, le_antisymm, Iff.mp, Nat.totient_pos, rfl, Nat.totient_eq_one_iff
-- Module: Mathlib.Data.Nat.Totient
Goal:
han : LT.lt (α := ℕ) 0 1
ha : φ 1 ≤ 1
⊢ Dvd.dvd (α := ℕ) 1 2

Tactic:
norm_num
-- Module: Mathlib.Data.Nat.Totient
Goal:
han : LT.lt (α := ℕ) 0 2
ha : φ 2 ≤ 1
⊢ Dvd.dvd (α := ℕ) 2 2

Tactic:
norm_num
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
⊢ Odd (φ n) ↔ φ n = 1

Tactic:
simp [Nat.odd_totient_iff, Nat.totient_eq_one_iff]

Premises used: Nat.odd_totient_iff, Nat.totient_eq_one_iff
-- Module: Mathlib.Data.Nat.Totient
Goal:
m n : ℕ
mp : (φ m).Coprime (φ n) → (m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2
mpr : (m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2 → (φ m).Coprime (φ n)
⊢ (φ m).Coprime (φ n) ↔ (m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2

Tactic:
constructor
-- Module: Mathlib.Data.Nat.Totient
Goal:
m n : ℕ
mp : ¬((m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2) → ¬(φ m).Coprime (φ n)
⊢ (φ m).Coprime (φ n) → (m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2

Tactic:
rw [← not_imp_not]

Premises used: not_imp_not
-- Module: Mathlib.Data.Nat.Totient
Goal:
m n : ℕ
mp : 2 ∣ φ m ∧ 2 ∣ φ n → ¬(φ m).Coprime (φ n)
⊢ ¬((m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2) → ¬(φ m).Coprime (φ n)

Tactic:
simp_rw [← odd_totient_iff, not_or, not_odd_iff_even, even_iff_two_dvd]

Premises used: Nat.odd_totient_iff, Nat.not_odd_iff_even, not_or, even_iff_two_dvd
-- Module: Mathlib.Data.Nat.Totient
Goal:
m n : ℕ
⊢ 2 ∣ φ m ∧ 2 ∣ φ n → ¬(φ m).Coprime (φ n)

Tactic:
fun h ↦ Nat.not_coprime_of_dvd_of_dvd one_lt_two h.1 h.2

Premises used: Nat.not_coprime_of_dvd_of_dvd, And.right, And.left, one_lt_two
-- Module: Mathlib.Data.Nat.Totient
Goal:
m n : ℕ
⊢ 2 ∣ φ m ∧ 2 ∣ φ n → ¬(φ m).Coprime (φ n)

Tactic:
exact fun h ↦ Nat.not_coprime_of_dvd_of_dvd one_lt_two h.1 h.2

Premises used: Nat.not_coprime_of_dvd_of_dvd, one_lt_two
-- Module: Mathlib.Data.Nat.Totient
Goal:
m n : ℕ
mpr : φ m = 1 ∨ φ n = 1 → (φ m).Coprime (φ n)
⊢ (m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2 → (φ m).Coprime (φ n)

Tactic:
simp_rw [← totient_eq_one_iff]

Premises used: Nat.totient_eq_one_iff
-- Module: Mathlib.Data.Nat.Totient
Goal:
m n : ℕ
h : φ m = 1
mpr : Coprime 1 (φ n)
⊢ (φ m).Coprime (φ n)

Tactic:
rw [h]
-- Module: Mathlib.Data.Nat.Totient
Goal:
m n : ℕ
h : φ n = 1
mpr : (φ m).Coprime 1
⊢ (φ m).Coprime (φ n)

Tactic:
rw [h]
-- Module: Mathlib.Data.Nat.Totient
Goal:
m n : ℕ
h : φ m = 1
⊢ Coprime 1 (φ n)

Tactic:
Nat.coprime_one_left _

Premises used: Nat.coprime_one_left
-- Module: Mathlib.Data.Nat.Totient
Goal:
m n : ℕ
h : φ n = 1
⊢ (φ m).Coprime 1

Tactic:
Nat.coprime_one_right _

Premises used: Nat.coprime_one_right
-- Module: Mathlib.Data.Nat.Totient
Goal:
m n : ℕ
h : φ m = 1
⊢ Coprime 1 (φ n)

Tactic:
exacts [Nat.coprime_one_left _, Nat.coprime_one_right _]

Premises used: Nat.coprime_one_left, Nat.coprime_one_right
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : n ≠ 0
rw :
  Eq (α := ℕ) (n.factorization.prod fun (p k : ℕ) ↦ φ (p ^ k))
    (n.factorization.prod fun (p k : ℕ) ↦ p ^ (k - 1) * (p - 1))
⊢ φ n = n.factorization.prod fun (p k : ℕ) ↦ p ^ (k - 1) * (p - 1)

Tactic:
rw [multiplicative_factorization φ (@totient_mul) totient_one hn]

Premises used: Nat.totient_mul, Nat.totient, Nat.multiplicative_factorization, Nat.totient_one
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : n ≠ 0
apply :
  ∀ x ∈ n.factorization.support,
    φ (HPow.hPow (β := ℕ) x ((n.factorization : (a : ℕ) → ℕ) x : ℕ)) =
      x ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) x : ℕ) (1 : ℕ) * (x - 1)
⊢ Eq (α := ℕ) (n.factorization.prod fun (p k : ℕ) ↦ φ (p ^ k))
    (n.factorization.prod fun (p k : ℕ) ↦ p ^ (k - 1) * (p - 1))

Tactic:
apply Finsupp.prod_congr _

Premises used: Finsupp.prod_congr
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ∈ n.factorization.support
⊢ LT.lt (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
have h := zero_lt_iff.mpr (Finsupp.mem_support_iff.mp hp)
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ∈ n.factorization.support
h : LT.lt (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
rw rw₁ :
  p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1) =
    p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1)
⊢ φ (HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ)) =
    p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1)

Tactic:
rw [totient_prime_pow (prime_of_mem_primeFactors hp) h]

Premises used: Nat.totient_prime_pow, Nat.prime_of_mem_primeFactors
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
pos : ∀ (hn : n = 0), φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)
neg : ∀ (hn : ¬n = 0), φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : n = 0
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
simp [hn]
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : ¬n = 0
neg :
  HMul.hMul (α := ℕ) (n.factorization.prod fun (p k : ℕ) ↦ p ^ (k - 1) * (p - 1)) (∏ p ∈ n.primeFactors, p) =
    n * ∏ p ∈ n.primeFactors, (p - 1)
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
rw [totient_eq_prod_factorization hn]

Premises used: Nat.totient_eq_prod_factorization
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : ¬n = 0
neg :
  HMul.hMul (α := ℕ) (n.factorization.prod fun (p k : ℕ) ↦ p ^ (k - 1) * (p - 1)) (∏ p ∈ n.primeFactors, p) =
    HMul.hMul (α := ℕ) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (∏ p ∈ n.primeFactors, (p - 1))
⊢ HMul.hMul (α := ℕ) (n.factorization.prod fun (p k : ℕ) ↦ p ^ (k - 1) * (p - 1)) (∏ p ∈ n.primeFactors, p) =
    n * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
nth_rw 3 [← prod_factorization_pow_eq_self hn]

Premises used: Nat.prod_factorization_pow_eq_self
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : ¬n = 0
neg :
  Eq (α := ℕ) (n.factorization.prod fun (a b : ℕ) ↦ a ^ (b - 1) * (a - 1) * a)
    (n.factorization.prod fun (a b : ℕ) ↦ a ^ b * (a - 1))
⊢ HMul.hMul (α := ℕ) (n.factorization.prod fun (p k : ℕ) ↦ p ^ (k - 1) * (p - 1)) (∏ p ∈ n.primeFactors, p) =
    HMul.hMul (α := ℕ) (n.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) (∏ p ∈ n.primeFactors, (p - 1))

Tactic:
simp only [prod_primeFactors_prod_factorization, ← Finsupp.prod_mul]

Premises used: Finsupp.prod_mul, Nat.prod_primeFactors_prod_factorization
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : ¬n = 0
⊢ Eq (α := ℕ) (n.factorization.prod fun (a b : ℕ) ↦ a ^ (b - 1) * (a - 1) * a)
    (n.factorization.prod fun (a b : ℕ) ↦ a ^ b * (a - 1))

Tactic:
Finsupp.prod_congr (M := ℕ) (N := ℕ) fun p hp => ?_

Premises used: Finsupp.prod_congr
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : ¬n = 0
neg :
  ∀ (p : ℕ) (hp : p ∈ n.factorization.support),
    p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1) * p =
      HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
⊢ Eq (α := ℕ) (n.factorization.prod fun (a b : ℕ) ↦ a ^ (b - 1) * (a - 1) * a)
    (n.factorization.prod fun (a b : ℕ) ↦ a ^ b * (a - 1))

Tactic:
refine Finsupp.prod_congr (M := ℕ) (N := ℕ) fun p hp => ?_

Premises used: Finsupp.prod_congr
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : ¬n = 0
p : ℕ
hp : p ∈ n.factorization.support
⊢ LT.lt (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rw [Finsupp.mem_support_iff, ← zero_lt_iff] at hp

Premises used: Finsupp.mem_support_iff, zero_lt_iff
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : ¬n = 0
p : ℕ
hp : LT.lt (α := ℕ) (0 : ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ)
neg :
  p * (p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1)) =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
neg₁ :
  p * p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1) =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
neg₂ :
  p ^ (HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)).succ * (p - 1) =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
neg₃ :
  p ^ (pred ((n.factorization : (a : ℕ) → ℕ) p)).succ * (p - 1) =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
neg₄ neg₅ :
  HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1) =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)
⊢ p ^ HSub.hSub (α := ℕ) (β := ℕ) ((n.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) * (p - 1) * p =
    HPow.hPow (β := ℕ) p ((n.factorization : (a : ℕ) → ℕ) p : ℕ) * (p - 1)

Tactic:
rw [mul_comm, ← mul_assoc, ← pow_succ', Nat.sub_one, Nat.succ_pred_eq_of_pos hp]

Premises used: Nat.pow_succ', Nat.succ_pred_eq_of_pos, mul_assoc, mul_comm, Nat.sub_one
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
rw : LT.lt (α := ℕ) 0 (∏ p ∈ n.primeFactors, p)
⊢ φ n = (n / ∏ p ∈ n.primeFactors, p) * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
rw [← mul_div_left n.totient, totient_mul_prod_primeFactors, mul_comm,
    Nat.mul_div_assoc _ (prod_primeFactors_dvd n), mul_comm]

Premises used: Nat.prod_primeFactors_dvd, Nat.totient, Nat.mul_div_left, mul_comm, Nat.mul_div_assoc, Nat.totient_mul_prod_primeFactors
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
⊢ LT.lt (α := ℕ) 0 (∏ p ∈ n.primeFactors, p)

Tactic:
prod_pos (fun p => pos_of_mem_primeFactors)

Premises used: Finset.prod_pos, Nat.pos_of_mem_primeFactors
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
⊢ LT.lt (α := ℕ) 0 (∏ p ∈ n.primeFactors, p)

Tactic:
exact prod_pos (fun p => pos_of_mem_primeFactors)

Premises used: Finset.prod_pos, Nat.pos_of_mem_primeFactors
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
pos : ∀ (hn : n = 0), (↑(φ n) : ℚ) = HMul.hMul (α := ℚ) (↑n : ℚ) (∏ p ∈ n.primeFactors, HSub.hSub (α := ℚ) 1 (↑p : ℚ)⁻¹)
neg :
  ∀ (hn : ¬n = 0), (↑(φ n) : ℚ) = HMul.hMul (α := ℚ) (↑n : ℚ) (∏ p ∈ n.primeFactors, HSub.hSub (α := ℚ) 1 (↑p : ℚ)⁻¹)
⊢ (↑(φ n) : ℚ) = HMul.hMul (α := ℚ) (↑n : ℚ) (∏ p ∈ n.primeFactors, HSub.hSub (α := ℚ) 1 (↑p : ℚ)⁻¹)

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : n = 0
⊢ (↑(φ n) : ℚ) = HMul.hMul (α := ℚ) (↑n : ℚ) (∏ p ∈ n.primeFactors, HSub.hSub (α := ℚ) 1 (↑p : ℚ)⁻¹)

Tactic:
simp [hn]
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : ¬n = 0
⊢ Ne (α := ℚ) (↑n : ℚ) 0

Tactic:
simp [hn]
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : ¬n = 0
⊢ Ne (α := ℚ) (↑n : ℚ) 0

Tactic:
have hn' : (n : ℚ) ≠ 0 := by simp [hn]
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : ¬n = 0
hn' : Ne (α := ℚ) (↑n : ℚ) 0
rw : LT.lt (α := ℕ) 0 (n.factorization.prod fun (p x : ℕ) ↦ p)
⊢ Ne (α := ℚ) (∏ p ∈ n.primeFactors, (↑p : ℚ)) 0

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

Premises used: Nat.cast_prod, Nat.prod_primeFactors_prod_factorization, zero_lt_iff, Nat.cast_ne_zero
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : ¬n = 0
hn' : Ne (α := ℚ) (↑n : ℚ) 0
⊢ LT.lt (α := ℕ) 0 (n.factorization.prod fun (p x : ℕ) ↦ p)

Tactic:
prod_pos fun p hp => pos_of_mem_primeFactors hp

Premises used: Finset.prod_pos, Finsupp.prod, Nat.pos_of_mem_primeFactors
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : ¬n = 0
hn' : Ne (α := ℚ) (↑n : ℚ) 0
⊢ LT.lt (α := ℕ) 0 (n.factorization.prod fun (p x : ℕ) ↦ p)

Tactic:
exact prod_pos fun p hp => pos_of_mem_primeFactors hp

Premises used: Finset.prod_pos, Nat.pos_of_mem_primeFactors
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : ¬n = 0
hn' : Ne (α := ℚ) (↑n : ℚ) 0
⊢ Ne (α := ℚ) (∏ p ∈ n.primeFactors, (↑p : ℚ)) 0

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
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : ¬n = 0
hn' : Ne (α := ℚ) (↑n : ℚ) 0
hpQ : Ne (α := ℚ) (∏ p ∈ n.primeFactors, (↑p : ℚ)) 0
neg :
  Eq (α := ℚ) (∏ i ∈ n.primeFactors, (↑(i - 1) : ℚ)) (∏ x ∈ n.primeFactors, HSub.hSub (α := ℚ) 1 (↑x : ℚ)⁻¹ * (↑x : ℚ))
⊢ (↑(φ n) : ℚ) = HMul.hMul (α := ℚ) (↑n : ℚ) (∏ p ∈ n.primeFactors, HSub.hSub (α := ℚ) 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]

Premises used: Finset.prod_mul_distrib, Nat.prod_primeFactors_dvd, Nat.cast_div_charZero, Nat.cast_prod, div_eq_iff, Nat.cast_mul, mul_comm_div, mul_right_inj', Nat.totient_eq_div_primeFactors_mul
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : ¬n = 0
hn' : Ne (α := ℚ) (↑n : ℚ) 0
hpQ : Ne (α := ℚ) (∏ p ∈ n.primeFactors, (↑p : ℚ)) 0
⊢ Eq (α := ℚ) (∏ i ∈ n.primeFactors, (↑(i - 1) : ℚ)) (∏ x ∈ n.primeFactors, HSub.hSub (α := ℚ) 1 (↑x : ℚ)⁻¹ * (↑x : ℚ))

Tactic:
prod_congr rfl fun p hp => ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : ¬n = 0
hn' : Ne (α := ℚ) (↑n : ℚ) 0
hpQ : Ne (α := ℚ) (∏ p ∈ n.primeFactors, (↑p : ℚ)) 0
neg : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (↑(p - 1) : ℚ) = HSub.hSub (α := ℚ) 1 (↑p : ℚ)⁻¹ * (↑p : ℚ)
⊢ Eq (α := ℚ) (∏ i ∈ n.primeFactors, (↑(i - 1) : ℚ)) (∏ x ∈ n.primeFactors, HSub.hSub (α := ℚ) 1 (↑x : ℚ)⁻¹ * (↑x : ℚ))

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

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : ¬n = 0
hn' : Ne (α := ℚ) (↑n : ℚ) 0
hpQ : Ne (α := ℚ) (∏ p ∈ n.primeFactors, (↑p : ℚ)) 0
p : ℕ
hp : p ∈ n.primeFactors
⊢ 0 < p

Tactic:
have hp := pos_of_mem_primeFactorsList (List.mem_toFinset.mp hp)
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : ¬n = 0
hn' : Ne (α := ℚ) (↑n : ℚ) 0
hpQ : Ne (α := ℚ) (∏ p ∈ n.primeFactors, (↑p : ℚ)) 0
p : ℕ
hp_1 : p ∈ n.primeFactors
hp : 0 < p
⊢ Ne (α := ℚ) (↑p : ℚ) 0

Tactic:
have hp' : (p : ℚ) ≠ 0 := cast_ne_zero.mpr hp.ne.symm
-- Module: Mathlib.Data.Nat.Totient
Goal:
n : ℕ
hn : ¬n = 0
hn' : Ne (α := ℚ) (↑n : ℚ) 0
hpQ : Ne (α := ℚ) (∏ p ∈ n.primeFactors, (↑p : ℚ)) 0
p : ℕ
hp_1 : p ∈ n.primeFactors
hp : 0 < p
hp' : Ne (α := ℚ) (↑p : ℚ) 0
neg : (↑(p - 1) : ℚ) = HMul.hMul (α := ℚ) 1 (↑p : ℚ) - HMul.hMul (α := ℚ) (↑p : ℚ)⁻¹ (↑p : ℚ)
neg₁ : (↑(p - 1) : ℚ) = (↑p : ℚ) - HMul.hMul (α := ℚ) (↑p : ℚ)⁻¹ (↑p : ℚ)
neg₂ : (↑(p - 1) : ℚ) = (↑p : ℚ) - HMul.hMul (α := ℚ) (↑p : ℚ) (↑p : ℚ)⁻¹
neg₃ : (↑(p - 1) : ℚ) = HSub.hSub (α := ℚ) (↑p : ℚ) 1
neg₄ neg₅ : HSub.hSub (α := ℚ) (↑p : ℚ) 1 = HSub.hSub (α := ℚ) (↑p : ℚ) 1
⊢ (↑(p - 1) : ℚ) = HSub.hSub (α := ℚ) 1 (↑p : ℚ)⁻¹ * (↑p : ℚ)

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

Premises used: mul_inv_cancel₀, Nat.cast_pred, sub_mul, mul_comm, one_mul
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
⊢ a1 / b1 * c1 * (a2 / b2 * c2) = a1 / b1 * (a2 / b2) * (c1 * c2)

Tactic:
apply mul_mul_mul_comm

Premises used: mul_mul_mul_comm
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
e_a : a1 / b1 * (a2 / b2) = a1 * a2 / (b1 * b2)
⊢ a1 / b1 * (a2 / b2) * (c1 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)

Tactic:
congr 1
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
⊢ a1 / b1 * (a2 / b2) = a1 * a2 / (b1 * b2)

Tactic:
div_mul_div_comm h1 h2

Premises used: Nat.div_mul_div_comm
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
⊢ a1 / b1 * (a2 / b2) = a1 * a2 / (b1 * b2)

Tactic:
exact div_mul_div_comm h1 h2

Premises used: Nat.div_mul_div_comm
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
a1₁ : a1 / b1 * c1 * (a2 / b2 * c2) = a1 / b1 * (a2 / b2) * (c1 * c2)
a1₂ : a1 / b1 * (a2 / b2) * (c1 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)

Tactic:
calc
      a1 / b1 * c1 * (a2 / b2 * c2) = a1 / b1 * (a2 / b2) * (c1 * c2) := by apply mul_mul_mul_comm
      _ = a1 * a2 / (b1 * b2) * (c1 * c2) := by
        congr 1
        exact div_mul_div_comm h1 h2

Premises used: HMul.hMul, HDiv.hDiv
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
⊢ ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)

Tactic:
have shuffle :
    ∀ a1 a2 b1 b2 c1 c2 : ℕ,
      b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2) := by
    intro a1 a2 b1 b2 c1 c2 h1 h2
    calc
      a1 / b1 * c1 * (a2 / b2 * c2) = a1 / b1 * (a2 / b2) * (c1 * c2) := by apply mul_mul_mul_comm
      _ = a1 * a2 / (b1 * b2) * (c1 * c2) := by
        congr 1
        exact div_mul_div_comm h1 h2
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
simp :
  ((a.gcd b / ∏ p ∈ (a.gcd b).primeFactors, p) * ∏ p ∈ (a.gcd b).primeFactors, (p - 1)) *
      ((a * b / ∏ p ∈ (a * b).primeFactors, p) * ∏ p ∈ (a * b).primeFactors, (p - 1)) =
    ((a / ∏ p ∈ a.primeFactors, p) * ∏ p ∈ a.primeFactors, (p - 1)) *
        ((b / ∏ p ∈ b.primeFactors, p) * ∏ p ∈ b.primeFactors, (p - 1)) *
      a.gcd b
⊢ φ (a.gcd b) * φ (a * b) = φ a * φ b * a.gcd b

Tactic:
simp only [totient_eq_div_primeFactors_mul]

Premises used: Nat.totient_eq_div_primeFactors_mul
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
rw :
  a.gcd b * (a * b) / HMul.hMul (α := ℕ) (∏ p ∈ (a.gcd b).primeFactors, p) (∏ p ∈ (a * b).primeFactors, p) *
      HMul.hMul (α := ℕ) (∏ p ∈ (a.gcd b).primeFactors, (p - 1)) (∏ p ∈ (a * b).primeFactors, (p - 1)) =
    a * b / HMul.hMul (α := ℕ) (∏ p ∈ a.primeFactors, p) (∏ p ∈ b.primeFactors, p) *
        HMul.hMul (α := ℕ) (∏ p ∈ a.primeFactors, (p - 1)) (∏ p ∈ b.primeFactors, (p - 1)) *
      a.gcd b
a₁ : ∏ p ∈ a.primeFactors, p ∣ a
a₂ : ∏ p ∈ b.primeFactors, p ∣ b
a₃ : ∏ p ∈ (a.gcd b).primeFactors, p ∣ a.gcd b
a₄ : ∏ p ∈ (a * b).primeFactors, p ∣ a * b
⊢ ((a.gcd b / ∏ p ∈ (a.gcd b).primeFactors, p) * ∏ p ∈ (a.gcd b).primeFactors, (p - 1)) *
      ((a * b / ∏ p ∈ (a * b).primeFactors, p) * ∏ p ∈ (a * b).primeFactors, (p - 1)) =
    ((a / ∏ p ∈ a.primeFactors, p) * ∏ p ∈ a.primeFactors, (p - 1)) *
        ((b / ∏ p ∈ b.primeFactors, p) * ∏ p ∈ b.primeFactors, (p - 1)) *
      a.gcd b

Tactic:
rw [shuffle, shuffle]
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ a.primeFactors, p ∣ a

Tactic:
apply prod_primeFactors_dvd

Premises used: Nat.prod_primeFactors_dvd
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ b.primeFactors, p ∣ b

Tactic:
apply prod_primeFactors_dvd

Premises used: Nat.prod_primeFactors_dvd
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ (a.gcd b).primeFactors, p ∣ a.gcd b

Tactic:
apply prod_primeFactors_dvd

Premises used: Nat.prod_primeFactors_dvd
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ (a * b).primeFactors, p ∣ a * b

Tactic:
apply prod_primeFactors_dvd

Premises used: Nat.prod_primeFactors_dvd
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
simp :
  a.gcd b * (a * b) / HMul.hMul (α := ℕ) (∏ p ∈ a.primeFactors, p) (∏ p ∈ b.primeFactors, p) *
      HMul.hMul (α := ℕ) (∏ p ∈ a.primeFactors, (p - 1)) (∏ p ∈ b.primeFactors, (p - 1)) =
    a * b / HMul.hMul (α := ℕ) (∏ p ∈ a.primeFactors, p) (∏ p ∈ b.primeFactors, p) *
        HMul.hMul (α := ℕ) (∏ p ∈ a.primeFactors, (p - 1)) (∏ p ∈ b.primeFactors, (p - 1)) *
      a.gcd b
⊢ a.gcd b * (a * b) / HMul.hMul (α := ℕ) (∏ p ∈ (a.gcd b).primeFactors, p) (∏ p ∈ (a * b).primeFactors, p) *
      HMul.hMul (α := ℕ) (∏ p ∈ (a.gcd b).primeFactors, (p - 1)) (∏ p ∈ (a * b).primeFactors, (p - 1)) =
    a * b / HMul.hMul (α := ℕ) (∏ p ∈ a.primeFactors, p) (∏ p ∈ b.primeFactors, p) *
        HMul.hMul (α := ℕ) (∏ p ∈ a.primeFactors, (p - 1)) (∏ p ∈ b.primeFactors, (p - 1)) *
      a.gcd b

Tactic:
simp only [prod_primeFactors_gcd_mul_prod_primeFactors_mul]

Premises used: Nat.prod_primeFactors_gcd_mul_prod_primeFactors_mul
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
H : HMul.hMul (α := ℕ) (∏ p ∈ a.primeFactors, p) (∏ p ∈ b.primeFactors, p) ∣ a * b
⊢ a.gcd b * (a * b) / HMul.hMul (α := ℕ) (∏ p ∈ a.primeFactors, p) (∏ p ∈ b.primeFactors, p) *
      HMul.hMul (α := ℕ) (∏ p ∈ a.primeFactors, (p - 1)) (∏ p ∈ b.primeFactors, (p - 1)) =
    a * b / HMul.hMul (α := ℕ) (∏ p ∈ a.primeFactors, p) (∏ p ∈ b.primeFactors, p) *
        HMul.hMul (α := ℕ) (∏ p ∈ a.primeFactors, (p - 1)) (∏ p ∈ b.primeFactors, (p - 1)) *
      a.gcd b

Tactic:
rw [eq_comm, mul_comm, ← mul_assoc, ← Nat.mul_div_assoc]

Premises used: mul_assoc, eq_comm, mul_comm, Nat.mul_div_assoc
-- Module: Mathlib.Data.Nat.Totient
Goal:
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ HMul.hMul (α := ℕ) (∏ p ∈ a.primeFactors, p) (∏ p ∈ b.primeFactors, p) ∣ a * b

Tactic:
mul_dvd_mul (prod_primeFactors_dvd a) (prod_primeFactors_dvd b)

Premises used: Nat.prod_primeFactors_dvd, mul_dvd_mul