obtain ⟨⟨q, hq⟩, _, hp_dvd_pow⟩ := Prime.exists_mem_finset_dvd hpp.prime hp_dvd
case pos.h
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∉ d.primeFactors
hpp : p.Prime
hp_dvd : p ∣ i a ha
⊢ False
case pos.h.intro.mk.intro
M : ℕ
hM : M ≠ 0
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
d : ℕ
hd : Squarefree d
i : (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) → (a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) → ℕ :=
  fun a x => ∏ p ∈ d.primeFactors.attach, ↑p ^ a ↑p ⋯
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M
p : ℕ
hp : p ∉ d.primeFactors
hpp : p.Prime
hp_dvd : p ∣ i a ha
q : ℕ
hq : q ∈ d.primeFactors
left✝ : ⟨q, hq⟩ ∈ d.primeFactors.attach
hp_dvd_pow : p ∣ ↑⟨q, hq⟩ ^ a ↑⟨q, hq⟩ ⋯
⊢ False