c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = false
gn : g n = true
h3 : c < 1
⊢ cantorFunction c f < cantorFunction c g
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = false
gn : g n = true
⊢ cantorFunction c f < cantorFunction c g
have h3 : c < 1 := by
  apply h2.trans
  norm_num
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
⊢ cantorFunction c f < cantorFunction c g

case succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n✝ : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n✝ → f✝ k = g✝ k
fn✝ : f✝ n✝ = false
gn✝ : g✝ n✝ = true
h3 : c < 1
n : ℕ
ih :
  ∀ {f g : ℕ → Bool},
    (∀ (k : ℕ), k < n → f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < succ n → f k = g k
fn : f (succ n) = false
gn : g (succ n) = true
⊢ cantorFunction c f < cantorFunction c g
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = false
gn : g n = true
h3 : c < 1
⊢ cantorFunction c f < cantorFunction c g
induction' n with n ih generalizing f g
case succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n✝ : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n✝ → f✝ k = g✝ k
fn✝ : f✝ n✝ = false
gn✝ : g✝ n✝ = true
h3 : c < 1
n : ℕ
ih :
  ∀ {f g : ℕ → Bool},
    (∀ (k : ℕ), k < n → f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < succ n → f k = g k
fn : f (succ n) = false
gn : g (succ n) = true
⊢ ((bif f 0 then 1 else 0) + c * cantorFunction c fun n => f (n + 1)) <
    (bif g 0 then 1 else 0) + c * cantorFunction c fun n => g (n + 1)
case succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n✝ : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n✝ → f✝ k = g✝ k
fn✝ : f✝ n✝ = false
gn✝ : g✝ n✝ = true
h3 : c < 1
n : ℕ
ih :
  ∀ {f g : ℕ → Bool},
    (∀ (k : ℕ), k < n → f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < succ n → f k = g k
fn : f (succ n) = false
gn : g (succ n) = true
⊢ cantorFunction c f < cantorFunction c g
rw [cantorFunction_succ f (le_of_lt h1) h3, cantorFunction_succ g (le_of_lt h1) h3]
case succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n✝ : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n✝ → f✝ k = g✝ k
fn✝ : f✝ n✝ = false
gn✝ : g✝ n✝ = true
h3 : c < 1
n : ℕ
ih :
  ∀ {f g : ℕ → Bool},
    (∀ (k : ℕ), k < n → f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < succ n → f k = g k
fn : f (succ n) = false
gn : g (succ n) = true
⊢ ((bif g 0 then 1 else 0) + c * cantorFunction c fun n => f (n + 1)) <
    (bif g 0 then 1 else 0) + c * cantorFunction c fun n => g (n + 1)
case succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n✝ : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n✝ → f✝ k = g✝ k
fn✝ : f✝ n✝ = false
gn✝ : g✝ n✝ = true
h3 : c < 1
n : ℕ
ih :
  ∀ {f g : ℕ → Bool},
    (∀ (k : ℕ), k < n → f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < succ n → f k = g k
fn : f (succ n) = false
gn : g (succ n) = true
⊢ ((bif f 0 then 1 else 0) + c * cantorFunction c fun n => f (n + 1)) <
    (bif g 0 then 1 else 0) + c * cantorFunction c fun n => g (n + 1)
rw [hn 0 <| zero_lt_succ n]
case succ.bc
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n✝ : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n✝ → f✝ k = g✝ k
fn✝ : f✝ n✝ = false
gn✝ : g✝ n✝ = true
h3 : c < 1
n : ℕ
ih :
  ∀ {f g : ℕ → Bool},
    (∀ (k : ℕ), k < n → f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < succ n → f k = g k
fn : f (succ n) = false
gn : g (succ n) = true
⊢ (c * cantorFunction c fun n => f (n + 1)) < c * cantorFunction c fun n => g (n + 1)
case succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n✝ : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n✝ → f✝ k = g✝ k
fn✝ : f✝ n✝ = false
gn✝ : g✝ n✝ = true
h3 : c < 1
n : ℕ
ih :
  ∀ {f g : ℕ → Bool},
    (∀ (k : ℕ), k < n → f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < succ n → f k = g k
fn : f (succ n) = false
gn : g (succ n) = true
⊢ ((bif g 0 then 1 else 0) + c * cantorFunction c fun n => f (n + 1)) <
    (bif g 0 then 1 else 0) + c * cantorFunction c fun n => g (n + 1)
apply add_lt_add_left
case succ.bc
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n✝ : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n✝ → f✝ k = g✝ k
fn✝ : f✝ n✝ = false
gn✝ : g✝ n✝ = true
h3 : c < 1
n : ℕ
ih :
  ∀ {f g : ℕ → Bool},
    (∀ (k : ℕ), k < n → f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < succ n → f k = g k
fn : f (succ n) = false
gn : g (succ n) = true
⊢ (cantorFunction c fun n => f (n + 1)) < cantorFunction c fun n => g (n + 1)
case succ.bc
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n✝ : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n✝ → f✝ k = g✝ k
fn✝ : f✝ n✝ = false
gn✝ : g✝ n✝ = true
h3 : c < 1
n : ℕ
ih :
  ∀ {f g : ℕ → Bool},
    (∀ (k : ℕ), k < n → f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < succ n → f k = g k
fn : f (succ n) = false
gn : g (succ n) = true
⊢ (c * cantorFunction c fun n => f (n + 1)) < c * cantorFunction c fun n => g (n + 1)
rw [mul_lt_mul_left h1]
no goals
case succ.bc
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n✝ : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n✝ → f✝ k = g✝ k
fn✝ : f✝ n✝ = false
gn✝ : g✝ n✝ = true
h3 : c < 1
n : ℕ
ih :
  ∀ {f g : ℕ → Bool},
    (∀ (k : ℕ), k < n → f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < succ n → f k = g k
fn : f (succ n) = false
gn : g (succ n) = true
⊢ (cantorFunction c fun n => f (n + 1)) < cantorFunction c fun n => g (n + 1)
exact ih (fun k hk => hn _ <| Nat.succ_lt_succ hk) fn gn
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = false
gn : g n = true
⊢ 1 / 2 < 1
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = false
gn : g n = true
⊢ c < 1
apply h2.trans
no goals
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = false
gn : g n = true
⊢ 1 / 2 < 1
norm_num
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
⊢ cantorFunction c f < cantorFunction c g
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
⊢ cantorFunction c f < cantorFunction c g
let f_max : ℕ → Bool := fun n => Nat.rec false (fun _ _ => true) n
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
⊢ cantorFunction c f < cantorFunction c g
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
⊢ cantorFunction c f < cantorFunction c g
have hf_max : ∀ n, f n → f_max n := by
  intro n hn
  cases n
  rw [fn] at hn
  contradiction
  apply rfl
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
⊢ cantorFunction c f < cantorFunction c g
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
⊢ cantorFunction c f < cantorFunction c g
let g_min : ℕ → Bool := fun n => Nat.rec true (fun _ _ => false) n
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ cantorFunction c f < cantorFunction c g
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
⊢ cantorFunction c f < cantorFunction c g
have hg_min : ∀ n, g_min n → g n := by
  intro n hn
  cases n
  rw [gn]
  simp at hn
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ (cantorFunction c fun n => f_max n) < cantorFunction c g
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ cantorFunction c f < cantorFunction c g
apply (cantorFunction_le (le_of_lt h1) h3 hf_max).trans_lt
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ (cantorFunction c fun n => f_max n) < cantorFunction c fun n => g_min n
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ (cantorFunction c fun n => f_max n) < cantorFunction c g
refine' lt_of_lt_of_le _ (cantorFunction_le (le_of_lt h1) h3 hg_min)
case h.e'_3
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ (cantorFunction c fun n => f_max n) = c / (1 - c)

case h.e'_4
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ (cantorFunction c fun n => g_min n) = 1
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ (cantorFunction c fun n => f_max n) < cantorFunction c fun n => g_min n
convert this
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n✝ : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n✝ → f✝ k = g✝ k
fn✝ : f✝ n✝ = false
gn✝ : g✝ n✝ = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
n : ℕ
hn : f n = true
⊢ f_max n = true
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
⊢ ∀ (n : ℕ), f n = true → f_max n = true
intro n hn
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hn : f zero = true
⊢ f_max zero = true

case succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
n✝ : ℕ
hn : f (succ n✝) = true
⊢ f_max (succ n✝) = true
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n✝ : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n✝ → f✝ k = g✝ k
fn✝ : f✝ n✝ = false
gn✝ : g✝ n✝ = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
n : ℕ
hn : f n = true
⊢ f_max n = true
cases n
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hn : false = true
⊢ f_max zero = true

case succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
n✝ : ℕ
hn : f (succ n✝) = true
⊢ f_max (succ n✝) = true
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hn : f zero = true
⊢ f_max zero = true

case succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
n✝ : ℕ
hn : f (succ n✝) = true
⊢ f_max (succ n✝) = true
rw [fn] at hn
case succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
n✝ : ℕ
hn : f (succ n✝) = true
⊢ f_max (succ n✝) = true
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hn : false = true
⊢ f_max zero = true

case succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
n✝ : ℕ
hn : f (succ n✝) = true
⊢ f_max (succ n✝) = true
contradiction
no goals
case succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
n✝ : ℕ
hn : f (succ n✝) = true
⊢ f_max (succ n✝) = true
apply rfl
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n✝ : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n✝ → f✝ k = g✝ k
fn✝ : f✝ n✝ = false
gn✝ : g✝ n✝ = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
n : ℕ
hn : g_min n = true
⊢ g n = true
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
⊢ ∀ (n : ℕ), g_min n = true → g n = true
intro n hn
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hn : g_min zero = true
⊢ g zero = true

case succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
n✝ : ℕ
hn : g_min (succ n✝) = true
⊢ g (succ n✝) = true
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n✝ : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n✝ → f✝ k = g✝ k
fn✝ : f✝ n✝ = false
gn✝ : g✝ n✝ = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
n : ℕ
hn : g_min n = true
⊢ g n = true
cases n
case succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
n✝ : ℕ
hn : g_min (succ n✝) = true
⊢ g (succ n✝) = true
case zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hn : g_min zero = true
⊢ g zero = true

case succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
n✝ : ℕ
hn : g_min (succ n✝) = true
⊢ g (succ n✝) = true
rw [gn]
no goals
case succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
n✝ : ℕ
hn : g_min (succ n✝) = true
⊢ g (succ n✝) = true
simp at hn
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ c + c < 1

c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ 0 < 1 - c
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ c / (1 - c) < 1
rw [div_lt_one, lt_sub_iff_add_lt]
no goals
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ 0 < 1 - c
rwa [sub_pos]
case h.e'_4
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ 1 = 1 / 2 + 1 / 2
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ c + c < 1
convert _root_.add_lt_add h2 h2
no goals
case h.e'_4
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ 1 = 1 / 2 + 1 / 2
norm_num
case h.e'_3
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ ((bif f_max 0 then 1 else 0) + c * cantorFunction c fun n => f_max (n + 1)) = c * ∑' (n : ℕ), c ^ n
case h.e'_3
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ (cantorFunction c fun n => f_max n) = c / (1 - c)
rw [cantorFunction_succ _ (le_of_lt h1) h3, div_eq_mul_inv, ←
  tsum_geometric_of_lt_1 (le_of_lt h1) h3]
no goals
case h.e'_3
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ ((bif f_max 0 then 1 else 0) + c * cantorFunction c fun n => f_max (n + 1)) = c * ∑' (n : ℕ), c ^ n
apply zero_add
case h.e'_4.refine'_1
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ ∀ (b' : ℕ), b' ≠ 0 → cantorFunctionAux c (fun n => g_min n) b' = 0

case h.e'_4.refine'_2
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ cantorFunctionAux c (fun n => g_min n) 0 = 1
case h.e'_4
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ (cantorFunction c fun n => g_min n) = 1
refine' (tsum_eq_single 0 _).trans _
case h.e'_4.refine'_1
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n✝ : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n✝ → f✝ k = g✝ k
fn✝ : f✝ n✝ = false
gn✝ : g✝ n✝ = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
n : ℕ
hn : n ≠ 0
⊢ cantorFunctionAux c (fun n => g_min n) n = 0
case h.e'_4.refine'_1
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ ∀ (b' : ℕ), b' ≠ 0 → cantorFunctionAux c (fun n => g_min n) b' = 0
intro n hn
case h.e'_4.refine'_1.zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
hn : zero ≠ 0
⊢ cantorFunctionAux c (fun n => g_min n) zero = 0

case h.e'_4.refine'_1.succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
n✝ : ℕ
hn : succ n✝ ≠ 0
⊢ cantorFunctionAux c (fun n => g_min n) (succ n✝) = 0
case h.e'_4.refine'_1
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n✝ : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n✝ → f✝ k = g✝ k
fn✝ : f✝ n✝ = false
gn✝ : g✝ n✝ = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
n : ℕ
hn : n ≠ 0
⊢ cantorFunctionAux c (fun n => g_min n) n = 0
cases n
case h.e'_4.refine'_1.succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
n✝ : ℕ
hn : succ n✝ ≠ 0
⊢ cantorFunctionAux c (fun n => g_min n) (succ n✝) = 0
case h.e'_4.refine'_1.zero
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
hn : zero ≠ 0
⊢ cantorFunctionAux c (fun n => g_min n) zero = 0

case h.e'_4.refine'_1.succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
n✝ : ℕ
hn : succ n✝ ≠ 0
⊢ cantorFunctionAux c (fun n => g_min n) (succ n✝) = 0
contradiction
no goals
case h.e'_4.refine'_1.succ
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝¹ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝¹ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
n✝ : ℕ
hn : succ n✝ ≠ 0
⊢ cantorFunctionAux c (fun n => g_min n) (succ n✝) = 0
rfl
no goals
case h.e'_4.refine'_2
c : ℝ
f✝¹ g✝¹ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f✝ g✝ : ℕ → Bool
hn✝ : ∀ (k : ℕ), k < n → f✝ k = g✝ k
fn✝ : f✝ n = false
gn✝ : g✝ n = true
h3 : c < 1
f g : ℕ → Bool
hn : ∀ (k : ℕ), k < zero → f k = g k
fn : f zero = false
gn : g zero = true
f_max : ℕ → Bool := fun n => rec false (fun x x => true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n => rec true (fun x x => false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ cantorFunctionAux c (fun n => g_min n) 0 = 1
exact cantorFunctionAux_zero _