rw [←Nat.Ico_succ_right, geom_sum_Ico, ←mul_div_mul_left (c:= (-1:ℝ)) (f p ^ Nat.succ M - f p ^ 1)]
case h1
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
⊢ ∑ n ∈ Finset.Icc 1 M, f p ^ n ≤ f p / (1 - f p)
case h1
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
⊢ -1 * (f p ^ M.succ - f p ^ 1) / (-1 * (f p - 1)) ≤ f p / (1 - f p)

case h1.hc
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
⊢ -1 ≠ 0

case h1.hx
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
⊢ f p ≠ 1

case h1.hmn
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
⊢ 1 ≤ M.succ