awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
h : 1 < b
L : List ℕ
w₁ : ∀ l ∈ L, l < b
w₂ : ∀ (h : L ≠ []), L.getLast h ≠ 0
⊢ b.digits (ofDigits b L) = L
have nil : ∀ (w₁ : ∀ (l : ℕ), Membership.mem (γ := List ℕ) [] l → l < b)
  (w₂ : ∀ (h : Ne (α := List ℕ) [] []), List.getLast [] h ≠ 0), b.digits (ofDigits b []) = []
Tactic: induction L with
  | nil => simp
  | cons d L ih =>
    dsimp [ofDigits]
    replace w₂ := w₂ (by simp)
    rw [digits_add b h]
    · rw [ih]
      · intro l m
        apply w₁
        exact List.mem_cons_of_mem _ m
      · intro h
        rw [List.getLast_cons h] at w₂
        convert! w₂
    · exact w₁ d List.mem_cons_self
    · by_cases h' : L = []
      · rcases h' with rfl
        left
        simpa using w₂
      · right
        contrapose w₂
        refine digits_zero_of_eq_zero h.ne_bot w₂ _ ?_
        rw [List.getLast_cons h']
        exact List.getLast_mem h'
Cleared hypotheses: L, w₁, w₂
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
h : 1 < b
L : List ℕ
w₁ : ∀ l ∈ L, l < b
w₂ : ∀ (h : L ≠ []), L.getLast h ≠ 0
nil :
  ∀ (w₁ : ∀ (l : ℕ), Membership.mem (γ := List ℕ) [] l → l < b)
    (w₂ : ∀ (h : Ne (α := List ℕ) [] []), List.getLast [] h ≠ 0), b.digits (ofDigits b []) = []
⊢ b.digits (ofDigits b L) = L
have cons : ∀ (d : ℕ) (L : List ℕ)
  (ih : ∀ (w₁ : ∀ l ∈ L, l < b) (w₂ : ∀ (h : L ≠ []), L.getLast h ≠ 0), b.digits (ofDigits b L) = L)
  (w₁ : ∀ l ∈ d :: L, l < b) (w₂ : ∀ (h : d :: L ≠ []), (d :: L).getLast h ≠ 0), b.digits (ofDigits b (d :: L)) = d :: L
Tactic: induction L with
  | nil => simp
  | cons d L ih =>
    dsimp [ofDigits]
    replace w₂ := w₂ (by simp)
    rw [digits_add b h]
    · rw [ih]
      · intro l m
        apply w₁
        exact List.mem_cons_of_mem _ m
      · intro h
        rw [List.getLast_cons h] at w₂
        convert! w₂
    · exact w₁ d List.mem_cons_self
    · by_cases h' : L = []
      · rcases h' with rfl
        left
        simpa using w₂
      · right
        contrapose w₂
        refine digits_zero_of_eq_zero h.ne_bot w₂ _ ?_
        rw [List.getLast_cons h']
        exact List.getLast_mem h'
Cleared hypotheses: L, w₁, w₂
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b n : ℕ
⊢ ofDigits b (b.digits n) = n
have zero : ofDigits 0 (digits 0 n) = n
Tactic: rcases b with - | b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b n : ℕ
zero : ofDigits 0 (digits 0 n) = n
⊢ ofDigits b (b.digits n) = n
have succ : ∀ (b : ℕ), ofDigits (b + 1) ((b + 1).digits n) = n
Tactic: rcases b with - | b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
n : ℕ
⊢ ofDigits 0 (digits 0 n) = n
have zero : Eq (α := ℕ) (ofDigits 0 (digits 0 0)) 0
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
n : ℕ
zero : Eq (α := ℕ) (ofDigits 0 (digits 0 0)) 0
⊢ ofDigits 0 (digits 0 n) = n
have zero₁ : ∀ (n : ℕ), ofDigits 0 (digits 0 (n + 1)) = n + 1
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
n b : ℕ
⊢ ofDigits (b + 1) ((b + 1).digits n) = n
have succ : ofDigits (HAdd.hAdd (α := ℕ) 0 1) ((HAdd.hAdd (α := ℕ) 0 1).digits n) = n
Tactic: rcases b with - | b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
n b : ℕ
succ : ofDigits (HAdd.hAdd (α := ℕ) 0 1) ((HAdd.hAdd (α := ℕ) 0 1).digits n) = n
⊢ ofDigits (b + 1) ((b + 1).digits n) = n
have succ₁ : ∀ (b : ℕ), ofDigits (b + 1 + 1) ((b + 1 + 1).digits n) = n
Tactic: rcases b with - | b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
n : ℕ
⊢ ofDigits (HAdd.hAdd (α := ℕ) 0 1) ((HAdd.hAdd (α := ℕ) 0 1).digits n) = n
have succ : ofDigits (HAdd.hAdd (α := ℕ) 0 1) ((HAdd.hAdd (α := ℕ) 0 1).digits 0) = 0
Tactic: induction n with
      | zero => rfl
      | succ n ih =>
        rw [Nat.zero_add] at ih ⊢
        simp only [ih, add_comm 1, ofDigits_one_cons, Nat.cast_id, digits_one_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
n : ℕ
succ : ofDigits (HAdd.hAdd (α := ℕ) 0 1) ((HAdd.hAdd (α := ℕ) 0 1).digits 0) = 0
⊢ ofDigits (HAdd.hAdd (α := ℕ) 0 1) ((HAdd.hAdd (α := ℕ) 0 1).digits n) = n
have succ₁ : ∀ (n : ℕ) (ih : ofDigits (HAdd.hAdd (α := ℕ) 0 1) ((HAdd.hAdd (α := ℕ) 0 1).digits n) = n),
  ofDigits (HAdd.hAdd (α := ℕ) 0 1) ((HAdd.hAdd (α := ℕ) 0 1).digits (n + 1)) = n + 1
Tactic: induction n with
      | zero => rfl
      | succ n ih =>
        rw [Nat.zero_add] at ih ⊢
        simp only [ih, add_comm 1, ofDigits_one_cons, Nat.cast_id, digits_one_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
n b : ℕ
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits n) = n
have succ : ∀ (n : ℕ) (h : ∀ m < n, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m),
  ofDigits (b + 1 + 1) ((b + 1 + 1).digits n) = n
Tactic: induction n using Nat.strongRecOn with | ind n h => ?_
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b n : ℕ
h : ∀ m < n, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits n) = n
have succ : ∀ (h : ∀ m < 0, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m), ofDigits (b + 1 + 1) ((b + 1 + 1).digits 0) = 0
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b n : ℕ
h : ∀ m < n, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
succ : ∀ (h : ∀ m < 0, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m), ofDigits (b + 1 + 1) ((b + 1 + 1).digits 0) = 0
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits n) = n
have succ₁ : ∀ (n : ℕ) (h : ∀ m < n + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m),
  ofDigits (b + 1 + 1) ((b + 1 + 1).digits (n + 1)) = n + 1
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b n : ℕ
h : ∀ m < n + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits (n + 1)) = n + 1
have succ : ofDigits (b + 1 + 1) ((n + 1) % (b + 2) :: (b + 2).digits ((n + 1) / (b + 2))) = n + 1
Tactic: simp only [digits_add_two_add_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b n : ℕ
h : ∀ m < n + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ (n + 1) % (b + 2) + (b + 1 + 1) * ofDigits (b + 1 + 1) ((b + 2).digits ((n + 1) / (b + 2))) = n + 1
have succ : (n + 1) % (b + 2) + (b + 1 + 1) * ((n + 1) / (b + 2)) = n + 1
Tactic: rw [h _ (Nat.div_lt_self' _ b)]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b n : ℕ
h : ∀ m < n + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ (n + 1) % (b + 2) + (b + 1 + 1) * ((n + 1) / (b + 2)) = n + 1
have succ : n + 1 = n + 1
Tactic: rw [Nat.mod_add_div]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
L : List ℕ
⊢ ofDigits 1 L = L.sum
have nil : Eq (α := ℕ) (ofDigits 1 []) (List.sum [])
Tactic: induction L with
  | nil => rfl
  | cons _ _ ih => simp [ofDigits, List.sum_cons, ih]
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
L : List ℕ
nil : Eq (α := ℕ) (ofDigits 1 []) (List.sum [])
⊢ ofDigits 1 L = L.sum
have cons : ∀ (head : ℕ) (tail : List ℕ) (ih : ofDigits 1 tail = tail.sum), ofDigits 1 (head :: tail) = (head :: tail).sum
Tactic: induction L with
  | nil => rfl
  | cons _ _ ih => simp [ofDigits, List.sum_cons, ih]
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b n : ℕ
⊢ b.digits n = [] ↔ n = 0
have mp : b.digits n = [] → n = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b n : ℕ
mp : b.digits n = [] → n = 0
⊢ b.digits n = [] ↔ n = 0
have mpr : n = 0 → b.digits n = []
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b n : ℕ
h : b.digits n = []
⊢ ofDigits b (b.digits n) = ofDigits b []
have rw : ofDigits b [] = ofDigits b []
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (hypothesis)
Goal:
b n : ℕ
h : b.digits n = []
⊢ n = 0
have this : ofDigits b (b.digits n) = ofDigits b []
Tactic: have : ofDigits b (digits b n) = ofDigits b [] := by rw [h]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b n : ℕ
h : b.digits n = []
this : ofDigits b (b.digits n) = ofDigits b []
⊢ n = 0
have h₁ : n = ofDigits b (b.digits n)
Tactic: convert! this
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b n : ℕ
h : b.digits n = []
this : ofDigits b (b.digits n) = ofDigits b []
⊢ n = ofDigits b (b.digits n)
have h₁ : n = n
Tactic: rw [ofDigits_digits]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b m : ℕ
h : 1 < b
p : b.digits m ≠ []
q : b.digits (m / b) ≠ []
⊢ (b.digits m).getLast p = (b.digits (m / b)).getLast q
have pos : ∀ (hm : m = 0), (b.digits m).getLast p = (b.digits (m / b)).getLast q
Tactic: by_cases hm : m = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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
⊢ (b.digits m).getLast p = (b.digits (m / b)).getLast q
have neg : ∀ (hm : ¬m = 0), (b.digits m).getLast p = (b.digits (m / b)).getLast q
Tactic: by_cases hm : m = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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
have neg : (m % b :: b.digits (m / b)).getLast sorry = (b.digits (m / b)).getLast q
Tactic: simp only [digits_eq_cons_digits_div h hm]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b m : ℕ
h : 1 < b
p : b.digits m ≠ []
q : b.digits (m / b) ≠ []
hm : ¬m = 0
⊢ (m % b :: b.digits (m / b)).getLast ⋯ = (b.digits (m / b)).getLast q
have neg : (b.digits (m / b)).getLast q = (b.digits (m / b)).getLast q
Tactic: rw [List.getLast_cons]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
n b 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))
have cons : n * (hd + b * ofDigits b tl) = n * hd + b * (n * ofDigits b tl)
Tactic: rw [List.map_cons, ofDigits_cons, ofDigits_cons, ← ih]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
n b : ℕ
l : List ℕ
⊢ n * ofDigits b l = ofDigits b (List.map (fun (x : ℕ) ↦ n * x) l)
have nil : n * ofDigits b [] = ofDigits b (List.map (fun (x : ℕ) ↦ n * x) [])
Tactic: induction l with
  | nil => rfl
  | cons hd tl ih =>
    rw [List.map_cons, ofDigits_cons, ofDigits_cons, ← ih]
    ring
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
n b : ℕ
l : List ℕ
nil : n * ofDigits b [] = ofDigits b (List.map (fun (x : ℕ) ↦ n * x) [])
⊢ n * ofDigits b l = ofDigits b (List.map (fun (x : ℕ) ↦ n * x) l)
have 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))
Tactic: induction l with
  | nil => rfl
  | cons hd tl ih =>
    rw [List.map_cons, ofDigits_cons, ofDigits_cons, ← ih]
    ring
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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
⊢ L1 = L2
have 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
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 => ?_
Cleared hypotheses: L1, L2, len, w1, w2, h
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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
have 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
Tactic: obtain ⟨d, l, rfl⟩ := List.exists_cons_of_length_eq_add_one len.symm
Cleared hypotheses: L2, len, w2, h
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (hypothesis)
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)
⊢ D :: L = d :: l
have len₁ : L.length = l.length
Tactic: simp only [List.length_cons, add_left_inj] at len
Cleared hypotheses: len
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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
have rw : (d + b * ofDigits b l) % b = (d + b * ofDigits b l) % b
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (hypothesis)
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
have H : (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]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (hypothesis)
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 :: L = d :: l
have eqd : 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
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (hypothesis)
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
⊢ D :: L = d :: l
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (hypothesis)
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
⊢ D :: L = d :: l
have this : 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
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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
⊢ D :: L = d :: l
have cons : d :: L = d :: l
Tactic: rw [eqd, this]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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
⊢ D :: L = d :: l
have cons₁ : d :: l = d :: l
Tactic: rw [eqd, this]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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
⊢ ofDigits b (hd₁ :: tl₁) + ofDigits b (hd₂ :: tl₂) =
    ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) (hd₁ :: tl₁) (hd₂ :: tl₂))
have 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₂)
Tactic: simp_all only [List.length_cons, ofDigits_cons, add_left_inj,
        eq_comm, List.zipWith_cons_cons]
Cleared hypotheses: ih₂, ih₁, h
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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 (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) tl₁ tl₂)
have cons : hd₁ + b * ofDigits b tl₁ + (hd₂ + b * ofDigits b tl₂) = hd₁ + hd₂ + (b * ofDigits b tl₁ + b * ofDigits b tl₂)
Tactic: rw [← ih₁ h.symm, mul_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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
⊢ ofDigits b (hd₁ :: tl₁) + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) (hd₁ :: tl₁) l2)
have 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₁) [])
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
Cleared hypotheses: tl₁, ih₁, l2, h
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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₁) [])
⊢ ofDigits b (hd₁ :: tl₁) + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) (hd₁ :: tl₁) l2)
have 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₂))
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
Cleared hypotheses: tl₁, ih₁, l2, h
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
l1 l2 : List ℕ
h : l1.length = l2.length
⊢ ofDigits b l1 + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) l1 l2)
have nil : ∀ {l2 : List ℕ} (h : List.length (α := ℕ) [] = l2.length),
  ofDigits b [] + ofDigits b l2 = ofDigits b (List.zipWith (fun (x1 x2 : ℕ) ↦ x1 + x2) [] 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
Cleared hypotheses: l1, l2, h