c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
hfg : cantorFunction c f = cantorFunction c g
⊢ f = g
c : ℝ
f g : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
⊢ Function.Injective (cantorFunction c)
intro f g hfg
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
c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
hfg : cantorFunction c f = cantorFunction c g
⊢ f = g
by_contra h
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
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
revert hfg
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
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
have : ∃ n, f n ≠ g n := by
  rw [← not_forall]
  intro h'
  apply h
  ext
  apply 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
⊢ cantorFunction c f = cantorFunction c g → 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
⊢ cantorFunction c f = cantorFunction c g → False
let n := Nat.find this
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
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
have hn : ∀ k : ℕ, k < n → f k = g k := by
  intro k hk
  apply of_not_not
  exact Nat.find_min this hk
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

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
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
cases fn : f n
c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
⊢ ¬∀ (x : ℕ), f x = g x
c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
⊢ ∃ n, f n ≠ g n
rw [← not_forall]
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
c : ℝ
f✝ g✝ : ℕ → Bool
n : ℕ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
⊢ ¬∀ (x : ℕ), f x = g x
intro 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
⊢ f = g
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
apply h
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✝
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
ext
no goals
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✝
apply 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
k : ℕ
hk : k < n
⊢ f k = g k
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
intro k hk
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
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
apply of_not_not
no goals
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
exact Nat.find_min this hk
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
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
apply _root_.ne_of_lt
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
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
refine' increasing_cantorFunction h1 h2 hn fn _
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
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
apply Bool.eq_true_of_not_eq_false
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
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
rw [← fn]
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
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
apply Ne.symm
no goals
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
exact Nat.find_spec this
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
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
apply _root_.ne_of_gt
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
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
refine' increasing_cantorFunction h1 h2 (fun k hk => (hn k hk).symm) _ fn
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
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
apply Bool.eq_false_of_not_eq_true
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
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
rw [← fn]
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
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
apply Ne.symm
no goals
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
exact Nat.find_spec this