awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
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
⊢ c / (1 - c) < 1
have rw₁ : 0 < 1 - c
Tactic: rw [div_lt_one, lt_sub_iff_add_lt]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
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
have h : 1 = 1 / 2 + 1 / 2
Tactic: convert! _root_.add_lt_add h2 h2
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (hypothesis)
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_min
have this : 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]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
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 f_max < cantorFunction c g_min
have h : cantorFunction c f_max = c / (1 - c)
Tactic: convert! this
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
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)
⊢ cantorFunction c f_max < cantorFunction c g_min
have h₁ : cantorFunction c g_min = 1
Tactic: convert! this
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
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 f_max = c / (1 - c)
have h : ((bif f_max 0 then 1 else 0) + c * cantorFunction c fun (n : ℕ) ↦ f_max (n + 1)) = c * ∑' (n : ℕ), c ^ n
Tactic: rw [cantorFunction_succ _ (le_of_lt h1) h3, div_eq_mul_inv, ←
        tsum_geometric_of_lt_one (le_of_lt h1) h3]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
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
have h : ∀ (b' : ℕ), b' ≠ 0 → cantorFunctionAux c g_min b' = 0
Tactic: refine (tsum_eq_single 0 ?_).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
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
⊢ cantorFunction c g_min = 1
have h₁ : cantorFunctionAux c g_min 0 = 1
Tactic: refine (tsum_eq_single 0 ?_).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
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
⊢ cantorFunctionAux c g_min n = 0
have h : ∀ (hn : Ne (α := ℕ) 0 0), cantorFunctionAux c g_min 0 = 0
Tactic: cases n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
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
⊢ cantorFunctionAux c g_min n = 0
have h₁ : ∀ (n : ℕ) (hn : n + 1 ≠ 0), cantorFunctionAux c g_min (n + 1) = 0
Tactic: cases n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
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 f < cantorFunction c g
have 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)
Tactic: rw [cantorFunction_succ f h1.le h3, cantorFunction_succ g h1.le h3]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
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
⊢ ((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)
have 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)
Tactic: rw [hn 0 <| zero_lt_succ n]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
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
⊢ ((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)
have succ : (cantorFunction c fun (n : ℕ) ↦ f (n + 1)) < cantorFunction c fun (n : ℕ) ↦ g (n + 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
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
h3 : c < 1
⊢ cantorFunction c f < cantorFunction c g
have zero : ∀ {f g : ℕ → Bool} (hn : ∀ k < 0, f k = g k) (fn : f 0 = false) (gn : g 0 = true),
  cantorFunction c f < cantorFunction c g
Tactic: induction n generalizing f g with
  | zero =>
    let f_max : ℕ → Bool := fun n => Nat.rec false (fun _ _ => true) n
    have hf_max : ∀ n, f n → f_max n := by
      intro n hn
      cases n
      · rw [fn] at hn
        contradiction
      simp [f_max]
    let g_min : ℕ → Bool := fun n => Nat.rec true (fun _ _ => false) n
    have hg_min : ∀ n, g_min n → g n := by
      intro n hn
      cases n
      · rw [gn]
      simp at hn
    apply (cantorFunction_le (le_of_lt h1) h3 hf_max).trans_lt
    refine lt_of_lt_of_le ?_ (cantorFunction_le (le_of_lt h1) h3 hg_min)
    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]
    convert! this
    · rw [cantorFunction_succ _ (le_of_lt h1) h3, div_eq_mul_inv, ←
        tsum_geometric_of_lt_one (le_of_lt h1) h3]
      apply zero_add
    · refine (tsum_eq_single 0 ?_).trans ?_
      · intro n hn
        cases n
        · contradiction
        simp [g_min]
      · exact cantorFunctionAux_zero _
  | succ n ih =>
  rw [cantorFunction_succ f h1.le h3, cantorFunction_succ g h1.le h3]
  rw [hn 0 <| zero_lt_succ n]
  gcongr
  exact ih (fun k hk => hn _ <| Nat.succ_lt_succ hk) fn gn
Cleared hypotheses: n, f, g, hn, fn, gn
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
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
h3 : c < 1
zero :
  ∀ {f g : ℕ → Bool} (hn : ∀ k < 0, f k = g k) (fn : f 0 = false) (gn : g 0 = true),
    cantorFunction c f < cantorFunction c g
⊢ cantorFunction c f < cantorFunction c g
have succ : ∀ (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 f < cantorFunction c g
Tactic: induction n generalizing f g with
  | zero =>
    let f_max : ℕ → Bool := fun n => Nat.rec false (fun _ _ => true) n
    have hf_max : ∀ n, f n → f_max n := by
      intro n hn
      cases n
      · rw [fn] at hn
        contradiction
      simp [f_max]
    let g_min : ℕ → Bool := fun n => Nat.rec true (fun _ _ => false) n
    have hg_min : ∀ n, g_min n → g n := by
      intro n hn
      cases n
      · rw [gn]
      simp at hn
    apply (cantorFunction_le (le_of_lt h1) h3 hf_max).trans_lt
    refine lt_of_lt_of_le ?_ (cantorFunction_le (le_of_lt h1) h3 hg_min)
    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]
    convert! this
    · rw [cantorFunction_succ _ (le_of_lt h1) h3, div_eq_mul_inv, ←
        tsum_geometric_of_lt_one (le_of_lt h1) h3]
      apply zero_add
    · refine (tsum_eq_single 0 ?_).trans ?_
      · intro n hn
        cases n
        · contradiction
        simp [g_min]
      · exact cantorFunctionAux_zero _
  | succ n ih =>
  rw [cantorFunction_succ f h1.le h3, cantorFunction_succ g h1.le h3]
  rw [hn 0 <| zero_lt_succ n]
  gcongr
  exact ih (fun k hk => hn _ <| Nat.succ_lt_succ hk) fn gn
Cleared hypotheses: n, f, g, hn, fn, gn
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
hfg : cantorFunction c f = cantorFunction c g
⊢ f = g
have contrapose : ∀ (h : ¬f = g), ¬cantorFunction c f = cantorFunction c g
Tactic: contrapose hfg with h
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (hypothesis)
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
⊢ ¬cantorFunction c f = cantorFunction c g
have this : ∃ (n : ℕ), f n ≠ g n
Tactic: have : ∃ n, f n ≠ g n := Function.ne_iff.mp h
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
k : ℕ
hk : k < n
⊢ f k = g k
have a : ¬¬f k = g k
Tactic: apply of_not_not
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (hypothesis)
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
⊢ ¬cantorFunction c f = cantorFunction c g
have hn : ∀ k < n, f k = g k
Tactic: have hn : ∀ k : ℕ, k < n → f k = g k := by
      intro k hk
      apply of_not_not
      exact Nat.find_min this hk
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
⊢ ¬cantorFunction c f = cantorFunction c g
have false : ∀ (fn : f n = false), ¬cantorFunction c f = cantorFunction c g
Tactic: cases fn : f n
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
false : ∀ (fn : f n = Bool.false), ¬cantorFunction c f = cantorFunction c g
⊢ ¬cantorFunction c f = cantorFunction c g
have true : ∀ (fn : f n = true), ¬cantorFunction c f = cantorFunction c g
Tactic: cases fn : f n
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = false
⊢ ¬cantorFunction c f = cantorFunction c g
have false : cantorFunction c f < cantorFunction c g
Tactic: apply _root_.ne_of_lt
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = false
⊢ cantorFunction c f < cantorFunction c g
have false : g n = true
Tactic: refine increasing_cantorFunction h1 h2 hn fn ?_
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = false
⊢ g n = true
have false : ¬g n = false
Tactic: apply Bool.eq_true_of_not_eq_false
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = false
⊢ ¬g n = false
have false : ¬g n = f n
Tactic: rw [← fn]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = false
⊢ ¬g n = f n
have false : f n ≠ g n
Tactic: apply Ne.symm
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = true
⊢ ¬cantorFunction c f = cantorFunction c g
have true : cantorFunction c g < cantorFunction c f
Tactic: apply _root_.ne_of_gt
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = true
⊢ cantorFunction c g < cantorFunction c f
have true : g n = false
Tactic: refine increasing_cantorFunction h1 h2 (fun k hk => (hn k hk).symm) ?_ fn
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = true
⊢ g n = false
have true : ¬g n = true
Tactic: apply Bool.eq_false_of_not_eq_true
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = true
⊢ ¬g n = true
have true : ¬g n = f n
Tactic: rw [← fn]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ (n : ℕ), f n ≠ g n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this
hn : ∀ k < n, f k = g k
fn : f n = true
⊢ ¬g n = f n
have true : f n ≠ g n
Tactic: apply Ne.symm
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
hfg : cantorFunction c f = cantorFunction c g
⊢ f = g
have contrapose : ∀ (hfg : cantorFunction c f = cantorFunction c g), f = g
Tactic: classical
    contrapose hfg with h
    have : ∃ n, f n ≠ g n := Function.ne_iff.mp 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
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
hfg : cantorFunction c f = cantorFunction c g
contrapose contrapose₁ : ∀ (hfg : cantorFunction c f = cantorFunction c g), f = g
⊢ f = g
have contrapose₂ : ¬f = g → ¬cantorFunction c f = cantorFunction c g
Tactic: classical
    contrapose hfg with h
    have : ∃ n, f n ≠ g n := Function.ne_iff.mp 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
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
hfg : cantorFunction c f = cantorFunction c g
contrapose contrapose₁ : ∀ (hfg : cantorFunction c f = cantorFunction c g), f = g
contrapose₂ contrapose₃ contrapose₄ : ∀ (h : ¬f = g), ¬cantorFunction c f = cantorFunction c g
⊢ f = g
have contrapose₅ : ∀ (h : ¬f = g) (this : ∃ (n : ℕ), f n ≠ g n), ¬cantorFunction c f = cantorFunction c g
Tactic: classical
    contrapose hfg with h
    have : ∃ n, f n ≠ g n := Function.ne_iff.mp 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
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
hfg : cantorFunction c f = cantorFunction c g
contrapose contrapose₁ : ∀ (hfg : cantorFunction c f = cantorFunction c g), f = g
contrapose₂ contrapose₃ contrapose₄ : ∀ (h : ¬f = g), ¬cantorFunction c f = cantorFunction c g
contrapose₅ contrapose₆ : ∀ (h : ¬f = g) (this : ∃ (n : ℕ), f n ≠ g n), ¬cantorFunction c f = cantorFunction c g
⊢ f = g
have contrapose₇ : ∀ (h : ¬f = g) (this : ∃ (n : ℕ), f n ≠ g n),
  let n := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this;
  ∀ (hn : ∀ k < n, f k = g k), ¬cantorFunction c f = cantorFunction c g
Tactic: classical
    contrapose hfg with h
    have : ∃ n, f n ≠ g n := Function.ne_iff.mp 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
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
hfg : cantorFunction c f = cantorFunction c g
contrapose contrapose₁ : ∀ (hfg : cantorFunction c f = cantorFunction c g), f = g
contrapose₂ contrapose₃ contrapose₄ : ∀ (h : ¬f = g), ¬cantorFunction c f = cantorFunction c g
contrapose₅ contrapose₆ : ∀ (h : ¬f = g) (this : ∃ (n : ℕ), f n ≠ g n), ¬cantorFunction c f = cantorFunction c g
contrapose₇ :
  ∀ (h : ¬f = g) (this : ∃ (n : ℕ), f n ≠ g n),
    let n := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this;
    ∀ (hn : ∀ k < n, f k = g k), ¬cantorFunction c f = cantorFunction c g
⊢ f = g
have false : ∀ (h : ¬f = g) (this : ∃ (n : ℕ), f n ≠ g n),
  let n := Nat.find (p := fun (n : ℕ) ↦ f n ≠ g n) this;
  ∀ (hn : ∀ k < n, f k = g k) (fn : f n = false), ¬cantorFunction c f = cantorFunction c g
Tactic: classical
    contrapose hfg with h
    have : ∃ n, f n ≠ g n := Function.ne_iff.mp 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
Cleared hypotheses: hfg