rw [←Nat.Prime.dvd_iff_one_le_factorization hp.1 hd.ne_zero]
case hab
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 ⋯
hfact_i :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) (p : ℕ),
    (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
hi_ne_zero : ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M), i a ha ≠ 0
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha✝ : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
p : ℕ
a✝ : p ∈ (i a ha✝).factorization.support
hp : p.Prime ∧ p ∣ d
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 1 ≤ a a_1 h ∧ a a_1 h ≤ M
⊢ 1 ≤ d.factorization p
case hab
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 ⋯
hfact_i :
  ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun p => Finset.Icc 1 M) (p : ℕ),
    (i a ha).factorization p = if hp : p ∈ d.primeFactors then a p hp else 0
hi_ne_zero : ∀ (a : (a : ℕ) → a ∈ d.primeFactors → ℕ) (ha : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M), i a ha ≠ 0
a : (a : ℕ) → a ∈ d.primeFactors → ℕ
ha✝ : a ∈ d.primeFactors.pi fun _p => Finset.Icc 1 M
p : ℕ
a✝ : p ∈ (i a ha✝).factorization.support
hp : p.Prime ∧ p ∣ d
ha : ∀ (a_1 : ℕ) (h : a_1 ∈ d.primeFactors), 1 ≤ a a_1 h ∧ a a_1 h ≤ M
⊢ p ∣ d