c : ℝ
f g : ℕ → Bool
n : ℕ
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
⊢ ∀ (i : ℕ), cantorFunctionAux c f i ≤ cantorFunctionAux c g i
c : ℝ
f g : ℕ → Bool
n : ℕ
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
⊢ cantorFunction c f ≤ cantorFunction c g
apply tsum_le_tsum _ (summable_cantor_function f h1 h2) (summable_cantor_function g h1 h2)
c : ℝ
f g : ℕ → Bool
n✝ : ℕ
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n
c : ℝ
f g : ℕ → Bool
n : ℕ
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
⊢ ∀ (i : ℕ), cantorFunctionAux c f i ≤ cantorFunctionAux c g i
intro n
case false
c : ℝ
f g : ℕ → Bool
n✝ : ℕ
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
h : f n = false
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n

case true
c : ℝ
f g : ℕ → Bool
n✝ : ℕ
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
h : f n = true
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n
c : ℝ
f g : ℕ → Bool
n✝ : ℕ
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n
cases h : f n
case true
c : ℝ
f g : ℕ → Bool
n✝ : ℕ
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
h : f n = true
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n
case false
c : ℝ
f g : ℕ → Bool
n✝ : ℕ
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
h : f n = false
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n

case true
c : ℝ
f g : ℕ → Bool
n✝ : ℕ
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
h : f n = true
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n
simp [h, cantorFunctionAux_nonneg h1]
case true
c : ℝ
f g : ℕ → Bool
n✝ : ℕ
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
h : f n = true
h3 : g n = true
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n
case true
c : ℝ
f g : ℕ → Bool
n✝ : ℕ
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
h : f n = true
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n
replace h3 : g n = true := h3 n h
no goals
case true
c : ℝ
f g : ℕ → Bool
n✝ : ℕ
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
h : f n = true
h3 : g n = true
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n
simp [h, h3]