awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n : ℕ
hxy : x ≠ 0 ∨ n + 1 ≠ 0
succ :
  (x + (b + 2) * (n + 1)) % (b + 2) :: (b + 2).digitsAux ⋯ ((x + (b + 2) * (n + 1)) / (b + 2)) =
    x :: (b + 2).digitsAux ⋯ (n + 1)
succ₁ : 0 < x + (b + 2) * (n + 1)
⊢ (b + 2).digitsAux ⋯ (x + (b + 2) * (n + 1)) = x :: (b + 2).digitsAux ⋯ (n + 1)

Tactic:
rw [digitsAux_def]

Premises used: Nat.digitsAux_def
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n : ℕ
hxy : x ≠ 0 ∨ n + 1 ≠ 0
succ : (x + (b + 2) * (n + 1)) % (b + 2) = x
succ₁ : (x + (b + 2) * (n + 1)) / (b + 2) = n + 1
⊢ (x + (b + 2) * (n + 1)) % (b + 2) :: (b + 2).digitsAux ⋯ ((x + (b + 2) * (n + 1)) / (b + 2)) =
    x :: (b + 2).digitsAux ⋯ (n + 1)

Tactic:
congr
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n : ℕ
hxy : x ≠ 0 ∨ n + 1 ≠ 0
⊢ (x + (b + 2) * (n + 1)) % (b + 2) = x

Tactic:
simp [Nat.add_mod, mod_eq_of_lt hxb]

Premises used: Nat.mod_eq_of_lt, Nat.add_mod
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n : ℕ
hxy : x ≠ 0 ∨ n + 1 ≠ 0
⊢ (x + (b + 2) * (n + 1)) / (b + 2) = n + 1

Tactic:
simp [add_mul_div_left, div_eq_of_lt hxb]

Premises used: Nat.div_eq_of_lt, Nat.add_mul_div_left
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n : ℕ
hxy : x ≠ 0 ∨ n + 1 ≠ 0
⊢ 0 < x + (b + 2) * (n + 1)

Tactic:
apply Nat.succ_pos

Premises used: Nat.succ_pos
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
α : Type u_1
inst : Semiring α
b : α
⊢ ofDigits b [] = List.foldr (fun (x : ℕ) (y : α) ↦ (↑x : α) + b * y) 0 []

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
α : Type u_1
inst : Semiring α
b : α
d : ℕ
L : List ℕ
ih : ofDigits b L = List.foldr (fun (x : ℕ) (y : α) ↦ (↑x : α) + b * y) 0 L
cons : (↑d : α) + b * ofDigits b L = (↑d : α) + b * List.foldr (fun (x : ℕ) (y : α) ↦ (↑x : α) + b * y) 0 L
⊢ ofDigits b (d :: L) = List.foldr (fun (x : ℕ) (y : α) ↦ (↑x : α) + b * y) 0 (d :: L)

Tactic:
dsimp [ofDigits]

Premises used: Nat.ofDigits
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
α : Type u_1
inst : Semiring α
b : α
d : ℕ
L : List ℕ
ih : ofDigits b L = List.foldr (fun (x : ℕ) (y : α) ↦ (↑x : α) + b * y) 0 L
cons cons₁ :
  (↑d : α) + b * List.foldr (fun (x : ℕ) (y : α) ↦ (↑x : α) + b * y) 0 L =
    (↑d : α) + b * List.foldr (fun (x : ℕ) (y : α) ↦ (↑x : α) + b * y) 0 L
⊢ (↑d : α) + b * ofDigits b L = (↑d : α) + b * List.foldr (fun (x : ℕ) (y : α) ↦ (↑x : α) + b * y) 0 L

Tactic:
rw [ih]
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
α : Type u_1
inst : Semiring α
b : α
L : List ℕ
nil : ofDigits b [] = List.foldr (fun (x : ℕ) (y : α) ↦ (↑x : α) + b * y) 0 []
cons :
  ∀ (d : ℕ) (L : List ℕ) (ih : ofDigits b L = List.foldr (fun (x : ℕ) (y : α) ↦ (↑x : α) + b * y) 0 L),
    ofDigits b (d :: L) = List.foldr (fun (x : ℕ) (y : α) ↦ (↑x : α) + b * y) 0 (d :: L)
⊢ ofDigits b L = List.foldr (fun (x : ℕ) (y : α) ↦ (↑x : α) + b * y) 0 L

Tactic:
induction L with
  | nil => rfl
  | cons d L ih => dsimp [ofDigits]; rw [ih]

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

Tactic:
rfl

Premises used: Nat.ofDigits, rfl
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b n : ℕ
⊢ ofDigits b [n] = n

Tactic:
simp [ofDigits]

Premises used: Nat.ofDigits
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
α : Type u_1
inst : Semiring α
h : ℕ
L : List ℕ
⊢ ofDigits 1 (h :: L) = HAdd.hAdd (α := α) (↑h : α) (ofDigits 1 L)

Tactic:
simp [ofDigits]

Premises used: Nat.ofDigits
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b hd : ℕ
tl : List ℕ
⊢ ofDigits b (hd :: tl) = hd + b * ofDigits b tl

Tactic:
rfl

Premises used: Nat.ofDigits, rfl
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
l2 : List ℕ
⊢ ofDigits b ([] ++ l2) = ofDigits b [] + b ^ List.length (α := ℕ) [] * ofDigits b l2

Tactic:
simp [ofDigits]

Premises used: Nat.ofDigits
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
l2 : List ℕ
hd : ℕ
tl : List ℕ
IH : ofDigits b (tl ++ l2) = ofDigits b tl + b ^ tl.length * ofDigits b l2
cons :
  (↑hd : ℕ) + b * (ofDigits b tl + b ^ tl.length * ofDigits b l2) =
    (↑hd : ℕ) + b * ofDigits b tl + b * b ^ tl.length * ofDigits b l2
⊢ ofDigits b (hd :: tl ++ l2) = ofDigits b (hd :: tl) + b ^ (hd :: tl).length * ofDigits b l2

Tactic:
rw [ofDigits, List.cons_append, ofDigits, IH, List.length_cons, pow_succ']

Premises used: Nat.pow_succ', List.length_cons, Nat.ofDigits, List.cons_append
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
l2 : List ℕ
hd : ℕ
tl : List ℕ
IH : ofDigits b (tl ++ l2) = ofDigits b tl + b ^ tl.length * ofDigits b l2
⊢ (↑hd : ℕ) + b * (ofDigits b tl + b ^ tl.length * ofDigits b l2) =
    (↑hd : ℕ) + b * ofDigits b tl + b * b ^ tl.length * ofDigits b l2

Tactic:
ring
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
l1 l2 : List ℕ
nil : ofDigits b ([] ++ l2) = ofDigits b [] + b ^ List.length (α := ℕ) [] * ofDigits b l2
cons :
  ∀ (hd : ℕ) (tl : List ℕ) (IH : ofDigits b (tl ++ l2) = ofDigits b tl + b ^ tl.length * ofDigits b l2),
    ofDigits b (hd :: tl ++ l2) = ofDigits b (hd :: tl) + b ^ (hd :: tl).length * ofDigits b l2
⊢ ofDigits b (l1 ++ l2) = ofDigits b l1 + b ^ l1.length * ofDigits b l2

Tactic:
induction l1 with
  | nil => simp [ofDigits]
  | cons hd tl IH =>
    rw [ofDigits, List.cons_append, ofDigits, IH, List.length_cons, pow_succ']
    ring

Premises used: Nat.pow_succ', List.length_cons, Nat.ofDigits, List.cons_append
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
l : List ℕ
rw : ofDigits b l + b ^ l.length * ofDigits b [0] = ofDigits b l
rw₁ : ofDigits b l + b ^ l.length * 0 = ofDigits b l
rw₂ : ofDigits b l + 0 = ofDigits b l
rw₃ rw₄ : ofDigits b l = ofDigits b l
⊢ ofDigits b (l ++ [0]) = ofDigits b l

Tactic:
rw [ofDigits_append, ofDigits_singleton, mul_zero, add_zero]

Premises used: MulZeroClass.mul_zero, Nat.ofDigits_append, Nat.ofDigits_singleton, add_zero
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
⊢ ofDigits b (List.replicate 0 0) = 0

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b k : ℕ
ih : ofDigits b (List.replicate k 0) = 0
⊢ ofDigits b (List.replicate (k + 1) 0) = 0

Tactic:
simp [List.replicate, ofDigits_cons, ih]

Premises used: List.replicate, Nat.ofDigits_cons
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b k : ℕ
zero : ofDigits b (List.replicate 0 0) = 0
succ : ∀ (k : ℕ) (ih : ofDigits b (List.replicate k 0) = 0), ofDigits b (List.replicate (k + 1) 0) = 0
⊢ ofDigits b (List.replicate k 0) = 0

Tactic:
induction k with
  | zero => rfl
  | succ k ih => simp [List.replicate, ofDigits_cons, ih]

Premises used: List.replicate, Nat.ofDigits_cons, Nat.zero, Nat.succ
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b k : ℕ
l : List ℕ
rw : ofDigits b l + b ^ l.length * ofDigits b (List.replicate k 0) = ofDigits b l
⊢ ofDigits b (l ++ List.replicate k 0) = ofDigits b l

Tactic:
rw [ofDigits_append]

Premises used: Nat.ofDigits_append
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b k : ℕ
l : List ℕ
⊢ ofDigits b l + b ^ l.length * ofDigits b (List.replicate k 0) = ofDigits b l

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
l : List ℕ
d : ℕ
simp : ofDigits b (l.reverse ++ [d]) = ofDigits b l.reverse + b ^ l.length * d
⊢ ofDigits b (d :: l).reverse = ofDigits b l.reverse + b ^ l.length * d

Tactic:
simp only [List.reverse_cons]

Premises used: List.reverse_cons
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
l : List ℕ
d : ℕ
rw : ofDigits b l.reverse + b ^ l.reverse.length * ofDigits b [d] = ofDigits b l.reverse + b ^ l.length * d
⊢ ofDigits b (l.reverse ++ [d]) = ofDigits b l.reverse + b ^ l.length * d

Tactic:
rw [ofDigits_append]

Premises used: Nat.ofDigits_append
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
l : List ℕ
d : ℕ
⊢ ofDigits b l.reverse + b ^ l.reverse.length * ofDigits b [d] = ofDigits b l.reverse + b ^ l.length * d

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
l : List ℕ
⊢ ofDigits b (0 :: l).reverse = ofDigits b l.reverse

Tactic:
simp only [List.reverse_cons, ofDigits_append_zero]

Premises used: Nat.ofDigits_append_zero, List.reverse_cons
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
α : Type u_1
inst : Semiring α
b : ℕ
⊢ Eq.{u_1 + 1} (α := α) (↑(ofDigits b []) : α) (ofDigits (↑b : α) [])

Tactic:
simp [ofDigits]

Premises used: Nat.ofDigits
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
α : Type u_1
inst : Semiring α
b d : ℕ
L : List ℕ
ih : Eq.{u_1 + 1} (α := α) (↑(ofDigits b L) : α) (ofDigits (↑b : α) L)
cons : (↑(d + b * ofDigits b L) : α) = (↑d : α) + HMul.hMul (α := α) (↑b : α) (ofDigits (↑b : α) L)
⊢ Eq.{u_1 + 1} (α := α) (↑(ofDigits b (d :: L)) : α) (ofDigits (↑b : α) (d :: L))

Tactic:
dsimp [ofDigits]

Premises used: Nat.ofDigits
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
α : Type u_1
inst : Semiring α
b d : ℕ
L : List ℕ
ih : Eq.{u_1 + 1} (α := α) (↑(ofDigits b L) : α) (ofDigits (↑b : α) L)
cons :
  (↑d : α) + HMul.hMul (α := α) (↑b : α) (↑(ofDigits b L) : α) =
    (↑d : α) + HMul.hMul (α := α) (↑b : α) (ofDigits (↑b : α) L)
⊢ (↑(d + b * ofDigits b L) : α) = (↑d : α) + HMul.hMul (α := α) (↑b : α) (ofDigits (↑b : α) L)

Tactic:
push_cast
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
α : Type u_1
inst : Semiring α
b d : ℕ
L : List ℕ
ih : Eq.{u_1 + 1} (α := α) (↑(ofDigits b L) : α) (ofDigits (↑b : α) L)
cons cons₁ :
  (↑d : α) + HMul.hMul (α := α) (↑b : α) (ofDigits (↑b : α) L) =
    (↑d : α) + HMul.hMul (α := α) (↑b : α) (ofDigits (↑b : α) L)
⊢ (↑d : α) + HMul.hMul (α := α) (↑b : α) (↑(ofDigits b L) : α) =
    (↑d : α) + HMul.hMul (α := α) (↑b : α) (ofDigits (↑b : α) L)

Tactic:
rw [ih]
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
α : Type u_1
inst : Semiring α
b : ℕ
L : List ℕ
nil : Eq.{u_1 + 1} (α := α) (↑(ofDigits b []) : α) (ofDigits (↑b : α) [])
cons :
  ∀ (d : ℕ) (L : List ℕ) (ih : Eq.{u_1 + 1} (α := α) (↑(ofDigits b L) : α) (ofDigits (↑b : α) L)),
    Eq.{u_1 + 1} (α := α) (↑(ofDigits b (d :: L)) : α) (ofDigits (↑b : α) (d :: L))
⊢ Eq.{u_1 + 1} (α := α) (↑(ofDigits b L) : α) (ofDigits (↑b : α) L)

Tactic:
induction L with
  | nil => simp [ofDigits]
  | cons d L ih => dsimp [ofDigits]; push_cast; rw [ih]

Premises used: Nat.ofDigits
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 1 < b
w₁ : ∀ (l : ℕ), Membership.mem (γ := List ℕ) [] l → l < b
w₂ : ∀ (h : Ne (α := List ℕ) [] []), List.getLast [] h ≠ 0
⊢ b.digits (ofDigits b []) = []

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 1 < b
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
cons : b.digits (d + b * ofDigits b L) = d :: L
⊢ b.digits (ofDigits b (d :: L)) = d :: L

Tactic:
dsimp [ofDigits]

Premises used: Nat.ofDigits
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 1 < b
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
⊢ d :: L ≠ []

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 1 < b
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
⊢ (d :: L).getLast ⋯ ≠ 0

Tactic:
replace w₂ := w₂ (by simp)
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 1 < b
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₂ : (d :: L).getLast ⋯ ≠ 0
cons : d :: b.digits (ofDigits b L) = d :: L
cons₁ : d < b
cons₂ : d ≠ 0 ∨ ofDigits b L ≠ 0
⊢ b.digits (d + b * ofDigits b L) = d :: L

Tactic:
rw [digits_add b h]

Premises used: Nat.digits_add
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 1 < b
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₂ : (d :: L).getLast ⋯ ≠ 0
cons : ∀ l ∈ L, l < b
cons₁ : ∀ (h : L ≠ []), L.getLast h ≠ 0
⊢ d :: b.digits (ofDigits b L) = d :: L

Tactic:
rw [ih]
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 1 < b
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₂ : (d :: L).getLast ⋯ ≠ 0
l : ℕ
m : l ∈ L
cons : l ∈ d :: L
⊢ l < b

Tactic:
apply w₁
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 1 < b
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₂ : (d :: L).getLast ⋯ ≠ 0
l : ℕ
m : l ∈ L
⊢ l ∈ d :: L

Tactic:
List.mem_cons_of_mem _ m

Premises used: List.mem_cons_of_mem
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 1 < b
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₂ : (d :: L).getLast ⋯ ≠ 0
l : ℕ
m : l ∈ L
⊢ l ∈ d :: L

Tactic:
exact List.mem_cons_of_mem _ m

Premises used: List.mem_cons_of_mem
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h_1 : 1 < b
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₂ : (d :: L).getLast ⋯ ≠ 0
h : L ≠ []
⊢ L.getLast h ≠ 0

Tactic:
rw [List.getLast_cons h] at w₂

Premises used: List.getLast_cons
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h_1 : 1 < b
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
h : L ≠ []
w₂ : L.getLast h ≠ 0
⊢ L.getLast h ≠ 0

Tactic:
w₂
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h_1 : 1 < b
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
h : L ≠ []
w₂ : L.getLast h ≠ 0
⊢ L.getLast h ≠ 0

Tactic:
convert! w₂
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 1 < b
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₂ : (d :: L).getLast ⋯ ≠ 0
⊢ d < b

Tactic:
w₁ d List.mem_cons_self

Premises used: List.mem_cons_self
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 1 < b
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₂ : (d :: L).getLast ⋯ ≠ 0
⊢ d < b

Tactic:
exact w₁ d List.mem_cons_self

Premises used: List.mem_cons_self
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 1 < b
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₂ : (d :: L).getLast ⋯ ≠ 0
pos : ∀ (h' : L = []), d ≠ 0 ∨ ofDigits b L ≠ 0
neg : ∀ (h' : ¬L = []), d ≠ 0 ∨ ofDigits b L ≠ 0
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0

Tactic:
by_cases h' : L = []
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 1 < b
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₂ : (d :: L).getLast ⋯ ≠ 0
h' : L = []
pos :
  ∀
    (ih :
      ∀ (w₁ : ∀ (l : ℕ), Membership.mem (γ := List ℕ) [] l → l < b)
        (w₂ : ∀ (h : Ne (α := List ℕ) [] []), List.getLast [] h ≠ 0), b.digits (ofDigits b []) = [])
    (w₁ : ∀ l ∈ [d], l < b) (w₂ : [d].getLast ⋯ ≠ 0), d ≠ 0 ∨ ofDigits b [] ≠ 0
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0

Tactic:
rcases h' with rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 1 < b
d : ℕ
ih :
  ∀ (w₁ : ∀ (l : ℕ), Membership.mem (γ := List ℕ) [] l → l < b)
    (w₂ : ∀ (h : Ne (α := List ℕ) [] []), List.getLast [] h ≠ 0), b.digits (ofDigits b []) = []
w₁ : ∀ l ∈ [d], l < b
w₂ : [d].getLast ⋯ ≠ 0
pos : d ≠ 0
⊢ d ≠ 0 ∨ ofDigits b [] ≠ 0

Tactic:
left
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 1 < b
d : ℕ
ih :
  ∀ (w₁ : ∀ (l : ℕ), Membership.mem (γ := List ℕ) [] l → l < b)
    (w₂ : ∀ (h : Ne (α := List ℕ) [] []), List.getLast [] h ≠ 0), b.digits (ofDigits b []) = []
w₁ : ∀ l ∈ [d], l < b
w₂ : [d].getLast ⋯ ≠ 0
⊢ d ≠ 0

Tactic:
simpa using w₂
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 1 < b
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₂ : (d :: L).getLast ⋯ ≠ 0
h' : ¬L = []
neg : ofDigits b L ≠ 0
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0

Tactic:
right
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 1 < b
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₂ : (d :: L).getLast ⋯ ≠ 0
h' : ¬L = []
neg : ∀ (w₂ : ofDigits b L = 0), (d :: L).getLast ⋯ = 0
⊢ ofDigits b L ≠ 0

Tactic:
contrapose w₂
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 1 < b
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
h' : ¬L = []
w₂ : ofDigits b L = 0
⊢ (d :: L).getLast ⋯ = 0

Tactic:
digits_zero_of_eq_zero h.ne_bot w₂ _ ?_

Premises used: Nat.digits_zero_of_eq_zero, LT.lt.ne_bot
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 1 < b
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
h' : ¬L = []
w₂ : ofDigits b L = 0
neg : (d :: L).getLast ⋯ ∈ L
⊢ (d :: L).getLast ⋯ = 0

Tactic:
refine digits_zero_of_eq_zero h.ne_bot w₂ _ ?_

Premises used: Nat.digits_zero_of_eq_zero, LT.lt.ne_bot
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 1 < b
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
h' : ¬L = []
w₂ : ofDigits b L = 0
neg : L.getLast h' ∈ L
⊢ (d :: L).getLast ⋯ ∈ L

Tactic:
rw [List.getLast_cons h']

Premises used: List.getLast_cons
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 1 < b
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
h' : ¬L = []
w₂ : ofDigits b L = 0
⊢ L.getLast h' ∈ L

Tactic:
List.getLast_mem h'

Premises used: List.getLast_mem
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : 1 < b
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
h' : ¬L = []
w₂ : ofDigits b L = 0
⊢ L.getLast h' ∈ L

Tactic:
exact List.getLast_mem h'

Premises used: List.getLast_mem
-- Module: Mathlib.Data.Nat.Digits.Defs
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 []) = []
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
⊢ b.digits (ofDigits b L) = 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'

Premises used: Nat.ofDigits, Nat.digits_add, rfl
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b n : ℕ
zero : ofDigits 0 (digits 0 n) = n
succ : ∀ (b : ℕ), ofDigits (b + 1) ((b + 1).digits n) = n
⊢ ofDigits b (b.digits n) = n

Tactic:
rcases b with - | b
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n : ℕ
zero : Eq (α := ℕ) (ofDigits 0 (digits 0 0)) 0
zero₁ : ∀ (n : ℕ), ofDigits 0 (digits 0 (n + 1)) = n + 1
⊢ ofDigits 0 (digits 0 n) = n

Tactic:
rcases n with - | n
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
⊢ Eq (α := ℕ) (ofDigits 0 (digits 0 0)) 0

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n : ℕ
⊢ ofDigits 0 (digits 0 (n + 1)) = n + 1

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n b : ℕ
succ : ofDigits (HAdd.hAdd (α := ℕ) 0 1) ((HAdd.hAdd (α := ℕ) 0 1).digits n) = n
succ₁ : ∀ (b : ℕ), ofDigits (b + 1 + 1) ((b + 1 + 1).digits n) = n
⊢ ofDigits (b + 1) ((b + 1).digits n) = n

Tactic:
rcases b with - | b
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
⊢ ofDigits (HAdd.hAdd (α := ℕ) 0 1) ((HAdd.hAdd (α := ℕ) 0 1).digits 0) = 0

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n : ℕ
ih : ofDigits (HAdd.hAdd (α := ℕ) 0 1) ((HAdd.hAdd (α := ℕ) 0 1).digits n) = n
⊢ ofDigits 1 (digits 1 n) = n

Tactic:
rw [Nat.zero_add] at ih ⊢

Premises used: Nat.zero_add
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n : ℕ
ih : ofDigits 1 (digits 1 n) = n
⊢ ofDigits 1 (digits 1 (n + 1)) = n + 1

Tactic:
simp only [ih, add_comm 1, ofDigits_one_cons, Nat.cast_id, digits_one_succ]

Premises used: Nat.cast_id, Nat.ofDigits_one_cons, add_comm, Nat.digits_one_succ, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n : ℕ
succ : ofDigits (HAdd.hAdd (α := ℕ) 0 1) ((HAdd.hAdd (α := ℕ) 0 1).digits 0) = 0
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
⊢ ofDigits (HAdd.hAdd (α := ℕ) 0 1) ((HAdd.hAdd (α := ℕ) 0 1).digits n) = n

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]

Premises used: Nat.cast_id, Nat.ofDigits_one_cons, add_comm, Nat.digits_one_succ, Nat.zero, Nat.zero_add, OfNat.ofNat, Nat.succ
-- Module: Mathlib.Data.Nat.Digits.Defs
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

Tactic:
?_
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
n b : ℕ
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
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits n) = n

Tactic:
induction n using Nat.strongRecOn with | ind n h => ?_
-- Module: Mathlib.Data.Nat.Digits.Defs
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
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
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits n) = n

Tactic:
cases n
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b : ℕ
h : ∀ m < 0, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) [] = 0

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b n : ℕ
h : ∀ m < n + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
succ : ofDigits (b + 1 + 1) ((n + 1) % (b + 2) :: (b + 2).digits ((n + 1) / (b + 2))) = n + 1
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits (n + 1)) = n + 1

Tactic:
simp only [digits_add_two_add_one]

Premises used: Nat.digits_add_two_add_one
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b n : ℕ
h : ∀ m < n + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
succ : (n + 1) % (b + 2) + (b + 1 + 1) * ((n + 1) / (b + 2)) = n + 1
⊢ (n + 1) % (b + 2) + (b + 1 + 1) * ofDigits (b + 1 + 1) ((b + 2).digits ((n + 1) / (b + 2))) = n + 1

Tactic:
rw [h _ (Nat.div_lt_self' _ b)]

Premises used: Nat.div_lt_self'
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
b n : ℕ
h : ∀ m < n + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
succ succ₁ : n + 1 = n + 1
⊢ (n + 1) % (b + 2) + (b + 1 + 1) * ((n + 1) / (b + 2)) = n + 1

Tactic:
rw [Nat.mod_add_div]

Premises used: Nat.mod_add_div
-- Module: Mathlib.Data.Nat.Digits.Defs
Goal:
⊢ Eq (α := ℕ) (ofDigits 1 []) (List.sum [])

Tactic:
rfl