case inl
R : Type ?u.590526
p k : ℕ
hp : Prime p
hk : k ≠ 0
h : k = 1
⊢ ↑μ (p ^ k) = -1

case inr
R : Type ?u.590526
p k : ℕ
hp : Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ ↑μ (p ^ k) = 0
R : Type ?u.590526
p k : ℕ
hp : Prime p
hk : k ≠ 0
⊢ ↑μ (p ^ k) = if k = 1 then -1 else 0
split_ifs with h
case inr
R : Type ?u.590526
p k : ℕ
hp : Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ ¬Squarefree (p ^ k)
case inr
R : Type ?u.590526
p k : ℕ
hp : Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ ↑μ (p ^ k) = 0
rw [moebius_eq_zero_of_not_squarefree]
case inr
R : Type ?u.590526
p k : ℕ
hp : Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ ¬Squarefree p ∨ ¬k = 1
case inr
R : Type ?u.590526
p k : ℕ
hp : Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ ¬Squarefree (p ^ k)
rw [squarefree_pow_iff hp.ne_one hk, not_and_or]
no goals
case inr
R : Type ?u.590526
p k : ℕ
hp : Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ ¬Squarefree p ∨ ¬k = 1
exact Or.inr h
no goals
case inl
R : Type ?u.590526
p k : ℕ
hp : Prime p
hk : k ≠ 0
h : k = 1
⊢ ↑μ (p ^ k) = -1
rw [h, pow_one, moebius_apply_prime hp]