awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
h : f n = true
⊢ g n = true

Tactic:
replace h3 : g n = true := h3 n h
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
h : f n = true
h3 : g n = true
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n

Tactic:
simp [h, h3]
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
rw :
  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)
⊢ cantorFunction c f = (bif f 0 then 1 else 0) + c * cantorFunction c fun (n : ℕ) ↦ f (n + 1)

Tactic:
rw [cantorFunction, (summable_cantor_function f h1 h2).tsum_eq_zero_add]

Premises used: Cardinal.cantorFunction, Summable.tsum_eq_zero_add, Cardinal.summable_cantor_function
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
rw :
  cantorFunctionAux c f 0 + ∑' (n : ℕ), c * cantorFunctionAux c (fun (n : ℕ) ↦ f (n + 1)) n =
    (bif f 0 then 1 else 0) + c * cantorFunction c fun (n : ℕ) ↦ f (n + 1)
rw₁ :
  cantorFunctionAux c f 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)
rw₂ :
  (bif f 0 then HPow.hPow (β := ℕ) c 0 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)
rw₃ :
  (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)
rw₄ rw₅ :
  (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 * ∑' (n : ℕ), cantorFunctionAux c (fun (n : ℕ) ↦ f (n + 1)) n
⊢ 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)

Tactic:
rw [cantorFunctionAux_succ, tsum_mul_left, cantorFunctionAux, pow_zero, cantorFunction]

Premises used: Cardinal.cantorFunction, Cardinal.cantorFunctionAux_succ, tsum_mul_left, pow_zero, Cardinal.cantorFunctionAux
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f g : ℕ → Bool
hn : ∀ k < n, f k = g k
fn : f n = false
gn : g n = true
apply : 1 / 2 < 1
⊢ c < 1

Tactic:
apply h2.trans

Premises used: LT.lt.trans
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f g : ℕ → Bool
hn : ∀ k < n, f k = g k
fn : f n = false
gn : g n = true
⊢ 1 / 2 < 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
n : ℕ
f g : ℕ → Bool
hn : ∀ k < n, f k = g k
fn : f n = false
gn : g n = true
⊢ c < 1

Tactic:
have h3 : c < 1 := by
    apply h2.trans
    norm_num
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn_1 : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
n : ℕ
hn : f n = true
zero : ∀ (hn : f 0 = true), f_max 0 = true
succ : ∀ (n : ℕ) (hn : f (n + 1) = true), f_max (n + 1) = true
⊢ f_max n = true

Tactic:
cases n
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn_1 : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hn : f 0 = true
⊢ false = true

Tactic:
rw [fn] at hn
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn_1 : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hn : false = true
⊢ f_max 0 = true

Tactic:
contradiction
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn_1 : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
n : ℕ
hn : f (n + 1) = true
⊢ f_max (n + 1) = true

Tactic:
simp [f_max]
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
⊢ ∀ (n : ℕ), f n = true → f_max n = true

Tactic:
have hf_max : ∀ n, f n → f_max n := by
      intro n hn
      cases n
      · rw [fn] at hn
        contradiction
      simp [f_max]
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn_1 : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) true (fun (x : ℕ) (x_1 : Bool) ↦ false) n
n : ℕ
hn : g_min n = true
zero : ∀ (hn : g_min 0 = true), g 0 = true
succ : ∀ (n : ℕ) (hn : g_min (n + 1) = true), g (n + 1) = true
⊢ g n = true

Tactic:
cases n
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn_1 : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) true (fun (x : ℕ) (x_1 : Bool) ↦ false) n
hn : g_min 0 = true
zero zero₁ : true = true
⊢ g 0 = true

Tactic:
rw [gn]
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn_1 : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) true (fun (x : ℕ) (x_1 : Bool) ↦ false) n
n : ℕ
hn : g_min (n + 1) = true
⊢ g (n + 1) = true

Tactic:
simp at hn
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) true (fun (x : ℕ) (x_1 : Bool) ↦ false) n
⊢ ∀ (n : ℕ), g_min n = true → g n = true

Tactic:
have hg_min : ∀ n, g_min n → g n := by
      intro n hn
      cases n
      · rw [gn]
      simp at hn
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) true (fun (x : ℕ) (x_1 : Bool) ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
zero : cantorFunction c f_max < cantorFunction c g
⊢ cantorFunction c f < cantorFunction c g

Tactic:
apply (cantorFunction_le (le_of_lt h1) h3 hf_max).trans_lt

Premises used: le_of_lt, LE.le.trans_lt, Cardinal.cantorFunction_le
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) true (fun (x : ℕ) (x_1 : Bool) ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ cantorFunction c f_max < cantorFunction c g

Tactic:
lt_of_lt_of_le ?_ (cantorFunction_le (le_of_lt h1) h3 hg_min)

Premises used: le_of_lt, lt_of_lt_of_le, Cardinal.cantorFunction_le
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) true (fun (x : ℕ) (x_1 : Bool) ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
zero : cantorFunction c f_max < cantorFunction c g_min
⊢ cantorFunction c f_max < cantorFunction c g

Tactic:
refine lt_of_lt_of_le ?_ (cantorFunction_le (le_of_lt h1) h3 hg_min)

Premises used: le_of_lt, lt_of_lt_of_le, Cardinal.cantorFunction_le
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) true (fun (x : ℕ) (x_1 : Bool) ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
rw : c + c < 1
rw₁ : 0 < 1 - c
⊢ c / (1 - c) < 1

Tactic:
rw [div_lt_one, lt_sub_iff_add_lt]

Premises used: div_lt_one, lt_sub_iff_add_lt
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) true (fun (x : ℕ) (x_1 : Bool) ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ c + c < 1 / 2 + 1 / 2

Tactic:
_root_.add_lt_add h2 h2

Premises used: add_lt_add
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) true (fun (x : ℕ) (x_1 : Bool) ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
h : 1 = 1 / 2 + 1 / 2
⊢ c + c < 1

Tactic:
convert! _root_.add_lt_add h2 h2

Premises used: add_lt_add
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) true (fun (x : ℕ) (x_1 : Bool) ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ 1 = 1 / 2 + 1 / 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) true (fun (x : ℕ) (x_1 : Bool) ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
rwa rwa₁ rwa₂ rwa₃ : c < 1
⊢ 0 < 1 - c

Tactic:
rwa [sub_pos]

Premises used: sub_pos
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) true (fun (x : ℕ) (x_1 : Bool) ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
⊢ c / (1 - c) < 1

Tactic:
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]
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) true (fun (x : ℕ) (x_1 : Bool) ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ c / (1 - c) < 1

Tactic:
this
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) true (fun (x : ℕ) (x_1 : Bool) ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
h : cantorFunction c f_max = c / (1 - c)
h₁ : cantorFunction c g_min = 1
⊢ cantorFunction c f_max < cantorFunction c g_min

Tactic:
convert! this
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) true (fun (x : ℕ) (x_1 : Bool) ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
h : ((bif f_max 0 then 1 else 0) + c * cantorFunction c fun (n : ℕ) ↦ f_max (n + 1)) = c * ∑' (n : ℕ), c ^ n
⊢ cantorFunction c f_max = c / (1 - c)

Tactic:
rw [cantorFunction_succ _ (le_of_lt h1) h3, div_eq_mul_inv, ←
        tsum_geometric_of_lt_one (le_of_lt h1) h3]

Premises used: le_of_lt, tsum_geometric_of_lt_one, div_eq_mul_inv, Cardinal.cantorFunction_succ
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) true (fun (x : ℕ) (x_1 : Bool) ↦ 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

Tactic:
apply zero_add

Premises used: zero_add
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) true (fun (x : ℕ) (x_1 : Bool) ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ cantorFunction c g_min = 1

Tactic:
(tsum_eq_single 0 ?_).trans ?_

Premises used: Cardinal.cantorFunction, tsum_eq_single, OfNat.ofNat, Eq.trans
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) true (fun (x : ℕ) (x_1 : Bool) ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
h : ∀ (b' : ℕ), b' ≠ 0 → cantorFunctionAux c g_min b' = 0
h₁ : cantorFunctionAux c g_min 0 = 1
⊢ cantorFunction c g_min = 1

Tactic:
refine (tsum_eq_single 0 ?_).trans ?_

Premises used: tsum_eq_single, OfNat.ofNat, Eq.trans
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn_1 : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) true (fun (x : ℕ) (x_1 : Bool) ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
n : ℕ
hn : n ≠ 0
h : ∀ (hn : Ne (α := ℕ) 0 0), cantorFunctionAux c g_min 0 = 0
h₁ : ∀ (n : ℕ) (hn : n + 1 ≠ 0), cantorFunctionAux c g_min (n + 1) = 0
⊢ cantorFunctionAux c g_min n = 0

Tactic:
cases n
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn_1 : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) true (fun (x : ℕ) (x_1 : Bool) ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
hn : Ne (α := ℕ) 0 0
⊢ cantorFunctionAux c g_min 0 = 0

Tactic:
contradiction
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn_1 : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) true (fun (x : ℕ) (x_1 : Bool) ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
n : ℕ
hn : n + 1 ≠ 0
⊢ cantorFunctionAux c g_min (n + 1) = 0

Tactic:
simp [g_min]
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) true (fun (x : ℕ) (x_1 : Bool) ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ cantorFunctionAux c g_min 0 = 1

Tactic:
cantorFunctionAux_zero _

Premises used: cond, Cardinal.cantorFunctionAux_zero
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) false (fun (x : ℕ) (x_1 : Bool) ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun (n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ Bool) true (fun (x : ℕ) (x_1 : Bool) ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ cantorFunctionAux c g_min 0 = 1

Tactic:
exact cantorFunctionAux_zero _

Premises used: Cardinal.cantorFunctionAux_zero
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
n : ℕ
ih :
  ∀ {f g : ℕ → Bool} (hn : ∀ k < n, f k = g k) (fn : f n = false) (gn : g n = true),
    cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ k < n + 1, f k = g k
fn : f (n + 1) = false
gn : g (n + 1) = true
succ :
  ((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)
⊢ cantorFunction c f < cantorFunction c g

Tactic:
rw [cantorFunction_succ f h1.le h3, cantorFunction_succ g h1.le h3]

Premises used: LT.lt.le, Cardinal.cantorFunction_succ
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
n : ℕ
ih :
  ∀ {f g : ℕ → Bool} (hn : ∀ k < n, f k = g k) (fn : f n = false) (gn : g n = true),
    cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ k < n + 1, f k = g k
fn : f (n + 1) = false
gn : g (n + 1) = true
succ :
  ((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)
⊢ ((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)

Tactic:
rw [hn 0 <| zero_lt_succ n]

Premises used: Nat.zero_lt_succ, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
n : ℕ
ih :
  ∀ {f g : ℕ → Bool} (hn : ∀ k < n, f k = g k) (fn : f n = false) (gn : g n = true),
    cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ k < n + 1, f k = g k
fn : f (n + 1) = false
gn : g (n + 1) = true
succ : (cantorFunction c fun (n : ℕ) ↦ f (n + 1)) < cantorFunction c fun (n : ℕ) ↦ g (n + 1)
⊢ ((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)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
n : ℕ
ih :
  ∀ {f g : ℕ → Bool} (hn : ∀ k < n, f k = g k) (fn : f n = false) (gn : g n = true),
    cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ k < n + 1, f k = g k
fn : f (n + 1) = false
gn : g (n + 1) = true
⊢ (cantorFunction c fun (n : ℕ) ↦ f (n + 1)) < cantorFunction c fun (n : ℕ) ↦ g (n + 1)

Tactic:
ih (fun k hk => hn _ <| Nat.succ_lt_succ hk) fn gn

Premises used: Nat.succ_lt_succ, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
n : ℕ
ih :
  ∀ {f g : ℕ → Bool} (hn : ∀ k < n, f k = g k) (fn : f n = false) (gn : g n = true),
    cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ k < n + 1, f k = g k
fn : f (n + 1) = false
gn : g (n + 1) = true
⊢ (cantorFunction c fun (n : ℕ) ↦ f (n + 1)) < cantorFunction c fun (n : ℕ) ↦ g (n + 1)

Tactic:
exact ih (fun k hk => hn _ <| Nat.succ_lt_succ hk) fn gn

Premises used: Nat.succ_lt_succ, Nat.succ