awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
pos : ∀ (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 : ℚ)⁻¹)
have neg : ∀ (hn : ¬n = 0), (↑(φ n) : ℚ) = HMul.hMul (α := ℚ) (↑n : ℚ) (∏ p ∈ n.primeFactors, HSub.hSub (α := ℚ) 1 (↑p : ℚ)⁻¹)
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
n : ℕ
hn : ¬n = 0
⊢ (↑(φ n) : ℚ) = HMul.hMul (α := ℚ) (↑n : ℚ) (∏ p ∈ n.primeFactors, HSub.hSub (α := ℚ) 1 (↑p : ℚ)⁻¹)
have hn' : Ne (α := ℚ) (↑n : ℚ) 0
Tactic: have hn' : (n : ℚ) ≠ 0 := by simp [hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : ¬n = 0
hn' : Ne (α := ℚ) (↑n : ℚ) 0
⊢ Ne (α := ℚ) (∏ p ∈ n.primeFactors, (↑p : ℚ)) 0
have rw : LT.lt (α := ℕ) 0 (n.factorization.prod fun (p x : ℕ) ↦ p)
Tactic: rw [← cast_prod, cast_ne_zero, ← zero_lt_iff, prod_primeFactors_prod_factorization]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
n : ℕ
hn : ¬n = 0
hn' : Ne (α := ℚ) (↑n : ℚ) 0
⊢ (↑(φ n) : ℚ) = HMul.hMul (α := ℚ) (↑n : ℚ) (∏ p ∈ n.primeFactors, HSub.hSub (α := ℚ) 1 (↑p : ℚ)⁻¹)
have hpQ : 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
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : ¬n = 0
hn' : Ne (α := ℚ) (↑n : ℚ) 0
hpQ : Ne (α := ℚ) (∏ p ∈ n.primeFactors, (↑p : ℚ)) 0
⊢ (↑(φ n) : ℚ) = HMul.hMul (α := ℚ) (↑n : ℚ) (∏ p ∈ n.primeFactors, HSub.hSub (α := ℚ) 1 (↑p : ℚ)⁻¹)
have neg : Eq (α := ℚ) (∏ i ∈ n.primeFactors, (↑(i - 1) : ℚ)) (∏ x ∈ n.primeFactors, HSub.hSub (α := ℚ) 1 (↑x : ℚ)⁻¹ * (↑x : ℚ))
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]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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 : ℚ))
have neg : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (↑(p - 1) : ℚ) = HSub.hSub (α := ℚ) 1 (↑p : ℚ)⁻¹ * (↑p : ℚ)
Tactic: refine prod_congr rfl fun p hp => ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
n : ℕ
hn : ¬n = 0
hn' : Ne (α := ℚ) (↑n : ℚ) 0
hpQ : Ne (α := ℚ) (∏ p ∈ n.primeFactors, (↑p : ℚ)) 0
p : ℕ
hp : p ∈ n.primeFactors
⊢ (↑(p - 1) : ℚ) = HSub.hSub (α := ℚ) 1 (↑p : ℚ)⁻¹ * (↑p : ℚ)
have hp₁ : 0 < p
Tactic: have hp := pos_of_mem_primeFactorsList (List.mem_toFinset.mp hp)
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
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
⊢ (↑(p - 1) : ℚ) = HSub.hSub (α := ℚ) 1 (↑p : ℚ)⁻¹ * (↑p : ℚ)
have hp' : Ne (α := ℚ) (↑p : ℚ) 0
Tactic: have hp' : (p : ℚ) ≠ 0 := cast_ne_zero.mpr hp.ne.symm
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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
⊢ (↑(p - 1) : ℚ) = HSub.hSub (α := ℚ) 1 (↑p : ℚ)⁻¹ * (↑p : ℚ)
have neg : (↑(p - 1) : ℚ) = HMul.hMul (α := ℚ) 1 (↑p : ℚ) - HMul.hMul (α := ℚ) (↑p : ℚ)⁻¹ (↑p : ℚ)
Tactic: rw [sub_mul, one_mul, mul_comm, mul_inv_cancel₀ hp', cast_pred hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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 : ℚ)
⊢ (↑(p - 1) : ℚ) = HSub.hSub (α := ℚ) 1 (↑p : ℚ)⁻¹ * (↑p : ℚ)
have neg₁ : (↑(p - 1) : ℚ) = (↑p : ℚ) - HMul.hMul (α := ℚ) (↑p : ℚ)⁻¹ (↑p : ℚ)
Tactic: rw [sub_mul, one_mul, mul_comm, mul_inv_cancel₀ hp', cast_pred hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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 : ℚ)
⊢ (↑(p - 1) : ℚ) = HSub.hSub (α := ℚ) 1 (↑p : ℚ)⁻¹ * (↑p : ℚ)
have neg₂ : (↑(p - 1) : ℚ) = (↑p : ℚ) - HMul.hMul (α := ℚ) (↑p : ℚ) (↑p : ℚ)⁻¹
Tactic: rw [sub_mul, one_mul, mul_comm, mul_inv_cancel₀ hp', cast_pred hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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 : ℚ)⁻¹
⊢ (↑(p - 1) : ℚ) = HSub.hSub (α := ℚ) 1 (↑p : ℚ)⁻¹ * (↑p : ℚ)
have neg₃ : (↑(p - 1) : ℚ) = HSub.hSub (α := ℚ) (↑p : ℚ) 1
Tactic: rw [sub_mul, one_mul, mul_comm, mul_inv_cancel₀ hp', cast_pred hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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
⊢ (↑(p - 1) : ℚ) = HSub.hSub (α := ℚ) 1 (↑p : ℚ)⁻¹ * (↑p : ℚ)
have neg₄ : HSub.hSub (α := ℚ) (↑p : ℚ) 1 = HSub.hSub (α := ℚ) (↑p : ℚ) 1
Tactic: rw [sub_mul, one_mul, mul_comm, mul_inv_cancel₀ hp', cast_pred hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
⊢ a1 / b1 * (a2 / b2) * (c1 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
have e_a : a1 / b1 * (a2 / b2) = a1 * a2 / (b1 * b2)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
⊢ a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
have a1₁ : a1 / b1 * c1 * (a2 / b2 * c2) = a1 / b1 * (a2 / 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
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
have a1₂ : a1 / b1 * (a2 / b2) * (c1 * 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
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
a b : ℕ
⊢ φ (a.gcd b) * φ (a * b) = φ a * φ b * a.gcd b
have shuffle : ∀ (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
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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)
⊢ φ (a.gcd b) * φ (a * b) = φ a * φ b * a.gcd b
have 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
Tactic: simp only [totient_eq_div_primeFactors_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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)
⊢ ((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
have 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
Tactic: rw [shuffle, shuffle]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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.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
have a₁ : ∏ p ∈ a.primeFactors, p ∣ a
Tactic: rw [shuffle, shuffle]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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.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
have a₂ : ∏ p ∈ b.primeFactors, p ∣ b
Tactic: rw [shuffle, shuffle]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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.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
have a₃ : ∏ p ∈ (a.gcd b).primeFactors, p ∣ a.gcd b
Tactic: rw [shuffle, shuffle]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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.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
have a₄ : ∏ p ∈ (a * b).primeFactors, p ∣ a * b
Tactic: rw [shuffle, shuffle]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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)
⊢ 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
have 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
Tactic: simp only [prod_primeFactors_gcd_mul_prod_primeFactors_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
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)
⊢ 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
have H : HMul.hMul (α := ℕ) (∏ p ∈ a.primeFactors, p) (∏ p ∈ b.primeFactors, p) ∣ a * b
Tactic: rw [eq_comm, mul_comm, ← mul_assoc, ← Nat.mul_div_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a b : ℕ
d : ℕ := a.gcd b
⊢ φ a * φ b ≤ φ (a * b)
have inl : φ 0 * φ b ≤ φ (0 * b)
Tactic: rcases eq_zero_or_pos a with (rfl | ha0)
Cleared hypotheses: a, d
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a b : ℕ
d : ℕ := a.gcd b
inl : φ 0 * φ b ≤ φ (0 * b)
⊢ φ a * φ b ≤ φ (a * b)
have inr : ∀ (ha0 : a > 0), φ a * φ b ≤ φ (a * b)
Tactic: rcases eq_zero_or_pos a with (rfl | ha0)
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
a b : ℕ
d : ℕ := a.gcd b
ha0 : a > 0
⊢ φ a * φ b ≤ φ (a * b)
have hd0 : 0 < d
Tactic: have hd0 : 0 < d := Nat.gcd_pos_of_pos_left _ ha0
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a b : ℕ
d : ℕ := a.gcd b
ha0 : a > 0
hd0 : 0 < d
⊢ φ a * φ b ≤ φ (a * b)
have apply : φ a * φ b * d ≤ φ (a * b) * d
Tactic: apply le_of_mul_le_mul_right _ hd0
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a b : ℕ
d : ℕ := a.gcd b
ha0 : a > 0
hd0 : 0 < d
⊢ φ a * φ b * d ≤ φ (a * b) * d
have grw : φ (a.gcd b) * φ (a * b) ≤ φ (a * b) * d
Tactic: grw [← totient_gcd_mul_totient_mul a b, mul_comm, d.totient_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a b : ℕ
d : ℕ := a.gcd b
ha0 : a > 0
hd0 : 0 < d
grw : φ (a.gcd b) * φ (a * b) ≤ φ (a * b) * d
⊢ φ a * φ b * d ≤ φ (a * b) * d
have grw₁ : φ (a * b) * φ (a.gcd b) ≤ φ (a * b) * d
Tactic: grw [← totient_gcd_mul_totient_mul a b, mul_comm, d.totient_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a b : ℕ
d : ℕ := a.gcd b
ha0 : a > 0
hd0 : 0 < d
grw : φ (a.gcd b) * φ (a * b) ≤ φ (a * b) * d
grw₁ : φ (a * b) * φ (a.gcd b) ≤ φ (a * b) * d
⊢ φ a * φ b * d ≤ φ (a * b) * d
have grw₂ : φ (a * b) * d ≤ φ (a * b) * d
Tactic: grw [← totient_gcd_mul_totient_mul a b, mul_comm, d.totient_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a b : ℕ
h : a ∣ b
⊢ φ a ∣ φ b
have inl : ∀ (h : 0 ∣ b), φ 0 ∣ φ b
Tactic: rcases eq_or_ne a 0 with (rfl | ha0)
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a b : ℕ
h : a ∣ b
inl : ∀ (h : 0 ∣ b), φ 0 ∣ φ b
⊢ φ a ∣ φ b
have inr : ∀ (ha0 : a ≠ 0), φ a ∣ φ b
Tactic: rcases eq_or_ne a 0 with (rfl | ha0)
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
⊢ φ a ∣ φ b
have inr : ∀ (h : a ∣ 0), φ a ∣ φ 0
Tactic: rcases eq_or_ne b 0 with (rfl | hb0)
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
inr : ∀ (h : a ∣ 0), φ a ∣ φ 0
⊢ φ a ∣ φ b
have inr₁ : ∀ (hb0 : b ≠ 0), φ a ∣ φ b
Tactic: rcases eq_or_ne b 0 with (rfl | hb0)
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ φ a ∣ φ b
have hab' : a.primeFactors ⊆ b.primeFactors
Tactic: have hab' := primeFactors_mono h hb0
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : a.primeFactors ⊆ b.primeFactors
⊢ φ a ∣ φ b
have inr : Dvd.dvd (α := ℕ) (a.factorization.prod fun (p k : ℕ) ↦ p ^ (k - 1) * (p - 1))
  (b.factorization.prod fun (p k : ℕ) ↦ p ^ (k - 1) * (p - 1))
Tactic: rw [totient_eq_prod_factorization ha0, totient_eq_prod_factorization hb0]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : a.primeFactors ⊆ b.primeFactors
⊢ Dvd.dvd (α := ℕ) (a.factorization.prod fun (p k : ℕ) ↦ p ^ (k - 1) * (p - 1))
    (b.factorization.prod fun (p k : ℕ) ↦ p ^ (k - 1) * (p - 1))
have inr : ∀ p ∈ a.factorization.support,
  p ^ HSub.hSub (α := ℕ) (β := ℕ) ((a.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ) ∣
    p ^ HSub.hSub (α := ℕ) (β := ℕ) ((b.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
Tactic: refine Finsupp.prod_dvd_prod_of_subset_of_dvd hab' fun p _ => mul_dvd_mul ?_ dvd_rfl
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
p n : ℕ
hp : Prime p
h : p ∣ n
⊢ φ (p * n) = p * φ n
have h1 : φ (p.gcd n) * φ (p * n) = φ p * φ n * p.gcd n
Tactic: have h1 := totient_gcd_mul_totient_mul p n
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
p n : ℕ
hp : Prime p
h : p ∣ n
h1 : φ (p.gcd n) * φ (p * n) = φ p * φ n * p.gcd n
⊢ φ (p * n) = p * φ n
have h1₁ : φ p * φ (p * n) = φ p * (φ n * p)
Tactic: rw [gcd_eq_left h, mul_assoc] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ φ (p * n) = (p - 1) * φ n
have rw : p.Coprime n
Tactic: rw [totient_mul _, totient_prime hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : Odd n
⊢ φ (2 * n) = φ n
have rw : HSub.hSub (α := ℕ) 2 1 * φ n = φ n
Tactic: rw [totient_mul_of_prime_of_not_dvd prime_two hn.not_two_dvd_nat, Nat.add_one_sub_one 1, one_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
n : ℕ
hn : Odd n
rw : HSub.hSub (α := ℕ) 2 1 * φ n = φ n
rw₁ : 1 * φ n = φ n
⊢ φ (2 * n) = φ n
have rw₂ : φ n = φ n
Tactic: rw [totient_mul_of_prime_of_not_dvd prime_two hn.not_two_dvd_nat, Nat.add_one_sub_one 1, one_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a b : ℕ
h : a ∣ b
h' : φ a = φ b
⊢ a = b ∨ 2 * a = b
have pos : ∀ (ha : a = 0), a = b ∨ 2 * a = b
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a b : ℕ
h : a ∣ b
h' : φ a = φ b
pos : ∀ (ha : a = 0), a = b ∨ 2 * a = b
⊢ a = b ∨ 2 * a = b
have neg : ∀ (ha : ¬a = 0), a = b ∨ 2 * a = b
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : a = 0
⊢ a = b ∨ 2 * a = b
have h'₁ : b = 0
Tactic: rw [ha, totient_zero, eq_comm, totient_eq_zero] at h'
Cleared hypotheses: h', ha
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : ¬a = 0
⊢ a = b ∨ 2 * a = b
have pos : ∀ (hb : b = 0), a = b ∨ 2 * a = b
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : ¬a = 0
pos : ∀ (hb : b = 0), a = b ∨ 2 * a = b
⊢ a = b ∨ 2 * a = b
have neg : ∀ (hb : ¬b = 0), a = b ∨ 2 * a = b
Tactic: by_cases hb : b = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : ¬a = 0
hb : b = 0
⊢ a = b ∨ 2 * a = b
have h'₁ : a = 0
Tactic: rw [hb, totient_zero, totient_eq_zero] at h'
Cleared hypotheses: h', ha, hb
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : ¬a = 0
hb : ¬b = 0
⊢ a = b ∨ 2 * a = b
have neg : ∀ (c : ℕ) (h' : φ a = φ (a * c)) (hb : ¬a * c = 0), a = a * c ∨ 2 * a = a * c
Tactic: obtain ⟨c, rfl⟩ := h
Cleared hypotheses: b, h, h', hb
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (hypothesis)
Goal:
a : ℕ
ha : ¬a = 0
c : ℕ
h' : φ a = φ (a * c)
hb : ¬a * c = 0
this : a.Coprime c
⊢ a = a * c ∨ 2 * a = a * c
have h'₁ : c = 1 ∨ c = 2
Tactic: rw [totient_mul this, eq_comm, mul_eq_left (totient_eq_zero.not.mpr ha),
      totient_eq_one_iff] at h'
Cleared hypotheses: h', hb, this
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a : ℕ
ha : ¬a = 0
c : ℕ
h' : c = 1 ∨ c = 2
hb : ¬a * c = 0
this : a.Coprime c
⊢ a = a * c ∨ 2 * a = a * c
have inl : ∀ (hb : ¬a * 1 = 0) (this : a.Coprime 1), a = a * 1 ∨ 2 * a = a * 1
Tactic: obtain rfl | rfl := h'
Cleared hypotheses: c, h', hb, this
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a : ℕ
ha : ¬a = 0
c : ℕ
h' : c = 1 ∨ c = 2
hb : ¬a * c = 0
this : a.Coprime c
inl : ∀ (hb : ¬a * 1 = 0) (this : a.Coprime 1), a = a * 1 ∨ 2 * a = a * 1
⊢ a = a * c ∨ 2 * a = a * c
have inr : ∀ (hb : ¬a * 2 = 0) (this : a.Coprime 2), a = a * 2 ∨ 2 * a = a * 2
Tactic: obtain rfl | rfl := h'
Cleared hypotheses: c, h', hb, this
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a : ℕ
ha : ¬a = 0
c : ℕ
h' : φ a = φ (a * c)
hb : ¬a * c = 0
⊢ a = a * c ∨ 2 * a = a * c
have neg : a.Coprime c
Tactic: suffices a.Coprime c by
    rw [totient_mul this, eq_comm, mul_eq_left (totient_eq_zero.not.mpr ha),
      totient_eq_one_iff] at h'
    obtain rfl | rfl := h'
    · simp
    · simp [mul_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Totient (goal)
Goal:
a : ℕ
ha : ¬a = 0
c : ℕ
h' : φ a = φ (a * c)
hb : ¬a * c = 0
⊢ a.Coprime c
have neg : ∀ (p : ℕ) (hp : Prime p) (hap : p ∣ a), ¬p ∣ c
Tactic: refine coprime_of_dvd fun p hp hap ↦ ?_