awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
this : Eq (α := ℝ) (∑ i ∈ Finset.range n, ofDigitsTerm x i) (∑ i ∈ Finset.range n, ofDigitsTerm y i)
rw :
  (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ *
      |(ofDigits (b := b) fun (i : ℕ) ↦ x (i + n)) - ofDigits (b := b) fun (i : ℕ) ↦ y (i + n)| ≤
    (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹
⊢ |(∑ i ∈ Finset.range n, ofDigitsTerm x i +
          (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ * ofDigits (b := b) fun (i : ℕ) ↦ x (i + n)) -
        (∑ i ∈ Finset.range n, ofDigitsTerm y i +
          (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ * ofDigits (b := b) fun (i : ℕ) ↦ y (i + n))| ≤
    (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹

Tactic:
rw [this, add_sub_add_left_eq_sub, ← mul_sub, abs_mul, abs_of_nonneg (by positivity)]

Premises used: mul_sub, add_sub_add_left_eq_sub, abs_mul, abs_of_nonneg
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
this : Eq (α := ℝ) (∑ i ∈ Finset.range n, ofDigitsTerm x i) (∑ i ∈ Finset.range n, ofDigitsTerm y i)
apply : |(ofDigits (b := b) fun (i : ℕ) ↦ x (i + n)) - ofDigits (b := b) fun (i : ℕ) ↦ y (i + n)| ≤ 1
⊢ (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹ *
      |(ofDigits (b := b) fun (i : ℕ) ↦ x (i + n)) - ofDigits (b := b) fun (i : ℕ) ↦ y (i + n)| ≤
    (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹

Tactic:
apply mul_le_of_le_one_right (by positivity)

Premises used: mul_le_of_le_one_right
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
this : Eq (α := ℝ) (∑ i ∈ Finset.range n, ofDigitsTerm x i) (∑ i ∈ Finset.range n, ofDigitsTerm y i)
⊢ |(ofDigits (b := b) fun (i : ℕ) ↦ x (i + n)) - ofDigits (b := b) fun (i : ℕ) ↦ y (i + n)| ≤ HSub.hSub (α := ℝ) 1 0

Tactic:
abs_sub_le_of_le_of_le (ofDigits_nonneg _) (ofDigits_le_one _) (ofDigits_nonneg _)
      (ofDigits_le_one _)

Premises used: Real.ofDigits_nonneg, abs_sub_le_of_le_of_le, Real.ofDigits_le_one
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
this : Eq (α := ℝ) (∑ i ∈ Finset.range n, ofDigitsTerm x i) (∑ i ∈ Finset.range n, ofDigitsTerm y i)
h : 1 = HSub.hSub (α := ℝ) 1 0
⊢ |(ofDigits (b := b) fun (i : ℕ) ↦ x (i + n)) - ofDigits (b := b) fun (i : ℕ) ↦ y (i + n)| ≤ 1

Tactic:
convert!
    abs_sub_le_of_le_of_le (ofDigits_nonneg _) (ofDigits_le_one _) (ofDigits_nonneg _)
      (ofDigits_le_one _)

Premises used: Real.ofDigits_nonneg, abs_sub_le_of_le_of_le, Real.ofDigits_le_one
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
x y : ℕ → Fin b
n : ℕ
hxy : ∀ i < n, x i = y i
this : Eq (α := ℝ) (∑ i ∈ Finset.range n, ofDigitsTerm x i) (∑ i ∈ Finset.range n, ofDigitsTerm y i)
⊢ 1 = HSub.hSub (α := ℝ) 1 0

Tactic:
simp
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
n : ℕ
⊢ b ≠ 0

Tactic:
have := NeZero.ne b
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
this : b ≠ 0
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 0 * ∑ i ∈ Finset.range 0, ofDigitsTerm (x.digits b) i =
    (↑⌊HPow.hPow (α := ℝ) (β := ℕ) (↑b : ℝ) 0 * x⌋₊ : ℝ)

Tactic:
simp [Nat.floor_eq_zero.mpr hx.right]

Premises used: Iff.mpr, And.right, Nat.floor_eq_zero
-- Module: Mathlib.Analysis.Real.OfDigits
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⌋₊ : ℝ)
⊢ HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1) ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Real.OfDigits
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⌋₊ : ℝ)
succ :
  HMul.hMul (α := ℝ) (↑b : ℝ) (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * x⌋₊ : ℝ) +
      (↑(↑(Fin.ofNat b ⌊(↑b : ℝ) * (HPow.hPow (α := ℝ) (↑b : ℝ) n * x)⌋₊) : ℕ) : ℝ) =
    (↑⌊(↑b : ℝ) * (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:
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]

Premises used: mul_inv_cancel₀, mul_assoc, mul_left_comm, Real.digits, Real.ofDigitsTerm, mul_comm, mul_add, mul_one, Finset.sum_range_succ, pow_succ'
-- Module: Mathlib.Analysis.Real.OfDigits
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⌋₊ : ℝ)
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⌋₊ : ℝ)
⊢ HMul.hMul (α := ℝ) (↑b : ℝ) (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * x⌋₊ : ℝ) +
      (↑(↑(Fin.ofNat b ⌊(↑b : ℝ) * (HPow.hPow (α := ℝ) (↑b : ℝ) n * x)⌋₊) : ℕ) : ℝ) =
    (↑⌊(↑b : ℝ) * (HPow.hPow (α := ℝ) (↑b : ℝ) n * x)⌋₊ : ℝ)

Tactic:
set y := (b : ℝ) ^ n * x

Premises used: Nat.cast
-- Module: Mathlib.Analysis.Real.OfDigits
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 * ⌊y⌋₊ + (↑(Fin.ofNat b ⌊(↑b : ℝ) * y⌋₊) : ℕ) = ⌊(↑b : ℝ) * y⌋₊
⊢ HMul.hMul (α := ℝ) (↑b : ℝ) (↑⌊y⌋₊ : ℝ) + (↑(↑(Fin.ofNat b ⌊(↑b : ℝ) * y⌋₊) : ℕ) : ℝ) = (↑⌊(↑b : ℝ) * y⌋₊ : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Real.OfDigits
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 ≠ 0

Tactic:
lia
-- Module: Mathlib.Analysis.Real.OfDigits
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⌋₊
succ₂ succ₃ : ⌊(↑b : ℝ) * y⌋₊ = ⌊(↑b : ℝ) * y⌋₊
⊢ b * ⌊y⌋₊ + (↑(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]

Premises used: Nat.div_add_mod, Nat.cast_mul_floor_div_cancel, Fin.val_ofNat
-- Module: Mathlib.Analysis.Real.OfDigits
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⌋₊ : ℝ)
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⌋₊ : ℝ)
⊢ HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i =
    (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * 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]

Premises used: Iff.mpr, mul_inv_cancel₀, Nat.div_add_mod, mul_assoc, mul_left_comm, Nat.cast, And.right, Real.digits, Real.ofDigitsTerm, mul_comm, Nat.floor_eq_zero, mul_add, mul_one, Finset.sum_range_succ, pow_succ', Fin.val_ofNat
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
n : ℕ
⊢ 0 < b

Tactic:
have := NeZero.pos b
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
n : ℕ
this : 0 < b
⊢ 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
-- Module: Mathlib.Analysis.Real.OfDigits
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⌋₊ : ℝ)
⊢ 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)
-- Module: Mathlib.Analysis.Real.OfDigits
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
⊢ 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
-- Module: Mathlib.Analysis.Real.OfDigits
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
⊢ 0 < HPow.hPow (α := ℝ) (↑b : ℝ) n

Tactic:
positivity
-- Module: Mathlib.Analysis.Real.OfDigits
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 ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Real.OfDigits
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
rw :
  HPow.hPow (α := ℝ) (↑b : ℝ) n * x - 1 ≤
    HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i
⊢ x - 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)]

Premises used: mul_inv_cancel₀, mul_sub, inv_pow, mul_le_mul_iff_right₀
-- Module: Mathlib.Analysis.Real.OfDigits
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
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
⊢ HPow.hPow (α := ℝ) (↑b : ℝ) n * x - 1 ≤
    HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i

Tactic:
linarith
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
n : ℕ
⊢ 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
-- Module: Mathlib.Analysis.Real.OfDigits
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 ≤ x

Tactic:
have := hx.left
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
n : ℕ
this_1 :
  HPow.hPow (α := ℝ) (↑b : ℝ) n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i =
    (↑⌊HPow.hPow (α := ℝ) (↑b : ℝ) n * x⌋₊ : ℝ)
this : 0 ≤ x
⊢ 0 ≤ HPow.hPow (α := ℝ) (↑b : ℝ) n * x

Tactic:
positivity
-- Module: Mathlib.Analysis.Real.OfDigits
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⌋₊ : ℝ)
⊢ (↑⌊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)
-- Module: Mathlib.Analysis.Real.OfDigits
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
⊢ b ≠ 0

Tactic:
have hb := NeZero.ne b
-- Module: Mathlib.Analysis.Real.OfDigits
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 * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i ≤ HPow.hPow (α := ℝ) (↑b : ℝ) n * x
hb : b ≠ 0
⊢ 0 < HPow.hPow (α := ℝ) (↑b : ℝ) n

Tactic:
positivity
-- Module: Mathlib.Analysis.Real.OfDigits
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
hb : b ≠ 0
⊢ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i ≤ x

Tactic:
rw [← this, mul_le_mul_iff_of_pos_left (by positivity)] at h_le

Premises used: mul_le_mul_iff_of_pos_left
-- Module: Mathlib.Analysis.Real.OfDigits
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
hb : b ≠ 0
h_le₁ : ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i ≤ x
⊢ b ≠ 0

Tactic:
rw [← this, mul_le_mul_iff_of_pos_left (by positivity)] at h_le

Premises used: mul_le_mul_iff_of_pos_left
-- Module: Mathlib.Analysis.Real.OfDigits
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 : ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i ≤ x
hb : b ≠ 0
⊢ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i ≤ x

Tactic:
h_le
-- Module: Mathlib.Analysis.Real.OfDigits
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 : ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i ≤ x
hb : b ≠ 0
⊢ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i ≤ x

Tactic:
exact h_le
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hb : 1 < b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ ‖ofDigitsTerm (x.digits b) i‖

Tactic:
summable_ofDigitsTerm.abs

Premises used: Summable.abs, Real.summable_ofDigitsTerm
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hb : 1 < b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ ‖ofDigitsTerm (x.digits b) i‖

Tactic:
exact summable_ofDigitsTerm.abs

Premises used: Summable.abs, Real.summable_ofDigitsTerm
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hb : 1 < b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
rw : Filter.Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i) Filter.atTop (nhds x)
⊢ HasSum (ofDigitsTerm (x.digits b)) x

Tactic:
rw [hasSum_iff_tendsto_nat_of_summable_norm (by exact summable_ofDigitsTerm.abs)]

Premises used: hasSum_iff_tendsto_nat_of_summable_norm
-- Module: Mathlib.Analysis.Real.OfDigits
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)

Tactic:
tendsto_of_tendsto_of_tendsto_of_le_of_le ?_ tendsto_const_nhds
    (le_sum_ofDigitsTerm_digits hx) (sum_ofDigitsTerm_digits_le hx)

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le, Real.sum_ofDigitsTerm_digits_le, tendsto_const_nhds, Real.le_sum_ofDigitsTerm_digits
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hb : 1 < b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
refine : Filter.Tendsto (fun (i : ℕ) ↦ x - HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ i) Filter.atTop (nhds x)
⊢ Filter.Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits 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)

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le, Real.sum_ofDigitsTerm_digits_le, tendsto_const_nhds, Real.le_sum_ofDigitsTerm_digits
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hb : 1 < b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
⊢ Filter.Tendsto (fun (x_1 : ℕ) ↦ x - HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ x_1) Filter.atTop (nhds (x - 0))

Tactic:
tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_zero_of_abs_lt_one _)

Premises used: tendsto_const_nhds, tendsto_pow_atTop_nhds_zero_of_abs_lt_one, Filter.Tendsto.sub
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hb : 1 < b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
h : x = x - 0
convert_3 : LT.lt (α := ℝ) |(↑b : ℝ)⁻¹| 1
⊢ Filter.Tendsto (fun (i : ℕ) ↦ x - HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ i) Filter.atTop (nhds x)

Tactic:
convert! tendsto_const_nhds.sub (tendsto_pow_atTop_nhds_zero_of_abs_lt_one _)

Premises used: tendsto_const_nhds, tendsto_pow_atTop_nhds_zero_of_abs_lt_one, Filter.Tendsto.sub
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hb : 1 < b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
⊢ x = x - 0

Tactic:
simp
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
x : ℝ
b : ℕ
inst : NeZero b
hb : 1 < b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
⊢ LT.lt (α := ℝ) |(↑b : ℝ)⁻¹| 1

Tactic:
simp [abs_of_nonneg, inv_lt_one_iff₀, hb]

Premises used: abs_of_nonneg, inv_lt_one_iff₀
-- Module: Mathlib.Analysis.Real.OfDigits
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
rw₁ : Summable (ofDigitsTerm (x.digits b))
⊢ ∑' (n : ℕ), ofDigitsTerm (x.digits b) n = x

Tactic:
rw [← Summable.hasSum_iff]

Premises used: Summable.hasSum_iff
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
inst : NeZero b
x : ℝ
hb : 1 < b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
⊢ HasSum (ofDigitsTerm (x.digits b)) x

Tactic:
hasSum_ofDigitsTerm_digits x hb hx

Premises used: Real.hasSum_ofDigitsTerm_digits
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
inst : NeZero b
x : ℝ
hb : 1 < b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
⊢ HasSum (ofDigitsTerm (x.digits b)) x

Tactic:
exact hasSum_ofDigitsTerm_digits x hb hx

Premises used: Real.hasSum_ofDigitsTerm_digits
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
inst : NeZero b
x : ℝ
hb : 1 < b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
⊢ Summable (ofDigitsTerm (x.digits b))

Tactic:
summable_ofDigitsTerm

Premises used: Real.summable_ofDigitsTerm
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
inst : NeZero b
x : ℝ
hb : 1 < b
hx : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) x
⊢ Summable (ofDigitsTerm (x.digits b))

Tactic:
exact summable_ofDigitsTerm

Premises used: Real.summable_ofDigitsTerm
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
inst : NeZero b
rw : LT.lt (α := ℝ) 1 (↑(b + 1) : ℝ)
⊢ 1 < |HAdd.hAdd (α := ℝ) (↑b : ℝ) 1|

Tactic:
rw [← Nat.cast_add_one, abs_of_nonneg (Nat.cast_nonneg _)]

Premises used: abs_of_nonneg, Nat.cast_add_one
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
inst : NeZero b
⊢ LT.lt (α := ℝ) 1 (↑(b + 1) : ℝ)

Tactic:
simp [NeZero.pos b]

Premises used: NeZero.pos
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
inst : NeZero b
⊢ 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]
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
inst : NeZero b
this : 1 < |HAdd.hAdd (α := ℝ) (↑b : ℝ) 1|
simp : Eq (α := ℝ) (∑' (n : ℕ), (↑(↑(Fin.last b) : ℕ) : ℝ) * HPow.hPow (α := ℝ) (↑(b + 1) : ℝ)⁻¹ (n + 1)) 1
⊢ (ofDigits (b := b + 1) fun (x : ℕ) ↦ Fin.last b) = 1

Tactic:
simp only [ofDigits, ofDigitsTerm, ← inv_pow]

Premises used: inv_pow, Real.ofDigitsTerm, Real.ofDigits
-- Module: Mathlib.Analysis.Real.OfDigits
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
hf : Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑(b + 1) : ℝ)⁻¹ (n + 1)
⊢ Eq (α := ℝ) (∑' (n : ℕ), (↑(↑(Fin.last b) : ℕ) : ℝ) * HPow.hPow (α := ℝ) (↑(b + 1) : ℝ)⁻¹ (n + 1)) 1

Tactic:
rw [Summable.tsum_mul_left]

Premises used: Summable.tsum_mul_left
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
inst : NeZero b
this : 1 < |HAdd.hAdd (α := ℝ) (↑b : ℝ) 1|
⊢ Norm.norm (E := ℝ) (↑(b + 1) : ℝ)⁻¹ < 1

Tactic:
simp [inv_lt_one_iff₀, this]

Premises used: inv_lt_one_iff₀
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
inst : NeZero b
this : 1 < |HAdd.hAdd (α := ℝ) (↑b : ℝ) 1|
⊢ LE.le (α := ℝ) 0 (↑(b + 1) : ℝ)⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
inst : NeZero b
this : 1 < |HAdd.hAdd (α := ℝ) (↑b : ℝ) 1|
⊢ LT.lt (α := ℝ) (↑(b + 1) : ℝ)⁻¹ 1

Tactic:
simp [inv_lt_one_iff₀, NeZero.pos b]

Premises used: NeZero.pos, inv_lt_one_iff₀