R : Type ?u.592093
⊢ ↑μ 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → coprime m n → ↑μ (m * n) = ↑μ m * ↑μ n
R : Type ?u.592093
⊢ IsMultiplicative μ
rw [IsMultiplicative.iff_ne_zero]
R : Type ?u.592093
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
⊢ ↑μ (n * m) = ↑μ n * ↑μ m
R : Type ?u.592093
⊢ ↑μ 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → coprime m n → ↑μ (m * n) = ↑μ m * ↑μ n
refine' ⟨by simp, fun {n m} hn hm hnm => _⟩
R : Type ?u.592093
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
⊢ ↑{ toFun := fun n => if Squarefree n then (-1) ^ ↑Ω n else 0,
          map_zero' := (_ : (fun n => if Squarefree n then (-1) ^ ↑Ω n else 0) 0 = 0) }
      (n * m) =
    ↑{ toFun := fun n => if Squarefree n then (-1) ^ ↑Ω n else 0,
            map_zero' := (_ : (fun n => if Squarefree n then (-1) ^ ↑Ω n else 0) 0 = 0) }
        n *
      ↑{ toFun := fun n => if Squarefree n then (-1) ^ ↑Ω n else 0,
            map_zero' := (_ : (fun n => if Squarefree n then (-1) ^ ↑Ω n else 0) 0 = 0) }
        m
R : Type ?u.592093
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
⊢ ↑μ (n * m) = ↑μ n * ↑μ m
simp only [moebius, ZeroHom.coe_mk]
R : Type ?u.592093
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
⊢ (if Squarefree (n * m) then (-1) ^ ↑Ω (n * m) else 0) =
    (if Squarefree n then (-1) ^ ↑Ω n else 0) * if Squarefree m then (-1) ^ ↑Ω m else 0
R : Type ?u.592093
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
⊢ ↑{ toFun := fun n => if Squarefree n then (-1) ^ ↑Ω n else 0,
          map_zero' := (_ : (fun n => if Squarefree n then (-1) ^ ↑Ω n else 0) 0 = 0) }
      (n * m) =
    ↑{ toFun := fun n => if Squarefree n then (-1) ^ ↑Ω n else 0,
            map_zero' := (_ : (fun n => if Squarefree n then (-1) ^ ↑Ω n else 0) 0 = 0) }
        n *
      ↑{ toFun := fun n => if Squarefree n then (-1) ^ ↑Ω n else 0,
            map_zero' := (_ : (fun n => if Squarefree n then (-1) ^ ↑Ω n else 0) 0 = 0) }
        m
dsimp only [coe_mk, ZeroHom.toFun_eq_coe, Eq.ndrec, ZeroHom.coe_mk]
R : Type ?u.592093
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
⊢ (if Squarefree n then if Squarefree m then (-1) ^ ↑Ω (n * m) else 0 else 0) =
    if Squarefree m then if Squarefree n then (-1) ^ ↑Ω n * (-1) ^ ↑Ω m else 0 else 0
R : Type ?u.592093
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
⊢ (if Squarefree (n * m) then (-1) ^ ↑Ω (n * m) else 0) =
    (if Squarefree n then (-1) ^ ↑Ω n else 0) * if Squarefree m then (-1) ^ ↑Ω m else 0
simp only [IsUnit.mul_iff, Nat.isUnit_iff, squarefree_mul hnm, ite_and, mul_ite, ite_mul,
  zero_mul, mul_zero]
R : Type ?u.592093
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
⊢ (if Squarefree n then if Squarefree m then (-1) ^ (↑Ω n + ↑Ω m) else 0 else 0) =
    if Squarefree m then if Squarefree n then (-1) ^ ↑Ω n * (-1) ^ ↑Ω m else 0 else 0
R : Type ?u.592093
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
⊢ (if Squarefree n then if Squarefree m then (-1) ^ ↑Ω (n * m) else 0 else 0) =
    if Squarefree m then if Squarefree n then (-1) ^ ↑Ω n * (-1) ^ ↑Ω m else 0 else 0
rw [cardFactors_mul hn hm]
R : Type ?u.592093
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
⊢ (if Squarefree n then if Squarefree m then (-1) ^ (↑Ω n + ↑Ω m) else 0 else 0) =
    if Squarefree m then if Squarefree n then (-1) ^ ↑Ω n * (-1) ^ ↑Ω m else 0 else 0
R : Type ?u.592093
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
⊢ (if Squarefree n then if Squarefree m then (-1) ^ (↑Ω n + ↑Ω m) else 0 else 0) =
    if Squarefree m then if Squarefree n then (-1) ^ ↑Ω n * (-1) ^ ↑Ω m else 0 else 0
simp only [moebius, ZeroHom.coe_mk, squarefree_mul hnm, ite_and, cardFactors_mul hn hm]
R : Type ?u.592093
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
⊢ (if Squarefree n then if Squarefree m then (-1) ^ (↑Ω n + ↑Ω m) else 0 else 0) =
    if Squarefree m then if Squarefree n then (-1) ^ ↑Ω n * (-1) ^ ↑Ω m else 0 else 0
R : Type ?u.592093
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
⊢ (if Squarefree n then if Squarefree m then (-1) ^ (↑Ω n + ↑Ω m) else 0 else 0) =
    if Squarefree m then if Squarefree n then (-1) ^ ↑Ω n * (-1) ^ ↑Ω m else 0 else 0
simp only [Nat.isUnit_iff, ZeroHom.toFun_eq_coe, IsUnit.mul_iff, mul_ite, ite_mul,
  zero_mul, mul_zero]
R : Type ?u.592093
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
⊢ ((if Squarefree m then (-1) ^ ↑Ω n else 0) * if Squarefree n then (-1) ^ ↑Ω m else 0) =
    if Squarefree m then if Squarefree n then (-1) ^ ↑Ω n * (-1) ^ ↑Ω m else 0 else 0
R : Type ?u.592093
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
⊢ (if Squarefree n then if Squarefree m then (-1) ^ (↑Ω n + ↑Ω m) else 0 else 0) =
    if Squarefree m then if Squarefree n then (-1) ^ ↑Ω n * (-1) ^ ↑Ω m else 0 else 0
rw [pow_add, ite_mul_zero_left, ite_mul_zero_right]
no goals
R : Type ?u.592093
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
hnm : coprime n m
⊢ ((if Squarefree m then (-1) ^ ↑Ω n else 0) * if Squarefree n then (-1) ^ ↑Ω m else 0) =
    if Squarefree m then if Squarefree n then (-1) ^ ↑Ω n * (-1) ^ ↑Ω m else 0 else 0
split_ifs <;>  simp
no goals
R : Type ?u.592093
⊢ ↑μ 1 = 1
simp