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)
⊢ φ (gcd a b) * φ (a * b) = φ a * φ b * gcd a b
a b : ℕ
⊢ φ (gcd a b) * φ (a * b) = φ a * φ b * gcd a 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) := 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
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)
⊢ ((gcd a b / ∏ p in List.toFinset (factors (gcd a b)), p) * ∏ p in List.toFinset (factors (gcd a b)), (p - 1)) *
      ((a * b / ∏ p in List.toFinset (factors (a * b)), p) * ∏ p in List.toFinset (factors (a * b)), (p - 1)) =
    ((a / ∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors a), (p - 1)) *
        ((b / ∏ p in List.toFinset (factors b), p) * ∏ p in List.toFinset (factors b), (p - 1)) *
      gcd a b
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)
⊢ φ (gcd a b) * φ (a * b) = φ a * φ b * gcd a b
simp only [totient_eq_div_factors_mul]
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)
⊢ gcd a b * (a * b) / ((∏ p in List.toFinset (factors (gcd a b)), p) * ∏ p in List.toFinset (factors (a * b)), p) *
      ((∏ p in List.toFinset (factors (gcd a b)), (p - 1)) * ∏ p in List.toFinset (factors (a * b)), (p - 1)) =
    a * b / ((∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p) *
        ((∏ p in List.toFinset (factors a), (p - 1)) * ∏ p in List.toFinset (factors b), (p - 1)) *
      gcd a b

case a
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 in List.toFinset (factors a), p ∣ a

case a
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 in List.toFinset (factors b), p ∣ b

case a
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 in List.toFinset (factors (gcd a b)), p ∣ gcd a b

case a
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 in List.toFinset (factors (a * b)), p ∣ a * b
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)
⊢ ((gcd a b / ∏ p in List.toFinset (factors (gcd a b)), p) * ∏ p in List.toFinset (factors (gcd a b)), (p - 1)) *
      ((a * b / ∏ p in List.toFinset (factors (a * b)), p) * ∏ p in List.toFinset (factors (a * b)), (p - 1)) =
    ((a / ∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors a), (p - 1)) *
        ((b / ∏ p in List.toFinset (factors b), p) * ∏ p in List.toFinset (factors b), (p - 1)) *
      gcd a b
rw [shuffle, shuffle]
case a
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 in List.toFinset (factors a), p ∣ a

case a
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 in List.toFinset (factors b), p ∣ b

case a
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 in List.toFinset (factors (gcd a b)), p ∣ gcd a b

case a
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 in List.toFinset (factors (a * b)), p ∣ a * b

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)
⊢ gcd a b * (a * b) / ((∏ p in List.toFinset (factors (gcd a b)), p) * ∏ p in List.toFinset (factors (a * b)), p) *
      ((∏ p in List.toFinset (factors (gcd a b)), (p - 1)) * ∏ p in List.toFinset (factors (a * b)), (p - 1)) =
    a * b / ((∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p) *
        ((∏ p in List.toFinset (factors a), (p - 1)) * ∏ p in List.toFinset (factors b), (p - 1)) *
      gcd a b
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)
⊢ gcd a b * (a * b) / ((∏ p in List.toFinset (factors (gcd a b)), p) * ∏ p in List.toFinset (factors (a * b)), p) *
      ((∏ p in List.toFinset (factors (gcd a b)), (p - 1)) * ∏ p in List.toFinset (factors (a * b)), (p - 1)) =
    a * b / ((∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p) *
        ((∏ p in List.toFinset (factors a), (p - 1)) * ∏ p in List.toFinset (factors b), (p - 1)) *
      gcd a b

case a
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 in List.toFinset (factors a), p ∣ a

case a
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 in List.toFinset (factors b), p ∣ b

case a
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 in List.toFinset (factors (gcd a b)), p ∣ gcd a b

case a
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 in List.toFinset (factors (a * b)), p ∣ a * b
rotate_left
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)
⊢ gcd a b * (a * b) / ((∏ p in List.toFinset (factors (gcd a b)), p) * ∏ p in List.toFinset (factors (a * b)), p) *
      ((∏ p in List.toFinset (factors (gcd a b)), (p - 1)) * ∏ p in List.toFinset (factors (a * b)), (p - 1)) =
    a * b / ((∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p) *
        ((∏ p in List.toFinset (factors a), (p - 1)) * ∏ p in List.toFinset (factors b), (p - 1)) *
      gcd a b
case a
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 in List.toFinset (factors a), p ∣ a

case a
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 in List.toFinset (factors b), p ∣ b

case a
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 in List.toFinset (factors (gcd a b)), p ∣ gcd a b

case a
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 in List.toFinset (factors (a * b)), p ∣ a * b

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)
⊢ gcd a b * (a * b) / ((∏ p in List.toFinset (factors (gcd a b)), p) * ∏ p in List.toFinset (factors (a * b)), p) *
      ((∏ p in List.toFinset (factors (gcd a b)), (p - 1)) * ∏ p in List.toFinset (factors (a * b)), (p - 1)) =
    a * b / ((∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p) *
        ((∏ p in List.toFinset (factors a), (p - 1)) * ∏ p in List.toFinset (factors b), (p - 1)) *
      gcd a b
repeat' apply prod_prime_factors_dvd
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)
a b : ℕ
⊢ ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
intro a1 a2 b1 b2 c1 c2 h1 h2
no goals
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)
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
no goals
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)
apply mul_mul_mul_comm
case e_a
a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
⊢ a1 / b1 * (a2 / b2) = a1 * a2 / (b1 * b2)
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)
congr 1
no goals
case e_a
a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
⊢ a1 / b1 * (a2 / b2) = a1 * a2 / (b1 * b2)
exact div_mul_div_comm h1 h2
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)
⊢ gcd a b * (a * b) / ((∏ p in List.toFinset (factors (gcd a b)), p) * ∏ p in List.toFinset (factors (a * b)), p) *
      ((∏ p in List.toFinset (factors (gcd a b)), (p - 1)) * ∏ p in List.toFinset (factors (a * b)), (p - 1)) =
    a * b / ((∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p) *
        ((∏ p in List.toFinset (factors a), (p - 1)) * ∏ p in List.toFinset (factors b), (p - 1)) *
      gcd a b
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)
⊢ gcd a b * (a * b) / ((∏ p in List.toFinset (factors (gcd a b)), p) * ∏ p in List.toFinset (factors (a * b)), p) *
      ((∏ p in List.toFinset (factors (gcd a b)), (p - 1)) * ∏ p in List.toFinset (factors (a * b)), (p - 1)) =
    a * b / ((∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p) *
        ((∏ p in List.toFinset (factors a), (p - 1)) * ∏ p in List.toFinset (factors b), (p - 1)) *
      gcd a b
apply prod_prime_factors_dvd
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)
⊢ gcd a b * (a * b) / ((∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p) *
      ((∏ p in List.toFinset (factors a), (p - 1)) * ∏ p in List.toFinset (factors b), (p - 1)) =
    a * b / ((∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p) *
        ((∏ p in List.toFinset (factors a), (p - 1)) * ∏ p in List.toFinset (factors b), (p - 1)) *
      gcd a b
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)
⊢ gcd a b * (a * b) / ((∏ p in List.toFinset (factors (gcd a b)), p) * ∏ p in List.toFinset (factors (a * b)), p) *
      ((∏ p in List.toFinset (factors (gcd a b)), (p - 1)) * ∏ p in List.toFinset (factors (a * b)), (p - 1)) =
    a * b / ((∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p) *
        ((∏ p in List.toFinset (factors a), (p - 1)) * ∏ p in List.toFinset (factors b), (p - 1)) *
      gcd a b
simp only [prod_factors_gcd_mul_prod_factors_mul]
case H
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 in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p ∣ a * b
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)
⊢ gcd a b * (a * b) / ((∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p) *
      ((∏ p in List.toFinset (factors a), (p - 1)) * ∏ p in List.toFinset (factors b), (p - 1)) =
    a * b / ((∏ p in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p) *
        ((∏ p in List.toFinset (factors a), (p - 1)) * ∏ p in List.toFinset (factors b), (p - 1)) *
      gcd a b
rw [eq_comm, mul_comm, ← mul_assoc, ← Nat.mul_div_assoc]
no goals
case H
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 in List.toFinset (factors a), p) * ∏ p in List.toFinset (factors b), p ∣ a * b
exact mul_dvd_mul (prod_prime_factors_dvd a) (prod_prime_factors_dvd b)