a b : ℕ
d : ℕ := gcd a b
⊢ φ a * φ b ≤ φ (a * b)
a b : ℕ
⊢ φ a * φ b ≤ φ (a * b)
let d := a.gcd b
case inl
b : ℕ
d : ℕ := gcd 0 b
⊢ φ 0 * φ b ≤ φ (0 * b)

case inr
a b : ℕ
d : ℕ := gcd a b
ha0 : 0 < a
⊢ φ a * φ b ≤ φ (a * b)
a b : ℕ
d : ℕ := gcd a b
⊢ φ a * φ b ≤ φ (a * b)
rcases(zero_le a).eq_or_lt with (rfl | ha0)
case inr
a b : ℕ
d : ℕ := gcd a b
ha0 : 0 < a
hd0 : 0 < d
⊢ φ a * φ b ≤ φ (a * b)
case inr
a b : ℕ
d : ℕ := gcd a b
ha0 : 0 < a
⊢ φ a * φ b ≤ φ (a * b)
have hd0 : 0 < d := Nat.gcd_pos_of_pos_left _ ha0
a b : ℕ
d : ℕ := gcd a b
ha0 : 0 < a
hd0 : 0 < d
⊢ φ a * φ b * d ≤ φ (a * b) * d
case inr
a b : ℕ
d : ℕ := gcd a b
ha0 : 0 < a
hd0 : 0 < d
⊢ φ a * φ b ≤ φ (a * b)
apply le_of_mul_le_mul_right _ hd0
a b : ℕ
d : ℕ := gcd a b
ha0 : 0 < a
hd0 : 0 < d
⊢ φ (a * b) * φ (gcd a b) ≤ φ (a * b) * d
a b : ℕ
d : ℕ := gcd a b
ha0 : 0 < a
hd0 : 0 < d
⊢ φ a * φ b * d ≤ φ (a * b) * d
rw [← totient_gcd_mul_totient_mul a b, mul_comm]
no goals
a b : ℕ
d : ℕ := gcd a b
ha0 : 0 < a
hd0 : 0 < d
⊢ φ (a * b) * φ (gcd a b) ≤ φ (a * b) * d
apply mul_le_mul_left' (Nat.totient_le d)
no goals
case inl
b : ℕ
d : ℕ := gcd 0 b
⊢ φ 0 * φ b ≤ φ (0 * b)
simp