awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact w₁ hd List.mem_cons_self

Premises used: List.mem_cons_self
-- 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 : p ≤ p * (p ^ i - ofDigits p tl % p ^ i)
⊢ p ≤ p * p ^ i - p * (ofDigits p tl % p ^ i)

Tactic:
rw [← Nat.mul_sub]

Premises used: Nat.mul_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
⊢ p ≤ p * (p ^ i - ofDigits p tl % p ^ i)

Tactic:
Nat.le_mul_of_pos_right _ <| Nat.sub_pos_of_lt <| mod_lt _ <| pow_pos hpos i

Premises used: pow_pos, Nat.le_mul_of_pos_right, Nat.sub_pos_of_lt, Nat.mod_lt
-- 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
⊢ p ≤ p * (p ^ i - ofDigits p tl % p ^ i)

Tactic:
exact Nat.le_mul_of_pos_right _ <| Nat.sub_pos_of_lt <| mod_lt _ <| pow_pos hpos i

Premises used: pow_pos, Nat.le_mul_of_pos_right, Nat.sub_pos_of_lt, Nat.mod_lt
-- 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)
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) [])
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))
⊢ ofDigits p digits % p ^ (i + 1) = ofDigits p (List.take (i + 1) digits)

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

Premises used: Nat.pow_succ', List.take_succ_cons, pow_pos, Nat.le_mul_of_pos_right, Nat.sub_pos_of_lt, Nat.ofDigits_cons, Nat.mod_eq_of_lt, Nat.mod_lt, Nat.add_lt_of_lt_sub, Nat.add_mod, Nat.mul_sub, lt_of_lt_of_le, Nat.mul_mod_mul_left
-- Module: Mathlib.Data.Nat.Digits.Defs
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)
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)
⊢ ofDigits p digits % p ^ i = ofDigits p (List.take i 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

Premises used: Nat.pow_succ', List.take_succ_cons, pow_pos, Nat.le_mul_of_pos_right, Nat.sub_pos_of_lt, Nat.mod_one, Nat.ofDigits_cons, Nat.mod_eq_of_lt, Nat.mod_lt, Nat.add_lt_of_lt_sub, Nat.zero, Nat.add_mod, Nat.mul_sub, Nat.succ, lt_of_lt_of_le, Nat.mul_mod_mul_left
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
p i n : ℕ
h : 2 ≤ p
⊢ ofDigits p (p.digits n) % p ^ i = ofDigits p (List.take i (p.digits n))

Tactic:
ofDigits_mod_pow_eq_ofDigits_take 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_mod_pow_eq_ofDigits_take, 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.take i (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)

Premises used: Nat.digits_lt_base, Nat.ofDigits_mod_pow_eq_ofDigits_take, Nat.zero_lt_of_lt, Nat.digits
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b n : ℕ
l1 l2 : List Char
hlen : l1.length = l2.length
⊢ l1.length = l2.length

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

Tactic:
simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]

Premises used: if_true, congrArg, HAdd.hAdd, OfNat.ofNat, List.length
-- Module: Mathlib.Data.Nat.Digits.Defs
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
simp :
  (b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
    (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

Tactic:
simp only [hx, if_false]

Premises used: if_false
-- Module: Mathlib.Data.Nat.Digits.Defs
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
⊢ ((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)

Premises used: HDiv.hDiv, Nat.digitChar, List.cons, HMod.hMod
-- Module: Mathlib.Data.Nat.Digits.Defs
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
⊢ 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

Premises used: congrArg, HAdd.hAdd, OfNat.ofNat, List.length
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b f n : ℕ
l1 l2 : List Char
hlen : l1.length = l2.length
hx : ¬n / b = 0
ih :
  True →
    (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

Tactic:
ih trivial

Premises used: trivial
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b f n : ℕ
l1 l2 : List Char
hlen : l1.length = l2.length
hx : ¬n / b = 0
ih :
  True →
    (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

Tactic:
exact ih trivial

Premises used: trivial
-- Module: Mathlib.Data.Nat.Digits.Defs
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₁ :
  ∀ (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₂ :
  ∀ (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₃ 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

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

Premises used: if_true, congrArg, if_false, HDiv.hDiv, Nat.digitChar, List.cons, HMod.hMod, HAdd.hAdd, OfNat.ofNat, List.length
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b f : ℕ
zero :
  ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore 0 n l1).length = (b.toDigitsCore 0 n l2).length
zero₁ : ∀ (n : ℕ) (l1 l2 : List Char) (hlen : l1.length = l2.length), l1.length = l2.length
succ :
  ∀ (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),
    l1.length = l2.length → (b.toDigitsCore (f + 1) n l1).length = (b.toDigitsCore (f + 1) n l2).length
succ₁ :
  ∀ (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
⊢ ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f 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

Premises used: if_true, if_false, Nat.toDigitsCore, Nat.zero, Nat.succ, List.length
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b f : ℕ
ih : ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
n : ℕ
c : Char
tl : List Char
⊢ (if n / b = 0 then (n % b).digitChar :: c :: tl else b.toDigitsCore f (n / b) ((n % b).digitChar :: c :: tl)).length =
    (if n / b = 0 then (n % b).digitChar :: tl else b.toDigitsCore f (n / b) ((n % b).digitChar :: tl)).length + 1

Tactic:
grind
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b n : ℕ
c : Char
tl : List Char
⊢ (b.toDigitsCore 0 n (c :: tl)).length = (b.toDigitsCore 0 n tl).length + 1

Tactic:
simp only [Nat.toDigitsCore, List.length]

Premises used: Nat.toDigitsCore, List.length
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b f : ℕ
succ :
  ∀ (f : ℕ)
    (ih :
      ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1)
    (n : ℕ) (c : Char) (tl : List Char),
    (b.toDigitsCore (f + 1) n (c :: tl)).length = (b.toDigitsCore (f + 1) n tl).length + 1
succ₁ :
  ∀ (f : ℕ)
    (ih :
      ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1)
    (n : ℕ) (c : Char) (tl : List Char),
    (if n / b = 0 then (n % b).digitChar :: c :: tl
        else b.toDigitsCore f (n / b) ((n % b).digitChar :: c :: tl)).length =
      (if n / b = 0 then (n % b).digitChar :: tl else b.toDigitsCore f (n / b) ((n % b).digitChar :: tl)).length + 1
zero : ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore 0 n (c :: tl)).length = (b.toDigitsCore 0 n tl).length + 1
⊢ ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1

Tactic:
induction f with (intro n c tl; simp only [Nat.toDigitsCore, List.length])
  | succ f ih =>
    grind

Premises used: Nat.toDigitsCore, Nat.succ, List.length
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n b e : ℕ
h_b_pos : 0 < b
simp : n < b ^ e * b → n / b < b ^ e
⊢ n < b ^ e.succ → n / b < b ^ e

Tactic:
simp only [Nat.pow_succ]

Premises used: Nat.pow_succ
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n b e : ℕ
h_b_pos : 0 < b
⊢ n < b ^ e * b → n / b < b ^ e

Tactic:
(@Nat.div_lt_iff_lt_mul b n (b ^ e) h_b_pos).mpr

Premises used: Iff.mpr, Nat.div_lt_iff_lt_mul
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n b e : ℕ
h_b_pos : 0 < b
⊢ n < b ^ e * b → n / b < b ^ e

Tactic:
exact (@Nat.div_lt_iff_lt_mul b n (b ^ e) h_b_pos).mpr

Premises used: Iff.mpr, Nat.div_lt_iff_lt_mul
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b n e : ℕ
h_e_pos : 0 < e
hlt : n < b ^ e
⊢ (b.toDigitsCore 0 n []).length ≤ e

Tactic:
simp only [toDigitsCore, List.length, zero_le]

Premises used: Nat.zero_le, Nat.toDigitsCore, List.length
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b f : ℕ
ih : ∀ (n e : ℕ) (h_e_pos : 0 < e) (hlt : n < b ^ e), (b.toDigitsCore f n []).length ≤ e
n : ℕ
h_e_pos : LT.lt (α := ℕ) 0 0
hlt : n < HPow.hPow (β := ℕ) b 0
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ 0

Tactic:
False.elim (Nat.lt_irrefl 0 h_e_pos)

Premises used: False.elim, Nat.lt_irrefl, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b f : ℕ
ih : ∀ (n e : ℕ) (h_e_pos : 0 < e) (hlt : n < b ^ e), (b.toDigitsCore f n []).length ≤ e
n : ℕ
h_e_pos : LT.lt (α := ℕ) 0 0
hlt : n < HPow.hPow (β := ℕ) b 0
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ 0

Tactic:
exact False.elim (Nat.lt_irrefl 0 h_e_pos)

Premises used: False.elim, Nat.lt_irrefl, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b f : ℕ
ih : ∀ (n e : ℕ) (h_e_pos : 0 < e) (hlt : n < b ^ e), (b.toDigitsCore f n []).length ≤ e
n : ℕ
h_e_pos : 0 < HAdd.hAdd (α := ℕ) 0 1
hlt : n < b ^ HAdd.hAdd (α := ℕ) 0 1
⊢ n < b

Tactic:
rw [zero_add, pow_one] at hlt

Premises used: zero_add, pow_one
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b f : ℕ
ih : ∀ (n e : ℕ) (h_e_pos : 0 < e) (hlt : n < b ^ e), (b.toDigitsCore f n []).length ≤ e
n : ℕ
h_e_pos : 0 < HAdd.hAdd (α := ℕ) 0 1
hlt : n < b
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤
    HAdd.hAdd (α := ℕ) 0 1

Tactic:
simp [Nat.div_eq_of_lt hlt]

Premises used: Nat.div_eq_of_lt
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b f : ℕ
ih : ∀ (n e : ℕ) (h_e_pos : 0 < e) (hlt : n < b ^ e), (b.toDigitsCore f n []).length ≤ e
n e : ℕ
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
rwa rwa₁ rwa₂ rwa₃ : n < b ^ (e + 1 + 1)
⊢ n < b * b ^ (e + 1)

Tactic:
rwa [← pow_add_one']

Premises used: Nat.pow_add_one'
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b f : ℕ
ih : ∀ (n e : ℕ) (h_e_pos : 0 < e) (hlt : n < b ^ e), (b.toDigitsCore f n []).length ≤ e
n e : ℕ
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
⊢ (b.toDigitsCore f (n / b) []).length ≤ e + 1

Tactic:
specialize ih (n / b) _ (add_one_pos e) (Nat.div_lt_of_lt_mul <| by rwa [← pow_add_one'])

Premises used: Nat.add_one_pos, HDiv.hDiv, Nat.div_lt_of_lt_mul
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b f n e : ℕ
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
ih : (b.toDigitsCore f (n / b) []).length ≤ e + 1
pos : n / b = 0 → [(n % b).digitChar].length ≤ e + 1 + 1
neg : ¬n / b = 0 → (b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1 + 1
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1 + 1

Tactic:
split_ifs
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b f n e : ℕ
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
ih : (b.toDigitsCore f (n / b) []).length ≤ e + 1
h : n / b = 0
⊢ [(n % b).digitChar].length ≤ e + 1 + 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b f n e : ℕ
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
ih : (b.toDigitsCore f (n / b) []).length ≤ e + 1
h : ¬n / b = 0
⊢ (b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1 + 1

Tactic:
simp only [toDigitsCore_lens_eq b f (n / b) (Nat.digitChar <| n % b),
            Nat.succ_le_succ_iff, ih]

Premises used: HDiv.hDiv, Nat.digitChar, HMod.hMod, Nat.succ_le_succ_iff, Nat.toDigitsCore_lens_eq
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b f : ℕ
ih : ∀ (n e : ℕ) (h_e_pos : 0 < e) (hlt : n < b ^ e), (b.toDigitsCore f n []).length ≤ e
n e : ℕ
h_e_pos : 0 < e + 1
hlt : n < b ^ (e + 1)
succ :
  ∀ (h_e_pos : 0 < HAdd.hAdd (α := ℕ) 0 1) (hlt : n < b ^ HAdd.hAdd (α := ℕ) 0 1),
    (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤
      HAdd.hAdd (α := ℕ) 0 1
succ₁ :
  ∀ (e : ℕ) (h_e_pos : 0 < e + 1 + 1) (hlt : n < b ^ (e + 1 + 1)),
    (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1 + 1
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1

Tactic:
cases e with
      | zero =>
        rw [zero_add, pow_one] at hlt
        simp [Nat.div_eq_of_lt hlt]
      | succ e =>
        specialize ih (n / b) _ (add_one_pos e) (Nat.div_lt_of_lt_mul <| by rwa [← pow_add_one'])
        split_ifs
        · simp
        · simp only [toDigitsCore_lens_eq b f (n / b) (Nat.digitChar <| n % b),
            Nat.succ_le_succ_iff, ih]

Premises used: Nat.add_one_pos, HDiv.hDiv, Nat.digitChar, zero_add, Nat.div_lt_of_lt_mul, HMod.hMod, Nat.succ_le_succ_iff, pow_one, Nat.zero, Nat.div_eq_of_lt, Nat.succ, Nat.toDigitsCore_lens_eq
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b f : ℕ
ih : ∀ (n e : ℕ) (h_e_pos : 0 < e) (hlt : n < b ^ e), (b.toDigitsCore f n []).length ≤ e
n e : ℕ
h_e_pos : 0 < e
hlt : n < b ^ e
succ :
  ∀ (h_e_pos : LT.lt (α := ℕ) 0 0) (hlt : n < HPow.hPow (β := ℕ) b 0),
    (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ 0
succ₁ :
  ∀ (e : ℕ) (h_e_pos : 0 < e + 1) (hlt : n < b ^ (e + 1)),
    (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e

Tactic:
cases e with
    | zero => exact False.elim (Nat.lt_irrefl 0 h_e_pos)
    | succ e =>
      cases e with
      | zero =>
        rw [zero_add, pow_one] at hlt
        simp [Nat.div_eq_of_lt hlt]
      | succ e =>
        specialize ih (n / b) _ (add_one_pos e) (Nat.div_lt_of_lt_mul <| by rwa [← pow_add_one'])
        split_ifs
        · simp
        · simp only [toDigitsCore_lens_eq b f (n / b) (Nat.digitChar <| n % b),
            Nat.succ_le_succ_iff, ih]

Premises used: Nat.add_one_pos, HDiv.hDiv, Nat.digitChar, zero_add, Nat.div_lt_of_lt_mul, HMod.hMod, Nat.succ_le_succ_iff, pow_one, Nat.zero, Nat.div_eq_of_lt, Nat.succ, Nat.toDigitsCore_lens_eq
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b f n e : ℕ
h_e_pos : 0 < e
hlt : n < b ^ e
zero : ∀ (n e : ℕ) (h_e_pos : 0 < e) (hlt : n < b ^ e), (b.toDigitsCore 0 n []).length ≤ e
succ :
  ∀ (f : ℕ) (ih : ∀ (n e : ℕ) (h_e_pos : 0 < e) (hlt : n < b ^ e), (b.toDigitsCore f n []).length ≤ e) (n e : ℕ)
    (h_e_pos : 0 < e) (hlt : n < b ^ e), (b.toDigitsCore (f + 1) n []).length ≤ e
⊢ (b.toDigitsCore f n []).length ≤ e

Tactic:
induction f generalizing n e hlt h_e_pos with
  | zero => simp only [toDigitsCore, List.length, zero_le]
  | succ f ih =>
    simp only [toDigitsCore]
    cases e with
    | zero => exact False.elim (Nat.lt_irrefl 0 h_e_pos)
    | succ e =>
      cases e with
      | zero =>
        rw [zero_add, pow_one] at hlt
        simp [Nat.div_eq_of_lt hlt]
      | succ e =>
        specialize ih (n / b) _ (add_one_pos e) (Nat.div_lt_of_lt_mul <| by rwa [← pow_add_one'])
        split_ifs
        · simp
        · simp only [toDigitsCore_lens_eq b f (n / b) (Nat.digitChar <| n % b),
            Nat.succ_le_succ_iff, ih]

Premises used: Nat.zero_le, HDiv.hDiv, Nat.digitChar, Nat.toDigitsCore, zero_add, HMod.hMod, Nat.succ_le_succ_iff, pow_one, Nat.zero, Nat.div_eq_of_lt, Nat.succ, List.length, Nat.toDigitsCore_lens_eq
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b n e : ℕ
⊢ 0 < e → n < b ^ e → (b.toDigits n).length ≤ e

Tactic:
toDigitsCore_length _ _ _ _

Premises used: Nat.toDigits, Nat.toDigitsCore_length
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
n : ℕ
⊢ HMod.hMod (α := ℕ) 10 3 = 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
n : ℕ
⊢ HMod.hMod (α := ℕ) 10 9 = 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
n : ℕ
⊢ HMod.hMod (α := ℤ) (↑10 : ℤ) (↑11 : ℤ) = HMod.hMod (α := ℤ) (-1) (↑11 : ℤ)

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
n : ℕ
⊢ (↑n : ℤ) ≡ ofDigits (-1) (digits 10 n) [ZMOD (↑11 : ℤ)]

Tactic:
have t := zmodeq_ofDigits_digits 11 10 (-1 : ℤ) (by unfold Int.ModEq; rfl) n
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
n : ℕ
t : (↑n : ℤ) ≡ ofDigits (-1) (digits 10 n) [ZMOD (↑11 : ℤ)]
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (t : (↑n : ℤ) ≡ List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)) [ZMOD (↑11 : ℤ)]),
    (↑n : ℤ) ≡ List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)) [ZMOD 11]
⊢ (↑n : ℤ) ≡ List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)) [ZMOD 11]

Tactic:
rwa [ofDigits_neg_one] at t

Premises used: Nat.ofDigits_neg_one
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
rw : b ∣ n ↔ b ∣ ofDigits 1 (b'.digits n)
⊢ b ∣ n ↔ b ∣ (b'.digits n).sum

Tactic:
rw [← ofDigits_one]

Premises used: Nat.ofDigits_one
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
rw : b ∣ ofDigits b' (b'.digits n)
| b ∣ n

Tactic:
rw [← ofDigits_digits b' n]

Premises used: Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
conv_lhs : b ∣ ofDigits b' (b'.digits n) ↔ b ∣ ofDigits 1 (b'.digits n)
⊢ b ∣ n ↔ b ∣ ofDigits 1 (b'.digits n)

Tactic:
conv_lhs => rw [← ofDigits_digits b' n]

Premises used: Nat.ofDigits_digits