Theorem: Bulgaria1998P3.geom_sum_bound (Compfiles/Bulgaria1998P3.lean)

State before:
n : ℕ
⊢ ∑ i ∈ Finset.range n, 1 / 2 ^ i = ∑ i ∈ Finset.range n, (1 / 2) ^ i
Tactic:
congr
State after:
case e_f
n : ℕ
⊢ (fun i => 1 / 2 ^ i) = fun i => (1 / 2) ^ i

State before:
case e_f
n : ℕ
⊢ (fun i => 1 / 2 ^ i) = fun i => (1 / 2) ^ i
Tactic:
simp [div_eq_mul_inv]
State after:
no goals

State before:
n : ℕ
⊢ 2 < 3
Tactic:
norm_num
State after:
no goals