How can I handle the partial sum of geometric series

Stream: new members

[Heliopolis]

I am solving this problem:

theorem partial_sum_of_geometric_series (n : ℕ) (h : ∑ i ∈ Finset.range n, (1 / 4) * (1 / 2 : ℝ) ^ i = 255 / 512) :
    n = 8 := by sorry

I don't know how to solve it. I searched for useful theorems but found nothing. Could someone help me? Just telling me the ideas is OK. Thanks a lot!

[Ruben Van de Velde]

First step is to take out the constant (docs#Finset.mul_sum) and then you can use the closed form (docs#geom_sum_eq). Then it's arithmetic

[Alex Brodbelt]

Following Ruben's advice and injectivity

import Mathlib

theorem partial_sum_of_geometric_series (n : ℕ) (h : ∑ i ∈ Finset.range n, (1 / 4) * (1 / 2 : ℝ) ^ i = 255 / 512) :
    n = 8 := by
    rw [← Finset.mul_sum, geom_sum_eq (by norm_num)] at h
    have helper : 1 / 4 * (((1 / 2) ^ 8 - 1) / (1 / 2 - 1)) = 255 / (512 :  ℝ) := by norm_num
    -- from here we use injectivity on all relevant operations to single out that n = 8.
    rw [← helper, mul_right_inj' (by norm_num), div_left_inj' (by norm_num),
            sub_left_inj, pow_right_inj (by norm_num) (by norm_num)] at h
    exact h

[Heliopolis]

@Alex Brodbelt @Ruben Van de Velde Great solution! Thanks!!!

[Kevin Buzzard]

@Alex Brodbelt weird zulip tip: code in spoilers needs to be enclosed by four backticks not three! (Because the spoiler already stole the three backtick option)