awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
this : b ≠ 0
n : ℕ
ih :
  HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i =
    (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * x⌋₊ : ℝ)
⊢ HMul.hMul (α := ℝ) (↑b : ℝ) (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * x⌋₊ : ℝ) +
      (↑(↑(Fin.ofNat b ⌊(↑b : ℝ) * (HPow.hPow (α := ℝ) (↑b : ℝ) n * x)⌋₊) : ℕ) : ℝ) =
    (↑⌊(↑b : ℝ) * (HPow.hPow (α := ℝ) (↑b : ℝ) n * x)⌋₊ : ℝ)
have succ : let y := HPow.hPow (α := ℝ) (↑b : ℝ) n * x;
∀ (ih : HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = (↑⌊y⌋₊ : ℝ)),
  HMul.hMul (α := ℝ) (↑b : ℝ) (↑⌊y⌋₊ : ℝ) + (↑(↑(Fin.ofNat b ⌊(↑b : ℝ) * y⌋₊) : ℕ) : ℝ) = (↑⌊(↑b : ℝ) * y⌋₊ : ℝ)
Tactic: set y := (b : ℝ) ^ n * x
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
this : b ≠ 0
n : ℕ
y : ℝ := HPow.hPow (α := ℝ) (↑b : ℝ) n * x
ih : HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = (↑⌊y⌋₊ : ℝ)
⊢ HMul.hMul (α := ℝ) (↑b : ℝ) (↑⌊y⌋₊ : ℝ) + (↑(↑(Fin.ofNat b ⌊(↑b : ℝ) * y⌋₊) : ℕ) : ℝ) = (↑⌊(↑b : ℝ) * y⌋₊ : ℝ)
have succ : b * ⌊y⌋₊ + (↑(Fin.ofNat b ⌊(↑b : ℝ) * y⌋₊) : ℕ) = ⌊(↑b : ℝ) * y⌋₊
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
this : b ≠ 0
n : ℕ
y : ℝ := HPow.hPow (α := ℝ) (↑b : ℝ) n * x
ih : HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = (↑⌊y⌋₊ : ℝ)
⊢ b * ⌊y⌋₊ + (↑(Fin.ofNat b ⌊(↑b : ℝ) * y⌋₊) : ℕ) = ⌊(↑b : ℝ) * y⌋₊
have succ : b * (⌊(↑b : ℝ) * y⌋₊ / b) + (↑(Fin.ofNat b ⌊(↑b : ℝ) * y⌋₊) : ℕ) = ⌊(↑b : ℝ) * y⌋₊
Tactic: rw [← Nat.cast_mul_floor_div_cancel (a := y) (show b ≠ 0 by lia),
      Fin.val_ofNat, Nat.div_add_mod]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
this : b ≠ 0
n : ℕ
y : ℝ := HPow.hPow (α := ℝ) (↑b : ℝ) n * x
ih : HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = (↑⌊y⌋₊ : ℝ)
succ : b * (⌊(↑b : ℝ) * y⌋₊ / b) + (↑(Fin.ofNat b ⌊(↑b : ℝ) * y⌋₊) : ℕ) = ⌊(↑b : ℝ) * y⌋₊
⊢ b * ⌊y⌋₊ + (↑(Fin.ofNat b ⌊(↑b : ℝ) * y⌋₊) : ℕ) = ⌊(↑b : ℝ) * y⌋₊
have succ₁ : b * (⌊(↑b : ℝ) * y⌋₊ / b) + ⌊(↑b : ℝ) * y⌋₊ % b = ⌊(↑b : ℝ) * y⌋₊
Tactic: rw [← Nat.cast_mul_floor_div_cancel (a := y) (show b ≠ 0 by lia),
      Fin.val_ofNat, Nat.div_add_mod]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
this : b ≠ 0
n : ℕ
y : ℝ := HPow.hPow (α := ℝ) (↑b : ℝ) n * x
ih : HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = (↑⌊y⌋₊ : ℝ)
succ : b * (⌊(↑b : ℝ) * y⌋₊ / b) + (↑(Fin.ofNat b ⌊(↑b : ℝ) * y⌋₊) : ℕ) = ⌊(↑b : ℝ) * y⌋₊
succ₁ : b * (⌊(↑b : ℝ) * y⌋₊ / b) + ⌊(↑b : ℝ) * y⌋₊ % b = ⌊(↑b : ℝ) * y⌋₊
⊢ b * ⌊y⌋₊ + (↑(Fin.ofNat b ⌊(↑b : ℝ) * y⌋₊) : ℕ) = ⌊(↑b : ℝ) * y⌋₊
have succ₂ : ⌊(↑b : ℝ) * y⌋₊ = ⌊(↑b : ℝ) * y⌋₊
Tactic: rw [← Nat.cast_mul_floor_div_cancel (a := y) (show b ≠ 0 by lia),
      Fin.val_ofNat, Nat.div_add_mod]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
n : ℕ
this : b ≠ 0
⊢ HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i =
    (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * x⌋₊ : ℝ)
have zero : HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 0 * ∑ i ∈ Finset.range 0, ofDigitsTerm (x.digits b) i =
  (↑⌊HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 0 * x⌋₊ : ℝ)
Tactic: induction n with
  | zero => simp [Nat.floor_eq_zero.mpr hx.right]
  | succ n ih =>
    rw [Finset.sum_range_succ, mul_add, pow_succ', mul_assoc, ih, ofDigitsTerm, digits, ← pow_succ',
      mul_left_comm, mul_inv_cancel₀ (by positivity), mul_one, mul_comm x, pow_succ', mul_assoc]
    set y := (b : ℝ) ^ n * x
    norm_cast
    rw [← Nat.cast_mul_floor_div_cancel (a := y) (show b ≠ 0 by lia),
      Fin.val_ofNat, Nat.div_add_mod]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
n : ℕ
this : b ≠ 0
zero :
  HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 0 * ∑ i ∈ Finset.range 0, ofDigitsTerm (x.digits b) i =
    (↑⌊HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 0 * x⌋₊ : ℝ)
⊢ HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i =
    (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * x⌋₊ : ℝ)
have succ : ∀ (n : ℕ)
  (ih :
    HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i =
      (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * x⌋₊ : ℝ)),
  HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1) * ∑ i ∈ Finset.range (n + 1), ofDigitsTerm (x.digits b) i =
    (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1) * x⌋₊ : ℝ)
Tactic: induction n with
  | zero => simp [Nat.floor_eq_zero.mpr hx.right]
  | succ n ih =>
    rw [Finset.sum_range_succ, mul_add, pow_succ', mul_assoc, ih, ofDigitsTerm, digits, ← pow_succ',
      mul_left_comm, mul_inv_cancel₀ (by positivity), mul_one, mul_comm x, pow_succ', mul_assoc]
    set y := (b : ℝ) ^ n * x
    norm_cast
    rw [← Nat.cast_mul_floor_div_cancel (a := y) (show b ≠ 0 by lia),
      Fin.val_ofNat, Nat.div_add_mod]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (hypothesis)
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
n : ℕ
⊢ x - HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ n ≤ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i
have this : 0 < b
Tactic: have := NeZero.pos b
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (hypothesis)
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
n : ℕ
this : 0 < b
⊢ x - HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ n ≤ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i
have this₁ : HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i =
  (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * x⌋₊ : ℝ)
Tactic: have := ofDigits_digits_sum_eq (b := b) hx n
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (hypothesis)
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
n : ℕ
this_1 : 0 < b
this :
  HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i =
    (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * x⌋₊ : ℝ)
⊢ x - HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ n ≤ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i
have h_le : HPow.hPow (α := ℝ) (↑b : ℝ) n * x < HAdd.hAdd (α := ℝ) (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * x⌋₊ : ℝ) 1
Tactic: have h_le := Nat.lt_floor_add_one (b ^ n * x)
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (hypothesis)
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
n : ℕ
this_1 : 0 < b
this :
  HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i =
    (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * x⌋₊ : ℝ)
h_le : HPow.hPow (α := ℝ) (↑b : ℝ) n * x < HAdd.hAdd (α := ℝ) (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * x⌋₊ : ℝ) 1
⊢ x - HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ n ≤ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i
have h_le₁ : HPow.hPow (α := ℝ) (↑b : ℝ) n * x <
  HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i + 1
Tactic: rw [← this] at h_le
Cleared hypotheses: h_le
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
n : ℕ
this_1 : 0 < b
this :
  HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i =
    (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * x⌋₊ : ℝ)
h_le :
  HPow.hPow (α := ℝ) (↑b : ℝ) n * x <
    HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i + 1
⊢ x - HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ n ≤ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i
have rw : HPow.hPow (α := ℝ) (↑b : ℝ) n * x - 1 ≤
  HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i
Tactic: rw [← mul_le_mul_iff_right₀ (show 0 < (b : ℝ) ^ n by positivity),
    mul_sub, inv_pow, mul_inv_cancel₀ (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
n : ℕ
this_1 : 0 < b
this :
  HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i =
    (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * x⌋₊ : ℝ)
h_le :
  HPow.hPow (α := ℝ) (↑b : ℝ) n * x <
    HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i + 1
⊢ HPow.hPow (α := ℝ) (↑b : ℝ) n * x - 1 ≤
    HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i
have linarith : HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i <
    HPow.hPow (α := ℝ) (↑b : ℝ) n * x - 1 →
  HPow.hPow (α := ℝ) (↑b : ℝ) n * x -
        (HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i + 1) +
      (HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i -
        (HPow.hPow (α := ℝ) (↑b : ℝ) n * x - 1)) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (hypothesis)
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
n : ℕ
⊢ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i ≤ x
have this : HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i =
  (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * x⌋₊ : ℝ)
Tactic: have := ofDigits_digits_sum_eq (b := b) hx n
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (hypothesis)
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
n : ℕ
this :
  HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i =
    (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * x⌋₊ : ℝ)
⊢ 0 ≤ HPow.hPow (α := ℝ) (↑b : ℝ) n * x
have this₁ : 0 ≤ x
Tactic: have := hx.left
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (hypothesis)
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
n : ℕ
this :
  HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i =
    (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * x⌋₊ : ℝ)
⊢ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i ≤ x
have h_le : (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * x⌋₊ : ℝ) ≤ HPow.hPow (α := ℝ) (↑b : ℝ) n * x
Tactic: have h_le := Nat.floor_le (a := b ^ n * x) (by have := hx.left; positivity)
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (hypothesis)
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
n : ℕ
this :
  HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i =
    (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * x⌋₊ : ℝ)
h_le : (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * x⌋₊ : ℝ) ≤ HPow.hPow (α := ℝ) (↑b : ℝ) n * x
⊢ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i ≤ x
have hb : b ≠ 0
Tactic: have hb := NeZero.ne b
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hb : 1 < b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
⊢ HasSum (ofDigitsTerm (x.digits b)) x
have rw : Filter.Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i) Filter.atTop (nhds x)
Tactic: rw [hasSum_iff_tendsto_nat_of_summable_norm (by exact summable_ofDigitsTerm.abs)]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hb : 1 < b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
⊢ Filter.Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i) Filter.atTop (nhds x)
have refine : Filter.Tendsto (fun (i : ℕ) ↦ x - HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ i) Filter.atTop (nhds x)
Tactic: refine tendsto_of_tendsto_of_tendsto_of_le_of_le ?_ tendsto_const_nhds
    (le_sum_ofDigitsTerm_digits hx) (sum_ofDigitsTerm_digits_le hx)
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hb : 1 < b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
⊢ Filter.Tendsto (fun (i : ℕ) ↦ x - HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ i) Filter.atTop (nhds x)
have h : x = x - 0
Tactic: convert! tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_zero_of_abs_lt_one _)
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hb : 1 < b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
h : x = x - 0
⊢ Filter.Tendsto (fun (i : ℕ) ↦ x - HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ i) Filter.atTop (nhds x)
have convert_3 : LT.lt (α := ℝ) |(↑b : ℝ)⁻¹| 1
Tactic: convert! tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_zero_of_abs_lt_one _)
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
inst : NeZero b
x : ℝ
hb : 1 < b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
⊢ ∑' (n : ℕ), ofDigitsTerm (x.digits b) n = x
have rw : HasSum (ofDigitsTerm (x.digits b)) x
Tactic: rw [← Summable.hasSum_iff]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
inst : NeZero b
x : ℝ
hb : 1 < b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
rw : HasSum (ofDigitsTerm (x.digits b)) x
⊢ ∑' (n : ℕ), ofDigitsTerm (x.digits b) n = x
have rw₁ : Summable (ofDigitsTerm (x.digits b))
Tactic: rw [← Summable.hasSum_iff]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
inst : NeZero b
⊢ 1 < |HAdd.hAdd (α := ℝ) (↑b : ℝ) 1|
have rw : LT.lt (α := ℝ) 1 (↑(b + 1) : ℝ)
Tactic: rw [← Nat.cast_add_one, abs_of_nonneg (Nat.cast_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (hypothesis)
Goal:
b : ℕ
inst : NeZero b
⊢ (ofDigits (b := b + 1) fun (x : ℕ) ↦ Fin.last b) = 1
have this : 1 < |HAdd.hAdd (α := ℝ) (↑b : ℝ) 1|
Tactic: have : 1 < |(b + 1 : ℝ)| := by
    rw [← Nat.cast_add_one, abs_of_nonneg (Nat.cast_nonneg _)]
    simp [NeZero.pos b]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
inst : NeZero b
this : 1 < |HAdd.hAdd (α := ℝ) (↑b : ℝ) 1|
⊢ (ofDigits (b := b + 1) fun (x : ℕ) ↦ Fin.last b) = 1
have simp : Eq (α := ℝ) (∑' (n : ℕ), (↑(↑(Fin.last b) : ℕ) : ℝ) * HPow.hPow (α := ℝ) (↑(b + 1) : ℝ)⁻¹ (n + 1)) 1
Tactic: simp only [ofDigits, ofDigitsTerm, ← inv_pow]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
inst : NeZero b
this : 1 < |HAdd.hAdd (α := ℝ) (↑b : ℝ) 1|
⊢ Eq (α := ℝ) (∑' (n : ℕ), (↑(↑(Fin.last b) : ℕ) : ℝ) * HPow.hPow (α := ℝ) (↑(b + 1) : ℝ)⁻¹ (n + 1)) 1
have rw : HMul.hMul (α := ℝ) (↑(↑(Fin.last b) : ℕ) : ℝ) (∑' (i : ℕ), HPow.hPow (α := ℝ) (↑(b + 1) : ℝ)⁻¹ (i + 1)) = 1
Tactic: rw [Summable.tsum_mul_left]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
inst : NeZero b
this : 1 < |HAdd.hAdd (α := ℝ) (↑b : ℝ) 1|
rw : HMul.hMul (α := ℝ) (↑(↑(Fin.last b) : ℕ) : ℝ) (∑' (i : ℕ), HPow.hPow (α := ℝ) (↑(b + 1) : ℝ)⁻¹ (i + 1)) = 1
⊢ Eq (α := ℝ) (∑' (n : ℕ), (↑(↑(Fin.last b) : ℕ) : ℝ) * HPow.hPow (α := ℝ) (↑(b + 1) : ℝ)⁻¹ (n + 1)) 1
have hf : Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑(b + 1) : ℝ)⁻¹ (n + 1)
Tactic: rw [Summable.tsum_mul_left]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
inst : NeZero b
this : 1 < |HAdd.hAdd (α := ℝ) (↑b : ℝ) 1|
⊢ HMul.hMul (α := ℝ) (↑(↑(Fin.last b) : ℕ) : ℝ) (∑' (i : ℕ), HPow.hPow (α := ℝ) (↑(b + 1) : ℝ)⁻¹ (i + 1)) = 1
have rw : (↑(↑(Fin.last b) : ℕ) : ℝ) * ((HSub.hSub (α := ℝ) 1 (↑(b + 1) : ℝ)⁻¹)⁻¹ - 1) = 1
Tactic: rw [geom_series_succ _ (by simp [inv_lt_one_iff₀, this]),
      tsum_geometric_of_lt_one (by positivity) (by simp [inv_lt_one_iff₀, NeZero.pos b])]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
inst : NeZero b
this : 1 < |HAdd.hAdd (α := ℝ) (↑b : ℝ) 1|
⊢ (↑(↑(Fin.last b) : ℕ) : ℝ) * ((HSub.hSub (α := ℝ) 1 (↑(b + 1) : ℝ)⁻¹)⁻¹ - 1) = 1
have push_cast : (↑b : ℝ) * ((1 - (HAdd.hAdd (α := ℝ) (↑b : ℝ) 1)⁻¹)⁻¹ - 1) = 1
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (hypothesis)
Goal:
b : ℕ
inst : NeZero b
this : 1 < |HAdd.hAdd (α := ℝ) (↑b : ℝ) 1|
⊢ (↑b : ℝ) * ((1 - (HAdd.hAdd (α := ℝ) (↑b : ℝ) 1)⁻¹)⁻¹ - 1) = 1
have this₁ : Ne (α := ℝ) (↑b : ℝ) 0
Tactic: have : (b : ℝ) ≠ 0 := mod_cast NeZero.ne b
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
inst : NeZero b
this : 1 < |HAdd.hAdd (α := ℝ) (↑b : ℝ) 1|
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑(b + 1) : ℝ)⁻¹ (n + 1)
have hf : Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑(b + 1) : ℝ)⁻¹ n
Tactic: rw [summable_nat_add_iff (f := fun n ↦ ((b + 1 : ℕ) : ℝ)⁻¹ ^ n) 1]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
hb : 1 < b
⊢ (ofDigits (b := b) fun (x : ℕ) ↦ (⟨b - 1, ⋯⟩ : Fin b)) = 1
have h : b = b - 1 + 1
Tactic: convert! ofDigits_const_last_eq_one (b - 1)
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
hb : 1 < b
h : b = b - 1 + 1
⊢ (ofDigits (b := b) fun (x : ℕ) ↦ (⟨b - 1, ⋯⟩ : Fin b)) = 1
have convert! : NeZero (b - 1)
Tactic: convert! ofDigits_const_last_eq_one (b - 1)
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
hb : 1 < b
⊢ NeZero (b - 1)
have out : b - 1 ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (hypothesis)
Goal:
b : ℕ
hb : 1 < b
⊢ Set.SurjOn (α := ℕ → Fin b) ofDigits Set.univ (Set.Icc 0 1)
have this : NeZero b
Tactic: have : NeZero b := ⟨by grind⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
hb : 1 < b
this : NeZero b
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) y
⊢ y ∈ Set.image (α := ℕ → Fin b) ofDigits Set.univ
have pos : ∀ (hy' : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) y), y ∈ Set.image (α := ℕ → Fin b) ofDigits Set.univ
Tactic: by_cases hy' : y ∈ Set.Ico 0 1
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
hb : 1 < b
this : NeZero b
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) y
pos : ∀ (hy' : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) y), y ∈ Set.image (α := ℕ → Fin b) ofDigits Set.univ
⊢ y ∈ Set.image (α := ℕ → Fin b) ofDigits Set.univ
have neg : ∀ (hy' : y ∉ Set.Ico 0 1), y ∈ Set.image (α := ℕ → Fin b) ofDigits Set.univ
Tactic: by_cases hy' : y ∈ Set.Ico 0 1
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
hb : 1 < b
this : NeZero b
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) y
hy' : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) y
⊢ y ∈ Set.image (α := ℕ → Fin b) ofDigits Set.univ
have h : Membership.mem (γ := Set (ℕ → Fin b)) Set.univ (y.digits b) ∧ ofDigits (y.digits b) = y
Tactic: use digits y b
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b : ℕ
hb : 1 < b
this : NeZero b
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) y
hy' : y ∉ Set.Ico 0 1
⊢ y ∈ Set.image (α := ℕ → Fin b) ofDigits Set.univ
have neg : ∃ (y : ℕ → Fin b), ofDigits y = 1
Tactic: simp only [Set.image_univ, show y = 1 by grind, Set.mem_range]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (hypothesis)
Goal:
b n : ℕ
⊢ Continuous (X := ℕ → Fin (n + 2)) ofDigits
have hb0 : 0 < n + 2
Tactic: obtain ⟨hb0, hb⟩ : 0 < n + 2 ∧ 1 < n + 2 := by grind
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (hypothesis)
Goal:
b n : ℕ
hb0 : 0 < n + 2
⊢ Continuous (X := ℕ → Fin (n + 2)) ofDigits
have hb : 1 < n + 2
Tactic: obtain ⟨hb0, hb⟩ : 0 < n + 2 ∧ 1 < n + 2 := by grind
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b n : ℕ
hb0 : 0 < n + 2
hb : 1 < n + 2
⊢ Continuous (X := ℕ → Fin (n + 2)) ofDigits
have generalize : ∀ (b : ℕ) (hb : 1 < b), Continuous (X := ℕ → Fin b) ofDigits
Tactic: generalize n + 2 = b at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (hypothesis)
Goal:
b_1 n : ℕ
hb0 : 0 < n + 2
b : ℕ
hb : 1 < b
⊢ Continuous (X := ℕ → Fin b) ofDigits
have hb0₁ : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
Tactic: rify at hb0 hb
Cleared hypotheses: hb0, hb
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (hypothesis)
Goal:
b_1 n : ℕ
hb0 : 0 < n + 2
b : ℕ
hb : 1 < b
hb0₁ : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
⊢ Continuous (X := ℕ → Fin b) ofDigits
have hb₁ : LT.lt (α := ℝ) 1 (↑b : ℝ)
Tactic: rify at hb0 hb
Cleared hypotheses: hb0, hb
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b_1 n b : ℕ
hb0 : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ Continuous (X := ℕ → Fin b) ofDigits
have refine_1 : ∀ (i : ℕ), Continuous (Y := ℝ) fun (x : ℕ → Fin b) ↦ ofDigitsTerm x i
Tactic: refine continuous_tsum (u := fun i ↦ (b : ℝ)⁻¹ ^ i) ?_ ?_ fun n x ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b_1 n b : ℕ
hb0 : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
refine_1 : ∀ (i : ℕ), Continuous (Y := ℝ) fun (x : ℕ → Fin b) ↦ ofDigitsTerm x i
⊢ Continuous (X := ℕ → Fin b) ofDigits
have refine_2 : Summable (α := ℝ) fun (i : ℕ) ↦ HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ i
Tactic: refine continuous_tsum (u := fun i ↦ (b : ℝ)⁻¹ ^ i) ?_ ?_ fun n x ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b_1 n b : ℕ
hb0 : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
refine_1 : ∀ (i : ℕ), Continuous (Y := ℝ) fun (x : ℕ → Fin b) ↦ ofDigitsTerm x i
refine_2 : Summable (α := ℝ) fun (i : ℕ) ↦ HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ i
⊢ Continuous (X := ℕ → Fin b) ofDigits
have refine_3 : ∀ (n : ℕ) (x : ℕ → Fin b), ‖ofDigitsTerm x n‖ ≤ (fun (i : ℕ) ↦ HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ i) n
Tactic: refine continuous_tsum (u := fun i ↦ (b : ℝ)⁻¹ ^ i) ?_ ?_ fun n x ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b_1 n_1 b : ℕ
hb0 : 0 < HAdd.hAdd (α := ℝ) (↑n_1 : ℝ) 2
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
n : ℕ
x : ℕ → Fin b
⊢ ‖ofDigitsTerm x n‖ ≤ (fun (i : ℕ) ↦ HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ i) n
have refine_3 : ofDigitsTerm x n ≤ (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹
Tactic: simp only [norm_eq_abs, abs_of_nonneg ofDigitsTerm_nonneg, inv_pow]
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b_1 n_1 b : ℕ
hb0 : 0 < HAdd.hAdd (α := ℝ) (↑n_1 : ℝ) 2
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
n : ℕ
x : ℕ → Fin b
⊢ ofDigitsTerm x n ≤ (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹
have refine_3 : HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹ ≤ (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹
Tactic: apply ofDigitsTerm_le.trans
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b_1 n_1 b : ℕ
hb0 : 0 < HAdd.hAdd (α := ℝ) (↑n_1 : ℝ) 2
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
n : ℕ
x : ℕ → Fin b
⊢ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹ ≤
    (↑b : ℝ) * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹
have hbc : HSub.hSub (α := ℝ) (↑b : ℝ) 1 ≤ (↑b : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b_1 n_1 b : ℕ
hb0 : 0 < HAdd.hAdd (α := ℝ) (↑n_1 : ℝ) 2
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
n : ℕ
x : ℕ → Fin b
⊢ HSub.hSub (α := ℝ) (↑b : ℝ) 1 ≤ (↑b : ℝ)
have linarith : (↑b : ℝ) < HSub.hSub (α := ℝ) (↑b : ℝ) 1 → -1 + ((↑b : ℝ) - HSub.hSub (α := ℝ) (↑b : ℝ) 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b_1 n_1 b : ℕ
hb0 : 0 < HAdd.hAdd (α := ℝ) (↑n_1 : ℝ) 2
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
n : ℕ
x : ℕ → Fin b
⊢ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹ ≤ (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹
have _ : HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹ ≤
  (↑b : ℝ) * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹
Tactic: calc
        _ ≤ b * ((b : ℝ) ^ (n + 1))⁻¹ := by
          gcongr
          linarith
        _ = _ := by
          grind
-- Lean 4 proof step from Mathlib.Analysis.Real.OfDigits (goal)
Goal:
b_1 n_1 b : ℕ
hb0 : 0 < HAdd.hAdd (α := ℝ) (↑n_1 : ℝ) 2
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
n : ℕ
x : ℕ → Fin b
_ :
  HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹ ≤
    (↑b : ℝ) * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹
⊢ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹ ≤ (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹
have _₁ : (↑b : ℝ) * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹ = (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹
Tactic: calc
        _ ≤ b * ((b : ℝ) ^ (n + 1))⁻¹ := by
          gcongr
          linarith
        _ = _ := by
          grind