case intro.intro.intro.intro
R : Type ?u.591476
p k : ℕ
hp : Prime p
hk : 0 < k
hn : IsPrimePow (p ^ k)
hn' : ¬Prime (p ^ k)
⊢ ↑μ (p ^ k) = 0
R : Type ?u.591476
n : ℕ
hn : IsPrimePow n
hn' : ¬Prime n
⊢ ↑μ n = 0
obtain ⟨p, k, hp, hk, rfl⟩ := (isPrimePow_nat_iff _).1 hn
case intro.intro.intro.intro.hnc
R : Type ?u.591476
p k : ℕ
hp : Prime p
hk : 0 < k
hn : IsPrimePow (p ^ k)
hn' : ¬Prime (p ^ k)
⊢ ¬k = 1
case intro.intro.intro.intro
R : Type ?u.591476
p k : ℕ
hp : Prime p
hk : 0 < k
hn : IsPrimePow (p ^ k)
hn' : ¬Prime (p ^ k)
⊢ ↑μ (p ^ k) = 0
rw [moebius_apply_prime_pow hp hk.ne', if_neg]
case intro.intro.intro.intro.hnc
R : Type ?u.591476
p : ℕ
hp : Prime p
hk : 0 < 1
hn : IsPrimePow (p ^ 1)
hn' : ¬Prime (p ^ 1)
⊢ False
case intro.intro.intro.intro.hnc
R : Type ?u.591476
p k : ℕ
hp : Prime p
hk : 0 < k
hn : IsPrimePow (p ^ k)
hn' : ¬Prime (p ^ k)
⊢ ¬k = 1
rintro rfl
no goals
case intro.intro.intro.intro.hnc
R : Type ?u.591476
p : ℕ
hp : Prime p
hk : 0 < 1
hn : IsPrimePow (p ^ 1)
hn' : ¬Prime (p ^ 1)
⊢ False
exact hn' (by simpa)
no goals
R : Type ?u.591476
p : ℕ
hp : Prime p
hk : 0 < 1
hn : IsPrimePow (p ^ 1)
hn' : ¬Prime (p ^ 1)
⊢ Prime (p ^ 1)
simpa