case h.e'_5
α : Type ?u.240216
β : Type ?u.240219
ι : Type ?u.240222
a : ℝ
⊢ (fun n => a / 2 / 2 ^ n) = fun i => a / 2 * (1 / 2) ^ i

case h.e'_6
α : Type ?u.240216
β : Type ?u.240219
ι : Type ?u.240222
a : ℝ
⊢ a = a / 2 * (1 - 1 / 2)⁻¹
α : Type ?u.240216
β : Type ?u.240219
ι : Type ?u.240222
a : ℝ
⊢ HasSum (fun n => a / 2 / 2 ^ n) a
convert HasSum.mul_left (a / 2)
    (hasSum_geometric_of_lt_1 (le_of_lt one_half_pos) one_half_lt_one) using 1
case h.e'_5.h
α : Type ?u.240216
β : Type ?u.240219
ι : Type ?u.240222
a : ℝ
n : ℕ
⊢ a / 2 / 2 ^ n = a / 2 * (1 / 2) ^ n
case h.e'_5
α : Type ?u.240216
β : Type ?u.240219
ι : Type ?u.240222
a : ℝ
⊢ (fun n => a / 2 / 2 ^ n) = fun i => a / 2 * (1 / 2) ^ i
funext n
case h.e'_5.h
α : Type ?u.240216
β : Type ?u.240219
ι : Type ?u.240222
a : ℝ
n : ℕ
⊢ a / 2 / 2 ^ n = a / 2 * (2 ^ n)⁻¹
case h.e'_5.h
α : Type ?u.240216
β : Type ?u.240219
ι : Type ?u.240222
a : ℝ
n : ℕ
⊢ a / 2 / 2 ^ n = a / 2 * (1 / 2) ^ n
simp
no goals
case h.e'_5.h
α : Type ?u.240216
β : Type ?u.240219
ι : Type ?u.240222
a : ℝ
n : ℕ
⊢ a / 2 / 2 ^ n = a / 2 * (2 ^ n)⁻¹
rfl
no goals
case h.e'_6
α : Type ?u.240216
β : Type ?u.240219
ι : Type ?u.240222
a : ℝ
⊢ a = a / 2 * (1 - 1 / 2)⁻¹
norm_num