awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
L : List ℕ
nil :
  Eq (α := ℕ) (List.foldr (fun (x y : ℕ) ↦ (↑x : ℕ) + b * y) 0 [])
    (List.sum
      (List.zipWith (α := ℕ)
        (Function.curry fun (x : ℕ × ℕ) ↦
          match (motive := ℕ × ℕ → ℕ) x with
          | (a, i) => a * b ^ i)
        [] (List.range (List.length (α := ℕ) []))))
⊢ Eq (α := ℕ) (List.foldr (fun (x y : ℕ) ↦ (↑x : ℕ) + b * y) 0 L)
    (List.sum
      (List.zipWith
        (Function.curry fun (x : ℕ × ℕ) ↦
          match (motive := ℕ × ℕ → ℕ) x with
          | (a, i) => a * b ^ i)
        L (List.range L.length)))
have cons : ∀ (hd : ℕ) (tl : List ℕ)
  (hl :
    Eq (α := ℕ) (List.foldr (fun (x y : ℕ) ↦ (↑x : ℕ) + b * y) 0 tl)
      (List.sum
        (List.zipWith
          (Function.curry fun (x : ℕ × ℕ) ↦
            match (motive := ℕ × ℕ → ℕ) x with
            | (a, i) => a * b ^ i)
          tl (List.range tl.length)))),
  Eq (α := ℕ) (List.foldr (fun (x y : ℕ) ↦ (↑x : ℕ) + b * y) 0 (hd :: tl))
    (List.sum
      (List.zipWith
        (Function.curry fun (x : ℕ × ℕ) ↦
          match (motive := ℕ × ℕ → ℕ) x with
          | (a, i) => a * b ^ i)
        (hd :: tl) (List.range (hd :: tl).length)))
Tactic: induction L with
  | nil => simp
  | cons hd tl hl =>
    simpa [List.range_succ_eq_map, List.zipWith_map_right, ofDigits_eq_sum_mapIdx_aux] using
      Or.inl hl
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ (b.digits n).length = log b n + 1
have h : ∀ (n : ℕ) (IH : ∀ m < n, ∀ (hn : m ≠ 0), (b.digits m).length = log b m + 1) (hn : n ≠ 0),
  (b.digits n).length = log b n + 1
Tactic: induction n using Nat.strong_induction_on with | _ n IH
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, ∀ (hn : m ≠ 0), (b.digits m).length = log b m + 1
hn : n ≠ 0
⊢ (b.digits n).length = log b n + 1
have h : (b.digits (n / b)).length + 1 = log b n + 1
Tactic: rw [digits_eq_cons_digits_div hb hn, List.length]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, ∀ (hn : m ≠ 0), (b.digits m).length = log b m + 1
hn : n ≠ 0
⊢ (b.digits (n / b)).length + 1 = log b n + 1
have pos : ∀ (h : n / b = 0), (b.digits (n / b)).length + 1 = log b n + 1
Tactic: by_cases h : n / b = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, ∀ (hn : m ≠ 0), (b.digits m).length = log b m + 1
hn : n ≠ 0
pos : ∀ (h : n / b = 0), (b.digits (n / b)).length + 1 = log b n + 1
⊢ (b.digits (n / b)).length + 1 = log b n + 1
have neg : ∀ (h : ¬n / b = 0), (b.digits (n / b)).length + 1 = log b n + 1
Tactic: by_cases h : n / b = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, ∀ (hn : m ≠ 0), (b.digits m).length = log b m + 1
hn : n ≠ 0
h : n / b = 0
⊢ (b.digits (n / b)).length + 1 = log b n + 1
have pos : n < b ∨ b ≤ 1
Tactic: simp [h]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (hypothesis)
Goal:
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, ∀ (hn : m ≠ 0), (b.digits m).length = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
⊢ (b.digits (n / b)).length + 1 = log b n + 1
have this : n / b < n
Tactic: have : n / b < n := div_lt_self (Nat.pos_of_ne_zero hn) hb
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, ∀ (hn : m ≠ 0), (b.digits m).length = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
this : n / b < n
⊢ (b.digits (n / b)).length + 1 = log b n + 1
have neg : 1 ≤ log b n
Tactic: rw [IH _ this h, log_div_base, tsub_add_cancel_of_le]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, ∀ (hn : m ≠ 0), (b.digits m).length = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
this : n / b < n
⊢ 1 ≤ log b n
have neg : b ≤ n
Tactic: refine Nat.succ_le_of_lt (log_pos hb ?_)
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, ∀ (hn : m ≠ 0), (b.digits m).length = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
this : n / b < n
⊢ b ≤ n
have neg : ∀ (h : n < b), n / b = 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b k : ℕ
hb : 1 < b
n : ℕ
⊢ (b.digits n).length ≤ k ↔ n < b ^ k
have pos : ∀ (h : n = 0), (b.digits n).length ≤ k ↔ n < b ^ k
Tactic: by_cases h : n = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b k : ℕ
hb : 1 < b
n : ℕ
pos : ∀ (h : n = 0), (b.digits n).length ≤ k ↔ n < b ^ k
⊢ (b.digits n).length ≤ k ↔ n < b ^ k
have neg : ∀ (h : ¬n = 0), (b.digits n).length ≤ k ↔ n < b ^ k
Tactic: by_cases h : n = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (hypothesis)
Goal:
b k : ℕ
hb : 1 < b
n : ℕ
h : n = 0
⊢ (b.digits n).length ≤ k ↔ n < b ^ k
have this : 0 < b ^ k
Tactic: have : 0 < b ^ k := by positivity
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b k : ℕ
hb : 1 < b
n : ℕ
h : ¬n = 0
⊢ (b.digits n).length ≤ k ↔ n < b ^ k
have neg : log b n + 1 ≤ k ↔ log b n < k
Tactic: rw [length_digits b n hb h, ← log_lt_iff_lt_pow hb h]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b k : ℕ
hb : 1 < b
n : ℕ
⊢ k < (b.digits n).length ↔ b ^ k ≤ n
have contrapose! : (b.digits n).length ≤ k ↔ n < b ^ k
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b m : ℕ
hm : m ≠ 0
⊢ (b.digits m).getLast ⋯ ≠ 0
have zero : (digits 0 m).getLast sorry ≠ 0
Tactic: rcases b with (_ | _ | b)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b m : ℕ
hm : m ≠ 0
zero : (digits 0 m).getLast ⋯ ≠ 0
⊢ (b.digits m).getLast ⋯ ≠ 0
have succ : ((HAdd.hAdd (α := ℕ) 0 1).digits m).getLast sorry ≠ 0
Tactic: rcases b with (_ | _ | b)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b m : ℕ
hm : m ≠ 0
zero : (digits 0 m).getLast ⋯ ≠ 0
succ : ((HAdd.hAdd (α := ℕ) 0 1).digits m).getLast ⋯ ≠ 0
⊢ (b.digits m).getLast ⋯ ≠ 0
have succ₁ : ∀ (b : ℕ), ((b + 1 + 1).digits m).getLast sorry ≠ 0
Tactic: rcases b with (_ | _ | b)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
m : ℕ
hm : m ≠ 0
⊢ (digits 0 m).getLast ⋯ ≠ 0
have zero : ∀ (hm : Ne (α := ℕ) 0 0), (digits 0 0).getLast sorry ≠ 0
Tactic: cases m
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
m : ℕ
hm : m ≠ 0
zero : ∀ (hm : Ne (α := ℕ) 0 0), (digits 0 0).getLast ⋯ ≠ 0
⊢ (digits 0 m).getLast ⋯ ≠ 0
have zero₁ : ∀ (n : ℕ) (hm : n + 1 ≠ 0), (digits 0 (n + 1)).getLast sorry ≠ 0
Tactic: cases m
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
m : ℕ
hm : m ≠ 0
b : ℕ
⊢ ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
have succ : ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast sorry ≠ 0
Tactic: revert hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
m b : ℕ
⊢ ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
have succ : ∀ (n : ℕ) (IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast sorry ≠ 0) (hm : n ≠ 0),
  ((b + 1 + 1).digits n).getLast sorry ≠ 0
Tactic: induction m using Nat.strongRecOn with | ind n IH => ?_
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
⊢ ((b + 1 + 1).digits n).getLast ⋯ ≠ 0
have pos : ∀ (hnb : n < b + 2), ((b + 1 + 1).digits n).getLast sorry ≠ 0
Tactic: by_cases! hnb : n < b + 2
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
pos : ∀ (hnb : n < b + 2), ((b + 1 + 1).digits n).getLast ⋯ ≠ 0
⊢ ((b + 1 + 1).digits n).getLast ⋯ ≠ 0
have neg : ∀ (hnb : b + 2 ≤ n), ((b + 1 + 1).digits n).getLast sorry ≠ 0
Tactic: by_cases! hnb : n < b + 2
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : b + 2 ≤ n
⊢ ((b + 1 + 1).digits n).getLast ⋯ ≠ 0
have neg : ((b + 2).digits (n / (b + 2))).getLast sorry ≠ 0
Tactic: rw [digits_getLast n (le_add_left 2 b)]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : b + 2 ≤ n
neg : ((b + 2).digits (n / (b + 2))).getLast ⋯ ≠ 0
⊢ ((b + 1 + 1).digits n).getLast ⋯ ≠ 0
have neg₁ : (b + 2).digits (n / (b + 2)) ≠ []
Tactic: rw [digits_getLast n (le_add_left 2 b)]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : b + 2 ≤ n
⊢ n / b.succ.succ ≠ 0
have neg : 0 < n / b.succ.succ
Tactic: rw [← pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b m n : ℕ
hb : 0 < b
⊢ b.digits n ++ b.digits m = b.digits (n + b ^ (b.digits n).length * m)
have inl : ∀ (hb : 0 < succ 0),
  (succ 0).digits n ++ (succ 0).digits m = (succ 0).digits (n + succ 0 ^ ((succ 0).digits n).length * m)
Tactic: rcases eq_or_lt_of_le (Nat.succ_le_of_lt hb) with (rfl | hb)
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b m n : ℕ
hb : 0 < b
inl :
  ∀ (hb : 0 < succ 0),
    (succ 0).digits n ++ (succ 0).digits m = (succ 0).digits (n + succ 0 ^ ((succ 0).digits n).length * m)
⊢ b.digits n ++ b.digits m = b.digits (n + b ^ (b.digits n).length * m)
have inr : ∀ (hb : succ 0 < b), b.digits n ++ b.digits m = b.digits (n + b ^ (b.digits n).length * m)
Tactic: rcases eq_or_lt_of_le (Nat.succ_le_of_lt hb) with (rfl | hb)
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b m n : ℕ
hb_1 : 0 < b
hb : succ 0 < b
⊢ b.digits n ++ b.digits m = b.digits (n + b ^ (b.digits n).length * m)
have inr : b.digits n ++ b.digits m = b.digits (ofDigits b (b.digits n ++ b.digits m))
Tactic: rw [← ofDigits_digits_append_digits]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b m n : ℕ
hb_1 : 0 < b
hb : succ 0 < b
⊢ b.digits n ++ b.digits m = b.digits (ofDigits b (b.digits n ++ b.digits m))
have inr : ∀ (l : ℕ) (hl : l ∈ b.digits n ++ b.digits m), l < b
Tactic: refine (digits_ofDigits b hb _ (fun l hl => ?_) (fun h_append => ?_)).symm
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b m n : ℕ
hb_1 : 0 < b
hb : succ 0 < b
inr : ∀ (l : ℕ) (hl : l ∈ b.digits n ++ b.digits m), l < b
⊢ b.digits n ++ b.digits m = b.digits (ofDigits b (b.digits n ++ b.digits m))
have inr₁ : ∀ (h_append : b.digits n ++ b.digits m ≠ []), (b.digits n ++ b.digits m).getLast h_append ≠ 0
Tactic: refine (digits_ofDigits b hb _ (fun l hl => ?_) (fun h_append => ?_)).symm
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b m n : ℕ
hb_1 : 0 < b
hb : succ 0 < b
l : ℕ
hl : l ∈ b.digits n ++ b.digits m
⊢ l < b
have inr : ∀ (h : l ∈ b.digits n), l < b
Tactic: rcases (List.mem_append.mp hl) with (h | h)
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b m n : ℕ
hb_1 : 0 < b
hb : succ 0 < b
l : ℕ
hl : l ∈ b.digits n ++ b.digits m
inr : ∀ (h : l ∈ b.digits n), l < b
⊢ l < b
have inr₁ : ∀ (h : l ∈ b.digits m), l < b
Tactic: rcases (List.mem_append.mp hl) with (h | h)
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b m n : ℕ
hb_1 : 0 < b
hb : succ 0 < b
h_append : b.digits n ++ b.digits m ≠ []
⊢ (b.digits n ++ b.digits m).getLast h_append ≠ 0
have pos : ∀ (h : b.digits m = []), (b.digits n ++ b.digits m).getLast h_append ≠ 0
Tactic: by_cases h : digits b m = []
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b m n : ℕ
hb_1 : 0 < b
hb : succ 0 < b
h_append : b.digits n ++ b.digits m ≠ []
pos : ∀ (h : b.digits m = []), (b.digits n ++ b.digits m).getLast h_append ≠ 0
⊢ (b.digits n ++ b.digits m).getLast h_append ≠ 0
have neg : ∀ (h : ¬b.digits m = []), (b.digits n ++ b.digits m).getLast h_append ≠ 0
Tactic: by_cases h : digits b m = []
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b m n : ℕ
hb_1 : 0 < b
hb : succ 0 < b
h_append : b.digits n ++ b.digits m ≠ []
h : b.digits m = []
⊢ (b.digits n ++ b.digits m).getLast h_append ≠ 0
have pos : ∀ (h_append_1 : b.digits n ≠ []), (b.digits n).getLast sorry ≠ 0
Tactic: simp only [h, List.append_nil] at h_append ⊢
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b k m n : ℕ
hb : 1 < b
hm : 0 < m
⊢ b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ ((b.digits n).length + k) * m)
have rw : b.digits n ++ b.digits (b ^ k * m) = b.digits (n + b ^ ((b.digits n).length + k) * m)
Tactic: rw [List.append_assoc, ← digits_base_pow_mul hb hm]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b k m n : ℕ
hb : 1 < b
hm : 0 < m
⊢ b.digits n ++ b.digits (b ^ k * m) = b.digits (n + b ^ ((b.digits n).length + k) * m)
have simp : b ^ (b.digits n).length * (b ^ k * m) = b ^ ((b.digits n).length + k) * m
Tactic: simp only [digits_append_digits (zero_lt_of_lt hb), digits_inj_iff, add_right_inj]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b n : ℕ
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length
have inl : (b.digits 0).length ≤ (b.digits (HAdd.hAdd (α := ℕ) 0 1)).length
Tactic: rcases Decidable.eq_or_ne n 0 with (rfl | hn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b n : ℕ
inl : (b.digits 0).length ≤ (b.digits (HAdd.hAdd (α := ℕ) 0 1)).length
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length
have inr : ∀ (hn : n ≠ 0), (b.digits n).length ≤ (b.digits (n + 1)).length
Tactic: rcases Decidable.eq_or_ne n 0 with (rfl | hn)
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b n : ℕ
hn : n ≠ 0
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length
have inr : ∀ (hb : b ≤ 1), (b.digits n).length ≤ (b.digits (n + 1)).length
Tactic: rcases le_or_gt b 1 with hb | hb
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b n : ℕ
hn : n ≠ 0
inr : ∀ (hb : b ≤ 1), (b.digits n).length ≤ (b.digits (n + 1)).length
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length
have inr₁ : ∀ (hb : 1 < b), (b.digits n).length ≤ (b.digits (n + 1)).length
Tactic: rcases le_or_gt b 1 with hb | hb
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b n : ℕ
hn : n ≠ 0
hb : b ≤ 1
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length
have inr : ∀ (hb : LE.le (α := ℕ) 0 1), (digits 0 n).length ≤ (digits 0 (n + 1)).length
Tactic: interval_cases b
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b n : ℕ
hn : n ≠ 0
hb : b ≤ 1
inr : ∀ (hb : LE.le (α := ℕ) 0 1), (digits 0 n).length ≤ (digits 0 (n + 1)).length
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length
have inr₁ : ∀ (hb : LE.le (α := ℕ) 1 1), (digits 1 n).length ≤ (digits 1 (n + 1)).length
Tactic: interval_cases b
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ (b + 2) ^ l.length ≤ (b + 2) * ofDigits (b + 2) l
have rw : (b + 2) ^ (l.dropLast ++ [l.getLast hl]).length ≤ (b + 2) * ofDigits (b + 2) (l.dropLast ++ [l.getLast hl])
Tactic: rw [← List.dropLast_append_getLast hl]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ (b + 2) ^ (l.dropLast ++ [l.getLast hl]).length ≤ (b + 2) * ofDigits (b + 2) (l.dropLast ++ [l.getLast hl])
have simp : (b + 2) * (b + 2) ^ (l.length - 1) ≤ (b + 2) * (ofDigits (b + 2) l.dropLast + (b + 2) ^ (l.length - 1) * l.getLast hl)
Tactic: simp only [List.length_append, List.length, zero_add, List.length_dropLast, ofDigits_append,
    List.length_dropLast, ofDigits_singleton, add_comm (l.length - 1), pow_add, pow_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ (b + 2) * (b + 2) ^ (l.length - 1) ≤ (b + 2) * (ofDigits (b + 2) l.dropLast + (b + 2) ^ (l.length - 1) * l.getLast hl)
have h : (b + 2) ^ (l.length - 1) ≤ ofDigits (b + 2) l.dropLast + (b + 2) ^ (l.length - 1) * l.getLast hl
Tactic: apply Nat.mul_le_mul_left
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ (b + 2) ^ (l.length - 1) ≤ ofDigits (b + 2) l.dropLast + (b + 2) ^ (l.length - 1) * l.getLast hl
have h : (b + 2) ^ (l.length - 1) ≤ (b + 2) ^ (l.length - 1) * l.getLast hl
Tactic: refine le_trans ?_ (Nat.le_add_left _ _)
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (hypothesis)
Goal:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ (b + 2) ^ (l.length - 1) ≤ (b + 2) ^ (l.length - 1) * l.getLast hl
have this : 0 < l.getLast hl
Tactic: have : 0 < l.getLast hl := by rwa [pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
this : 0 < l.getLast hl
⊢ (b + 2) ^ (l.length - 1) ≤ (b + 2) ^ (l.length - 1) * l.getLast hl
have h : (b + 2) ^ (l.length - 1) = (b + 2) ^ (l.length - 1) * succ 0
Tactic: convert! Nat.mul_le_mul_left ((b + 2) ^ (l.length - 1)) this using 1
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
this : 0 < l.getLast hl
⊢ (b + 2) ^ (l.length - 1) = (b + 2) ^ (l.length - 1) * succ 0
have h : (b + 2) ^ (l.length - 1) = (b + 2) ^ (l.length - 1)
Tactic: rw [Nat.mul_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (hypothesis)
Goal:
b m : ℕ
hm : m ≠ 0
⊢ (b + 2) ^ ((b + 2).digits m).length ≤ (b + 2) * m
have this : (b + 2).digits m ≠ []
Tactic: have : digits (b + 2) m ≠ [] := digits_ne_nil_iff_ne_zero.mpr hm
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b m : ℕ
hm : m ≠ 0
this : (b + 2).digits m ≠ []
⊢ (b + 2) ^ ((b + 2).digits m).length ≤ (b + 2) * m
have h : m = ofDigits (b + 2) ((b + 2).digits m)
Tactic: convert! @pow_length_le_mul_ofDigits b (digits (b + 2) m) this (getLast_digit_ne_zero _ hm)
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b m : ℕ
hm : m ≠ 0
this : (b + 2).digits m ≠ []
⊢ m = ofDigits (b + 2) ((b + 2).digits m)
have h : m = m
Tactic: rw [ofDigits_digits]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b m : ℕ
hb : 1 < b
⊢ m ≠ 0 → b ^ (b.digits m).length ≤ b * m
have zero : ∀ (hb : LT.lt (α := ℕ) 1 0), m ≠ 0 → HPow.hPow (α := ℕ) 0 (digits 0 m).length ≤ 0 * m
Tactic: rcases b with (_ | _ | b)
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b m : ℕ
hb : 1 < b
zero : ∀ (hb : LT.lt (α := ℕ) 1 0), m ≠ 0 → HPow.hPow (α := ℕ) 0 (digits 0 m).length ≤ 0 * m
⊢ m ≠ 0 → b ^ (b.digits m).length ≤ b * m
have succ : ∀ (hb : 1 < HAdd.hAdd (α := ℕ) 0 1),
  m ≠ 0 → HAdd.hAdd (α := ℕ) 0 1 ^ ((HAdd.hAdd (α := ℕ) 0 1).digits m).length ≤ HAdd.hAdd (α := ℕ) 0 1 * m
Tactic: rcases b with (_ | _ | b)
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b m : ℕ
hb : 1 < b
zero : ∀ (hb : LT.lt (α := ℕ) 1 0), m ≠ 0 → HPow.hPow (α := ℕ) 0 (digits 0 m).length ≤ 0 * m
succ :
  ∀ (hb : 1 < HAdd.hAdd (α := ℕ) 0 1),
    m ≠ 0 → HAdd.hAdd (α := ℕ) 0 1 ^ ((HAdd.hAdd (α := ℕ) 0 1).digits m).length ≤ HAdd.hAdd (α := ℕ) 0 1 * m
⊢ m ≠ 0 → b ^ (b.digits m).length ≤ b * m
have succ₁ : ∀ (b : ℕ) (hb : 1 < b + 1 + 1), m ≠ 0 → (b + 1 + 1) ^ ((b + 1 + 1).digits m).length ≤ (b + 1 + 1) * m
Tactic: rcases b with (_ | _ | b)
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
p : ℕ
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : L.getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ L, l < p
⊢ (p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum
have inl : ∀ (h : 1 < p), (p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum
Tactic: obtain h | rfl | h : 1 < p ∨ 1 = p ∨ p < 1 := trichotomous 1 p
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
p : ℕ
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : L.getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ L, l < p
inl : ∀ (h : 1 < p), (p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum
⊢ (p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum
have inr : ∀ (h_lt : ∀ l ∈ L, l < 1),
  HSub.hSub (α := ℕ) 1 1 * ∑ i ∈ range L.length, ofDigits 1 L / HPow.hPow (α := ℕ) 1 i.succ = ofDigits 1 L - L.sum
Tactic: obtain h | rfl | h : 1 < p ∨ 1 = p ∨ p < 1 := trichotomous 1 p
Cleared hypotheses: p, h_lt
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
p : ℕ
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : L.getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ L, l < p
inl : ∀ (h : 1 < p), (p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum
inr :
  ∀ (h_lt : ∀ l ∈ L, l < 1),
    HSub.hSub (α := ℕ) 1 1 * ∑ i ∈ range L.length, ofDigits 1 L / HPow.hPow (α := ℕ) 1 i.succ = ofDigits 1 L - L.sum
⊢ (p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum
have inr₁ : ∀ (h : p < 1), (p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum
Tactic: obtain h | rfl | h : 1 < p ∨ 1 = p ∨ p < 1 := trichotomous 1 p
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih :
  ∀ {h_nonempty : tl ≠ []} (h_ne_zero : tl.getLast h_nonempty ≠ 0) (h_lt : ∀ l ∈ tl, l < p),
    (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
⊢ (p - 1) * ∑ i ∈ range (hd :: tl).length, ofDigits p (hd :: tl) / p ^ i.succ = ofDigits p (hd :: tl) - (hd :: tl).sum
have inl : (p - 1) * ∑ x ∈ range (tl.length + 1), ofDigits p (List.drop x.succ (hd :: tl)) = ofDigits p (hd :: tl) - (hd + tl.sum)
Tactic: simp only [List.length_cons, List.sum_cons, self_div_pow_eq_ofDigits_drop _ _ h,
          digits_ofDigits p h (hd :: tl) h_lt (fun _ => h_ne_zero)]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih :
  ∀ {h_nonempty : tl ≠ []} (h_ne_zero : tl.getLast h_nonempty ≠ 0) (h_lt : ∀ l ∈ tl, l < p),
    (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
⊢ (p - 1) * ∑ x ∈ range (tl.length + 1), ofDigits p (List.drop x.succ (hd :: tl)) =
    (↑hd : ℕ) + p * ofDigits p tl - (hd + tl.sum)
have inl : (p - 1) *
    (∑ x ∈ range tl.length, ofDigits p (List.drop x.succ (hd :: tl)) +
      ofDigits p (List.drop tl.length.succ (hd :: tl))) =
  hd + p * ofDigits p tl - (hd + tl.sum)
Tactic: rw [sum_range_succ, Nat.cast_id]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih :
  ∀ {h_nonempty : tl ≠ []} (h_ne_zero : tl.getLast h_nonempty ≠ 0) (h_lt : ∀ l ∈ tl, l < p),
    (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
h_nonempty : hd :: tl ≠ []
h_ne_zero : (hd :: tl).getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ hd :: tl, l < p
⊢ (p - 1) *
      (∑ x ∈ range tl.length, ofDigits p (List.drop x.succ (hd :: tl)) +
        ofDigits p (List.drop tl.length.succ (hd :: tl))) =
    hd + p * ofDigits p tl - (hd + tl.sum)
have inl : (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) = hd + p * ofDigits p tl - (hd + tl.sum)
Tactic: simp only [List.drop, List.drop_length]