case mp
R : Type ?u.586134
n : ℕ
h : ↑μ n ≠ 0
⊢ ↑μ n = 1 ∨ ↑μ n = -1

case mpr
R : Type ?u.586134
n : ℕ
h : ↑μ n = 1 ∨ ↑μ n = -1
⊢ ↑μ n ≠ 0
R : Type ?u.586134
n : ℕ
⊢ ↑μ n ≠ 0 ↔ ↑μ n = 1 ∨ ↑μ n = -1
constructor <;> intro h
case mp
R : Type ?u.586134
n : ℕ
h : Squarefree n
⊢ ↑μ n = 1 ∨ ↑μ n = -1
case mp
R : Type ?u.586134
n : ℕ
h : ↑μ n ≠ 0
⊢ ↑μ n = 1 ∨ ↑μ n = -1
rw [moebius_ne_zero_iff_squarefree] at h
case mp
R : Type ?u.586134
n : ℕ
h : Squarefree n
⊢ (-1) ^ ↑Ω n = 1 ∨ (-1) ^ ↑Ω n = -1
case mp
R : Type ?u.586134
n : ℕ
h : Squarefree n
⊢ ↑μ n = 1 ∨ ↑μ n = -1
rw [moebius_apply_of_squarefree h]
no goals
case mp
R : Type ?u.586134
n : ℕ
h : Squarefree n
⊢ (-1) ^ ↑Ω n = 1 ∨ (-1) ^ ↑Ω n = -1
apply neg_one_pow_eq_or
no goals
case mpr
R : Type ?u.586134
n : ℕ
h : ↑μ n = 1 ∨ ↑μ n = -1
⊢ ↑μ n ≠ 0
rcases h with (h | h) <;> simp [h]