awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
l1 l2 : List ℕ
h : l1.length = l2.length
nil :
  ∀ {l2 : List ℕ} (h : List.length (α := ℕ) [] = l2.length),
    ofDigits b [] + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) [] l2)
⊢ ofDigits b l1 + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) l1 l2)
have cons : ∀ (hd₁ : ℕ) (tl₁ : List ℕ)
  (ih₁ :
    ∀ {l2 : List ℕ} (h : tl₁.length = l2.length),
      ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) tl₁ l2))
  {l2 : List ℕ} (h : (hd₁ :: tl₁).length = l2.length),
  ofDigits b (hd₁ :: tl₁) + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) (hd₁ :: tl₁) l2)
Tactic: induction l1 generalizing l2 with
  | nil => simp_all [eq_comm, List.length_eq_zero_iff, ofDigits]
  | cons hd₁ tl₁ ih₁ =>
    induction l2 generalizing tl₁ with
    | nil => simp_all
    | cons hd₂ tl₂ ih₂ =>
      simp_all only [List.length_cons, ofDigits_cons, add_left_inj,
        eq_comm, List.zipWith_cons_cons]
      rw [← ih₁ h.symm, mul_add]
      ac_rfl
Cleared hypotheses: l1, l2, h
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b m : ℕ
⊢ ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
have ind : ∀ (n : ℕ) (IH : ∀ m < n, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2) {d : ℕ}, d ∈ (b + 2).digits n → d < b + 2
Tactic: induction m using Nat.strongRecOn with | ind n IH => ?_
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b n : ℕ
IH : ∀ m < n, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
d : ℕ
hd : d ∈ (b + 2).digits n
⊢ d < b + 2
have ind : ∀ (IH : ∀ m < 0, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2) (hd : d ∈ (b + 2).digits 0), d < b + 2
Tactic: rcases n with - | n
Cleared hypotheses: n, IH, hd
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b n : ℕ
IH : ∀ m < n, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
d : ℕ
hd : d ∈ (b + 2).digits n
ind : ∀ (IH : ∀ m < 0, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2) (hd : d ∈ (b + 2).digits 0), d < b + 2
⊢ d < b + 2
have ind₁ : ∀ (n : ℕ) (IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2) (hd : d ∈ (b + 2).digits (n + 1)), d < b + 2
Tactic: rcases n with - | n
Cleared hypotheses: n, IH, hd
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (hypothesis)
Goal:
b d : ℕ
IH : ∀ m < 0, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
hd : d ∈ (b + 2).digits 0
⊢ d < b + 2
have hd₁ : Membership.mem (γ := List ℕ) [] d
Tactic: rw [digits_zero] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (hypothesis)
Goal:
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
hd : d ∈ (b + 2).digits (n + 1)
⊢ d < b + 2
have hd₁ : d ∈ (n + 1) % (b + 2) :: (b + 2).digits ((n + 1) / (b + 2))
Tactic: rw [digits_add_two_add_one] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
hd : d ∈ (n + 1) % (b + 2) :: (b + 2).digits ((n + 1) / (b + 2))
⊢ d < b + 2
have ind : (n + 1) % (b + 2) < b + 2
Tactic: cases hd
Cleared hypotheses: d, hd
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
hd : d ∈ (n + 1) % (b + 2) :: (b + 2).digits ((n + 1) / (b + 2))
ind : (n + 1) % (b + 2) < b + 2
⊢ d < b + 2
have ind₁ : List.Mem d ((b + 2).digits ((n + 1) / (b + 2))) → d < b + 2
Tactic: cases hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
⊢ 0 < b + 2
have linarith : b + 2 ≤ 0 → HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 0 (↑b : ℤ) + (HAdd.hAdd (α := ℤ) (↑b : ℤ) 2 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
linarith :
  b + 2 ≤ 0 → HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 0 (↑b : ℤ) + (HAdd.hAdd (α := ℤ) (↑b : ℤ) 2 - 0) = 0
⊢ 0 < b + 2
have linarith₁ : b + 2 ≤ 0 → GT.gt (α := ℤ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
h : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ d < b + 2
have ind : (n + 1) / (b + 2) < n + 1
Tactic: apply IH ((n + 1) / (b + 2))
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
h : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
ind : (n + 1) / (b + 2) < n + 1
⊢ d < b + 2
have ind₁ : d ∈ (b + 2).digits ((n + 1) / (b + 2))
Tactic: apply IH ((n + 1) / (b + 2))
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
h : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ (n + 1) / (b + 2) < n + 1
have ind : 0 < n + 1
Tactic: apply Nat.div_lt_self
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
h : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
ind : 0 < n + 1
⊢ (n + 1) / (b + 2) < n + 1
have ind₁ : 1 < b + 2
Tactic: apply Nat.div_lt_self
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b m d : ℕ
hb : 1 < b
hd : d ∈ b.digits m
⊢ d < b
have zero : ∀ (hb : LT.lt (α := ℕ) 1 0) (hd : d ∈ digits 0 m), d < 0
Tactic: rcases b with (_ | _ | b)
Cleared hypotheses: b, hb, hd
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b m d : ℕ
hb : 1 < b
hd : d ∈ b.digits m
zero : ∀ (hb : LT.lt (α := ℕ) 1 0) (hd : d ∈ digits 0 m), d < 0
⊢ d < b
have succ : ∀ (hb : 1 < HAdd.hAdd (α := ℕ) 0 1) (hd : d ∈ (HAdd.hAdd (α := ℕ) 0 1).digits m), d < HAdd.hAdd (α := ℕ) 0 1
Tactic: rcases b with (_ | _ | b)
Cleared hypotheses: b, hb, hd
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b m d : ℕ
hb : 1 < b
hd : d ∈ b.digits m
zero : ∀ (hb : LT.lt (α := ℕ) 1 0) (hd : d ∈ digits 0 m), d < 0
succ : ∀ (hb : 1 < HAdd.hAdd (α := ℕ) 0 1) (hd : d ∈ (HAdd.hAdd (α := ℕ) 0 1).digits m), d < HAdd.hAdd (α := ℕ) 0 1
⊢ d < b
have succ₁ : ∀ (b : ℕ) (hb : 1 < b + 1 + 1) (hd : d ∈ (b + 1 + 1).digits m), d < b + 1 + 1
Tactic: rcases b with (_ | _ | b)
Cleared hypotheses: b, hb, hd
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b hd : ℕ
tl : List ℕ
IH : ∀ (hl : ∀ x ∈ tl, x < b + 2), ofDigits (b + 2) tl < (b + 2) ^ tl.length
hl : ∀ x ∈ hd :: tl, x < b + 2
⊢ ofDigits (b + 2) (hd :: tl) < (b + 2) ^ (hd :: tl).length
have cons : (↑hd : ℕ) + (b + 2) * ofDigits (b + 2) tl < (b + 2) ^ tl.length * (b + 2)
Tactic: rw [ofDigits, List.length_cons, pow_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (hypothesis)
Goal:
b hd : ℕ
tl : List ℕ
IH : ∀ (hl : ∀ x ∈ tl, x < b + 2), ofDigits (b + 2) tl < (b + 2) ^ tl.length
hl : ∀ x ∈ hd :: tl, x < b + 2
⊢ (↑hd : ℕ) + (b + 2) * ofDigits (b + 2) tl < (b + 2) ^ tl.length * (b + 2)
have this : (ofDigits (b + 2) tl + 1) * (b + 2) ≤ (b + 2) ^ tl.length * (b + 2)
Tactic: have : (ofDigits (b + 2) tl + 1) * (b + 2) ≤ (b + 2) ^ tl.length * (b + 2) :=
      mul_le_mul (IH fun x hx => hl _ (List.mem_cons_of_mem _ hx)) (by rfl) (by simp only [zero_le])
        (Nat.zero_le _)
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b hd : ℕ
tl : List ℕ
IH : ∀ (hl : ∀ x ∈ tl, x < b + 2), ofDigits (b + 2) tl < (b + 2) ^ tl.length
hl : ∀ x ∈ hd :: tl, x < b + 2
this_1 : (ofDigits (b + 2) tl + 1) * (b + 2) ≤ (b + 2) ^ tl.length * (b + 2)
this : hd < b + 2
⊢ (↑hd : ℕ) + (b + 2) * ofDigits (b + 2) tl < (b + 2) ^ tl.length * (b + 2)
have linarith : (b + 2) ^ tl.length * (b + 2) ≤ (↑hd : ℕ) + (b + 2) * ofDigits (b + 2) tl →
  -1 +
          ((ofDigits (HAdd.hAdd (α := ℤ) (↑b : ℤ) 2) tl + 1) * HAdd.hAdd (α := ℤ) (↑b : ℤ) 2 -
            HAdd.hAdd (α := ℤ) (↑b : ℤ) 2 ^ tl.length * HAdd.hAdd (α := ℤ) (↑b : ℤ) 2) +
        (HAdd.hAdd (α := ℤ) (↑hd : ℤ) 1 - HAdd.hAdd (α := ℤ) (↑b : ℤ) 2) +
      (HAdd.hAdd (α := ℤ) (↑b : ℤ) 2 ^ tl.length * HAdd.hAdd (α := ℤ) (↑b : ℤ) 2 -
        ((↑hd : ℤ) + HAdd.hAdd (α := ℤ) (↑b : ℤ) 2 * ofDigits (HAdd.hAdd (α := ℤ) (↑b : ℤ) 2) tl)) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b hd : ℕ
tl : List ℕ
IH : ∀ (hl : ∀ x ∈ tl, x < b + 2), ofDigits (b + 2) tl < (b + 2) ^ tl.length
hl : ∀ x ∈ hd :: tl, x < b + 2
this : (ofDigits (b + 2) tl + 1) * (b + 2) ≤ (b + 2) ^ tl.length * (b + 2)
⊢ (↑hd : ℕ) + (b + 2) * ofDigits (b + 2) tl < (b + 2) ^ tl.length * (b + 2)
have cons : hd < b + 2
Tactic: suffices ↑hd < b + 2 by linarith
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
l : List ℕ
hl : ∀ x ∈ l, x < b + 2
⊢ ofDigits (b + 2) l < (b + 2) ^ l.length
have nil : ∀ (hl : ∀ (x : ℕ), Membership.mem (γ := List ℕ) [] x → x < b + 2),
  ofDigits (b + 2) [] < (b + 2) ^ List.length (α := ℕ) []
Tactic: induction l with
  | nil => simp [ofDigits]
  | cons hd tl IH =>
    rw [ofDigits, List.length_cons, pow_succ]
    have : (ofDigits (b + 2) tl + 1) * (b + 2) ≤ (b + 2) ^ tl.length * (b + 2) :=
      mul_le_mul (IH fun x hx => hl _ (List.mem_cons_of_mem _ hx)) (by rfl) (by simp only [zero_le])
        (Nat.zero_le _)
    suffices ↑hd < b + 2 by linarith
    exact hl hd List.mem_cons_self
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
l : List ℕ
hl : ∀ x ∈ l, x < b + 2
nil :
  ∀ (hl : ∀ (x : ℕ), Membership.mem (γ := List ℕ) [] x → x < b + 2),
    ofDigits (b + 2) [] < (b + 2) ^ List.length (α := ℕ) []
⊢ ofDigits (b + 2) l < (b + 2) ^ l.length
have cons : ∀ (hd : ℕ) (tl : List ℕ) (IH : ∀ (hl : ∀ x ∈ tl, x < b + 2), ofDigits (b + 2) tl < (b + 2) ^ tl.length)
  (hl : ∀ x ∈ hd :: tl, x < b + 2), ofDigits (b + 2) (hd :: tl) < (b + 2) ^ (hd :: tl).length
Tactic: induction l with
  | nil => simp [ofDigits]
  | cons hd tl IH =>
    rw [ofDigits, List.length_cons, pow_succ]
    have : (ofDigits (b + 2) tl + 1) * (b + 2) ≤ (b + 2) ^ tl.length * (b + 2) :=
      mul_le_mul (IH fun x hx => hl _ (List.mem_cons_of_mem _ hx)) (by rfl) (by simp only [zero_le])
        (Nat.zero_le _)
    suffices ↑hd < b + 2 by linarith
    exact hl hd List.mem_cons_self
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
l : List ℕ
hb : 1 < b
hl : ∀ x ∈ l, x < b
⊢ ofDigits b l < b ^ l.length
have zero : ∀ (hb : LT.lt (α := ℕ) 1 0) (hl : ∀ x ∈ l, x < 0), ofDigits 0 l < HPow.hPow (α := ℕ) 0 l.length
Tactic: rcases b with (_ | _ | b)
Cleared hypotheses: b, hb, hl
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
l : List ℕ
hb : 1 < b
hl : ∀ x ∈ l, x < b
zero : ∀ (hb : LT.lt (α := ℕ) 1 0) (hl : ∀ x ∈ l, x < 0), ofDigits 0 l < HPow.hPow (α := ℕ) 0 l.length
⊢ ofDigits b l < b ^ l.length
have succ : ∀ (hb : 1 < HAdd.hAdd (α := ℕ) 0 1) (hl : ∀ x ∈ l, x < HAdd.hAdd (α := ℕ) 0 1),
  ofDigits (HAdd.hAdd (α := ℕ) 0 1) l < HAdd.hAdd (α := ℕ) 0 1 ^ l.length
Tactic: rcases b with (_ | _ | b)
Cleared hypotheses: b, hb, hl
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
l : List ℕ
hb : 1 < b
hl : ∀ x ∈ l, x < b
zero : ∀ (hb : LT.lt (α := ℕ) 1 0) (hl : ∀ x ∈ l, x < 0), ofDigits 0 l < HPow.hPow (α := ℕ) 0 l.length
succ :
  ∀ (hb : 1 < HAdd.hAdd (α := ℕ) 0 1) (hl : ∀ x ∈ l, x < HAdd.hAdd (α := ℕ) 0 1),
    ofDigits (HAdd.hAdd (α := ℕ) 0 1) l < HAdd.hAdd (α := ℕ) 0 1 ^ l.length
⊢ ofDigits b l < b ^ l.length
have succ₁ : ∀ (b : ℕ) (hb : 1 < b + 1 + 1) (hl : ∀ x ∈ l, x < b + 1 + 1), ofDigits (b + 1 + 1) l < (b + 1 + 1) ^ l.length
Tactic: rcases b with (_ | _ | b)
Cleared hypotheses: b, hb, hl
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b m : ℕ
⊢ m < (b + 2) ^ ((b + 2).digits m).length
have h : m = ofDigits (b + 2) ((b + 2).digits m)
Tactic: convert! @ofDigits_lt_base_pow_length' b (digits (b + 2) m) fun _ => digits_lt_base'
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b m : ℕ
⊢ m = ofDigits (b + 2) ((b + 2).digits m)
have h : m = m
Tactic: rw [ofDigits_digits (b + 2) m]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b m : ℕ
hb : 1 < b
⊢ m < b ^ (b.digits m).length
have zero : ∀ (hb : LT.lt (α := ℕ) 1 0), m < HPow.hPow (α := ℕ) 0 (digits 0 m).length
Tactic: rcases b with (_ | _ | b)
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b m : ℕ
hb : 1 < b
zero : ∀ (hb : LT.lt (α := ℕ) 1 0), m < HPow.hPow (α := ℕ) 0 (digits 0 m).length
⊢ m < b ^ (b.digits m).length
have succ : ∀ (hb : 1 < HAdd.hAdd (α := ℕ) 0 1), m < HAdd.hAdd (α := ℕ) 0 1 ^ ((HAdd.hAdd (α := ℕ) 0 1).digits m).length
Tactic: rcases b with (_ | _ | b)
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b m : ℕ
hb : 1 < b
zero : ∀ (hb : LT.lt (α := ℕ) 1 0), m < HPow.hPow (α := ℕ) 0 (digits 0 m).length
succ : ∀ (hb : 1 < HAdd.hAdd (α := ℕ) 0 1), m < HAdd.hAdd (α := ℕ) 0 1 ^ ((HAdd.hAdd (α := ℕ) 0 1).digits m).length
⊢ m < b ^ (b.digits m).length
have succ₁ : ∀ (b : ℕ) (hb : 1 < b + 1 + 1), m < (b + 1 + 1) ^ ((b + 1 + 1).digits m).length
Tactic: rcases b with (_ | _ | b)
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b m : ℕ
hb : 1 < b
hm : 0 < m
⊢ b.digits (b * m) = 0 :: b.digits m
have rw : b * m % b :: b.digits (b * m / b) = 0 :: b.digits m
Tactic: rw [digits_def' hb (by positivity)]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ} (hm : 0 < m), b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
⊢ b.digits (b ^ (k + 1) * m) = List.replicate (k + 1) 0 ++ b.digits m
have succ : b.digits (b * b ^ k * m) = List.replicate (k + 1) 0 ++ b.digits m
Tactic: rw [pow_succ', mul_assoc, digits_base_mul hb (by positivity), ih hm, List.replicate_succ,
      List.cons_append]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ} (hm : 0 < m), b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
succ : b.digits (b * b ^ k * m) = List.replicate (k + 1) 0 ++ b.digits m
⊢ b.digits (b ^ (k + 1) * m) = List.replicate (k + 1) 0 ++ b.digits m
have succ₁ : b.digits (b * (b ^ k * m)) = List.replicate (k + 1) 0 ++ b.digits m
Tactic: rw [pow_succ', mul_assoc, digits_base_mul hb (by positivity), ih hm, List.replicate_succ,
      List.cons_append]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ} (hm : 0 < m), b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
succ : b.digits (b * b ^ k * m) = List.replicate (k + 1) 0 ++ b.digits m
succ₁ : b.digits (b * (b ^ k * m)) = List.replicate (k + 1) 0 ++ b.digits m
⊢ b.digits (b ^ (k + 1) * m) = List.replicate (k + 1) 0 ++ b.digits m
have succ₂ : 0 :: b.digits (b ^ k * m) = List.replicate (k + 1) 0 ++ b.digits m
Tactic: rw [pow_succ', mul_assoc, digits_base_mul hb (by positivity), ih hm, List.replicate_succ,
      List.cons_append]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ} (hm : 0 < m), b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
succ : b.digits (b * b ^ k * m) = List.replicate (k + 1) 0 ++ b.digits m
succ₁ : b.digits (b * (b ^ k * m)) = List.replicate (k + 1) 0 ++ b.digits m
succ₂ : 0 :: b.digits (b ^ k * m) = List.replicate (k + 1) 0 ++ b.digits m
⊢ b.digits (b ^ (k + 1) * m) = List.replicate (k + 1) 0 ++ b.digits m
have succ₃ : 0 :: (List.replicate k 0 ++ b.digits m) = List.replicate (k + 1) 0 ++ b.digits m
Tactic: rw [pow_succ', mul_assoc, digits_base_mul hb (by positivity), ih hm, List.replicate_succ,
      List.cons_append]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ} (hm : 0 < m), b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
succ : b.digits (b * b ^ k * m) = List.replicate (k + 1) 0 ++ b.digits m
succ₁ : b.digits (b * (b ^ k * m)) = List.replicate (k + 1) 0 ++ b.digits m
succ₂ : 0 :: b.digits (b ^ k * m) = List.replicate (k + 1) 0 ++ b.digits m
succ₃ : 0 :: (List.replicate k 0 ++ b.digits m) = List.replicate (k + 1) 0 ++ b.digits m
⊢ b.digits (b ^ (k + 1) * m) = List.replicate (k + 1) 0 ++ b.digits m
have succ₄ : 0 :: (List.replicate k 0 ++ b.digits m) = 0 :: List.replicate k 0 ++ b.digits m
Tactic: rw [pow_succ', mul_assoc, digits_base_mul hb (by positivity), ih hm, List.replicate_succ,
      List.cons_append]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
hb : 1 < b
k : ℕ
ih : ∀ {m : ℕ} (hm : 0 < m), b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
m : ℕ
hm : 0 < m
succ : b.digits (b * b ^ k * m) = List.replicate (k + 1) 0 ++ b.digits m
succ₁ : b.digits (b * (b ^ k * m)) = List.replicate (k + 1) 0 ++ b.digits m
succ₂ : 0 :: b.digits (b ^ k * m) = List.replicate (k + 1) 0 ++ b.digits m
succ₃ : 0 :: (List.replicate k 0 ++ b.digits m) = List.replicate (k + 1) 0 ++ b.digits m
succ₄ : 0 :: (List.replicate k 0 ++ b.digits m) = 0 :: List.replicate k 0 ++ b.digits m
⊢ b.digits (b ^ (k + 1) * m) = List.replicate (k + 1) 0 ++ b.digits m
have succ₅ : 0 :: (List.replicate k 0 ++ b.digits m) = 0 :: (List.replicate k 0 ++ b.digits m)
Tactic: rw [pow_succ', mul_assoc, digits_base_mul hb (by positivity), ih hm, List.replicate_succ,
      List.cons_append]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b k m : ℕ
hb : 1 < b
hm : 0 < m
⊢ b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
have zero : ∀ {m : ℕ} (hm : 0 < m), b.digits (HPow.hPow (β := ℕ) b 0 * m) = List.replicate 0 0 ++ b.digits m
Tactic: induction k generalizing m with
  | zero => simp
  | succ k ih =>
    rw [pow_succ', mul_assoc, digits_base_mul hb (by positivity), ih hm, List.replicate_succ,
      List.cons_append]
Cleared hypotheses: k, m, hm
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b k m : ℕ
hb : 1 < b
hm : 0 < m
zero : ∀ {m : ℕ} (hm : 0 < m), b.digits (HPow.hPow (β := ℕ) b 0 * m) = List.replicate 0 0 ++ b.digits m
⊢ b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m
have succ : ∀ (k : ℕ) (ih : ∀ {m : ℕ} (hm : 0 < m), b.digits (b ^ k * m) = List.replicate k 0 ++ b.digits m) {m : ℕ} (hm : 0 < m),
  b.digits (b ^ (k + 1) * m) = List.replicate (k + 1) 0 ++ b.digits m
Tactic: induction k generalizing m with
  | zero => simp
  | succ k ih =>
    rw [pow_succ', mul_assoc, digits_base_mul hb (by positivity), ih hm, List.replicate_succ,
      List.cons_append]
Cleared hypotheses: k, m, hm
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b m n : ℕ
⊢ ofDigits b (b.digits n ++ b.digits m) = n + b ^ (b.digits n).length * m
have rw : ofDigits b (b.digits n) + b ^ (b.digits n).length * ofDigits b (b.digits m) = n + b ^ (b.digits n).length * m
Tactic: rw [ofDigits_append, ofDigits_digits, ofDigits_digits]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b m n : ℕ
rw : ofDigits b (b.digits n) + b ^ (b.digits n).length * ofDigits b (b.digits m) = n + b ^ (b.digits n).length * m
⊢ ofDigits b (b.digits n ++ b.digits m) = n + b ^ (b.digits n).length * m
have rw₁ : n + b ^ (b.digits n).length * ofDigits b (b.digits m) = n + b ^ (b.digits n).length * m
Tactic: rw [ofDigits_append, ofDigits_digits, ofDigits_digits]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b m n : ℕ
rw : ofDigits b (b.digits n) + b ^ (b.digits n).length * ofDigits b (b.digits m) = n + b ^ (b.digits n).length * m
rw₁ : n + b ^ (b.digits n).length * ofDigits b (b.digits m) = n + b ^ (b.digits n).length * m
⊢ ofDigits b (b.digits n ++ b.digits m) = n + b ^ (b.digits n).length * m
have rw₂ : n + b ^ (b.digits n).length * m = n + b ^ (b.digits n).length * m
Tactic: rw [ofDigits_append, ofDigits_digits, ofDigits_digits]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p q : ℕ
h : p ≤ q
head : ℕ
tail : List ℕ
hi : ofDigits p tail ≤ ofDigits q tail
⊢ ofDigits p (head :: tail) ≤ ofDigits q (head :: tail)
have cons : p * ofDigits p tail ≤ q * ofDigits q tail
Tactic: simp only [ofDigits, cast_id, add_le_add_iff_left]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p q : ℕ
L : List ℕ
h : p ≤ q
⊢ ofDigits p L ≤ ofDigits q L
have nil : ofDigits p [] ≤ ofDigits p []
Tactic: induction L with
  | nil => rfl
  | cons _ _ hi =>
    simp only [ofDigits, cast_id, add_le_add_iff_left]
    exact Nat.mul_le_mul h hi
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p q : ℕ
L : List ℕ
h : p ≤ q
nil : ofDigits p [] ≤ ofDigits p []
⊢ ofDigits p L ≤ ofDigits q L
have cons : ∀ (head : ℕ) (tail : List ℕ) (hi : ofDigits p tail ≤ ofDigits q tail),
  ofDigits p (head :: tail) ≤ ofDigits q (head :: tail)
Tactic: induction L with
  | nil => rfl
  | cons _ _ hi =>
    simp only [ofDigits, cast_id, add_le_add_iff_left]
    exact Nat.mul_le_mul h hi
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
n : ℕ
h : (digits 0 n).sum ≤ n
⊢ (digits 0 (n + 1)).sum ≤ n + 1
have succ : [n + 1].sum ≤ n + 1
Tactic: rw [digits_zero_succ, List.sum_cons, List.sum_nil, add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
n : ℕ
h : (digits 0 n).sum ≤ n
succ : [n + 1].sum ≤ n + 1
⊢ (digits 0 (n + 1)).sum ≤ n + 1
have succ₁ : n + 1 + List.sum [] ≤ n + 1
Tactic: rw [digits_zero_succ, List.sum_cons, List.sum_nil, add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
n : ℕ
h : (digits 0 n).sum ≤ n
succ : [n + 1].sum ≤ n + 1
succ₁ : n + 1 + List.sum [] ≤ n + 1
⊢ (digits 0 (n + 1)).sum ≤ n + 1
have succ₂ : n + 1 + 0 ≤ n + 1
Tactic: rw [digits_zero_succ, List.sum_cons, List.sum_nil, add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
n : ℕ
h : (digits 0 n).sum ≤ n
succ : [n + 1].sum ≤ n + 1
succ₁ : n + 1 + List.sum [] ≤ n + 1
succ₂ : n + 1 + 0 ≤ n + 1
⊢ (digits 0 (n + 1)).sum ≤ n + 1
have succ₃ : n + 1 ≤ n + 1
Tactic: rw [digits_zero_succ, List.sum_cons, List.sum_nil, add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
n p : ℕ
h : (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
h_1 : ((p + 1).digits n).sum ≤ n
⊢ ((p + 1).digits (n + 1)).sum ≤ n + 1
have succ : ((p + 1).digits (n + 1)).sum ≤ ofDigits p.succ (p.succ.digits (n + 1))
Tactic: nth_rw 2 [← ofDigits_digits p.succ (n + 1)]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
n p : ℕ
h : (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
h_1 : ((p + 1).digits n).sum ≤ n
⊢ ((p + 1).digits (n + 1)).sum ≤ ofDigits p.succ (p.succ.digits (n + 1))
have succ : ofDigits 1 (p.succ.digits n.succ) ≤ ofDigits p.succ (p.succ.digits (n + 1))
Tactic: rw [← ofDigits_one <| digits p.succ n.succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p n : ℕ
h : (p.digits n).sum ≤ n
⊢ (p.digits (n + 1)).sum ≤ n + 1
have succ : (digits 0 n).sum ≤ n → (digits 0 (n + 1)).sum ≤ n + 1
Tactic: induction p with
    | zero => rw [digits_zero_succ, List.sum_cons, List.sum_nil, add_zero]
    | succ p =>
      nth_rw 2 [← ofDigits_digits p.succ (n + 1)]
      rw [← ofDigits_one <| digits p.succ n.succ]
      exact ofDigits_monotone (digits p.succ n.succ) <| Nat.succ_pos p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p n : ℕ
h : (p.digits n).sum ≤ n
succ : (digits 0 n).sum ≤ n → (digits 0 (n + 1)).sum ≤ n + 1
⊢ (p.digits (n + 1)).sum ≤ n + 1
have succ₁ : ∀ (p : ℕ),
  ((p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1) →
    ((p + 1).digits n).sum ≤ n → ((p + 1).digits (n + 1)).sum ≤ n + 1
Tactic: induction p with
    | zero => rw [digits_zero_succ, List.sum_cons, List.sum_nil, add_zero]
    | succ p =>
      nth_rw 2 [← ofDigits_digits p.succ (n + 1)]
      rw [← ofDigits_one <| digits p.succ n.succ]
      exact ofDigits_monotone (digits p.succ n.succ) <| Nat.succ_pos p
Cleared hypotheses: p, h