linarith only [this]
case h1.hac
M : ℕ
f : ArithmeticFunction ℝ
hf : CompletelyMultiplicative f
hf_nonneg : ∀ (n : ℕ), 0 ≤ f n
d : ℕ
hd : Squarefree d
hf_size : ∀ (n : ℕ), n.Prime → n ∣ d → f n < 1
p : ℕ
hp : p.Prime ∧ p ∣ d
this : 0 ≤ f p ^ M.succ
⊢ -1 * (f p ^ M.succ - f p) ≤ f p
no goals