c : ℝ
f✝ g : ℕ → Bool
n : ℕ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ (cantorFunctionAux c f 0 + ∑' (b : ℕ), cantorFunctionAux c f (b + 1)) =
    (bif f 0 then 1 else 0) + c * cantorFunction c fun n => f (n + 1)
c : ℝ
f✝ g : ℕ → Bool
n : ℕ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ cantorFunction c f = (bif f 0 then 1 else 0) + c * cantorFunction c fun n => f (n + 1)
rw [cantorFunction, tsum_eq_zero_add (summable_cantor_function f h1 h2)]
c : ℝ
f✝ g : ℕ → Bool
n : ℕ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ ((bif f 0 then 1 else 0) + c * ∑' (x : ℕ), cantorFunctionAux c (fun n => f (n + 1)) x) =
    (bif f 0 then 1 else 0) + c * cantorFunction c fun n => f (n + 1)
c : ℝ
f✝ g : ℕ → Bool
n : ℕ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ (cantorFunctionAux c f 0 + ∑' (b : ℕ), cantorFunctionAux c f (b + 1)) =
    (bif f 0 then 1 else 0) + c * cantorFunction c fun n => f (n + 1)
rw [cantorFunctionAux_succ, tsum_mul_left, cantorFunctionAux, _root_.pow_zero]
no goals
c : ℝ
f✝ g : ℕ → Bool
n : ℕ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ ((bif f 0 then 1 else 0) + c * ∑' (x : ℕ), cantorFunctionAux c (fun n => f (n + 1)) x) =
    (bif f 0 then 1 else 0) + c * cantorFunction c fun n => f (n + 1)
rfl