awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Digits.Defs
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
cons : (↑hd : ℕ) + (b + 2) * ofDigits (b + 2) tl < (b + 2) ^ tl.length * (b + 2)
⊢ ofDigits (b + 2) (hd :: tl) < (b + 2) ^ (hd :: tl).length

Tactic:
rw [ofDigits, List.length_cons, pow_succ]

Premises used: List.length_cons, pow_succ, Nat.ofDigits
-- Module: Mathlib.Data.Nat.Digits.Defs
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
⊢ b + 2 ≤ b + 2

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Digits.Defs
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
⊢ 0 ≤ b + 2

Tactic:
simp only [zero_le]

Premises used: Nat.zero_le
-- Module: Mathlib.Data.Nat.Digits.Defs
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) 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 _)
-- Module: Mathlib.Data.Nat.Digits.Defs
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
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
⊢ (↑hd : ℕ) + (b + 2) * ofDigits (b + 2) tl < (b + 2) ^ tl.length * (b + 2)

Tactic:
linarith
-- Module: Mathlib.Data.Nat.Digits.Defs
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)
cons : hd < b + 2
⊢ (↑hd : ℕ) + (b + 2) * ofDigits (b + 2) tl < (b + 2) ^ tl.length * (b + 2)

Tactic:
suffices ↑hd < b + 2 by linarith
-- Module: Mathlib.Data.Nat.Digits.Defs
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

Tactic:
hl hd List.mem_cons_self

Premises used: List.mem_cons_self
-- Module: Mathlib.Data.Nat.Digits.Defs
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

Tactic:
exact hl hd List.mem_cons_self

Premises used: List.mem_cons_self
-- Module: Mathlib.Data.Nat.Digits.Defs
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 (α := ℕ) []
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
⊢ ofDigits (b + 2) l < (b + 2) ^ l.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

Premises used: List.length_cons, pow_succ, Nat.ofDigits
-- Module: Mathlib.Data.Nat.Digits.Defs
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
succ₁ : ∀ (b : ℕ) (hb : 1 < b + 1 + 1) (hl : ∀ x ∈ l, x < b + 1 + 1), ofDigits (b + 1 + 1) l < (b + 1 + 1) ^ l.length
⊢ ofDigits b l < b ^ l.length

Tactic:
rcases b with (_ | _ | b)
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
l : List ℕ
hb : LT.lt (α := ℕ) 1 0
hl : ∀ x ∈ l, x < 0
⊢ ofDigits 0 l < HPow.hPow (α := ℕ) 0 l.length

Tactic:
simp_all [ofDigits_lt_base_pow_length']

Premises used: Nat.ofDigits_lt_base_pow_length'
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
l : List ℕ
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:
simp_all [ofDigits_lt_base_pow_length']

Premises used: Nat.ofDigits_lt_base_pow_length'
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
l : List ℕ
b : ℕ
hb : 1 < b + 1 + 1
hl : ∀ x ∈ l, x < b + 1 + 1
⊢ ofDigits (b + 1 + 1) l < (b + 1 + 1) ^ l.length

Tactic:
simp_all [ofDigits_lt_base_pow_length']

Premises used: Nat.ofDigits_lt_base_pow_length'
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b m : ℕ
⊢ ofDigits (b + 2) ((b + 2).digits m) < (b + 2) ^ ((b + 2).digits m).length

Tactic:
@ofDigits_lt_base_pow_length' b (digits (b + 2) m) fun _ => digits_lt_base'

Premises used: Nat.ofDigits_lt_base_pow_length', Nat.digits_lt_base'
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b m : ℕ
h : m = ofDigits (b + 2) ((b + 2).digits m)
⊢ m < (b + 2) ^ ((b + 2).digits m).length

Tactic:
convert! @ofDigits_lt_base_pow_length' b (digits (b + 2) m) fun _ => digits_lt_base'

Premises used: Nat.ofDigits_lt_base_pow_length', Nat.digits_lt_base'
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b m : ℕ
h h₁ : m = m
⊢ m = ofDigits (b + 2) ((b + 2).digits m)

Tactic:
rw [ofDigits_digits (b + 2) m]

Premises used: HAdd.hAdd, OfNat.ofNat, Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Defs
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
succ₁ : ∀ (b : ℕ) (hb : 1 < b + 1 + 1), m < (b + 1 + 1) ^ ((b + 1 + 1).digits m).length
⊢ m < b ^ (b.digits m).length

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

Tactic:
simp_all [lt_base_pow_length_digits']

Premises used: Nat.lt_base_pow_length_digits'
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
m : ℕ
hb : 1 < HAdd.hAdd (α := ℕ) 0 1
⊢ m < HAdd.hAdd (α := ℕ) 0 1 ^ ((HAdd.hAdd (α := ℕ) 0 1).digits m).length

Tactic:
simp_all [lt_base_pow_length_digits']

Premises used: Nat.lt_base_pow_length_digits'
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
m b : ℕ
hb : 1 < b + 1 + 1
⊢ m < (b + 1 + 1) ^ ((b + 1 + 1).digits m).length

Tactic:
simp_all [lt_base_pow_length_digits']

Premises used: Nat.lt_base_pow_length_digits'
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b m : ℕ
hb : 1 < b
hm : 0 < m
⊢ 0 < b * m

Tactic:
positivity
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b m : ℕ
hb : 1 < b
hm : 0 < m
rw : b * m % b :: b.digits (b * m / b) = 0 :: b.digits m
⊢ b.digits (b * m) = 0 :: b.digits m

Tactic:
rw [digits_def' hb (by positivity)]

Premises used: Nat.digits_def'
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b m : ℕ
hb : 1 < b
hm : 0 < m
⊢ 0 < b

Tactic:
positivity
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b m : ℕ
hb : 1 < b
hm : 0 < m
⊢ b * m % b :: b.digits (b * m / b) = 0 :: b.digits m

Tactic:
simp [mul_div_right m (by positivity)]

Premises used: Nat.mul_div_right
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
hb : 1 < b
m : ℕ
hm : 0 < m
⊢ b.digits (HPow.hPow (β := ℕ) b 0 * m) = List.replicate 0 0 ++ b.digits m

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Defs
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
⊢ 0 < b ^ k * m

Tactic:
positivity
-- Module: Mathlib.Data.Nat.Digits.Defs
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
succ₅ 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

Tactic:
rw [pow_succ', mul_assoc, digits_base_mul hb (by positivity), ih hm, List.replicate_succ,
      List.cons_append]

Premises used: Nat.pow_succ', mul_assoc, List.replicate_succ, Nat.digits_base_mul, List.cons_append
-- Module: Mathlib.Data.Nat.Digits.Defs
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
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
⊢ b.digits (b ^ k * m) = List.replicate k 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]

Premises used: Nat.pow_succ', mul_assoc, List.replicate_succ, Nat.digits_base_mul, Nat.zero, Nat.succ, List.cons_append
-- Module: Mathlib.Data.Nat.Digits.Defs
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
rw₂ rw₃ : n + b ^ (b.digits n).length * m = n + b ^ (b.digits n).length * m
⊢ ofDigits b (b.digits n ++ b.digits m) = n + b ^ (b.digits n).length * m

Tactic:
rw [ofDigits_append, ofDigits_digits, ofDigits_digits]

Premises used: Nat.ofDigits_append, Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
p q : ℕ
h : p ≤ q
⊢ ofDigits p [] ≤ ofDigits p []

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
p q : ℕ
h : p ≤ q
head : ℕ
tail : List ℕ
hi : ofDigits p tail ≤ ofDigits q tail
cons : p * ofDigits p tail ≤ q * ofDigits q tail
⊢ ofDigits p (head :: tail) ≤ ofDigits q (head :: tail)

Tactic:
simp only [ofDigits, cast_id, add_le_add_iff_left]

Premises used: Nat.cast_id, Nat.ofDigits, add_le_add_iff_left
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
p q : ℕ
h : p ≤ q
head : ℕ
tail : List ℕ
hi : ofDigits p tail ≤ ofDigits q tail
⊢ p * ofDigits p tail ≤ q * ofDigits q tail

Tactic:
Nat.mul_le_mul h hi

Premises used: Nat.mul_le_mul
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
p q : ℕ
h : p ≤ q
head : ℕ
tail : List ℕ
hi : ofDigits p tail ≤ ofDigits q tail
⊢ p * ofDigits p tail ≤ q * ofDigits q tail

Tactic:
exact Nat.mul_le_mul h hi

Premises used: Nat.mul_le_mul
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
p q : ℕ
L : List ℕ
h : p ≤ q
nil : ofDigits p [] ≤ ofDigits p []
cons :
  ∀ (head : ℕ) (tail : List ℕ) (hi : ofDigits p tail ≤ ofDigits q tail),
    ofDigits p (head :: tail) ≤ ofDigits q (head :: tail)
⊢ ofDigits p L ≤ ofDigits q L

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

Premises used: Nat.cast_id, Nat.ofDigits, add_le_add_iff_left
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
p : ℕ
L : List ℕ
h : 1 ≤ p
⊢ L.sum ≤ ofDigits p L

Tactic:
(ofDigits_one L).symm ▸ ofDigits_monotone L h

Premises used: Nat.ofDigits_one, Eq.rec, Nat.ofDigits_monotone, Eq.symm
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
p : ℕ
⊢ (p.digits 0).sum ≤ 0

Tactic:
digits_zero _ ▸ Nat.le_refl (List.sum [])

Premises used: Nat.le_refl, List.sum, Eq.rec, Nat.digits_zero, Eq.symm, List.nil
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
p : ℕ
⊢ (p.digits 0).sum ≤ 0

Tactic:
exact digits_zero _ ▸ Nat.le_refl (List.sum [])
-- Module: Mathlib.Data.Nat.Digits.Defs
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
succ₃ succ₄ : n + 1 ≤ n + 1
⊢ (digits 0 (n + 1)).sum ≤ n + 1

Tactic:
rw [digits_zero_succ, List.sum_cons, List.sum_nil, add_zero]

Premises used: List.sum_nil, Nat.digits_zero_succ, List.sum_cons, add_zero
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n p : ℕ
h : (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
h_1 : ((p + 1).digits n).sum ≤ n
succ : ((p + 1).digits (n + 1)).sum ≤ ofDigits p.succ (p.succ.digits (n + 1))
⊢ ((p + 1).digits (n + 1)).sum ≤ n + 1

Tactic:
nth_rw 2 [← ofDigits_digits p.succ (n + 1)]

Premises used: HAdd.hAdd, OfNat.ofNat, Nat.succ, Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n p : ℕ
h : (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
h_1 : ((p + 1).digits n).sum ≤ n
succ : ofDigits 1 (p.succ.digits n.succ) ≤ ofDigits p.succ (p.succ.digits (n + 1))
⊢ ((p + 1).digits (n + 1)).sum ≤ ofDigits p.succ (p.succ.digits (n + 1))

Tactic:
rw [← ofDigits_one <| digits p.succ n.succ]

Premises used: Nat.ofDigits_one, Nat.digits, Nat.succ
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n p : ℕ
h : (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
h_1 : ((p + 1).digits n).sum ≤ n
⊢ ofDigits 1 (p.succ.digits n.succ) ≤ ofDigits p.succ (p.succ.digits (n + 1))

Tactic:
ofDigits_monotone (digits p.succ n.succ) <| Nat.succ_pos p

Premises used: Nat.ofDigits_monotone, Nat.succ_pos, Nat.digits, Nat.succ
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n p : ℕ
h : (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
h_1 : ((p + 1).digits n).sum ≤ n
⊢ ofDigits 1 (p.succ.digits n.succ) ≤ ofDigits p.succ (p.succ.digits (n + 1))

Tactic:
exact ofDigits_monotone (digits p.succ n.succ) <| Nat.succ_pos p

Premises used: Nat.ofDigits_monotone, Nat.succ_pos, Nat.digits, Nat.succ
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
p n : ℕ
h : (p.digits n).sum ≤ n
succ : (digits 0 n).sum ≤ n → (digits 0 (n + 1)).sum ≤ n + 1
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
⊢ (p.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

Premises used: List.sum_nil, Nat.ofDigits_one, Nat.digits_zero_succ, Nat.ofDigits_monotone, HAdd.hAdd, List.sum_cons, Nat.succ_pos, Nat.zero, Nat.digits, add_zero, OfNat.ofNat, Nat.succ, Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
p n : ℕ
zero : (p.digits 0).sum ≤ 0
succ : ∀ (n : ℕ), (p.digits n).sum ≤ n → (p.digits (n + 1)).sum ≤ n + 1
⊢ (p.digits n).sum ≤ n

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

Premises used: List.sum_nil, Nat.ofDigits_one, Nat.digits_zero_succ, Nat.ofDigits_monotone, HAdd.hAdd, List.sum_cons, Nat.succ_pos, Nat.zero, Nat.digits, add_zero, OfNat.ofNat, Nat.succ, Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
p : ℕ
hpos : 0 < p
w₁ : ∀ (l : ℕ), Membership.mem (γ := List ℕ) [] l → l < p
⊢ ofDigits p [] / p = ofDigits p (List.tail [])

Tactic:
simp [ofDigits]

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

Tactic:
Eq.trans (add_mul_div_left hd _ hpos) ?_

Premises used: Nat.add_mul_div_left, Eq.trans
-- Module: Mathlib.Data.Nat.Digits.Defs
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 : hd / p + ofDigits p tl = ofDigits p (hd :: tl).tail
⊢ ofDigits p (hd :: tl) / p = ofDigits p (hd :: tl).tail

Tactic:
refine Eq.trans (add_mul_div_left hd _ hpos) ?_

Premises used: Nat.add_mul_div_left, Eq.trans
-- Module: Mathlib.Data.Nat.Digits.Defs
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
cons₂ cons₃ : ofDigits p tl = ofDigits p tl
⊢ hd / p + 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]

Premises used: List.tail_cons, zero_add, Nat.div_eq_of_lt, List.mem_cons_self
-- Module: Mathlib.Data.Nat.Digits.Defs
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 [])
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
⊢ ofDigits p digits / p = ofDigits p digits.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]

Premises used: Nat.ofDigits, List.tail_cons, zero_add, Nat.div_eq_of_lt
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
⊢ ofDigits p digits / HPow.hPow (β := ℕ) p 0 = ofDigits p (List.drop 0 digits)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Defs
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)
succ₆ succ₇ : ofDigits p (List.drop (1 + i) digits) = ofDigits p (List.drop (1 + i) digits)
⊢ ofDigits p digits / p ^ (i + 1) = 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]

Premises used: List.drop_drop, Nat.pow_succ, add_comm, List.drop_one, List.drop, List.mem_of_mem_drop, Nat.ofDigits_div_eq_ofDigits_tail, Nat.div_div_eq_div_mul
-- Module: Mathlib.Data.Nat.Digits.Defs
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)
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)
⊢ ofDigits p digits / p ^ i = ofDigits p (List.drop i 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]

Premises used: List.drop_drop, Nat.pow_succ, add_comm, List.drop_one, List.drop, Nat.zero, List.mem_of_mem_drop, Nat.succ, Nat.ofDigits_div_eq_ofDigits_tail, Nat.div_div_eq_div_mul
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
p i n : ℕ
h : 2 ≤ p
⊢ ofDigits p (p.digits n) / p ^ i = ofDigits p (List.drop i (p.digits n))

Tactic:
ofDigits_div_pow_eq_ofDigits_drop i (zero_lt_of_lt h) (p.digits n)
      (fun l hl ↦ digits_lt_base h hl)

Premises used: Nat.digits_lt_base, Nat.ofDigits_div_pow_eq_ofDigits_drop, Nat.zero_lt_of_lt, Nat.digits
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
p i n : ℕ
h : 2 ≤ p
h₁ : n = ofDigits p (p.digits n)
⊢ n / p ^ i = ofDigits p (List.drop i (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)

Premises used: Nat.digits_lt_base, Nat.ofDigits_div_pow_eq_ofDigits_drop, Nat.zero_lt_of_lt, Nat.digits
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
p i n : ℕ
h : 2 ≤ p
⊢ n = ofDigits p (p.digits n)

Tactic:
(ofDigits_digits p n).symm

Premises used: Eq.symm, Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
p i n : ℕ
h : 2 ≤ p
⊢ n = ofDigits p (p.digits n)

Tactic:
exact (ofDigits_digits p n).symm

Premises used: Eq.symm, Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
p : ℕ
hpos : 0 < p
digits : List ℕ
w₁ : ∀ l ∈ digits, l < p
⊢ ofDigits p digits % HPow.hPow (β := ℕ) p 0 = ofDigits p (List.take 0 digits)

Tactic:
simp [mod_one]

Premises used: Nat.mod_one
-- Module: Mathlib.Data.Nat.Digits.Defs
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)
w₁ : ∀ (l : ℕ), Membership.mem (γ := List ℕ) [] l → l < p
⊢ ofDigits p [] % p ^ (i + 1) = ofDigits p (List.take (i + 1) [])

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Defs
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 * (ofDigits p tl % p ^ i) < p * p ^ i
⊢ ofDigits p (hd :: tl) % p ^ (i + 1) = ofDigits p (List.take (i + 1) (hd :: tl))

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]

Premises used: Nat.pow_succ', List.take_succ_cons, List.mem_cons_of_mem, Nat.add_one_pos, Nat.ofDigits_cons, Nat.mod_eq_of_lt, Nat.le_pow, Nat.add_mod, List.mem_cons_self, lt_of_lt_of_le, Nat.mul_mod_mul_left
-- Module: Mathlib.Data.Nat.Digits.Defs
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 * p ^ i - p * (ofDigits p tl % p ^ i)
⊢ hd + p * (ofDigits p tl % p ^ i) < p * p ^ i

Tactic:
apply add_lt_of_lt_sub

Premises used: Nat.add_lt_of_lt_sub
-- Module: Mathlib.Data.Nat.Digits.Defs
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
succ₁ : p ≤ p * p ^ i - p * (ofDigits p tl % p ^ i)
⊢ hd < p * p ^ i - p * (ofDigits p tl % p ^ i)

Tactic:
apply lt_of_lt_of_le (b := p)

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

Tactic:
w₁ hd List.mem_cons_self

Premises used: List.mem_cons_self