awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p n : ℕ
⊢ (p.digits n).sum ≤ n
have zero : (p.digits 0).sum ≤ 0
Tactic: induction n with
  | zero => exact digits_zero _ ▸ Nat.le_refl (List.sum [])
  | succ n =>
    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: n
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p n : ℕ
zero : (p.digits 0).sum ≤ 0
⊢ (p.digits n).sum ≤ n
have succ : ∀ (n : ℕ), (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
Tactic: induction n with
  | zero => exact digits_zero _ ▸ Nat.le_refl (List.sum [])
  | succ n =>
    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: n
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p : ℕ
hpos : 0 < p
hd : ℕ
tl : List ℕ
tail_ih : ∀ (w₁ : ∀ l ∈ tl, l < p), ofDigits p tl / p = ofDigits p tl.tail
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ ofDigits p (hd :: tl) / p = ofDigits p (hd :: tl).tail
have cons : hd / p + ofDigits p tl = ofDigits p (hd :: tl).tail
Tactic: refine Eq.trans (add_mul_div_left hd _ hpos) ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p : ℕ
hpos : 0 < p
hd : ℕ
tl : List ℕ
tail_ih : ∀ (w₁ : ∀ l ∈ tl, l < p), ofDigits p tl / p = ofDigits p tl.tail
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ hd / p + ofDigits p tl = ofDigits p (hd :: tl).tail
have cons : 0 + ofDigits p tl = ofDigits p (hd :: tl).tail
Tactic: rw [Nat.div_eq_of_lt <| w₁ _ List.mem_cons_self, zero_add, List.tail_cons]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p : ℕ
hpos : 0 < p
hd : ℕ
tl : List ℕ
tail_ih : ∀ (w₁ : ∀ l ∈ tl, l < p), ofDigits p tl / p = ofDigits p tl.tail
w₁ : ∀ l ∈ hd :: tl, l < p
cons : 0 + ofDigits p tl = ofDigits p (hd :: tl).tail
⊢ hd / p + ofDigits p tl = ofDigits p (hd :: tl).tail
have cons₁ : ofDigits p tl = ofDigits p (hd :: tl).tail
Tactic: rw [Nat.div_eq_of_lt <| w₁ _ List.mem_cons_self, zero_add, List.tail_cons]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p : ℕ
hpos : 0 < p
hd : ℕ
tl : List ℕ
tail_ih : ∀ (w₁ : ∀ l ∈ tl, l < p), ofDigits p tl / p = ofDigits p tl.tail
w₁ : ∀ l ∈ hd :: tl, l < p
cons : 0 + ofDigits p tl = ofDigits p (hd :: tl).tail
cons₁ : ofDigits p tl = ofDigits p (hd :: tl).tail
⊢ hd / p + ofDigits p tl = ofDigits p (hd :: tl).tail
have cons₂ : ofDigits p tl = ofDigits p tl
Tactic: rw [Nat.div_eq_of_lt <| w₁ _ List.mem_cons_self, zero_add, List.tail_cons]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
⊢ ofDigits p digits / p = ofDigits p digits.tail
have nil : ∀ (w₁ : ∀ (l : ℕ), Membership.mem (γ := List ℕ) [] l → l < p), ofDigits p [] / p = ofDigits p (List.tail [])
Tactic: induction digits with
  | nil => simp [ofDigits]
  | cons hd tl =>
    refine Eq.trans (add_mul_div_left hd _ hpos) ?_
    rw [Nat.div_eq_of_lt <| w₁ _ List.mem_cons_self, zero_add, List.tail_cons]
Cleared hypotheses: digits, w₁
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
nil : ∀ (w₁ : ∀ (l : ℕ), Membership.mem (γ := List ℕ) [] l → l < p), ofDigits p [] / p = ofDigits p (List.tail [])
⊢ ofDigits p digits / p = ofDigits p digits.tail
have cons : ∀ (hd : ℕ) (tl : List ℕ),
  (∀ (w₁ : ∀ l ∈ tl, l < p), ofDigits p tl / p = ofDigits p tl.tail) →
    ∀ (w₁ : ∀ l ∈ hd :: tl, l < p), ofDigits p (hd :: tl) / p = ofDigits p (hd :: tl).tail
Tactic: induction digits with
  | nil => simp [ofDigits]
  | cons hd tl =>
    refine Eq.trans (add_mul_div_left hd _ hpos) ?_
    rw [Nat.div_eq_of_lt <| w₁ _ List.mem_cons_self, zero_add, List.tail_cons]
Cleared hypotheses: digits, w₁
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
i : ℕ
hi : ofDigits p digits / p ^ i = ofDigits p (List.drop i digits)
⊢ ofDigits p digits / p ^ (i + 1) = ofDigits p (List.drop (i + 1) digits)
have succ : ofDigits p digits / (p ^ i * p) = ofDigits p (List.drop (i + 1) digits)
Tactic: rw [Nat.pow_succ, ← Nat.div_div_eq_div_mul, hi, ofDigits_div_eq_ofDigits_tail hpos
      (List.drop i digits) fun x hx ↦ w₁ x <| List.mem_of_mem_drop hx, ← List.drop_one,
      List.drop_drop, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
i : ℕ
hi : ofDigits p digits / p ^ i = ofDigits p (List.drop i digits)
succ : ofDigits p digits / (p ^ i * p) = ofDigits p (List.drop (i + 1) digits)
⊢ ofDigits p digits / p ^ (i + 1) = ofDigits p (List.drop (i + 1) digits)
have succ₁ : ofDigits p digits / p ^ i / p = ofDigits p (List.drop (i + 1) digits)
Tactic: rw [Nat.pow_succ, ← Nat.div_div_eq_div_mul, hi, ofDigits_div_eq_ofDigits_tail hpos
      (List.drop i digits) fun x hx ↦ w₁ x <| List.mem_of_mem_drop hx, ← List.drop_one,
      List.drop_drop, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
i : ℕ
hi : ofDigits p digits / p ^ i = ofDigits p (List.drop i digits)
succ : ofDigits p digits / (p ^ i * p) = ofDigits p (List.drop (i + 1) digits)
succ₁ : ofDigits p digits / p ^ i / p = ofDigits p (List.drop (i + 1) digits)
⊢ ofDigits p digits / p ^ (i + 1) = ofDigits p (List.drop (i + 1) digits)
have succ₂ : ofDigits p (List.drop i digits) / p = ofDigits p (List.drop (i + 1) digits)
Tactic: rw [Nat.pow_succ, ← Nat.div_div_eq_div_mul, hi, ofDigits_div_eq_ofDigits_tail hpos
      (List.drop i digits) fun x hx ↦ w₁ x <| List.mem_of_mem_drop hx, ← List.drop_one,
      List.drop_drop, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
i : ℕ
hi : ofDigits p digits / p ^ i = ofDigits p (List.drop i digits)
succ : ofDigits p digits / (p ^ i * p) = ofDigits p (List.drop (i + 1) digits)
succ₁ : ofDigits p digits / p ^ i / p = ofDigits p (List.drop (i + 1) digits)
succ₂ : ofDigits p (List.drop i digits) / p = ofDigits p (List.drop (i + 1) digits)
⊢ ofDigits p digits / p ^ (i + 1) = ofDigits p (List.drop (i + 1) digits)
have succ₃ : ofDigits p (List.drop i digits).tail = ofDigits p (List.drop (i + 1) digits)
Tactic: rw [Nat.pow_succ, ← Nat.div_div_eq_div_mul, hi, ofDigits_div_eq_ofDigits_tail hpos
      (List.drop i digits) fun x hx ↦ w₁ x <| List.mem_of_mem_drop hx, ← List.drop_one,
      List.drop_drop, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
i : ℕ
hi : ofDigits p digits / p ^ i = ofDigits p (List.drop i digits)
succ : ofDigits p digits / (p ^ i * p) = ofDigits p (List.drop (i + 1) digits)
succ₁ : ofDigits p digits / p ^ i / p = ofDigits p (List.drop (i + 1) digits)
succ₂ : ofDigits p (List.drop i digits) / p = ofDigits p (List.drop (i + 1) digits)
succ₃ : ofDigits p (List.drop i digits).tail = ofDigits p (List.drop (i + 1) digits)
⊢ ofDigits p digits / p ^ (i + 1) = ofDigits p (List.drop (i + 1) digits)
have succ₄ : ofDigits p (List.drop 1 (List.drop i digits)) = ofDigits p (List.drop (i + 1) digits)
Tactic: rw [Nat.pow_succ, ← Nat.div_div_eq_div_mul, hi, ofDigits_div_eq_ofDigits_tail hpos
      (List.drop i digits) fun x hx ↦ w₁ x <| List.mem_of_mem_drop hx, ← List.drop_one,
      List.drop_drop, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
i : ℕ
hi : ofDigits p digits / p ^ i = ofDigits p (List.drop i digits)
succ : ofDigits p digits / (p ^ i * p) = ofDigits p (List.drop (i + 1) digits)
succ₁ : ofDigits p digits / p ^ i / p = ofDigits p (List.drop (i + 1) digits)
succ₂ : ofDigits p (List.drop i digits) / p = ofDigits p (List.drop (i + 1) digits)
succ₃ : ofDigits p (List.drop i digits).tail = ofDigits p (List.drop (i + 1) digits)
succ₄ : ofDigits p (List.drop 1 (List.drop i digits)) = ofDigits p (List.drop (i + 1) digits)
⊢ ofDigits p digits / p ^ (i + 1) = ofDigits p (List.drop (i + 1) digits)
have succ₅ : ofDigits p (List.drop (i + 1) digits) = ofDigits p (List.drop (i + 1) digits)
Tactic: rw [Nat.pow_succ, ← Nat.div_div_eq_div_mul, hi, ofDigits_div_eq_ofDigits_tail hpos
      (List.drop i digits) fun x hx ↦ w₁ x <| List.mem_of_mem_drop hx, ← List.drop_one,
      List.drop_drop, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
i : ℕ
hi : ofDigits p digits / p ^ i = ofDigits p (List.drop i digits)
succ : ofDigits p digits / (p ^ i * p) = ofDigits p (List.drop (i + 1) digits)
succ₁ : ofDigits p digits / p ^ i / p = ofDigits p (List.drop (i + 1) digits)
succ₂ : ofDigits p (List.drop i digits) / p = ofDigits p (List.drop (i + 1) digits)
succ₃ : ofDigits p (List.drop i digits).tail = ofDigits p (List.drop (i + 1) digits)
succ₄ : ofDigits p (List.drop 1 (List.drop i digits)) = ofDigits p (List.drop (i + 1) digits)
succ₅ : ofDigits p (List.drop (i + 1) digits) = ofDigits p (List.drop (i + 1) digits)
⊢ ofDigits p digits / p ^ (i + 1) = ofDigits p (List.drop (i + 1) digits)
have succ₆ : ofDigits p (List.drop (1 + i) digits) = ofDigits p (List.drop (1 + i) digits)
Tactic: rw [Nat.pow_succ, ← Nat.div_div_eq_div_mul, hi, ofDigits_div_eq_ofDigits_tail hpos
      (List.drop i digits) fun x hx ↦ w₁ x <| List.mem_of_mem_drop hx, ← List.drop_one,
      List.drop_drop, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p i : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
⊢ ofDigits p digits / p ^ i = ofDigits p (List.drop i digits)
have zero : ofDigits p digits / HPow.hPow (β := ℕ) p 0 = ofDigits p (List.drop 0 digits)
Tactic: induction i with
  | zero => simp
  | succ i hi =>
    rw [Nat.pow_succ, ← Nat.div_div_eq_div_mul, hi, ofDigits_div_eq_ofDigits_tail hpos
      (List.drop i digits) fun x hx ↦ w₁ x <| List.mem_of_mem_drop hx, ← List.drop_one,
      List.drop_drop, add_comm]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p i : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
zero : ofDigits p digits / HPow.hPow (β := ℕ) p 0 = ofDigits p (List.drop 0 digits)
⊢ ofDigits p digits / p ^ i = ofDigits p (List.drop i digits)
have succ : ∀ (i : ℕ) (hi : ofDigits p digits / p ^ i = ofDigits p (List.drop i digits)),
  ofDigits p digits / p ^ (i + 1) = ofDigits p (List.drop (i + 1) digits)
Tactic: induction i with
  | zero => simp
  | succ i hi =>
    rw [Nat.pow_succ, ← Nat.div_div_eq_div_mul, hi, ofDigits_div_eq_ofDigits_tail hpos
      (List.drop i digits) fun x hx ↦ w₁ x <| List.mem_of_mem_drop hx, ← List.drop_one,
      List.drop_drop, add_comm]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p i n : ℕ
h : 2 ≤ p
⊢ n / p ^ i = ofDigits p (List.drop i (p.digits n))
have h₁ : n = ofDigits p (p.digits n)
Tactic: convert!
    ofDigits_div_pow_eq_ofDigits_drop i (zero_lt_of_lt h) (p.digits n)
      (fun l hl ↦ digits_lt_base h hl)
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ) (w₁ : ∀ l ∈ digits, l < p), ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ ofDigits p (hd :: tl) % p ^ (i + 1) = ofDigits p (List.take (i + 1) (hd :: tl))
have succ : hd + p * (ofDigits p tl % p ^ i) < p * p ^ i
Tactic: rw [List.take_succ_cons, ofDigits_cons, ofDigits_cons,
        ← ih _ fun x hx ↦ w₁ x <| List.mem_cons_of_mem hd hx, add_mod,
        mod_eq_of_lt <| lt_of_lt_of_le (w₁ hd List.mem_cons_self) (le_pow <| add_one_pos i),
        pow_succ', mul_mod_mul_left, mod_eq_of_lt]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ) (w₁ : ∀ l ∈ digits, l < p), ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ hd + p * (ofDigits p tl % p ^ i) < p * p ^ i
have succ : hd < p * p ^ i - p * (ofDigits p tl % p ^ i)
Tactic: apply add_lt_of_lt_sub
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ) (w₁ : ∀ l ∈ digits, l < p), ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ hd < p * p ^ i - p * (ofDigits p tl % p ^ i)
have succ : hd < p
Tactic: apply lt_of_lt_of_le (b := p)
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ) (w₁ : ∀ l ∈ digits, l < p), ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
succ : hd < p
⊢ hd < p * p ^ i - p * (ofDigits p tl % p ^ i)
have succ₁ : p ≤ p * p ^ i - p * (ofDigits p tl % p ^ i)
Tactic: apply lt_of_lt_of_le (b := p)
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ) (w₁ : ∀ l ∈ digits, l < p), ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
hd : ℕ
tl : List ℕ
w₁ : ∀ l ∈ hd :: tl, l < p
⊢ p ≤ p * p ^ i - p * (ofDigits p tl % p ^ i)
have succ : p ≤ p * (p ^ i - ofDigits p tl % p ^ i)
Tactic: rw [← Nat.mul_sub]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ) (w₁ : ∀ l ∈ digits, l < p), ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
⊢ ofDigits p digits % p ^ (i + 1) = ofDigits p (List.take (i + 1) digits)
have succ : ∀ (w₁ : ∀ (l : ℕ), Membership.mem (γ := List ℕ) [] l → l < p),
  ofDigits p [] % p ^ (i + 1) = ofDigits p (List.take (i + 1) [])
Tactic: cases digits with
    | nil => simp
    | cons hd tl =>
      rw [List.take_succ_cons, ofDigits_cons, ofDigits_cons,
        ← ih _ fun x hx ↦ w₁ x <| List.mem_cons_of_mem hd hx, add_mod,
        mod_eq_of_lt <| lt_of_lt_of_le (w₁ hd List.mem_cons_self) (le_pow <| add_one_pos i),
        pow_succ', mul_mod_mul_left, mod_eq_of_lt]
      apply add_lt_of_lt_sub
      apply lt_of_lt_of_le (b := p)
      · exact w₁ hd List.mem_cons_self
      · rw [← Nat.mul_sub]
        exact Nat.le_mul_of_pos_right _ <| Nat.sub_pos_of_lt <| mod_lt _ <| pow_pos hpos i
Cleared hypotheses: digits, w₁
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p : ℕ
hpos : 0 < p
i : ℕ
ih : ∀ (digits : List ℕ) (w₁ : ∀ l ∈ digits, l < p), ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
succ :
  ∀ (w₁ : ∀ (l : ℕ), Membership.mem (γ := List ℕ) [] l → l < p),
    ofDigits p [] % p ^ (i + 1) = ofDigits p (List.take (i + 1) [])
⊢ ofDigits p digits % p ^ (i + 1) = ofDigits p (List.take (i + 1) digits)
have succ₁ : ∀ (hd : ℕ) (tl : List ℕ) (w₁ : ∀ l ∈ hd :: tl, l < p),
  ofDigits p (hd :: tl) % p ^ (i + 1) = ofDigits p (List.take (i + 1) (hd :: tl))
Tactic: cases digits with
    | nil => simp
    | cons hd tl =>
      rw [List.take_succ_cons, ofDigits_cons, ofDigits_cons,
        ← ih _ fun x hx ↦ w₁ x <| List.mem_cons_of_mem hd hx, add_mod,
        mod_eq_of_lt <| lt_of_lt_of_le (w₁ hd List.mem_cons_self) (le_pow <| add_one_pos i),
        pow_succ', mul_mod_mul_left, mod_eq_of_lt]
      apply add_lt_of_lt_sub
      apply lt_of_lt_of_le (b := p)
      · exact w₁ hd List.mem_cons_self
      · rw [← Nat.mul_sub]
        exact Nat.le_mul_of_pos_right _ <| Nat.sub_pos_of_lt <| mod_lt _ <| pow_pos hpos i
Cleared hypotheses: digits, w₁
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p i : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
⊢ ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
have zero : ∀ (digits : List ℕ) (w₁ : ∀ l ∈ digits, l < p),
  ofDigits p digits % HPow.hPow (β := ℕ) p 0 = ofDigits p (List.take 0 digits)
Tactic: induction i generalizing digits with
  | zero => simp [mod_one]
  | succ i ih =>
    cases digits with
    | nil => simp
    | cons hd tl =>
      rw [List.take_succ_cons, ofDigits_cons, ofDigits_cons,
        ← ih _ fun x hx ↦ w₁ x <| List.mem_cons_of_mem hd hx, add_mod,
        mod_eq_of_lt <| lt_of_lt_of_le (w₁ hd List.mem_cons_self) (le_pow <| add_one_pos i),
        pow_succ', mul_mod_mul_left, mod_eq_of_lt]
      apply add_lt_of_lt_sub
      apply lt_of_lt_of_le (b := p)
      · exact w₁ hd List.mem_cons_self
      · rw [← Nat.mul_sub]
        exact Nat.le_mul_of_pos_right _ <| Nat.sub_pos_of_lt <| mod_lt _ <| pow_pos hpos i
Cleared hypotheses: i, digits, w₁
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p i : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
zero :
  ∀ (digits : List ℕ) (w₁ : ∀ l ∈ digits, l < p),
    ofDigits p digits % HPow.hPow (β := ℕ) p 0 = ofDigits p (List.take 0 digits)
⊢ ofDigits p digits % p ^ i = ofDigits p (List.take i digits)
have succ : ∀ (i : ℕ)
  (ih : ∀ (digits : List ℕ) (w₁ : ∀ l ∈ digits, l < p), ofDigits p digits % p ^ i = ofDigits p (List.take i digits))
  (digits : List ℕ) (w₁ : ∀ l ∈ digits, l < p), ofDigits p digits % p ^ (i + 1) = ofDigits p (List.take (i + 1) digits)
Tactic: induction i generalizing digits with
  | zero => simp [mod_one]
  | succ i ih =>
    cases digits with
    | nil => simp
    | cons hd tl =>
      rw [List.take_succ_cons, ofDigits_cons, ofDigits_cons,
        ← ih _ fun x hx ↦ w₁ x <| List.mem_cons_of_mem hd hx, add_mod,
        mod_eq_of_lt <| lt_of_lt_of_le (w₁ hd List.mem_cons_self) (le_pow <| add_one_pos i),
        pow_succ', mul_mod_mul_left, mod_eq_of_lt]
      apply add_lt_of_lt_sub
      apply lt_of_lt_of_le (b := p)
      · exact w₁ hd List.mem_cons_self
      · rw [← Nat.mul_sub]
        exact Nat.le_mul_of_pos_right _ <| Nat.sub_pos_of_lt <| mod_lt _ <| pow_pos hpos i
Cleared hypotheses: i, digits, w₁
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
p i n : ℕ
h : 2 ≤ p
⊢ n % p ^ i = ofDigits p (List.take i (p.digits n))
have h₁ : n = ofDigits p (p.digits n)
Tactic: convert!
    ofDigits_mod_pow_eq_ofDigits_take i (zero_lt_of_lt h) (p.digits n)
      (fun l hl ↦ digits_lt_base h hl)
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
n : ℕ
l1 l2 : List Char
hlen : l1.length = l2.length
hx : ¬n / b = 0
⊢ (if n / b = 0 then (n % b).digitChar :: l1 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
    (if n / b = 0 then (n % b).digitChar :: l2 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
have simp : (b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
  (b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
Tactic: simp only [hx, if_false]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (hypothesis)
Goal:
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
n : ℕ
l1 l2 : List Char
hlen : l1.length = l2.length
hx : ¬n / b = 0
⊢ (b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
    (b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
have ih₁ : ((n % b).digitChar :: l1).length = ((n % b).digitChar :: l2).length →
  (b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
    (b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
Tactic: specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2)
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (hypothesis)
Goal:
b f n : ℕ
l1 l2 : List Char
hlen : l1.length = l2.length
hx : ¬n / b = 0
ih :
  ((n % b).digitChar :: l1).length = ((n % b).digitChar :: l2).length →
    (b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
      (b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
⊢ (b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
    (b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
have ih₁ : True →
  (b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
    (b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
Tactic: simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
n : ℕ
l1 l2 : List Char
hlen : l1.length = l2.length
⊢ (if n / b = 0 then (n % b).digitChar :: l1 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
    (if n / b = 0 then (n % b).digitChar :: l2 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
have if : ∀ (hx : n / b = 0),
  (if n / b = 0 then (n % b).digitChar :: l1 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
    (if n / b = 0 then (n % b).digitChar :: l2 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
Tactic: if hx : n / b = 0 then
      simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]
    else
      simp only [hx, if_false]
      specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2)
      simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih
      exact ih trivial
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b f : ℕ
ih :
  ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
n : ℕ
l1 l2 : List Char
hlen : l1.length = l2.length
if :
  ∀ (hx : n / b = 0),
    (if n / b = 0 then (n % b).digitChar :: l1 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
      (if n / b = 0 then (n % b).digitChar :: l2 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
⊢ (if n / b = 0 then (n % b).digitChar :: l1 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
    (if n / b = 0 then (n % b).digitChar :: l2 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
have if₁ : ∀ (hx : ¬n / b = 0),
  (if n / b = 0 then (n % b).digitChar :: l1 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
    (if n / b = 0 then (n % b).digitChar :: l2 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
Tactic: if hx : n / b = 0 then
      simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]
    else
      simp only [hx, if_false]
      specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2)
      simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih
      exact ih trivial
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b f : ℕ
⊢ ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
have zero : ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore 0 n l1).length = (b.toDigitsCore 0 n l2).length
Tactic: induction f with (simp only [Nat.toDigitsCore]; intro n l1 l2 hlen)
  | zero => assumption
  | succ f ih =>
    if hx : n / b = 0 then
      simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]
    else
      simp only [hx, if_false]
      specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2)
      simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih
      exact ih trivial
Cleared hypotheses: f