awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Digits.Lemmas
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

Tactic:
(List.getLast_append_of_right_ne_nil _ _ h) ▸
          (getLast_digit_ne_zero _ <| digits_ne_nil_iff_ne_zero.mp h)

Premises used: List.getLast_append_of_right_ne_nil, Nat.getLast_digit_ne_zero, Eq.rec, Nat.digits_ne_nil_iff_ne_zero, Iff.mp, Eq.symm
-- Module: Mathlib.Data.Nat.Digits.Lemmas
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

Tactic:
exact (List.getLast_append_of_right_ne_nil _ _ h) ▸
          (getLast_digit_ne_zero _ <| digits_ne_nil_iff_ne_zero.mp h)
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b k m n : ℕ
hb : 1 < b
hm : 0 < m
rw : b.digits n ++ b.digits (b ^ k * m) = b.digits (n + b ^ ((b.digits n).length + k) * m)
⊢ b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ ((b.digits n).length + k) * m)

Tactic:
rw [List.append_assoc, ← digits_base_pow_mul hb hm]

Premises used: List.append_assoc, Nat.digits_base_pow_mul
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b k m n : ℕ
hb : 1 < b
hm : 0 < m
simp : b ^ (b.digits n).length * (b ^ k * m) = b ^ ((b.digits n).length + k) * m
⊢ b.digits n ++ b.digits (b ^ k * m) = b.digits (n + b ^ ((b.digits n).length + k) * m)

Tactic:
simp only [digits_append_digits (zero_lt_of_lt hb), digits_inj_iff, add_right_inj]

Premises used: Nat.zero_lt_of_lt, Nat.digits_append_digits, Nat.digits_inj_iff, add_right_inj
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b k m n : ℕ
hb : 1 < b
hm : 0 < m
⊢ b ^ (b.digits n).length * (b ^ k * m) = b ^ ((b.digits n).length + k) * m

Tactic:
ring
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b n : ℕ
inl : (b.digits 0).length ≤ (b.digits (HAdd.hAdd (α := ℕ) 0 1)).length
inr : ∀ (hn : n ≠ 0), (b.digits n).length ≤ (b.digits (n + 1)).length
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length

Tactic:
rcases Decidable.eq_or_ne n 0 with (rfl | hn)

Premises used: Decidable.eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
⊢ (b.digits 0).length ≤ (b.digits (HAdd.hAdd (α := ℕ) 0 1)).length

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b n : ℕ
hn : n ≠ 0
inr : ∀ (hb : b ≤ 1), (b.digits n).length ≤ (b.digits (n + 1)).length
inr₁ : ∀ (hb : 1 < b), (b.digits n).length ≤ (b.digits (n + 1)).length
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length

Tactic:
rcases le_or_gt b 1 with hb | hb

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b n : ℕ
hn : n ≠ 0
hb : b ≤ 1
inr : ∀ (hb : LE.le (α := ℕ) 0 1), (digits 0 n).length ≤ (digits 0 (n + 1)).length
inr₁ : ∀ (hb : LE.le (α := ℕ) 1 1), (digits 1 n).length ≤ (digits 1 (n + 1)).length
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length

Tactic:
interval_cases b
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b n : ℕ
hn : n ≠ 0
hb : LE.le (α := ℕ) 0 1
⊢ (digits 0 n).length ≤ (digits 0 (n + 1)).length

Tactic:
simp +arith [digits_zero_succ', hn]

Premises used: Nat.digits_zero_succ'
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b n : ℕ
hn : n ≠ 0
hb : LE.le (α := ℕ) 1 1
⊢ (digits 1 n).length ≤ (digits 1 (n + 1)).length

Tactic:
simp +arith [digits_zero_succ', hn]

Premises used: Nat.digits_zero_succ'
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b n : ℕ
hn : n ≠ 0
hb : 1 < b
⊢ (b.digits n).length ≤ (b.digits (n + 1)).length

Tactic:
simpa [length_digits, hb, hn] using log_mono_right (le_succ _)

Premises used: Nat.le_succ, Nat.length_digits, Nat.log_mono_right
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b n m : ℕ
h : n ≤ m
⊢ (b.digits n).length ≤ (b.digits m).length

Tactic:
monotone_nat_of_le_succ (length_digits_le_length_digits_succ b) h

Premises used: Nat.length_digits_le_length_digits_succ, monotone_nat_of_le_succ
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
rw : (b + 2) ^ (l.dropLast ++ [l.getLast hl]).length ≤ (b + 2) * ofDigits (b + 2) (l.dropLast ++ [l.getLast hl])
⊢ (b + 2) ^ l.length ≤ (b + 2) * ofDigits (b + 2) l

Tactic:
rw [← List.dropLast_append_getLast hl]

Premises used: List.dropLast_append_getLast
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
simp :
  (b + 2) * (b + 2) ^ (l.length - 1) ≤ (b + 2) * (ofDigits (b + 2) l.dropLast + (b + 2) ^ (l.length - 1) * l.getLast hl)
⊢ (b + 2) ^ (l.dropLast ++ [l.getLast hl]).length ≤ (b + 2) * ofDigits (b + 2) (l.dropLast ++ [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]

Premises used: HSub.hSub, List.length_dropLast, pow_add, List.length_append, zero_add, add_comm, pow_one, Nat.ofDigits_append, Nat.ofDigits_singleton, OfNat.ofNat, List.length
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
h : (b + 2) ^ (l.length - 1) ≤ ofDigits (b + 2) l.dropLast + (b + 2) ^ (l.length - 1) * l.getLast hl
⊢ (b + 2) * (b + 2) ^ (l.length - 1) ≤ (b + 2) * (ofDigits (b + 2) l.dropLast + (b + 2) ^ (l.length - 1) * l.getLast hl)

Tactic:
apply Nat.mul_le_mul_left

Premises used: Nat.mul_le_mul_left
-- Module: Mathlib.Data.Nat.Digits.Lemmas
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

Tactic:
le_trans ?_ (Nat.le_add_left _ _)

Premises used: Nat.le_add_left, le_trans
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
h : (b + 2) ^ (l.length - 1) ≤ (b + 2) ^ (l.length - 1) * l.getLast hl
⊢ (b + 2) ^ (l.length - 1) ≤ ofDigits (b + 2) l.dropLast + (b + 2) ^ (l.length - 1) * l.getLast hl

Tactic:
refine le_trans ?_ (Nat.le_add_left _ _)

Premises used: Nat.le_add_left, le_trans
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
rwa rwa₁ rwa₂ rwa₃ : l.getLast hl ≠ 0
⊢ 0 < l.getLast hl

Tactic:
rwa [pos_iff_ne_zero]

Premises used: pos_iff_ne_zero
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
⊢ 0 < l.getLast hl

Tactic:
have : 0 < l.getLast hl := by rwa [pos_iff_ne_zero]
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
this : 0 < l.getLast hl
⊢ (b + 2) ^ (l.length - 1) * succ 0 ≤ (b + 2) ^ (l.length - 1) * l.getLast hl

Tactic:
Nat.mul_le_mul_left ((b + 2) ^ (l.length - 1)) this

Premises used: HSub.hSub, Nat.mul_le_mul_left, HPow.hPow, HAdd.hAdd, OfNat.ofNat, List.length
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
this : 0 < l.getLast hl
h : (b + 2) ^ (l.length - 1) = (b + 2) ^ (l.length - 1) * succ 0
⊢ (b + 2) ^ (l.length - 1) ≤ (b + 2) ^ (l.length - 1) * l.getLast hl

Tactic:
convert! Nat.mul_le_mul_left ((b + 2) ^ (l.length - 1)) this using 1

Premises used: HSub.hSub, Nat.mul_le_mul_left, HPow.hPow, HAdd.hAdd, OfNat.ofNat, List.length
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
l : List ℕ
hl : l ≠ []
hl2 : l.getLast hl ≠ 0
this : 0 < l.getLast hl
h h₁ : (b + 2) ^ (l.length - 1) = (b + 2) ^ (l.length - 1)
⊢ (b + 2) ^ (l.length - 1) = (b + 2) ^ (l.length - 1) * succ 0

Tactic:
rw [Nat.mul_one]

Premises used: Nat.mul_one
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b m : ℕ
hm : m ≠ 0
⊢ (b + 2).digits m ≠ []

Tactic:
have : digits (b + 2) m ≠ [] := digits_ne_nil_iff_ne_zero.mpr hm
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b m : ℕ
hm : m ≠ 0
this : (b + 2).digits m ≠ []
⊢ (b + 2) ^ ((b + 2).digits m).length ≤ (b + 2) * ofDigits (b + 2) ((b + 2).digits m)

Tactic:
@pow_length_le_mul_ofDigits b (digits (b + 2) m) this (getLast_digit_ne_zero _ hm)

Premises used: Nat.pow_length_le_mul_ofDigits, Nat.getLast_digit_ne_zero
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b m : ℕ
hm : m ≠ 0
this : (b + 2).digits m ≠ []
h : m = ofDigits (b + 2) ((b + 2).digits m)
⊢ (b + 2) ^ ((b + 2).digits m).length ≤ (b + 2) * m

Tactic:
convert! @pow_length_le_mul_ofDigits b (digits (b + 2) m) this (getLast_digit_ne_zero _ hm)

Premises used: Nat.pow_length_le_mul_ofDigits, Nat.getLast_digit_ne_zero
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b m : ℕ
hm : m ≠ 0
this : (b + 2).digits m ≠ []
h h₁ : m = m
⊢ m = ofDigits (b + 2) ((b + 2).digits m)

Tactic:
rw [ofDigits_digits]

Premises used: Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
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
succ₁ : ∀ (b : ℕ) (hb : 1 < b + 1 + 1), m ≠ 0 → (b + 1 + 1) ^ ((b + 1 + 1).digits m).length ≤ (b + 1 + 1) * m
⊢ m ≠ 0 → b ^ (b.digits m).length ≤ b * m

Tactic:
rcases b with (_ | _ | b)
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
m : ℕ
hb : LT.lt (α := ℕ) 1 0
⊢ m ≠ 0 → HPow.hPow (α := ℕ) 0 (digits 0 m).length ≤ 0 * m

Tactic:
simp_all [base_pow_length_digits_le']

Premises used: Nat.base_pow_length_digits_le'
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
m : ℕ
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:
simp_all [base_pow_length_digits_le']

Premises used: Nat.base_pow_length_digits_le'
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
m b : ℕ
hb : 1 < b + 1 + 1
⊢ m ≠ 0 → (b + 1 + 1) ^ ((b + 1 + 1).digits m).length ≤ (b + 1 + 1) * m

Tactic:
simp_all [base_pow_length_digits_le']

Premises used: Nat.base_pow_length_digits_le'
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p : ℕ
L : List ℕ
h_nonempty : L ≠ []
h_ne_zero : L.getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ L, l < p
⊢ 1 < p ∨ 1 = p ∨ p < 1

Tactic:
trichotomous 1 p

Premises used: trichotomous, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Digits.Lemmas
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
inr₁ : ∀ (h : p < 1), (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

Tactic:
obtain h | rfl | h : 1 < p ∨ 1 = p ∨ p < 1 := trichotomous 1 p

Premises used: trichotomous, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p : ℕ
h : 1 < p
h_nonempty : Ne (α := List ℕ) [] []
h_ne_zero : List.getLast [] h_nonempty ≠ 0
h_lt : ∀ (l : ℕ), Membership.mem (γ := List ℕ) [] l → l < p
⊢ (p - 1) * ∑ i ∈ range (List.length (α := ℕ) []), ofDigits p [] / p ^ i.succ = ofDigits p [] - List.sum []

Tactic:
simp [ofDigits]

Premises used: Nat.ofDigits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
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
inl :
  (p - 1) * ∑ x ∈ range (tl.length + 1), ofDigits p (List.drop x.succ (hd :: tl)) =
    ofDigits p (hd :: tl) - (hd + tl.sum)
⊢ (p - 1) * ∑ i ∈ range (hd :: tl).length, ofDigits p (hd :: tl) / p ^ i.succ = 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)]

Premises used: List.length_cons, List.cons, List.sum_cons, Nat.digits_ofDigits, Nat.self_div_pow_eq_ofDigits_drop
-- Module: Mathlib.Data.Nat.Digits.Lemmas
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
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)
⊢ (p - 1) * ∑ x ∈ range (tl.length + 1), ofDigits p (List.drop x.succ (hd :: tl)) =
    (↑hd : ℕ) + p * ofDigits p tl - (hd + tl.sum)

Tactic:
rw [sum_range_succ, Nat.cast_id]

Premises used: Nat.cast_id, Finset.sum_range_succ
-- Module: Mathlib.Data.Nat.Digits.Lemmas
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
inl :
  (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)
⊢ (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:
simp only [List.drop, List.drop_length]

Premises used: List.drop, List.drop_length
-- Module: Mathlib.Data.Nat.Digits.Lemmas
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
inl :
  ∀
    (ih :
      ∀ {h_nonempty : Ne (α := List ℕ) [] []} (h_ne_zero : List.getLast [] h_nonempty ≠ 0)
        (h_lt : ∀ (l : ℕ), Membership.mem (γ := List ℕ) [] l → l < p),
        (p - 1) * ∑ i ∈ range (List.length (α := ℕ) []), ofDigits p [] / p ^ i.succ = ofDigits p [] - List.sum [])
    {h_nonempty : [hd] ≠ []} (h_ne_zero : [hd].getLast h_nonempty ≠ 0) (h_lt : ∀ l ∈ [hd], l < p),
    (p - 1) * (∑ x ∈ range (List.length (α := ℕ) []), ofDigits p (List.drop x []) + ofDigits p []) =
      hd + p * ofDigits p [] - (hd + List.sum [])
inl₁ :
  ∀ (h' : ¬tl = []),
    (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
      hd + p * ofDigits p tl - (hd + tl.sum)
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
obtain rfl | h' := em <| tl = []

Premises used: em, rfl
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p : ℕ
h : 1 < p
hd : ℕ
ih :
  ∀ {h_nonempty : Ne (α := List ℕ) [] []} (h_ne_zero : List.getLast [] h_nonempty ≠ 0)
    (h_lt : ∀ (l : ℕ), Membership.mem (γ := List ℕ) [] l → l < p),
    (p - 1) * ∑ i ∈ range (List.length (α := ℕ) []), ofDigits p [] / p ^ i.succ = ofDigits p [] - List.sum []
h_nonempty : [hd] ≠ []
h_ne_zero : [hd].getLast h_nonempty ≠ 0
h_lt : ∀ l ∈ [hd], l < p
⊢ (p - 1) * (∑ x ∈ range (List.length (α := ℕ) []), ofDigits p (List.drop x []) + ofDigits p []) =
    hd + p * ofDigits p [] - (hd + List.sum [])

Tactic:
simp [ofDigits]

Premises used: Nat.ofDigits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
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
h' : ¬tl = []
⊢ ∀ (l : ℕ) (hl : l ∈ tl), l < p

Tactic:
have w₁' := fun l hl ↦ h_lt l <| List.mem_cons_of_mem hd hl
-- Module: Mathlib.Data.Nat.Digits.Lemmas
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
h' : ¬tl = []
w₁' : ∀ (l : ℕ) (hl : l ∈ tl), l < p
⊢ ∀ (h : tl ≠ []), tl.getLast h ≠ 0

Tactic:
have w₂' := fun (h : tl ≠ []) ↦ (List.getLast_cons h) ▸ h_ne_zero
-- Module: Mathlib.Data.Nat.Digits.Lemmas
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
h' : ¬tl = []
w₁' : ∀ (l : ℕ) (hl : l ∈ tl), l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
⊢ (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum

Tactic:
have ih := ih (w₂' h') w₁'
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih_1 :
  ∀ {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
h' : ¬tl = []
w₁' : ∀ (l : ℕ) (hl : l ∈ tl), l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
⊢ (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum

Tactic:
simp only [self_div_pow_eq_ofDigits_drop _ _ h, digits_ofDigits p h tl w₁' w₂',
          ← Nat.one_add] at ih

Premises used: Nat.digits_ofDigits, Nat.one_add, Nat.self_div_pow_eq_ofDigits_drop
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih_1 :
  ∀ {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
h' : ¬tl = []
w₁' : ∀ (l : ℕ) (hl : l ∈ tl), l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
⊢ ∑ x ∈ {tl.length}, ofDigits p (List.drop x tl) = ofDigits p (List.drop tl.length tl)

Tactic:
have := sum_singleton (fun x ↦ ofDigits p <| tl.drop x) tl.length
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih_1 :
  ∀ {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
h' : ¬tl = []
w₁' : ∀ (l : ℕ) (hl : l ∈ tl), l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : ∑ x ∈ {tl.length}, ofDigits p (List.drop x tl) = ofDigits p (List.drop tl.length tl)
⊢ Eq (α := ℕ) (∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl)) 0

Tactic:
rw [← Ico_succ_singleton, List.drop_length, ofDigits] at this

Premises used: Nat.ofDigits, Nat.Ico_succ_singleton, List.drop_length
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih_1 :
  ∀ {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
h' : ¬tl = []
w₁' : ∀ (l : ℕ) (hl : l ∈ tl), l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : Eq (α := ℕ) (∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl)) 0
⊢ 1 ≤ tl.length

Tactic:
have h₁ : 1 ≤ tl.length := List.length_pos_iff.mpr h'
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih_1 :
  ∀ {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
h' : ¬tl = []
w₁' : ∀ (l : ℕ) (hl : l ∈ tl), l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : Eq (α := ℕ) (∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl)) 0
h₁ : 1 ≤ tl.length
inl : (p - 1) * ofDigits p tl + ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
rw [← sum_range_add_sum_Ico _ <| h₁, ← add_zero (∑ x ∈ Ico _ _, ofDigits p (tl.drop x)),
            ← this, sum_Ico_consecutive _ h₁ <| (le_add_right tl.length 1),
            ← sum_Ico_add _ 0 tl.length 1,
            Ico_zero_eq_range, mul_add, mul_add, ih, range_one, sum_singleton, List.drop, ofDigits,
            mul_zero, add_zero, ← Nat.add_sub_assoc <| sum_le_ofDigits _ <| Nat.le_of_lt h]

Premises used: Finset.sum_range_add_sum_Ico, Nat.sum_le_ofDigits, Nat.ofDigits, Nat.add_sub_assoc, Nat.le_add_right, Finset.Ico, Nat.le_of_lt, MulZeroClass.mul_zero, Finset.sum_singleton, Finset.sum_Ico_add, List.drop, Finset.sum_Ico_consecutive, Nat.Ico_zero_eq_range, mul_add, Finset.range_one, add_zero, OfNat.ofNat, List.length, Finset.sum
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih_1 :
  ∀ {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
h' : ¬tl = []
w₁' : ∀ (l : ℕ) (hl : l ∈ tl), l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : Eq (α := ℕ) (∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl)) 0
h₁ : 1 ≤ tl.length
inl : (p - 1) * ofDigits p tl + 1 * ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)
⊢ (p - 1) * ofDigits p tl + ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
nth_rw 2 [← one_mul <| ofDigits p tl]

Premises used: Nat.ofDigits, one_mul
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
p : ℕ
h : 1 < p
hd : ℕ
tl : List ℕ
ih_1 :
  ∀ {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
h' : ¬tl = []
w₁' : ∀ (l : ℕ) (hl : l ∈ tl), l < p
w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
ih : (p - 1) * ∑ x ∈ range tl.length, ofDigits p (List.drop (1 + x) tl) = ofDigits p tl - tl.sum
this : Eq (α := ℕ) (∑ x ∈ Ico tl.length (tl.length + 1), ofDigits p (List.drop x tl)) 0
h₁ : 1 ≤ tl.length
inl : (p - 1 + 1) * ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)
inl₁ : p * ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)
inl₂ inl₃ : p * ofDigits p tl - tl.sum = p * ofDigits p tl - tl.sum
⊢ (p - 1) * ofDigits p tl + 1 * ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)

Tactic:
rw [← add_mul, Nat.sub_add_cancel (one_le_of_lt h), Nat.add_sub_add_left]

Premises used: add_mul, Nat.add_sub_add_left, Nat.one_le_of_lt, Nat.sub_add_cancel