[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
h : f n = true
⊢ cantorFunctionAux c f n = c ^ n
[PROOFSTEP]
simp [cantorFunctionAux, h]
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
h : f n = false
⊢ cantorFunctionAux c f n = 0
[PROOFSTEP]
simp [cantorFunctionAux, h]
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
h : 0 ≤ c
⊢ 0 ≤ cantorFunctionAux c f n
[PROOFSTEP]
cases h' : f n
[GOAL]
case false
c : ℝ
f g : ℕ → Bool
n : ℕ
h : 0 ≤ c
h' : f n = false
⊢ 0 ≤ cantorFunctionAux c f n
[PROOFSTEP]
simp [h']
[GOAL]
case true
c : ℝ
f g : ℕ → Bool
n : ℕ
h : 0 ≤ c
h' : f n = true
⊢ 0 ≤ cantorFunctionAux c f n
[PROOFSTEP]
simp [h']
[GOAL]
case true
c : ℝ
f g : ℕ → Bool
n : ℕ
h : 0 ≤ c
h' : f n = true
⊢ 0 ≤ c ^ n
[PROOFSTEP]
apply pow_nonneg h
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
h : f n = g n
⊢ cantorFunctionAux c f n = cantorFunctionAux c g n
[PROOFSTEP]
simp [cantorFunctionAux, h]
[GOAL]
c : ℝ
f✝ g : ℕ → Bool
n : ℕ
f : ℕ → Bool
⊢ cantorFunctionAux c f 0 = bif f 0 then 1 else 0
[PROOFSTEP]
cases h : f 0
[GOAL]
case false
c : ℝ
f✝ g : ℕ → Bool
n : ℕ
f : ℕ → Bool
h : f 0 = false
⊢ cantorFunctionAux c f 0 = bif false then 1 else 0
[PROOFSTEP]
simp [h]
[GOAL]
case true
c : ℝ
f✝ g : ℕ → Bool
n : ℕ
f : ℕ → Bool
h : f 0 = true
⊢ cantorFunctionAux c f 0 = bif true then 1 else 0
[PROOFSTEP]
simp [h]
[GOAL]
c : ℝ
f✝ g : ℕ → Bool
n : ℕ
f : ℕ → Bool
⊢ (fun n => cantorFunctionAux c f (n + 1)) = fun n => c * cantorFunctionAux c (fun n => f (n + 1)) n
[PROOFSTEP]
ext n
[GOAL]
case h
c : ℝ
f✝ g : ℕ → Bool
n✝ : ℕ
f : ℕ → Bool
n : ℕ
⊢ cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun n => f (n + 1)) n
[PROOFSTEP]
cases h : f (n + 1)
[GOAL]
case h.false
c : ℝ
f✝ g : ℕ → Bool
n✝ : ℕ
f : ℕ → Bool
n : ℕ
h : f (n + 1) = false
⊢ cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun n => f (n + 1)) n
[PROOFSTEP]
simp [h, _root_.pow_succ]
[GOAL]
case h.true
c : ℝ
f✝ g : ℕ → Bool
n✝ : ℕ
f : ℕ → Bool
n : ℕ
h : f (n + 1) = true
⊢ cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun n => f (n + 1)) n
[PROOFSTEP]
simp [h, _root_.pow_succ]
[GOAL]
c : ℝ
f✝ g : ℕ → Bool
n : ℕ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ Summable (cantorFunctionAux c f)
[PROOFSTEP]
apply (summable_geometric_of_lt_1 h1 h2).summable_of_eq_zero_or_self
[GOAL]
c : ℝ
f✝ g : ℕ → Bool
n : ℕ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ ∀ (b : ℕ), cantorFunctionAux c f b = 0 ∨ cantorFunctionAux c f b = c ^ b
[PROOFSTEP]
intro n
[GOAL]
c : ℝ
f✝ g : ℕ → Bool
n✝ : ℕ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
⊢ cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n
[PROOFSTEP]
cases h : f n
[GOAL]
case false
c : ℝ
f✝ g : ℕ → Bool
n✝ : ℕ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
h : f n = false
⊢ cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n
[PROOFSTEP]
simp [h]
[GOAL]
case true
c : ℝ
f✝ g : ℕ → Bool
n✝ : ℕ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
h : f n = true
⊢ cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n
[PROOFSTEP]
simp [h]
[GOAL]
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
[PROOFSTEP]
apply tsum_le_tsum _ (summable_cantor_function f h1 h2) (summable_cantor_function g h1 h2)
[GOAL]
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
[PROOFSTEP]
intro n
[GOAL]
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
[PROOFSTEP]
cases h : f n
[GOAL]
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
[PROOFSTEP]
simp [h, cantorFunctionAux_nonneg h1]
[GOAL]
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
[PROOFSTEP]
replace h3 : g n = true := h3 n h
[GOAL]
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
[PROOFSTEP]
simp [h, h3]
[GOAL]
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)
[PROOFSTEP]
rw [cantorFunction, tsum_eq_zero_add (summable_cantor_function f h1 h2)]
[GOAL]
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)
[PROOFSTEP]
rw [cantorFunctionAux_succ, tsum_mul_left, cantorFunctionAux, _root_.pow_zero]
[GOAL]
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)
[PROOFSTEP]
rfl
[GOAL]
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
[PROOFSTEP]
have h3 : c < 1 := by
  apply h2.trans
  norm_num
[GOAL]
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
[PROOFSTEP]
apply h2.trans
[GOAL]
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
[PROOFSTEP]
norm_num
[GOAL]
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
[PROOFSTEP]
induction' n with n ih generalizing f g
[GOAL]
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
[PROOFSTEP]
let f_max : ℕ → Bool := fun n => Nat.rec false (fun _ _ => true) n
[GOAL]
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
[PROOFSTEP]
have hf_max : ∀ n, f n → f_max n := by
  intro n hn
  cases n
  rw [fn] at hn 
  contradiction
  apply rfl
[GOAL]
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
[PROOFSTEP]
intro n hn
[GOAL]
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
[PROOFSTEP]
cases n
[GOAL]
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
[PROOFSTEP]
rw [fn] at hn 
[GOAL]
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
[PROOFSTEP]
contradiction
[GOAL]
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
[PROOFSTEP]
apply rfl
[GOAL]
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
[PROOFSTEP]
let g_min : ℕ → Bool := fun n => Nat.rec true (fun _ _ => false) n
[GOAL]
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
[PROOFSTEP]
have hg_min : ∀ n, g_min n → g n := by
  intro n hn
  cases n
  rw [gn]
  simp at hn 
[GOAL]
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
[PROOFSTEP]
intro n hn
[GOAL]
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
[PROOFSTEP]
cases n
[GOAL]
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
[PROOFSTEP]
rw [gn]
[GOAL]
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
[PROOFSTEP]
simp at hn 
[GOAL]
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
[PROOFSTEP]
apply (cantorFunction_le (le_of_lt h1) h3 hf_max).trans_lt
[GOAL]
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
[PROOFSTEP]
refine' lt_of_lt_of_le _ (cantorFunction_le (le_of_lt h1) h3 hg_min)
[GOAL]
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
[PROOFSTEP]
have : c / (1 - c) < 1 := by
  rw [div_lt_one, lt_sub_iff_add_lt]
  · convert _root_.add_lt_add h2 h2
    norm_num
  rwa [sub_pos]
[GOAL]
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
[PROOFSTEP]
rw [div_lt_one, lt_sub_iff_add_lt]
[GOAL]
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
[PROOFSTEP]
convert _root_.add_lt_add h2 h2
[GOAL]
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
[PROOFSTEP]
norm_num
[GOAL]
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
[PROOFSTEP]
rwa [sub_pos]
[GOAL]
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
[PROOFSTEP]
convert this
[GOAL]
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)
[PROOFSTEP]
rw [cantorFunction_succ _ (le_of_lt h1) h3, div_eq_mul_inv, ← tsum_geometric_of_lt_1 (le_of_lt h1) h3]
[GOAL]
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
[PROOFSTEP]
apply zero_add
[GOAL]
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
[PROOFSTEP]
refine' (tsum_eq_single 0 _).trans _
[GOAL]
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
[PROOFSTEP]
intro n hn
[GOAL]
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
[PROOFSTEP]
cases n
[GOAL]
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
[PROOFSTEP]
contradiction
[GOAL]
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
[PROOFSTEP]
rfl
[GOAL]
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
[PROOFSTEP]
exact cantorFunctionAux_zero _
[GOAL]
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
[PROOFSTEP]
rw [cantorFunction_succ f (le_of_lt h1) h3, cantorFunction_succ g (le_of_lt h1) h3]
[GOAL]
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)
[PROOFSTEP]
rw [hn 0 <| zero_lt_succ n]
[GOAL]
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)
[PROOFSTEP]
apply add_lt_add_left
[GOAL]
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)
[PROOFSTEP]
rw [mul_lt_mul_left h1]
[GOAL]
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)
[PROOFSTEP]
exact ih (fun k hk => hn _ <| Nat.succ_lt_succ hk) fn gn
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
⊢ Function.Injective (cantorFunction c)
[PROOFSTEP]
intro f g hfg
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
hfg : cantorFunction c f = cantorFunction c g
⊢ f = g
[PROOFSTEP]
classical
by_contra h
revert hfg
have : ∃ n, f n ≠ g n := by
  rw [← not_forall]
  intro h'
  apply h
  ext
  apply h'
let n := Nat.find this
have hn : ∀ k : ℕ, k < n → f k = g k := by
  intro k hk
  apply of_not_not
  exact Nat.find_min this hk
cases fn : f n
· apply _root_.ne_of_lt
  refine' increasing_cantorFunction h1 h2 hn fn _
  apply Bool.eq_true_of_not_eq_false
  rw [← fn]
  apply Ne.symm
  exact Nat.find_spec this
· apply _root_.ne_of_gt
  refine' increasing_cantorFunction h1 h2 (fun k hk => (hn k hk).symm) _ fn
  apply Bool.eq_false_of_not_eq_true
  rw [← fn]
  apply Ne.symm
  exact Nat.find_spec this
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
hfg : cantorFunction c f = cantorFunction c g
⊢ f = g
[PROOFSTEP]
by_contra h
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
hfg : cantorFunction c f = cantorFunction c g
h : ¬f = g
⊢ False
[PROOFSTEP]
revert hfg
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
⊢ cantorFunction c f = cantorFunction c g → False
[PROOFSTEP]
have : ∃ n, f n ≠ g n := by
  rw [← not_forall]
  intro h'
  apply h
  ext
  apply h'
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
⊢ ∃ n, f n ≠ g n
[PROOFSTEP]
rw [← not_forall]
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
⊢ ¬∀ (x : ℕ), f x = g x
[PROOFSTEP]
intro h'
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
h' : ∀ (x : ℕ), f x = g x
⊢ False
[PROOFSTEP]
apply h
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
h' : ∀ (x : ℕ), f x = g x
⊢ f = g
[PROOFSTEP]
ext
[GOAL]
case h
c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
h' : ∀ (x : ℕ), f x = g x
x✝ : ℕ
⊢ f x✝ = g x✝
[PROOFSTEP]
apply h'
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
⊢ cantorFunction c f = cantorFunction c g → False
[PROOFSTEP]
let n := Nat.find this
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
⊢ cantorFunction c f = cantorFunction c g → False
[PROOFSTEP]
have hn : ∀ k : ℕ, k < n → f k = g k := by
  intro k hk
  apply of_not_not
  exact Nat.find_min this hk
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
⊢ ∀ (k : ℕ), k < n → f k = g k
[PROOFSTEP]
intro k hk
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
k : ℕ
hk : k < n
⊢ f k = g k
[PROOFSTEP]
apply of_not_not
[GOAL]
case a
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
k : ℕ
hk : k < n
⊢ ¬¬f k = g k
[PROOFSTEP]
exact Nat.find_min this hk
[GOAL]
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
⊢ cantorFunction c f = cantorFunction c g → False
[PROOFSTEP]
cases fn : f n
[GOAL]
case false
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = false
⊢ cantorFunction c f = cantorFunction c g → False
[PROOFSTEP]
apply _root_.ne_of_lt
[GOAL]
case false.h
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = false
⊢ cantorFunction c f < cantorFunction c g
[PROOFSTEP]
refine' increasing_cantorFunction h1 h2 hn fn _
[GOAL]
case false.h
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = false
⊢ g n = true
[PROOFSTEP]
apply Bool.eq_true_of_not_eq_false
[GOAL]
case false.h.a
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = false
⊢ ¬g n = false
[PROOFSTEP]
rw [← fn]
[GOAL]
case false.h.a
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = false
⊢ ¬g n = f n
[PROOFSTEP]
apply Ne.symm
[GOAL]
case false.h.a.h
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = false
⊢ f n ≠ g n
[PROOFSTEP]
exact Nat.find_spec this
[GOAL]
case true
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = true
⊢ cantorFunction c f = cantorFunction c g → False
[PROOFSTEP]
apply _root_.ne_of_gt
[GOAL]
case true.h
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = true
⊢ cantorFunction c g < cantorFunction c f
[PROOFSTEP]
refine' increasing_cantorFunction h1 h2 (fun k hk => (hn k hk).symm) _ fn
[GOAL]
case true.h
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = true
⊢ g n = false
[PROOFSTEP]
apply Bool.eq_false_of_not_eq_true
[GOAL]
case true.h.a
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = true
⊢ ¬g n = true
[PROOFSTEP]
rw [← fn]
[GOAL]
case true.h.a
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = true
⊢ ¬g n = f n
[PROOFSTEP]
apply Ne.symm
[GOAL]
case true.h.a.h
c : ℝ
f✝ g✝ : ℕ → Bool
n✝ : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
hn : ∀ (k : ℕ), k < n → f k = g k
fn : f n = true
⊢ f n ≠ g n
[PROOFSTEP]
exact Nat.find_spec this
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ #ℝ = 𝔠
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ #ℝ ≤ 𝔠
[PROOFSTEP]
rw [Real.equivCauchy.cardinal_eq]
[GOAL]
case a
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ #(CauSeq.Completion.Cauchy abs) ≤ 𝔠
[PROOFSTEP]
apply mk_quotient_le.trans
[GOAL]
case a
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ #(CauSeq ℚ abs) ≤ 𝔠
[PROOFSTEP]
apply (mk_subtype_le _).trans_eq
[GOAL]
case a
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ #(ℕ → ℚ) = 𝔠
[PROOFSTEP]
rw [← power_def, mk_nat, mkRat, aleph0_power_aleph0]
[GOAL]
case a
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 𝔠 ≤ #ℝ
[PROOFSTEP]
convert mk_le_of_injective (cantorFunction_injective _ _)
[GOAL]
case h.e'_3
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 𝔠 = #(ℕ → Bool)
case a.convert_1
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ ℝ
case a.convert_2
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 0 < ?a.convert_1✝
case a.convert_3 c : ℝ f g : ℕ → Bool n : ℕ ⊢ ?a.convert_1✝ < 1 / 2
[PROOFSTEP]
rw [← power_def, mk_bool, mk_nat, two_power_aleph0]
[GOAL]
case a.convert_1
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ ℝ
case a.convert_2
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 0 < ?a.convert_1✝
case a.convert_3 c : ℝ f g : ℕ → Bool n : ℕ ⊢ ?a.convert_1✝ < 1 / 2
[PROOFSTEP]
exact 1 / 3
[GOAL]
case a.convert_2
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 0 < 1 / 3
case a.convert_3 c : ℝ f g : ℕ → Bool n : ℕ ⊢ 1 / 3 < 1 / 2
[PROOFSTEP]
norm_num
[GOAL]
case a.convert_3
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 1 / 3 < 1 / 2
[PROOFSTEP]
norm_num
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ #↑Set.univ = 𝔠
[PROOFSTEP]
rw [mk_univ, mk_real]
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ ¬Set.Countable Set.univ
[PROOFSTEP]
rw [← le_aleph0_iff_set_countable, not_le, mk_univ_real]
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ ℵ₀ < 𝔠
[PROOFSTEP]
apply cantor
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
⊢ #↑(Ioi a) = 𝔠
[PROOFSTEP]
refine' le_antisymm (mk_real ▸ mk_set_le _) _
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
⊢ 𝔠 ≤ #↑(Ioi a)
[PROOFSTEP]
rw [← not_lt]
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
⊢ ¬#↑(Ioi a) < 𝔠
[PROOFSTEP]
intro h
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
⊢ False
[PROOFSTEP]
refine' _root_.ne_of_lt _ mk_univ_real
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
⊢ #↑Set.univ < 𝔠
[PROOFSTEP]
have hu : Iio a ∪ { a } ∪ Ioi a = Set.univ :=
  by
  convert @Iic_union_Ioi ℝ _ _
  exact Iio_union_right
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
⊢ Iio a ∪ {a} ∪ Ioi a = Set.univ
[PROOFSTEP]
convert @Iic_union_Ioi ℝ _ _
[GOAL]
case h.e'_2.h.e'_3
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
⊢ Iio a ∪ {a} = Iic a
[PROOFSTEP]
exact Iio_union_right
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #↑Set.univ < 𝔠
[PROOFSTEP]
rw [← hu]
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #↑(Iio a ∪ {a} ∪ Ioi a) < 𝔠
[PROOFSTEP]
refine' lt_of_le_of_lt (mk_union_le _ _) _
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #↑(Iio a ∪ {a}) + #↑(Ioi a) < 𝔠
[PROOFSTEP]
refine' lt_of_le_of_lt (add_le_add_right (mk_union_le _ _) _) _
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #↑(Iio a) + #↑{a} + #↑(Ioi a) < 𝔠
[PROOFSTEP]
have h2 : (fun x => a + a - x) '' Ioi a = Iio a :=
  by
  convert @image_const_sub_Ioi ℝ _ _ _
  simp
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ (fun x => a + a - x) '' Ioi a = Iio a
[PROOFSTEP]
convert @image_const_sub_Ioi ℝ _ _ _
[GOAL]
case h.e'_3.h.e'_3
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ a = a + a - a
[PROOFSTEP]
simp
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ #↑(Iio a) + #↑{a} + #↑(Ioi a) < 𝔠
[PROOFSTEP]
rw [← h2]
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ #↑((fun x => a + a - x) '' Ioi a) + #↑{a} + #↑(Ioi a) < 𝔠
[PROOFSTEP]
refine' add_lt_of_lt (cantor _).le _ h
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ #↑((fun x => a + a - x) '' Ioi a) + #↑{a} < 𝔠
[PROOFSTEP]
refine' add_lt_of_lt (cantor _).le (mk_image_le.trans_lt h) _
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ #↑{a} < 𝔠
[PROOFSTEP]
rw [mk_singleton]
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ 1 < 𝔠
[PROOFSTEP]
exact one_lt_aleph0.trans (cantor _)
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
⊢ #↑(Iio a) = 𝔠
[PROOFSTEP]
refine' le_antisymm (mk_real ▸ mk_set_le _) _
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
⊢ 𝔠 ≤ #↑(Iio a)
[PROOFSTEP]
have h2 : (fun x => a + a - x) '' Iio a = Ioi a := by simp only [image_const_sub_Iio, add_sub_cancel]
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
⊢ (fun x => a + a - x) '' Iio a = Ioi a
[PROOFSTEP]
simp only [image_const_sub_Iio, add_sub_cancel]
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a : ℝ
h2 : (fun x => a + a - x) '' Iio a = Ioi a
⊢ 𝔠 ≤ #↑(Iio a)
[PROOFSTEP]
exact mk_Ioi_real a ▸ h2 ▸ mk_image_le
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a b : ℝ
h : a < b
⊢ #↑(Ioo a b) = 𝔠
[PROOFSTEP]
refine' le_antisymm (mk_real ▸ mk_set_le _) _
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a b : ℝ
h : a < b
⊢ 𝔠 ≤ #↑(Ioo a b)
[PROOFSTEP]
have h1 : #((fun x => x - a) '' Ioo a b) ≤ #(Ioo a b) := mk_image_le
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a b : ℝ
h : a < b
h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)
⊢ 𝔠 ≤ #↑(Ioo a b)
[PROOFSTEP]
refine' le_trans _ h1
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a b : ℝ
h : a < b
h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)
⊢ 𝔠 ≤ #↑((fun x => x - a) '' Ioo a b)
[PROOFSTEP]
rw [image_sub_const_Ioo, sub_self]
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a b : ℝ
h : a < b
h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)
⊢ 𝔠 ≤ #↑(Ioo 0 (b - a))
[PROOFSTEP]
replace h := sub_pos_of_lt h
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a b : ℝ
h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)
h : 0 < b - a
⊢ 𝔠 ≤ #↑(Ioo 0 (b - a))
[PROOFSTEP]
have h2 : #(Inv.inv '' Ioo 0 (b - a)) ≤ #(Ioo 0 (b - a)) := mk_image_le
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a b : ℝ
h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)
h : 0 < b - a
h2 : #↑(Inv.inv '' Ioo 0 (b - a)) ≤ #↑(Ioo 0 (b - a))
⊢ 𝔠 ≤ #↑(Ioo 0 (b - a))
[PROOFSTEP]
refine' le_trans _ h2
[GOAL]
c : ℝ
f g : ℕ → Bool
n : ℕ
a b : ℝ
h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)
h : 0 < b - a
h2 : #↑(Inv.inv '' Ioo 0 (b - a)) ≤ #↑(Ioo 0 (b - a))
⊢ 𝔠 ≤ #↑(Inv.inv '' Ioo 0 (b - a))
[PROOFSTEP]
rw [image_inv, inv_Ioo_0_left h, mk_Ioi_real]
