awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)
have 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 [])
Tactic: obtain rfl | h' := em <| tl = []
Cleared hypotheses: tl, ih, h_nonempty, h_ne_zero, h_lt
-- 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
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 [])
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)
have 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)
Tactic: obtain rfl | h' := em <| tl = []
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (hypothesis)
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 = []
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)
have w₁' : ∀ (l : ℕ) (hl : l ∈ tl), l < p
Tactic: have w₁' := fun l hl ↦ h_lt l <| List.mem_cons_of_mem hd hl
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (hypothesis)
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
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)
have w₂' : ∀ (h : tl ≠ []), tl.getLast h ≠ 0
Tactic: have w₂' := fun (h : tl ≠ []) ↦ (List.getLast_cons h) ▸ h_ne_zero
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (hypothesis)
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) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)
have ih₁ : (p - 1) * ∑ i ∈ range tl.length, ofDigits p tl / p ^ i.succ = ofDigits p tl - tl.sum
Tactic: have ih := ih (w₂' h') w₁'
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (hypothesis)
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 x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)
have ih₁ : (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
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (hypothesis)
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
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)
have this : ∑ 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
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (hypothesis)
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)
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (hypothesis)
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
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)
have h₁ : 1 ≤ tl.length
Tactic: have h₁ : 1 ≤ tl.length := List.length_pos_iff.mpr h'
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
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
⊢ (p - 1) * (∑ x ∈ range tl.length, ofDigits p (List.drop x tl) + ofDigits p []) =
    hd + p * ofDigits p tl - (hd + tl.sum)
have inl : (p - 1) * ofDigits p tl + ofDigits p tl - tl.sum = 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
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
⊢ (p - 1) * ofDigits p tl + ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)
have inl : (p - 1) * ofDigits p tl + 1 * ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)
Tactic: nth_rw 2 [← one_mul <| ofDigits p tl]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
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
⊢ (p - 1) * ofDigits p tl + 1 * ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)
have inl : (p - 1 + 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
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)
⊢ (p - 1) * ofDigits p tl + 1 * ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)
have inl₁ : p * 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
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)
⊢ (p - 1) * ofDigits p tl + 1 * ofDigits p tl - tl.sum = hd + p * ofDigits p tl - (hd + tl.sum)
have inl₂ : p * ofDigits p tl - tl.sum = p * ofDigits p tl - tl.sum
Tactic: rw [← add_mul, Nat.sub_add_cancel (one_le_of_lt h), Nat.add_sub_add_left]
-- 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
h : 1 < p
⊢ (p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum
have inl : ∀ {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: induction L with
    | nil => simp [ofDigits]
    | cons hd tl ih =>
      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)]
      simp only [ofDigits]
      rw [sum_range_succ, Nat.cast_id]
      simp only [List.drop, List.drop_length]
      obtain rfl | h' := em <| tl = []
      · simp [ofDigits]
      · have w₁' := fun l hl ↦ h_lt l <| List.mem_cons_of_mem hd hl
        have w₂' := fun (h : tl ≠ []) ↦ (List.getLast_cons h) ▸ h_ne_zero
        have ih := ih (w₂' h') w₁'
        simp only [self_div_pow_eq_ofDigits_drop _ _ h, digits_ofDigits p h tl w₁' w₂',
          ← Nat.one_add] at ih
        have := sum_singleton (fun x ↦ ofDigits p <| tl.drop x) tl.length
        rw [← Ico_succ_singleton, List.drop_length, ofDigits] at this
        have h₁ : 1 ≤ tl.length := List.length_pos_iff.mpr h'
        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]
        nth_rw 2 [← one_mul <| ofDigits p tl]
        rw [← add_mul, Nat.sub_add_cancel (one_le_of_lt h), Nat.add_sub_add_left]
Cleared hypotheses: L, h_nonempty, h_ne_zero, 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
h : 1 < p
inl :
  ∀ {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 []
⊢ (p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum
have inl₁ : ∀ (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
Tactic: induction L with
    | nil => simp [ofDigits]
    | cons hd tl ih =>
      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)]
      simp only [ofDigits]
      rw [sum_range_succ, Nat.cast_id]
      simp only [List.drop, List.drop_length]
      obtain rfl | h' := em <| tl = []
      · simp [ofDigits]
      · have w₁' := fun l hl ↦ h_lt l <| List.mem_cons_of_mem hd hl
        have w₂' := fun (h : tl ≠ []) ↦ (List.getLast_cons h) ▸ h_ne_zero
        have ih := ih (w₂' h') w₁'
        simp only [self_div_pow_eq_ofDigits_drop _ _ h, digits_ofDigits p h tl w₁' w₂',
          ← Nat.one_add] at ih
        have := sum_singleton (fun x ↦ ofDigits p <| tl.drop x) tl.length
        rw [← Ico_succ_singleton, List.drop_length, ofDigits] at this
        have h₁ : 1 ≤ tl.length := List.length_pos_iff.mpr h'
        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]
        nth_rw 2 [← one_mul <| ofDigits p tl]
        rw [← add_mul, Nat.sub_add_cancel (one_le_of_lt h), Nat.add_sub_add_left]
Cleared hypotheses: L, h_nonempty, h_ne_zero, 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
h : p < 1
⊢ (p - 1) * ∑ i ∈ range L.length, ofDigits p L / p ^ i.succ = ofDigits p L - L.sum
have inr : 0 = ofDigits 0 L - L.sum
Tactic: simp [lt_one_iff.mp h]
-- 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
h : p < 1
⊢ 0 = ofDigits 0 L - L.sum
have inr : ∀ {h_nonempty : Ne (α := List ℕ) [] []} (h_ne_zero : List.getLast [] h_nonempty ≠ 0)
  (h_lt : ∀ (l : ℕ), Membership.mem (γ := List ℕ) [] l → l < p), 0 = HSub.hSub (α := ℕ) (ofDigits 0 []) (List.sum [])
Tactic: cases L
Cleared hypotheses: L, h_nonempty, h_ne_zero, 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
h : p < 1
inr :
  ∀ {h_nonempty : Ne (α := List ℕ) [] []} (h_ne_zero : List.getLast [] h_nonempty ≠ 0)
    (h_lt : ∀ (l : ℕ), Membership.mem (γ := List ℕ) [] l → l < p), 0 = HSub.hSub (α := ℕ) (ofDigits 0 []) (List.sum [])
⊢ 0 = ofDigits 0 L - L.sum
have inr₁ : ∀ (head : ℕ) (tail : List ℕ) {h_nonempty : head :: tail ≠ []} (h_ne_zero : (head :: tail).getLast h_nonempty ≠ 0)
  (h_lt : ∀ l ∈ head :: tail, l < p), 0 = ofDigits 0 (head :: tail) - (head :: tail).sum
Tactic: cases L
Cleared hypotheses: L, h_nonempty, h_ne_zero, h_lt
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
p n : ℕ
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum
have inl : ∀ (h : 1 < p), (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).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 n : ℕ
inl : ∀ (h : 1 < p), (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum
have inr : HSub.hSub (α := ℕ) 1 1 * ∑ i ∈ range (log 1 n).succ, n / HPow.hPow (α := ℕ) 1 i.succ = n - (digits 1 n).sum
Tactic: obtain h | rfl | h : 1 < p ∨ 1 = p ∨ p < 1 := trichotomous 1 p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
p n : ℕ
inl : ∀ (h : 1 < p), (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum
inr : HSub.hSub (α := ℕ) 1 1 * ∑ i ∈ range (log 1 n).succ, n / HPow.hPow (α := ℕ) 1 i.succ = n - (digits 1 n).sum
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum
have inr₁ : ∀ (h : p < 1), (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).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 n : ℕ
h : 1 < p
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum
have inl : (p - 1) * ∑ i ∈ range (log p 0).succ, 0 / p ^ i.succ = 0 - (p.digits 0).sum
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
p n : ℕ
h : 1 < p
inl : (p - 1) * ∑ i ∈ range (log p 0).succ, 0 / p ^ i.succ = 0 - (p.digits 0).sum
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum
have inl₁ : ∀ (hn : n ≠ 0), (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum
have h₁ : (log p n).succ = (p.digits n).length
Tactic: convert!
      sub_one_mul_sum_div_pow_eq_sub_sum_digits (p.digits n) (getLast_digit_ne_zero p hn) <|
        (fun l a ↦ digits_lt_base h a)
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
p n : ℕ
h : 1 < p
hn : n ≠ 0
h₁ : (log p n).succ = (p.digits n).length
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum
have h₂ : ∀ x ∈ range (p.digits n).length, n = ofDigits p (p.digits n)
Tactic: convert!
      sub_one_mul_sum_div_pow_eq_sub_sum_digits (p.digits n) (getLast_digit_ne_zero p hn) <|
        (fun l a ↦ digits_lt_base h a)
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
p n : ℕ
h : 1 < p
hn : n ≠ 0
h₁ : (log p n).succ = (p.digits n).length
h₂ : ∀ x ∈ range (p.digits n).length, n = ofDigits p (p.digits n)
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum
have h₃ : n = ofDigits p (p.digits n)
Tactic: convert!
      sub_one_mul_sum_div_pow_eq_sub_sum_digits (p.digits n) (getLast_digit_ne_zero p hn) <|
        (fun l a ↦ digits_lt_base h a)
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
p n : ℕ
h : p < 1
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum
have inr : 0 = n - (digits 0 n).sum
Tactic: simp [lt_one_iff.mp h]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
p n : ℕ
h : p < 1
⊢ 0 = n - (digits 0 n).sum
have inr : 0 = 0 - (digits 0 0).sum
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
p n : ℕ
h : p < 1
inr : 0 = 0 - (digits 0 0).sum
⊢ 0 = n - (digits 0 n).sum
have inr₁ : ∀ (n : ℕ), 0 = n + 1 - (digits 0 (n + 1)).sum
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : Bool
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun (b : Bool) ↦ bif b then 1 else 0) n.bits
⊢ digits 2 (bit b n) = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (bit b n).bits
have bit : digits 2 (bit b n) = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (b :: n.bits)
Tactic: rw [bits_append_bit _ _ fun hn => absurd hn h]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : Bool
n : ℕ
h : n ≠ 0
ih : digits 2 n = List.map (fun (b : Bool) ↦ bif b then 1 else 0) n.bits
⊢ digits 2 (bit b n) = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (b :: n.bits)
have bit : digits 2 (bit false n) = List.map (fun (b : Bool) ↦ bif b then 1 else 0) (false :: n.bits)
Tactic: cases b
Cleared hypotheses: b