awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
head : ℕ
tail : List ℕ
ih : ofDigits 1 tail = tail.sum
⊢ ofDigits 1 (head :: tail) = (head :: tail).sum

Tactic:
simp [ofDigits, List.sum_cons, ih]

Premises used: Nat.ofDigits, List.sum_cons
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
L : List ℕ
nil : Eq (α := ℕ) (ofDigits 1 []) (List.sum [])
cons : ∀ (head : ℕ) (tail : List ℕ) (ih : ofDigits 1 tail = tail.sum), ofDigits 1 (head :: tail) = (head :: tail).sum
⊢ ofDigits 1 L = L.sum

Tactic:
induction L with
  | nil => rfl
  | cons _ _ ih => simp [ofDigits, List.sum_cons, ih]

Premises used: Nat.ofDigits, List.sum_cons
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b n : ℕ
mp : b.digits n = [] → n = 0
mpr : n = 0 → b.digits n = []
⊢ b.digits n = [] ↔ n = 0

Tactic:
constructor
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b n : ℕ
h : b.digits n = []
rw rw₁ : ofDigits b [] = ofDigits b []
⊢ ofDigits b (b.digits n) = ofDigits b []

Tactic:
rw [h]
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b n : ℕ
h : b.digits n = []
⊢ ofDigits b (b.digits n) = ofDigits b []

Tactic:
have : ofDigits b (digits b n) = ofDigits b [] := by rw [h]
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b n : ℕ
h : b.digits n = []
this : ofDigits b (b.digits n) = ofDigits b []
⊢ ofDigits b (b.digits n) = ofDigits b []

Tactic:
this
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b n : ℕ
h : b.digits n = []
this : ofDigits b (b.digits n) = ofDigits b []
h₁ : n = ofDigits b (b.digits n)
⊢ n = 0

Tactic:
convert! this
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b n : ℕ
h : b.digits n = []
this : ofDigits b (b.digits n) = ofDigits b []
h₁ h₂ : n = n
⊢ n = ofDigits b (b.digits n)

Tactic:
rw [ofDigits_digits]

Premises used: Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
⊢ b.digits 0 = []

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b n : ℕ
⊢ b.digits n ≠ [] ↔ n ≠ 0

Tactic:
not_congr digits_eq_nil_iff_eq_zero

Premises used: Nat.digits_eq_nil_iff_eq_zero, not_congr
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b n : ℕ
h : 1 < b
w : n ≠ 0
⊢ b.digits n = n % b :: b.digits (n / b)

Tactic:
digits_def' h (Nat.pos_of_ne_zero w)

Premises used: Nat.pos_of_ne_zero, Nat.digits_def'
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b m : ℕ
h : 1 < b
p : b.digits m ≠ []
q : b.digits (m / b) ≠ []
pos : ∀ (hm : m = 0), (b.digits m).getLast p = (b.digits (m / b)).getLast q
neg : ∀ (hm : ¬m = 0), (b.digits m).getLast p = (b.digits (m / b)).getLast q
⊢ (b.digits m).getLast p = (b.digits (m / b)).getLast q

Tactic:
by_cases hm : m = 0
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b m : ℕ
h : 1 < b
p : b.digits m ≠ []
q : b.digits (m / b) ≠ []
hm : m = 0
⊢ (b.digits m).getLast p = (b.digits (m / b)).getLast q

Tactic:
simp [hm]
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b m : ℕ
h : 1 < b
p : b.digits m ≠ []
q : b.digits (m / b) ≠ []
hm : ¬m = 0
neg : (m % b :: b.digits (m / b)).getLast ⋯ = (b.digits (m / b)).getLast q
⊢ (b.digits m).getLast p = (b.digits (m / b)).getLast q

Tactic:
simp only [digits_eq_cons_digits_div h hm]

Premises used: Nat.digits_eq_cons_digits_div
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b m : ℕ
h : 1 < b
p : b.digits m ≠ []
q : b.digits (m / b) ≠ []
hm : ¬m = 0
neg : (b.digits (m / b)).getLast q = (b.digits (m / b)).getLast q
neg₁ : b.digits (m / b) ≠ []
neg₂ : (b.digits (m / b)).getLast q = (b.digits (m / b)).getLast q
neg₃ : b.digits (m / b) ≠ []
⊢ (m % b :: b.digits (m / b)).getLast ⋯ = (b.digits (m / b)).getLast q

Tactic:
rw [List.getLast_cons]

Premises used: List.getLast_cons
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
⊢ Function.Injective b.digits

Tactic:
Function.LeftInverse.injective (ofDigits_digits b)

Premises used: Function.LeftInverse.injective, Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b n m : ℕ
⊢ b.digits n = b.digits m ↔ n = m

Tactic:
(digits.injective b).eq_iff

Premises used: Function.Injective.eq_iff, Nat.digits.injective
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n b : ℕ
⊢ n * ofDigits b [] = ofDigits b (List.map (fun (x : ℕ) ↦ n * x) [])

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n b hd : ℕ
tl : List ℕ
ih : n * ofDigits b tl = ofDigits b (List.map (fun (x : ℕ) ↦ n * x) tl)
cons : n * (hd + b * ofDigits b tl) = n * hd + b * (n * ofDigits b tl)
⊢ n * ofDigits b (hd :: tl) = ofDigits b (List.map (fun (x : ℕ) ↦ n * x) (hd :: tl))

Tactic:
rw [List.map_cons, ofDigits_cons, ofDigits_cons, ← ih]

Premises used: List.map_cons, Nat.ofDigits_cons
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n b hd : ℕ
tl : List ℕ
ih : n * ofDigits b tl = ofDigits b (List.map (fun (x : ℕ) ↦ n * x) tl)
⊢ n * (hd + b * ofDigits b tl) = n * hd + b * (n * ofDigits b tl)

Tactic:
ring
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n b : ℕ
l : List ℕ
nil : n * ofDigits b [] = ofDigits b (List.map (fun (x : ℕ) ↦ n * x) [])
cons :
  ∀ (hd : ℕ) (tl : List ℕ) (ih : n * ofDigits b tl = ofDigits b (List.map (fun (x : ℕ) ↦ n * x) tl)),
    n * ofDigits b (hd :: tl) = ofDigits b (List.map (fun (x : ℕ) ↦ n * x) (hd :: tl))
⊢ n * ofDigits b l = ofDigits b (List.map (fun (x : ℕ) ↦ n * x) l)

Tactic:
induction l with
  | nil => rfl
  | cons hd tl ih =>
    rw [List.map_cons, ofDigits_cons, ofDigits_cons, ← ih]
    ring

Premises used: List.map_cons, Nat.ofDigits_cons
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
hb : 1 < b
L2 : List ℕ
len : 0 = L2.length
w1 : ∀ (l : ℕ), Membership.mem (γ := List ℕ) [] l → l < b
w2 : ∀ l ∈ L2, l < b
h : ofDigits b [] = ofDigits b L2
⊢ [] = L2

Tactic:
(List.length_eq_zero_iff.mp len.symm).symm

Premises used: Iff.mp, Eq.symm, List.length_eq_zero_iff
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
hb : 1 < b
L2 : List ℕ
len : 0 = L2.length
w1 : ∀ (l : ℕ), Membership.mem (γ := List ℕ) [] l → l < b
w2 : ∀ l ∈ L2, l < b
h : ofDigits b [] = ofDigits b L2
⊢ [] = L2

Tactic:
exact (List.length_eq_zero_iff.mp len.symm).symm

Premises used: Iff.mp, Eq.symm, List.length_eq_zero_iff
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ} (len : L.length = L2.length) (w1 : ∀ l ∈ L, l < b) (w2 : ∀ l ∈ L2, l < b)
    (h : ofDigits b L = ofDigits b L2), L = L2
L2 : List ℕ
len : (D :: L).length = L2.length
w1 : ∀ l ∈ D :: L, l < b
w2 : ∀ l ∈ L2, l < b
h : ofDigits b (D :: L) = ofDigits b L2
⊢ D :: L = L2

Tactic:
?_
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
hb : 1 < b
L1 L2 : List ℕ
len : L1.length = L2.length
w1 : ∀ l ∈ L1, l < b
w2 : ∀ l ∈ L2, l < b
h : ofDigits b L1 = ofDigits b L2
cons :
  ∀ (D : ℕ) (L : List ℕ)
    (ih :
      ∀ {L2 : List ℕ} (len : L.length = L2.length) (w1 : ∀ l ∈ L, l < b) (w2 : ∀ l ∈ L2, l < b)
        (h : ofDigits b L = ofDigits b L2), L = L2)
    {L2 : List ℕ} (len : (D :: L).length = L2.length) (w1 : ∀ l ∈ D :: L, l < b) (w2 : ∀ l ∈ L2, l < b)
    (h : ofDigits b (D :: L) = ofDigits b L2), D :: L = L2
⊢ L1 = L2

Tactic:
induction L1 generalizing L2 with
  | nil =>
    simp only [List.length_nil] at len
    exact (List.length_eq_zero_iff.mp len.symm).symm
  | cons D L ih => ?_

Premises used: Iff.mp, Eq.symm, List.length_nil, List.length_eq_zero_iff
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ} (len : L.length = L2.length) (w1 : ∀ l ∈ L, l < b) (w2 : ∀ l ∈ L2, l < b)
    (h : ofDigits b L = ofDigits b L2), L = L2
L2 : List ℕ
len : (D :: L).length = L2.length
w1 : ∀ l ∈ D :: L, l < b
w2 : ∀ l ∈ L2, l < b
h : ofDigits b (D :: L) = ofDigits b L2
cons :
  ∀ (d : ℕ) (l : List ℕ) (len : (D :: L).length = (d :: l).length) (w2 : ∀ l_1 ∈ d :: l, l_1 < b)
    (h : ofDigits b (D :: L) = ofDigits b (d :: l)), D :: L = d :: l
⊢ D :: L = L2

Tactic:
obtain ⟨d, l, rfl⟩ := List.exists_cons_of_length_eq_add_one len.symm

Premises used: List.exists_cons_of_length_eq_add_one, Eq.symm, rfl
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ} (len : L.length = L2.length) (w1 : ∀ l ∈ L, l < b) (w2 : ∀ l ∈ L2, l < b)
    (h : ofDigits b L = ofDigits b L2), L = L2
w1 : ∀ l ∈ D :: L, l < b
d : ℕ
l : List ℕ
len : (D :: L).length = (d :: l).length
w2 : ∀ l_1 ∈ d :: l, l_1 < b
h : ofDigits b (D :: L) = ofDigits b (d :: l)
⊢ L.length = l.length

Tactic:
simp only [List.length_cons, add_left_inj] at len

Premises used: List.length_cons, add_left_inj
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ} (len : L.length = L2.length) (w1 : ∀ l ∈ L, l < b) (w2 : ∀ l ∈ L2, l < b)
    (h : ofDigits b L = ofDigits b L2), L = L2
w1 : ∀ l ∈ D :: L, l < b
d : ℕ
l : List ℕ
w2 : ∀ l_1 ∈ d :: l, l_1 < b
h : D + b * ofDigits b L = d + b * ofDigits b l
len : L.length = l.length
rw rw₁ : (d + b * ofDigits b l) % b = (d + b * ofDigits b l) % b
⊢ (D + b * ofDigits b L) % b = (d + b * ofDigits b l) % b

Tactic:
rw [h]
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ} (len : L.length = L2.length) (w1 : ∀ l ∈ L, l < b) (w2 : ∀ l ∈ L2, l < b)
    (h : ofDigits b L = ofDigits b L2), L = L2
w1 : ∀ l ∈ D :: L, l < b
d : ℕ
l : List ℕ
w2 : ∀ l_1 ∈ d :: l, l_1 < b
h : D + b * ofDigits b L = d + b * ofDigits b l
len : L.length = l.length
⊢ (D + b * ofDigits b L) % b = (d + b * ofDigits b l) % b

Tactic:
have H : (D + b * ofDigits b L) % b = (d + b * ofDigits b l) % b := by rw [h]
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ} (len : L.length = L2.length) (w1 : ∀ l ∈ L, l < b) (w2 : ∀ l ∈ L2, l < b)
    (h : ofDigits b L = ofDigits b L2), L = L2
w1 : ∀ l ∈ D :: L, l < b
d : ℕ
l : List ℕ
w2 : ∀ l_1 ∈ d :: l, l_1 < b
h : D + b * ofDigits b L = d + b * ofDigits b l
len : L.length = l.length
H : (D + b * ofDigits b L) % b = (d + b * ofDigits b l) % b
⊢ D = d

Tactic:
simpa [mod_eq_of_lt (w2 d List.mem_cons_self),
      mod_eq_of_lt (w1 D List.mem_cons_self)] using H

Premises used: Nat.mod_eq_of_lt, List.mem_cons_self
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ} (len : L.length = L2.length) (w1 : ∀ l ∈ L, l < b) (w2 : ∀ l ∈ L2, l < b)
    (h : ofDigits b L = ofDigits b L2), L = L2
w1 : ∀ l ∈ D :: L, l < b
d : ℕ
l : List ℕ
w2 : ∀ l_1 ∈ d :: l, l_1 < b
h : D + b * ofDigits b L = d + b * ofDigits b l
len : L.length = l.length
⊢ D = d

Tactic:
have eqd : D = d := by
    have H : (D + b * ofDigits b L) % b = (d + b * ofDigits b l) % b := by rw [h]
    simpa [mod_eq_of_lt (w2 d List.mem_cons_self),
      mod_eq_of_lt (w1 D List.mem_cons_self)] using H
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ} (len : L.length = L2.length) (w1 : ∀ l ∈ L, l < b) (w2 : ∀ l ∈ L2, l < b)
    (h : ofDigits b L = ofDigits b L2), L = L2
w1 : ∀ l ∈ D :: L, l < b
d : ℕ
l : List ℕ
w2 : ∀ l_1 ∈ d :: l, l_1 < b
h : D + b * ofDigits b L = d + b * ofDigits b l
len : L.length = l.length
eqd : D = d
⊢ ofDigits b L = ofDigits b l

Tactic:
simp only [eqd, add_right_inj, mul_left_cancel_iff_of_pos (zero_lt_of_lt hb)] at h

Premises used: Nat.zero_lt_of_lt, add_right_inj, mul_left_cancel_iff_of_pos
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ} (len : L.length = L2.length) (w1 : ∀ l ∈ L, l < b) (w2 : ∀ l ∈ L2, l < b)
    (h : ofDigits b L = ofDigits b L2), L = L2
w1 : ∀ l ∈ D :: L, l < b
d : ℕ
l : List ℕ
w2 : ∀ l_1 ∈ d :: l, l_1 < b
len : L.length = l.length
eqd : D = d
h : ofDigits b L = ofDigits b l
⊢ L = l

Tactic:
have := ih len (fun a ha ↦ w1 a <| List.mem_cons_of_mem D ha)
    (fun a ha ↦ w2 a <| List.mem_cons_of_mem d ha) h
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
hb : 1 < b
D : ℕ
L : List ℕ
ih :
  ∀ {L2 : List ℕ} (len : L.length = L2.length) (w1 : ∀ l ∈ L, l < b) (w2 : ∀ l ∈ L2, l < b)
    (h : ofDigits b L = ofDigits b L2), L = L2
w1 : ∀ l ∈ D :: L, l < b
d : ℕ
l : List ℕ
w2 : ∀ l_1 ∈ d :: l, l_1 < b
len : L.length = l.length
eqd : D = d
h : ofDigits b L = ofDigits b l
this : L = l
cons : d :: L = d :: l
cons₁ cons₂ : d :: l = d :: l
⊢ D :: L = d :: l

Tactic:
rw [eqd, this]
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
l2 : List ℕ
h : List.length (α := ℕ) [] = l2.length
⊢ ofDigits b [] + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) [] l2)

Tactic:
simp_all [eq_comm, List.length_eq_zero_iff, ofDigits]

Premises used: Nat.ofDigits, eq_comm, List.length_eq_zero_iff
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b hd₁ : ℕ
tl₁ : List ℕ
ih₁ :
  ∀ {l2 : List ℕ} (h : tl₁.length = l2.length),
    ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) tl₁ l2)
h : (hd₁ :: tl₁).length = List.length (α := ℕ) []
⊢ ofDigits b (hd₁ :: tl₁) + ofDigits b [] = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) (hd₁ :: tl₁) [])

Tactic:
simp_all
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b hd₁ hd₂ : ℕ
tl₂ : List ℕ
ih₂ :
  ∀ (tl₁ : List ℕ)
    (ih₁ :
      ∀ {l2 : List ℕ} (h : tl₁.length = l2.length),
        ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) tl₁ l2))
    (h : (hd₁ :: tl₁).length = tl₂.length),
    ofDigits b (hd₁ :: tl₁) + ofDigits b tl₂ = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) (hd₁ :: tl₁) tl₂)
tl₁ : List ℕ
ih₁ :
  ∀ {l2 : List ℕ} (h : tl₁.length = l2.length),
    ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) tl₁ l2)
h : (hd₁ :: tl₁).length = (hd₂ :: tl₂).length
cons :
  ∀
    (ih₂ :
      ∀ (tl₁_1 : List ℕ)
        (ih₁ :
          ∀ {l2 : List ℕ} (h : tl₁_1.length = l2.length),
            ofDigits b tl₁_1 + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) tl₁_1 l2))
        (h : tl₁.length = tl₁_1.length + 1),
        hd₁ + b * ofDigits b tl₁_1 + ofDigits b tl₂ =
          ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) (hd₁ :: tl₁_1) tl₂))
    (ih₁ :
      ∀ {l2 : List ℕ} (h : tl₁.length = l2.length),
        ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) tl₁ l2))
    (h : tl₂.length = tl₁.length),
    hd₁ + b * ofDigits b tl₁ + (hd₂ + b * ofDigits b tl₂) =
      hd₁ + hd₂ + b * ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) tl₁ tl₂)
⊢ ofDigits b (hd₁ :: tl₁) + ofDigits b (hd₂ :: tl₂) =
    ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) (hd₁ :: tl₁) (hd₂ :: tl₂))

Tactic:
simp_all only [List.length_cons, ofDigits_cons, add_left_inj,
        eq_comm, List.zipWith_cons_cons]

Premises used: List.length_cons, add_left_inj, Nat.ofDigits_cons, eq_comm, List.zipWith_cons_cons
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b hd₁ hd₂ : ℕ
tl₂ tl₁ : List ℕ
ih₂ :
  ∀ (tl₁_1 : List ℕ)
    (ih₁ :
      ∀ {l2 : List ℕ} (h : tl₁_1.length = l2.length),
        ofDigits b tl₁_1 + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) tl₁_1 l2))
    (h : tl₁.length = tl₁_1.length + 1),
    hd₁ + b * ofDigits b tl₁_1 + ofDigits b tl₂ =
      ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) (hd₁ :: tl₁_1) tl₂)
ih₁ :
  ∀ {l2 : List ℕ} (h : tl₁.length = l2.length),
    ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) tl₁ l2)
h : tl₂.length = tl₁.length
cons : hd₁ + b * ofDigits b tl₁ + (hd₂ + b * ofDigits b tl₂) = hd₁ + hd₂ + (b * ofDigits b tl₁ + b * ofDigits b tl₂)
⊢ hd₁ + b * ofDigits b tl₁ + (hd₂ + b * ofDigits b tl₂) =
    hd₁ + hd₂ + b * ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) tl₁ tl₂)

Tactic:
rw [← ih₁ h.symm, mul_add]

Premises used: mul_add, Eq.symm
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b hd₁ hd₂ : ℕ
tl₂ tl₁ : List ℕ
ih₂ :
  ∀ (tl₁_1 : List ℕ)
    (ih₁ :
      ∀ {l2 : List ℕ} (h : tl₁_1.length = l2.length),
        ofDigits b tl₁_1 + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) tl₁_1 l2))
    (h : tl₁.length = tl₁_1.length + 1),
    hd₁ + b * ofDigits b tl₁_1 + ofDigits b tl₂ =
      ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) (hd₁ :: tl₁_1) tl₂)
ih₁ :
  ∀ {l2 : List ℕ} (h : tl₁.length = l2.length),
    ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) tl₁ l2)
h : tl₂.length = tl₁.length
⊢ hd₁ + b * ofDigits b tl₁ + (hd₂ + b * ofDigits b tl₂) = hd₁ + hd₂ + (b * ofDigits b tl₁ + b * ofDigits b tl₂)

Tactic:
ac_rfl
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b hd₁ : ℕ
tl₁ : List ℕ
ih₁ :
  ∀ {l2 : List ℕ} (h : tl₁.length = l2.length),
    ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) tl₁ l2)
l2 : List ℕ
h : (hd₁ :: tl₁).length = l2.length
cons :
  ∀ (tl₁ : List ℕ)
    (ih₁ :
      ∀ {l2 : List ℕ} (h : tl₁.length = l2.length),
        ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) tl₁ l2))
    (h : (hd₁ :: tl₁).length = List.length (α := ℕ) []),
    ofDigits b (hd₁ :: tl₁) + ofDigits b [] = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) (hd₁ :: tl₁) [])
cons₁ :
  ∀ (hd₂ : ℕ) (tl₂ : List ℕ)
    (ih₂ :
      ∀ (tl₁ : List ℕ)
        (ih₁ :
          ∀ {l2 : List ℕ} (h : tl₁.length = l2.length),
            ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) tl₁ l2))
        (h : (hd₁ :: tl₁).length = tl₂.length),
        ofDigits b (hd₁ :: tl₁) + ofDigits b tl₂ =
          ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) (hd₁ :: tl₁) tl₂))
    (tl₁ : List ℕ)
    (ih₁ :
      ∀ {l2 : List ℕ} (h : tl₁.length = l2.length),
        ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) tl₁ l2))
    (h : (hd₁ :: tl₁).length = (hd₂ :: tl₂).length),
    ofDigits b (hd₁ :: tl₁) + ofDigits b (hd₂ :: tl₂) =
      ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) (hd₁ :: tl₁) (hd₂ :: tl₂))
⊢ ofDigits b (hd₁ :: tl₁) + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) (hd₁ :: tl₁) l2)

Tactic:
induction l2 generalizing tl₁ with
    | nil => simp_all
    | cons hd₂ tl₂ ih₂ =>
      simp_all only [List.length_cons, ofDigits_cons, add_left_inj,
        eq_comm, List.zipWith_cons_cons]
      rw [← ih₁ h.symm, mul_add]
      ac_rfl

Premises used: List.length_cons, add_left_inj, Nat.ofDigits_cons, eq_comm, List.zipWith_cons_cons, mul_add
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
l1 l2 : List ℕ
h : l1.length = l2.length
nil :
  ∀ {l2 : List ℕ} (h : List.length (α := ℕ) [] = l2.length),
    ofDigits b [] + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) [] l2)
cons :
  ∀ (hd₁ : ℕ) (tl₁ : List ℕ)
    (ih₁ :
      ∀ {l2 : List ℕ} (h : tl₁.length = l2.length),
        ofDigits b tl₁ + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) tl₁ l2))
    {l2 : List ℕ} (h : (hd₁ :: tl₁).length = l2.length),
    ofDigits b (hd₁ :: tl₁) + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) (hd₁ :: tl₁) l2)
⊢ ofDigits b l1 + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) l1 l2)

Tactic:
induction l1 generalizing l2 with
  | nil => simp_all [eq_comm, List.length_eq_zero_iff, ofDigits]
  | cons hd₁ tl₁ ih₁ =>
    induction l2 generalizing tl₁ with
    | nil => simp_all
    | cons hd₂ tl₂ ih₂ =>
      simp_all only [List.length_cons, ofDigits_cons, add_left_inj,
        eq_comm, List.zipWith_cons_cons]
      rw [← ih₁ h.symm, mul_add]
      ac_rfl

Premises used: List.length_cons, Nat.ofDigits, add_left_inj, Nat.ofDigits_cons, eq_comm, List.zipWith_cons_cons, mul_add, List.length_eq_zero_iff
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b n : ℕ
IH : ∀ m < n, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
⊢ ∀ {d : ℕ}, d ∈ (b + 2).digits n → d < b + 2

Tactic:
?_
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b m : ℕ
ind : ∀ (n : ℕ) (IH : ∀ m < n, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2) {d : ℕ}, d ∈ (b + 2).digits n → d < b + 2
⊢ ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2

Tactic:
induction m using Nat.strongRecOn with | ind n IH => ?_
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b n : ℕ
IH : ∀ m < n, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
d : ℕ
hd : d ∈ (b + 2).digits n
ind : ∀ (IH : ∀ m < 0, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2) (hd : d ∈ (b + 2).digits 0), d < b + 2
ind₁ :
  ∀ (n : ℕ) (IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2) (hd : d ∈ (b + 2).digits (n + 1)), d < b + 2
⊢ d < b + 2

Tactic:
rcases n with - | n
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b d : ℕ
IH : ∀ m < 0, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
hd : d ∈ (b + 2).digits 0
⊢ Membership.mem (γ := List ℕ) [] d

Tactic:
rw [digits_zero] at hd

Premises used: Nat.digits_zero
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b d : ℕ
IH : ∀ m < 0, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
hd : Membership.mem (γ := List ℕ) [] d
⊢ d < b + 2

Tactic:
cases hd
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
hd : d ∈ (b + 2).digits (n + 1)
⊢ d ∈ (n + 1) % (b + 2) :: (b + 2).digits ((n + 1) / (b + 2))

Tactic:
rw [digits_add_two_add_one] at hd

Premises used: Nat.digits_add_two_add_one
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
hd : d ∈ (n + 1) % (b + 2) :: (b + 2).digits ((n + 1) / (b + 2))
ind : (n + 1) % (b + 2) < b + 2
ind₁ : List.Mem d ((b + 2).digits ((n + 1) / (b + 2))) → d < b + 2
⊢ d < b + 2

Tactic:
cases hd
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
linarith :
  b + 2 ≤ 0 → HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 0 (↑b : ℤ) + (HAdd.hAdd (α := ℤ) (↑b : ℤ) 2 - 0) = 0
linarith₁ : b + 2 ≤ 0 → GT.gt (α := ℤ) 2 0
⊢ 0 < b + 2

Tactic:
linarith
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
⊢ (n + 1) % (b + 2) < b + 2

Tactic:
exact n.succ.mod_lt (by linarith)

Premises used: Nat.mod_lt, Nat.succ
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
h : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
ind : (n + 1) / (b + 2) < n + 1
ind₁ : d ∈ (b + 2).digits ((n + 1) / (b + 2))
⊢ d < b + 2

Tactic:
apply IH ((n + 1) / (b + 2))

Premises used: HDiv.hDiv, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
h : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
ind : 0 < n + 1
ind₁ : 1 < b + 2
⊢ (n + 1) / (b + 2) < n + 1

Tactic:
apply Nat.div_lt_self

Premises used: Nat.div_lt_self
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
h : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ 0 < n + 1

Tactic:
lia
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
h : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ 1 < b + 2

Tactic:
lia
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b d n : ℕ
IH : ∀ m < n + 1, ∀ {d : ℕ}, d ∈ (b + 2).digits m → d < b + 2
h : List.Mem d ((b + 2).digits ((n + 1) / (b + 2)))
⊢ d ∈ (b + 2).digits ((n + 1) / (b + 2))

Tactic:
assumption
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b m d : ℕ
hb : 1 < b
hd : d ∈ b.digits m
zero : ∀ (hb : LT.lt (α := ℕ) 1 0) (hd : d ∈ digits 0 m), d < 0
succ : ∀ (hb : 1 < HAdd.hAdd (α := ℕ) 0 1) (hd : d ∈ (HAdd.hAdd (α := ℕ) 0 1).digits m), d < HAdd.hAdd (α := ℕ) 0 1
succ₁ : ∀ (b : ℕ) (hb : 1 < b + 1 + 1) (hd : d ∈ (b + 1 + 1).digits m), d < b + 1 + 1
⊢ d < b

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

Tactic:
simp_all [@digits_lt_base' _ m d]

Premises used: Nat.digits_lt_base'
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
m d : ℕ
hb : 1 < HAdd.hAdd (α := ℕ) 0 1
hd : d ∈ (HAdd.hAdd (α := ℕ) 0 1).digits m
⊢ d < HAdd.hAdd (α := ℕ) 0 1

Tactic:
simp_all [@digits_lt_base' _ m d]

Premises used: Nat.digits_lt_base'
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
m d b : ℕ
hb : 1 < b + 1 + 1
hd : d ∈ (b + 1 + 1).digits m
⊢ d < b + 1 + 1

Tactic:
simp_all [@digits_lt_base' _ m d]

Premises used: Nat.digits_lt_base'
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
hl : ∀ (x : ℕ), Membership.mem (γ := List ℕ) [] x → x < b + 2
⊢ ofDigits (b + 2) [] < (b + 2) ^ List.length (α := ℕ) []

Tactic:
simp [ofDigits]

Premises used: Nat.ofDigits