awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
⊢ sqrt a = (↑√((re : (a : 𝕜) → ℝ) a) : 𝕜)
have inr : (↑√(Complex.re ((complexRingEquiv h : (a : 𝕜) → ℂ) a)) : ℂ) =
  (complexRingEquiv h : (a : 𝕜) → ℂ) (↑√((re : (a : 𝕜) → ℝ) a) : 𝕜)
Tactic: rw [sqrt_eq_ite, dif_pos h, RingEquiv.symm_apply_eq, Complex.sqrt_of_nonneg (by simpa)]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
a : ℂ
ha : 0 ≤ a
⊢ (-a).sqrt = I * a.sqrt
have obtain : ∀ (α : ℝ) (hα : α ≥ 0) (ha : LE.le (α := ℂ) 0 (↑α : ℂ)), sqrt (-(↑α : ℂ)) = I * sqrt (↑α : ℂ)
Tactic: obtain ⟨α, hα, rfl⟩ := RCLike.nonneg_iff_exists_ofReal.mp ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
α : ℝ
hα : α ≥ 0
ha : LE.le (α := ℂ) 0 (↑α : ℂ)
⊢ sqrt (-(↑α : ℂ)) = I * sqrt (↑α : ℂ)
have rw : sqrt (-(↑α : ℂ)) = I * (↑√(re (↑α : ℂ)) : ℂ)
Tactic: rw [Complex.sqrt_of_nonneg ha]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
α : ℝ
hα : α ≥ 0
ha : LE.le (α := ℂ) 0 (↑α : ℂ)
⊢ sqrt (-(↑α : ℂ)) = I * (↑√(re (↑α : ℂ)) : ℂ)
have simp : (-(↑α : ℂ)).sqrt = I * (↑√α : ℂ)
Tactic: simp only [coe_algebraMap, ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
α : ℝ
hα : α ≥ 0
ha : LE.le (α := ℂ) 0 (↑α : ℂ)
⊢ (-(↑α : ℂ)).sqrt = I * (↑√α : ℂ)
have rw : (↑(-(↑α : ℂ)).sqrt.re : ℂ) + (↑(-(↑α : ℂ)).sqrt.im : ℂ) * I = I * (↑√α : ℂ)
Tactic: rw [← re_add_im (-(α : ℂ)).sqrt]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
⊢ sqrt (-a) = I * sqrt a
have inl : ∀ (h : Eq.{u_1 + 1} (α := 𝕜) I 0), sqrt (-a) = I * sqrt a
Tactic: obtain (h | h) := I_eq_zero_or_im_I_eq_one (K := 𝕜)
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
inl : ∀ (h : Eq.{u_1 + 1} (α := 𝕜) I 0), sqrt (-a) = I * sqrt a
⊢ sqrt (-a) = I * sqrt a
have inr : ∀ (h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)), sqrt (-a) = I * sqrt a
Tactic: obtain (h | h) := I_eq_zero_or_im_I_eq_one (K := 𝕜)
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
⊢ sqrt (-a) = I * sqrt a
have inr : Complex.I * Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) a) = (complexRingEquiv h : (a : 𝕜) → ℂ) (I * sqrt a)
Tactic: rw [sqrt_eq_ite, dif_pos h, RingEquiv.symm_apply_eq, map_neg,
    Complex.sqrt_neg_of_nonneg (by simpa)]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
⊢ I.sqrt = (↑√2⁻¹ : ℂ) * (1 + I)
have rw : (↑√((‖I‖ + I.re) / 2) : ℂ) + (↑√((‖I‖ - I.re) / 2) : ℂ) * I = (↑√2⁻¹ : ℂ) * (1 + I)
Tactic: rw [sqrt, ← re_add_im (I ^ 2⁻¹), cpow_inv_two_im_eq_sqrt (by simp), cpow_inv_two_re]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
⊢ (-I).sqrt = (↑√2⁻¹ : ℂ) * (1 - I)
have rw : (↑√((‖-I‖ + (-I).re) / 2) : ℂ) + (↑(-√((‖-I‖ - (-I).re) / 2)) : ℂ) * I = (↑√2⁻¹ : ℂ) * (1 - I)
Tactic: rw [sqrt, ← re_add_im ((-I) ^ 2⁻¹), cpow_inv_two_im_eq_neg_sqrt (by simp), cpow_inv_two_re]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
⊢ sqrt I = (↑√2⁻¹ : 𝕜) * HSub.hSub (α := 𝕜) 1 I * I
have rw : (if h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ) then
    ((complexRingEquiv h).symm : (a : ℂ) → 𝕜) (Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) I))
  else (↑√((re : (a : 𝕜) → ℝ) I) : 𝕜)) =
  (↑√2⁻¹ : 𝕜) * HSub.hSub (α := 𝕜) 1 I * I
Tactic: rw [sqrt_eq_ite]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
⊢ (if h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ) then
      ((complexRingEquiv h).symm : (a : ℂ) → 𝕜) (Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) I))
    else (↑√((re : (a : 𝕜) → ℝ) I) : 𝕜)) =
    (↑√2⁻¹ : 𝕜) * HSub.hSub (α := 𝕜) 1 I * I
have pos : ∀ (h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)),
  ((complexRingEquiv h).symm : (a : ℂ) → 𝕜) (Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) I)) =
    (↑√2⁻¹ : 𝕜) * HSub.hSub (α := 𝕜) 1 I * I
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
pos :
  ∀ (h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)),
    ((complexRingEquiv h).symm : (a : ℂ) → 𝕜) (Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) I)) =
      (↑√2⁻¹ : 𝕜) * HSub.hSub (α := 𝕜) 1 I * I
⊢ (if h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ) then
      ((complexRingEquiv h).symm : (a : ℂ) → 𝕜) (Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) I))
    else (↑√((re : (a : 𝕜) → ℝ) I) : 𝕜)) =
    (↑√2⁻¹ : 𝕜) * HSub.hSub (α := 𝕜) 1 I * I
have neg : ∀ (h : ¬Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)),
  (↑√((re : (a : 𝕜) → ℝ) I) : 𝕜) = (↑√2⁻¹ : 𝕜) * HSub.hSub (α := 𝕜) 1 I * I
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
⊢ ((complexRingEquiv h).symm : (a : ℂ) → 𝕜) (Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) I)) =
    (↑√2⁻¹ : 𝕜) * HSub.hSub (α := 𝕜) 1 I * I
have pos : Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) I) =
  HMul.hMul (β := ℂ)
    (HMul.hMul (α := ℂ) (β := ℂ) ((complexRingEquiv h : (a : 𝕜) → ℂ) (↑√2⁻¹ : 𝕜) : ℂ)
      ((complexRingEquiv h : (a : 𝕜) → ℂ) (HSub.hSub (α := 𝕜) 1 I) : ℂ))
    ((complexRingEquiv h : (a : 𝕜) → ℂ) I : ℂ)
Tactic: simp_rw [RingEquiv.symm_apply_eq, map_mul]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
⊢ sqrt (-I) = (↑√2⁻¹ : 𝕜) * HAdd.hAdd (α := 𝕜) 1 I * -I
have rw : (if h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ) then
    ((complexRingEquiv h).symm : (a : ℂ) → 𝕜) (Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) (-I)))
  else (↑√((re : (a : 𝕜) → ℝ) (-I)) : 𝕜)) =
  (↑√2⁻¹ : 𝕜) * HAdd.hAdd (α := 𝕜) 1 I * -I
Tactic: rw [sqrt_eq_ite]
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
⊢ (if h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ) then
      ((complexRingEquiv h).symm : (a : ℂ) → 𝕜) (Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) (-I)))
    else (↑√((re : (a : 𝕜) → ℝ) (-I)) : 𝕜)) =
    (↑√2⁻¹ : 𝕜) * HAdd.hAdd (α := 𝕜) 1 I * -I
have pos : ∀ (h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)),
  ((complexRingEquiv h).symm : (a : ℂ) → 𝕜) (Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) (-I))) =
    (↑√2⁻¹ : 𝕜) * HAdd.hAdd (α := 𝕜) 1 I * -I
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
pos :
  ∀ (h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)),
    ((complexRingEquiv h).symm : (a : ℂ) → 𝕜) (Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) (-I))) =
      (↑√2⁻¹ : 𝕜) * HAdd.hAdd (α := 𝕜) 1 I * -I
⊢ (if h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ) then
      ((complexRingEquiv h).symm : (a : ℂ) → 𝕜) (Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) (-I)))
    else (↑√((re : (a : 𝕜) → ℝ) (-I)) : 𝕜)) =
    (↑√2⁻¹ : 𝕜) * HAdd.hAdd (α := 𝕜) 1 I * -I
have neg : ∀ (h : ¬Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)),
  (↑√((re : (a : 𝕜) → ℝ) (-I)) : 𝕜) = (↑√2⁻¹ : 𝕜) * HAdd.hAdd (α := 𝕜) 1 I * -I
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.RCLike.Sqrt (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
h : Eq (α := ℝ) ((im : (a : 𝕜) → ℝ) I : ℝ) (1 : ℝ)
⊢ ((complexRingEquiv h).symm : (a : ℂ) → 𝕜) (Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) (-I))) =
    (↑√2⁻¹ : 𝕜) * HAdd.hAdd (α := 𝕜) 1 I * -I
have pos : Complex.sqrt ((complexRingEquiv h : (a : 𝕜) → ℂ) (-I)) =
  HMul.hMul (β := ℂ)
    (HMul.hMul (α := ℂ) (β := ℂ) ((complexRingEquiv h : (a : 𝕜) → ℂ) (↑√2⁻¹ : 𝕜) : ℂ)
      ((complexRingEquiv h : (a : 𝕜) → ℂ) (HAdd.hAdd (α := 𝕜) 1 I) : ℂ))
    ((complexRingEquiv h : (a : 𝕜) → ℂ) (-I) : ℂ)
Tactic: simp_rw [RingEquiv.symm_apply_eq, map_mul]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
f : ℕ → Bool
n : ℕ
h : 0 ≤ c
⊢ 0 ≤ cantorFunctionAux c f n
have false : ∀ (h' : f n = false), 0 ≤ cantorFunctionAux c f n
Tactic: cases h' : f n
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
f : ℕ → Bool
n : ℕ
h : 0 ≤ c
false : ∀ (h' : f n = Bool.false), 0 ≤ cantorFunctionAux c f n
⊢ 0 ≤ cantorFunctionAux c f n
have true : ∀ (h' : f n = true), 0 ≤ cantorFunctionAux c f n
Tactic: cases h' : f n
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
f : ℕ → Bool
⊢ cantorFunctionAux c f 0 = bif f 0 then 1 else 0
have false : ∀ (h : f 0 = false), cantorFunctionAux c f 0 = bif false then 1 else 0
Tactic: cases h : f 0
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
f : ℕ → Bool
false : ∀ (h : f 0 = Bool.false), cantorFunctionAux c f 0 = bif Bool.false then 1 else 0
⊢ cantorFunctionAux c f 0 = bif f 0 then 1 else 0
have true : ∀ (h : f 0 = true), cantorFunctionAux c f 0 = bif true then 1 else 0
Tactic: cases h : f 0
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
f : ℕ → Bool
⊢ Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ cantorFunctionAux c f (n + 1)) fun (n : ℕ) ↦
    c * cantorFunctionAux c (fun (n : ℕ) ↦ f (n + 1)) n
have h : ∀ (n : ℕ), cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun (n : ℕ) ↦ f (n + 1)) n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
f : ℕ → Bool
n : ℕ
⊢ cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun (n : ℕ) ↦ f (n + 1)) n
have h : ∀ (h : f (n + 1) = false), cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun (n : ℕ) ↦ f (n + 1)) n
Tactic: cases h : f (n + 1)
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
f : ℕ → Bool
n : ℕ
h : ∀ (h : f (n + 1) = false), cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun (n : ℕ) ↦ f (n + 1)) n
⊢ cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun (n : ℕ) ↦ f (n + 1)) n
have h₁ : ∀ (h : f (n + 1) = true), cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun (n : ℕ) ↦ f (n + 1)) n
Tactic: cases h : f (n + 1)
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
⊢ Summable (cantorFunctionAux c f)
have apply : ∀ (b : ℕ), cantorFunctionAux c f b = 0 ∨ cantorFunctionAux c f b = c ^ b
Tactic: apply (summable_geometric_of_lt_one h1 h2).summable_of_eq_zero_or_self
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
⊢ cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n
have false : ∀ (h : f n = false), cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n
Tactic: cases h : f n
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
false : ∀ (h : f n = Bool.false), cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n
⊢ cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n
have true : ∀ (h : f n = true), cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n
Tactic: cases h : f n
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
⊢ cantorFunction c f ≤ cantorFunction c g
have apply : ∀ (i : ℕ), cantorFunctionAux c f i ≤ cantorFunctionAux c g i
Tactic: apply (summable_cantor_function f h1 h2).tsum_le_tsum _ (summable_cantor_function g h1 h2)
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n
have false : ∀ (h : f n = false), cantorFunctionAux c f n ≤ cantorFunctionAux c g n
Tactic: cases h : f n
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
false : ∀ (h : f n = Bool.false), cantorFunctionAux c f n ≤ cantorFunctionAux c g n
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n
have true : ∀ (h : f n = true), cantorFunctionAux c f n ≤ cantorFunctionAux c g n
Tactic: cases h : f n
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (hypothesis)
Goal:
c : ℝ
f g : ℕ → Bool
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
have h3₁ : g n = true
Tactic: replace h3 : g n = true := h3 n h
Cleared hypotheses: h3
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
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)
have 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)
Tactic: rw [cantorFunction, (summable_cantor_function f h1 h2).tsum_eq_zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
Goal:
c : ℝ
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)
have 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)
Tactic: rw [cantorFunctionAux_succ, tsum_mul_left, cantorFunctionAux, pow_zero, cantorFunction]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
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)
⊢ 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)
have 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)
Tactic: rw [cantorFunctionAux_succ, tsum_mul_left, cantorFunctionAux, pow_zero, cantorFunction]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
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)
⊢ 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)
have 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)
Tactic: rw [cantorFunctionAux_succ, tsum_mul_left, cantorFunctionAux, pow_zero, cantorFunction]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
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)
⊢ 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)
have 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)
Tactic: rw [cantorFunctionAux_succ, tsum_mul_left, cantorFunctionAux, pow_zero, cantorFunction]
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (goal)
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)
⊢ 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)
have 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
Tactic: rw [cantorFunctionAux_succ, tsum_mul_left, cantorFunctionAux, pow_zero, cantorFunction]
-- 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
⊢ c < 1
have apply : 1 / 2 < 1
Tactic: apply h2.trans
-- Lean 4 proof step from Mathlib.Analysis.Real.Cardinality (hypothesis)
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
⊢ cantorFunction c f < cantorFunction c g
have h3 : c < 1
Tactic: have h3 : c < 1 := by
    apply h2.trans
    norm_num
-- 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
n : ℕ
hn : f n = true
⊢ f_max n = true
have zero : ∀ (hn : f 0 = true), f_max 0 = true
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
n : ℕ
hn : f n = true
zero : ∀ (hn : f 0 = true), f_max 0 = true
⊢ f_max n = true
have succ : ∀ (n : ℕ) (hn : f (n + 1) = true), f_max (n + 1) = true
Tactic: cases n
Cleared hypotheses: n, hn
-- 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_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
⊢ f_max 0 = true
have hn₁ : false = true
Tactic: rw [fn] at hn
Cleared hypotheses: hn
-- 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
⊢ cantorFunction c f < cantorFunction c g
have hf_max : ∀ (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]
-- 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
n : ℕ
hn : g_min n = true
⊢ g n = true
have zero : ∀ (hn : g_min 0 = true), g 0 = true
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
n : ℕ
hn : g_min n = true
zero : ∀ (hn : g_min 0 = true), g 0 = true
⊢ g n = true
have succ : ∀ (n : ℕ) (hn : g_min (n + 1) = true), g (n + 1) = true
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
hn : g_min 0 = true
⊢ g 0 = true
have zero : true = true
Tactic: rw [gn]
-- 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
⊢ cantorFunction c f < cantorFunction c g
have hg_min : ∀ (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
-- 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
⊢ cantorFunction c f < cantorFunction c g
have zero : cantorFunction c f_max < cantorFunction c g
Tactic: apply (cantorFunction_le (le_of_lt h1) h3 hf_max).trans_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
⊢ cantorFunction c f_max < cantorFunction c g
have zero : cantorFunction c f_max < cantorFunction c g_min
Tactic: refine lt_of_lt_of_le ?_ (cantorFunction_le (le_of_lt h1) h3 hg_min)
-- 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 / (1 - c) < 1
have rw : c + c < 1
Tactic: rw [div_lt_one, lt_sub_iff_add_lt]