awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
rw : n ≡ ofDigits 1 (b'.digits n) [MOD b]
⊢ n ≡ (b'.digits n).sum [MOD b]

Tactic:
rw [← ofDigits_one]

Premises used: Nat.ofDigits_one
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
n₁ : b
a : n
b₁ : ofDigits 1 (b'.digits n)
| n ≡ ofDigits 1 (b'.digits n) [MOD b]

Tactic:
congr
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
| b

Tactic:
· skip
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
a : ofDigits b' (b'.digits n)
| n

Tactic:
rw [← ofDigits_digits b' n]

Premises used: Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
| n

Tactic:
· rw [← ofDigits_digits b' n]

Premises used: Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
b₁ : ofDigits 1 (b'.digits n)
| n ≡ ofDigits 1 (b'.digits n) [MOD b]

Tactic:
congr
    · skip
    · rw [← ofDigits_digits b' n]

Premises used: Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
conv : ofDigits b' (b'.digits n) ≡ ofDigits 1 (b'.digits n) [MOD b]
⊢ n ≡ ofDigits 1 (b'.digits n) [MOD b]

Tactic:
conv =>
    congr
    · skip
    · rw [← ofDigits_digits b' n]

Premises used: Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ ofDigits b' (b'.digits n) ≡ ofDigits (b' % b) (b'.digits n) [MOD b]

Tactic:
ofDigits_modEq b' b (digits b' n)

Premises used: Nat.digits, Nat.ofDigits_modEq
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
h₁ : 1 = b' % b
⊢ ofDigits b' (b'.digits n) ≡ ofDigits 1 (b'.digits n) [MOD b]

Tactic:
convert! ofDigits_modEq b' b (digits b' n)

Premises used: Nat.digits, Nat.ofDigits_modEq
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ 1 = b' % b

Tactic:
h.symm

Premises used: Eq.symm
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ 1 = b' % b

Tactic:
exact h.symm

Premises used: Eq.symm
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' : ℕ
c : ℤ
h : (↑b' : ℤ) ≡ c [ZMOD (↑b : ℤ)]
n : ℕ
n₁ : (↑b : ℤ)
a : (↑n : ℤ)
b₁ : ofDigits c (b'.digits n)
| (↑n : ℤ) ≡ ofDigits c (b'.digits n) [ZMOD (↑b : ℤ)]

Tactic:
congr
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' : ℕ
c : ℤ
h : (↑b' : ℤ) ≡ c [ZMOD (↑b : ℤ)]
n : ℕ
| (↑b : ℤ)

Tactic:
· skip
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' : ℕ
c : ℤ
h : (↑b' : ℤ) ≡ c [ZMOD (↑b : ℤ)]
n : ℕ
a : (↑(ofDigits b' (b'.digits n)) : ℤ)
| (↑n : ℤ)

Tactic:
rw [← ofDigits_digits b' n]

Premises used: Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' : ℕ
c : ℤ
h : (↑b' : ℤ) ≡ c [ZMOD (↑b : ℤ)]
n : ℕ
| (↑n : ℤ)

Tactic:
· rw [← ofDigits_digits b' n]

Premises used: Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' : ℕ
c : ℤ
h : (↑b' : ℤ) ≡ c [ZMOD (↑b : ℤ)]
n : ℕ
b₁ : ofDigits c (b'.digits n)
| (↑n : ℤ) ≡ ofDigits c (b'.digits n) [ZMOD (↑b : ℤ)]

Tactic:
congr
    · skip
    · rw [← ofDigits_digits b' n]

Premises used: Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' : ℕ
c : ℤ
h : (↑b' : ℤ) ≡ c [ZMOD (↑b : ℤ)]
n : ℕ
conv : (↑(ofDigits b' (b'.digits n)) : ℤ) ≡ ofDigits c (b'.digits n) [ZMOD (↑b : ℤ)]
⊢ (↑n : ℤ) ≡ ofDigits c (b'.digits n) [ZMOD (↑b : ℤ)]

Tactic:
conv =>
    congr
    · skip
    · rw [← ofDigits_digits b' n]

Premises used: Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' : ℕ
c : ℤ
h : (↑b' : ℤ) ≡ c [ZMOD (↑b : ℤ)]
n : ℕ
rw : ofDigits (↑b' : ℤ) (b'.digits n) ≡ ofDigits c (b'.digits n) [ZMOD (↑b : ℤ)]
⊢ (↑(ofDigits b' (b'.digits n)) : ℤ) ≡ ofDigits c (b'.digits n) [ZMOD (↑b : ℤ)]

Tactic:
rw [coe_ofDigits]

Premises used: Nat.coe_ofDigits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b b' : ℕ
c : ℤ
h : (↑b' : ℤ) ≡ c [ZMOD (↑b : ℤ)]
n : ℕ
⊢ ofDigits (↑b' : ℤ) (b'.digits n) ≡ ofDigits c (b'.digits n) [ZMOD (↑b : ℤ)]

Tactic:
apply ofDigits_zmodeq' _ _ _ h

Premises used: Nat.ofDigits_zmodeq'
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
n : ℕ
⊢ Eq (α := ℤ) (ofDigits (-1) [n]) (List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) [n]))

Tactic:
simp [ofDigits, List.alternatingSum]

Premises used: Nat.ofDigits, List.alternatingSum
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
a b : ℕ
t : List ℕ
simp :
  (↑a : ℤ) + -1 * ((↑b : ℤ) + HMul.hMul (α := ℤ) (-1) (List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) t))) =
    HAdd.hAdd (α := ℤ) (↑a : ℤ) (-(↑b : ℤ)) + List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) t)
⊢ Eq (α := ℤ) (ofDigits (-1) (a :: b :: t)) (List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (a :: b :: t)))

Tactic:
simp only [ofDigits, List.alternatingSum, List.map_cons, ofDigits_neg_one t]

Premises used: List.map_cons, Nat.ofDigits, List.alternatingSum
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
a b : ℕ
t : List ℕ
⊢ (↑a : ℤ) + -1 * ((↑b : ℤ) + HMul.hMul (α := ℤ) (-1) (List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) t))) =
    HAdd.hAdd (α := ℤ) (↑a : ℤ) (-(↑b : ℤ)) + List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) t)

Tactic:
ring
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
n i b : ℕ
h : 2 ≤ b
obtain : ∀ (b : ℕ) (h : 2 ≤ b + 2), ((b + 2).digits n).getD i 0 = n / (b + 2) ^ i % (b + 2)
⊢ (b.digits n).getD i 0 = n / b ^ i % b

Tactic:
obtain ⟨b, rfl⟩ := Nat.exists_eq_add_of_le' h

Premises used: Nat.exists_eq_add_of_le', rfl
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b i : ℕ
⊢ (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits 0) i).getD 0 =
    0 / (b + 2) ^ i % (b + 2)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b n : ℕ
IH :
  ∀ m ≤ n,
    ∀ (i : ℕ),
      (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits m) i).getD 0 =
        m / (b + 2) ^ i % (b + 2)
i : ℕ
ind :
  (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits n.succ) 0).getD 0 =
    n.succ / HPow.hPow (β := ℕ) (b + 2) 0 % (b + 2)
ind₁ :
  ∀ (i : ℕ),
    (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits n.succ) (i + 1)).getD 0 =
      n.succ / (b + 2) ^ (i + 1) % (b + 2)
⊢ (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits n.succ) i).getD 0 =
    n.succ / (b + 2) ^ i % (b + 2)

Tactic:
rcases i with _ | i
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b n : ℕ
IH :
  ∀ m ≤ n,
    ∀ (i : ℕ),
      (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits m) i).getD 0 =
        m / (b + 2) ^ i % (b + 2)
⊢ b + 2 ≠ 1

Tactic:
grind
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b n : ℕ
IH :
  ∀ m ≤ n,
    ∀ (i : ℕ),
      (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits m) i).getD 0 =
        m / (b + 2) ^ i % (b + 2)
ind : n.succ % (b + 2) = n.succ / HPow.hPow (β := ℕ) (b + 2) default % (b + 2)
⊢ (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits n.succ) 0).getD 0 =
    n.succ / HPow.hPow (β := ℕ) (b + 2) 0 % (b + 2)

Tactic:
rw [← List.head?_eq_getElem?, ← default_eq_zero, ← List.head!_eq_head?_getD,
        head!_digits (by grind)]

Premises used: List.head?_eq_getElem?, List.head!_eq_head?_getD, Nat.head!_digits, Nat.default_eq_zero
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b n : ℕ
IH :
  ∀ m ≤ n,
    ∀ (i : ℕ),
      (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits m) i).getD 0 =
        m / (b + 2) ^ i % (b + 2)
⊢ n.succ % (b + 2) = n.succ / HPow.hPow (β := ℕ) (b + 2) default % (b + 2)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b n : ℕ
IH :
  ∀ m ≤ n,
    ∀ (i : ℕ),
      (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits m) i).getD 0 =
        m / (b + 2) ^ i % (b + 2)
i : ℕ
⊢ (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits n.succ) (i + 1)).getD 0 =
    n.succ / (b + 2) ^ (i + 1) % (b + 2)

Tactic:
simp [IH _ (le_of_lt_succ (div_lt_self' n b)), pow_succ', Nat.div_div_eq_div_mul]

Premises used: Nat.pow_succ', Nat.div_lt_self', Nat.le_of_lt_succ, Nat.div_div_eq_div_mul
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
n i b : ℕ
zero :
  ∀ (i : ℕ),
    (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits 0) i).getD 0 =
      0 / (b + 2) ^ i % (b + 2)
ind :
  ∀ (n : ℕ)
    (IH :
      ∀ m ≤ n,
        ∀ (i : ℕ),
          (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits m) i).getD 0 =
            m / (b + 2) ^ i % (b + 2))
    (i : ℕ),
    (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits n.succ) i).getD 0 =
      n.succ / (b + 2) ^ i % (b + 2)
⊢ (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) ((b + 2).digits n) i).getD 0 =
    n / (b + 2) ^ i % (b + 2)

Tactic:
induction n using Nat.caseStrongRecOn generalizing i with
  | zero => simp
  | ind n IH =>
    rcases i with _ | i
    · rw [← List.head?_eq_getElem?, ← default_eq_zero, ← List.head!_eq_head?_getD,
        head!_digits (by grind)]
      simp
    · simp [IH _ (le_of_lt_succ (div_lt_self' n b)), pow_succ', Nat.div_div_eq_div_mul]

Premises used: Nat.pow_succ', List.head?_eq_getElem?, List.head!_eq_head?_getD, Nat.zero, Nat.head!_digits, Nat.default_eq_zero, Nat.div_div_eq_div_mul
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
n b : ℕ
hb : 1 < b
l : ℕ
hn : n < b ^ l
rw : (b.digits n).length ≤ l
⊢ (b.digitsAppend l n).length = l

Tactic:
rw [digitsAppend, length_append, length_replicate, Nat.add_sub_cancel']

Premises used: Nat.digitsAppend, List.length_append, List.length_replicate, Nat.add_sub_cancel'
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
n b : ℕ
hb : 1 < b
l : ℕ
hn rwa rwa₁ rwa₂ rwa₃ : n < b ^ l
⊢ (b.digits n).length ≤ l

Tactic:
rwa [digits_length_le_iff hb]

Premises used: Nat.digits_length_le_iff
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
n b : ℕ
hb : 1 < b
l i : ℕ
hi : i ∈ b.digitsAppend l n
⊢ i ∈ b.digits n ∨ l - (b.digits n).length ≠ 0 ∧ i = 0

Tactic:
rw [digitsAppend, mem_append, mem_replicate] at hi

Premises used: Nat.digitsAppend, List.mem_append, List.mem_replicate
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
n b : ℕ
hb : 1 < b
l i : ℕ
hi : i ∈ b.digits n ∨ l - (b.digits n).length ≠ 0 ∧ i = 0
inl : ∀ (hi : i ∈ b.digits n), i < b
inr : l - (b.digits n).length ≠ 0 → 0 < b
⊢ i < b

Tactic:
obtain hi | ⟨_, rfl⟩ := hi

Premises used: rfl
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
n b : ℕ
hb : 1 < b
l i : ℕ
hi : i ∈ b.digits n
⊢ i < b

Tactic:
digits_lt_base hb hi

Premises used: Nat.digits_lt_base
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
n b : ℕ
hb : 1 < b
l i : ℕ
hi : i ∈ b.digits n
⊢ i < b

Tactic:
exact digits_lt_base hb hi

Premises used: Nat.digits_lt_base
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
n b : ℕ
hb : 1 < b
l : ℕ
left : l - (b.digits n).length ≠ 0
linarith : b ≤ 0 → HMul.hMul (α := ℤ) 2 (-1) + (HAdd.hAdd (α := ℤ) 1 1 - (↑b : ℤ)) + HSub.hSub (α := ℤ) (↑b : ℤ) 0 = 0
linarith₁ : b ≤ 0 → GT.gt (α := ℤ) 2 0
⊢ 0 < b

Tactic:
linarith
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.MapsTo (ofDigits b) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} {n : ℕ | n < b ^ l}

Tactic:
fun _ h ↦ Set.mem_setOf.mpr h.1 ▸ Nat.ofDigits_lt_base_pow_length hb h.2

Premises used: Iff.mpr, Nat.ofDigits_lt_base_pow_length, Eq.rec, Set.mem_setOf, And.right, And.left, Set.MapsTo
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l x : ℕ
h : Membership.mem (γ := Set ℕ) {n : ℕ | n < b ^ l} x
rw rw₁ : l = l
⊢ (b.digitsAppend l x).length = l

Tactic:
rw [length_digitsAppend hb _ h]

Premises used: Nat.length_digitsAppend
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
x : List ℕ
h_1 : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} x
x_1 : List ℕ
h_2 : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} x_1
h : ofDigits b x = ofDigits b x_1
⊢ x.length = x_1.length

Tactic:
simp_all
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
x : List ℕ
h_1 : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} x
x_1 : List ℕ
h_2 : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} x_1
h : ofDigits b x = ofDigits b x_1
⊢ ∀ l ∈ x, l < b

Tactic:
simp_all
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
x : List ℕ
h_1 : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} x
x_1 : List ℕ
h_2 : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} x_1
h : ofDigits b x = ofDigits b x_1
⊢ ∀ l ∈ x_1, l < b

Tactic:
simp_all
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l x : ℕ
h : Membership.mem (γ := Set ℕ) {n : ℕ | n < b ^ l} x
rw : ofDigits b (b.digits x ++ replicate (l - (b.digits x).length) 0) = x
rw₁ : ofDigits b (b.digits x) = x
rw₂ rw₃ : x = x
⊢ ofDigits b (b.digitsAppend l x) = x

Tactic:
rw [digitsAppend, ofDigits_append_replicate_zero,
    ofDigits_digits]

Premises used: Nat.digitsAppend, Nat.ofDigits_append_replicate_zero, Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
refine :
  ∀ (L : List ℕ) (hL : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} L),
    b.digitsAppend l (ofDigits b L) = L
⊢ Set.InvOn (b.digitsAppend l) (ofDigits b) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} {n : ℕ | n < b ^ l}

Tactic:
refine ⟨fun L hL ↦ ?_, fun _ _ ↦ by rw [digitsAppend, ofDigits_append_replicate_zero,
    ofDigits_digits]⟩
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} L
rw : ofDigits b (b.digits (ofDigits b L) ++ replicate (l - (b.digits (ofDigits b L)).length) 0) = ofDigits b L
rw₁ : ofDigits b (b.digits (ofDigits b L)) = ofDigits b L
rw₂ rw₃ : ofDigits b L = ofDigits b L
⊢ ofDigits b (b.digitsAppend l (ofDigits b L)) = ofDigits b L

Tactic:
rw [digitsAppend, ofDigits_append_replicate_zero, ofDigits_digits]

Premises used: Nat.digitsAppend, Nat.ofDigits_append_replicate_zero, Nat.ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} L
refine_1 : (b.digitsAppend l (ofDigits b L)).length = l
refine_2 : ∀ x ∈ b.digitsAppend l (ofDigits b L), x < b
⊢ b.digitsAppend l (ofDigits b L) = L

Tactic:
refine (injOn_ofDigits hb l) ⟨?_, ?_⟩ hL
    (by rw [digitsAppend, ofDigits_append_replicate_zero, ofDigits_digits])

Premises used: Nat.injOn_ofDigits, And.intro
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} L
refine_1 refine_1₁ : l = l
⊢ (b.digitsAppend l (ofDigits b L)).length = l

Tactic:
rw [length_digitsAppend hb _ (mapsTo_ofDigits hb _ hL)]

Premises used: Nat.length_digitsAppend, Nat.mapsTo_ofDigits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} L
⊢ ∀ x ∈ b.digitsAppend l (ofDigits b L), x < b

Tactic:
fun x hx ↦ lt_of_mem_digitsAppend hb l x hx

Premises used: Nat.lt_of_mem_digitsAppend
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} L
⊢ ∀ x ∈ b.digitsAppend l (ofDigits b L), x < b

Tactic:
exact fun x hx ↦ lt_of_mem_digitsAppend hb l x hx

Premises used: Nat.lt_of_mem_digitsAppend
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.BijOn (ofDigits b) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} {n : ℕ | n < b ^ l}

Tactic:
(setInvOn_digitsAppend_ofDigits hb l).bijOn (mapsTo_ofDigits hb l) (mapsTo_digitsAppend hb l)

Premises used: Nat.mapsTo_digitsAppend, Nat.setInvOn_digitsAppend_ofDigits, Nat.mapsTo_ofDigits, Set.InvOn.bijOn
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.BijOn (b.digitsAppend l) {n : ℕ | n < b ^ l} {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b}

Tactic:
(bijOn_ofDigits hb l).symm (setInvOn_digitsAppend_ofDigits hb l).symm

Premises used: Set.InvOn.symm, Nat.bijOn_ofDigits, Set.BijOn.symm, Nat.setInvOn_digitsAppend_ofDigits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} L
nth_rewrite : (b.digits (ofDigits b L)).sum = (b.digitsAppend l (ofDigits b L)).sum
⊢ (b.digits (ofDigits b L)).sum = L.sum

Tactic:
nth_rewrite 2 [← (setInvOn_digitsAppend_ofDigits hb l).1 hL]

Premises used: Nat.setInvOn_digitsAppend_ofDigits, And.left
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
hL : Membership.mem (γ := Set (List ℕ)) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} L
rw : (b.digits (ofDigits b L)).sum = (b.digits (ofDigits b L) ++ replicate (l - (b.digits (ofDigits b L)).length) 0).sum
rw₁ :
  (b.digits (ofDigits b L)).sum =
    (b.digits (ofDigits b L)).sum + sum (replicate (l - (b.digits (ofDigits b L)).length) 0)
rw₂ :
  (b.digits (ofDigits b L)).sum =
    (b.digits (ofDigits b L)).sum + HSMul.hSMul (β := ℕ) (l - (b.digits (ofDigits b L)).length) 0
rw₃ : (b.digits (ofDigits b L)).sum = (b.digits (ofDigits b L)).sum + 0
rw₄ rw₅ : (b.digits (ofDigits b L)).sum = (b.digits (ofDigits b L)).sum
⊢ (b.digits (ofDigits b L)).sum = (b.digitsAppend l (ofDigits b L)).sum

Tactic:
rw [digitsAppend, List.sum_append_nat, List.sum_replicate, nsmul_zero, add_zero]

Premises used: List.sum_append_nat, List.sum_replicate, Nat.digitsAppend, nsmul_zero, add_zero
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
have : (this : Fintype (↑{L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} : Type)) → Finset (List ℕ)
⊢ Finset (List ℕ)

Tactic:
have : Fintype {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} :=
    Fintype.ofInjective (Set.MapsTo.restrict _ _ _ (mapsTo_ofDigits hb l))
      <| (Set.MapsTo.restrict_inj (mapsTo_ofDigits hb l)).mpr <| injOn_ofDigits hb l
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
this : Fintype (↑{L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} : Type)
⊢ Finset (List ℕ)

Tactic:
exact {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b}.toFinset

Premises used: setOf, Set.toFinset, And, Eq, List.length
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
L : List ℕ
⊢ L ∈ fixedLengthDigits hb l ↔ L.length = l ∧ ∀ x ∈ L, x < b

Tactic:
simp [fixedLengthDigits]

Premises used: List.fixedLengthDigits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
rw : Set.BijOn (ofDigits b) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} (↑(Finset.range (b ^ l)) : Set ℕ)
⊢ Set.BijOn (ofDigits b) (↑(fixedLengthDigits hb l) : Set (List ℕ)) (↑(Finset.range (b ^ l)) : Set ℕ)

Tactic:
rw [fixedLengthDigits, Set.coe_toFinset]

Premises used: List.fixedLengthDigits, Set.coe_toFinset
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.BijOn (ofDigits b) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} {n : ℕ | n < b ^ l}

Tactic:
bijOn_ofDigits hb l

Premises used: Nat.bijOn_ofDigits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
h : (↑(Finset.range (b ^ l)) : Set ℕ) = {n : ℕ | n < b ^ l}
⊢ Set.BijOn (ofDigits b) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b} (↑(Finset.range (b ^ l)) : Set ℕ)

Tactic:
convert! bijOn_ofDigits hb l

Premises used: Nat.bijOn_ofDigits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
h : ∀ (x : ℕ), x ∈ (↑(Finset.range (b ^ l)) : Set ℕ) ↔ Membership.mem (γ := Set ℕ) {n : ℕ | n < b ^ l} x
⊢ (↑(Finset.range (b ^ l)) : Set ℕ) = {n : ℕ | n < b ^ l}

Tactic:
ext
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l x : ℕ
⊢ x ∈ (↑(Finset.range (b ^ l)) : Set ℕ) ↔ Membership.mem (γ := Set ℕ) {n : ℕ | n < b ^ l} x

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
rw : Set.BijOn (b.digitsAppend l) (↑(Finset.range (b ^ l)) : Set ℕ) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b}
⊢ Set.BijOn (b.digitsAppend l) (↑(Finset.range (b ^ l)) : Set ℕ) (↑(fixedLengthDigits hb l) : Set (List ℕ))

Tactic:
rw [fixedLengthDigits, Set.coe_toFinset]

Premises used: List.fixedLengthDigits, Set.coe_toFinset
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
⊢ Set.BijOn (b.digitsAppend l) {n : ℕ | n < b ^ l} {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b}

Tactic:
bijOn_digitsAppend hb l

Premises used: Nat.bijOn_digitsAppend
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
h : (↑(Finset.range (b ^ l)) : Set ℕ) = {n : ℕ | n < b ^ l}
⊢ Set.BijOn (b.digitsAppend l) (↑(Finset.range (b ^ l)) : Set ℕ) {L : List ℕ | L.length = l ∧ ∀ x ∈ L, x < b}

Tactic:
convert! bijOn_digitsAppend hb l

Premises used: Nat.bijOn_digitsAppend
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
h : ∀ (a : List ℕ), a ∈ fixedLengthDigits hb 0 ↔ Membership.mem (γ := Finset (List ℕ)) {[]} a
⊢ fixedLengthDigits hb 0 = {[]}

Tactic:
ext
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
a : List ℕ
h : a = [] → ∀ x ∈ a, x < b
⊢ a ∈ fixedLengthDigits hb 0 ↔ Membership.mem (γ := Finset (List ℕ)) {[]} a

Tactic:
simp [fixedLengthDigits]

Premises used: List.fixedLengthDigits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
a : List ℕ
⊢ a = [] → ∀ x ∈ a, x < b

Tactic:
grind
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
h :
  ∀ (a : List ℕ),
    a ∈ fixedLengthDigits hb 1 ↔
      Membership.mem (γ := Finset (List ℕ)) (Finset.image (fun (x : ℕ) ↦ [x]) (Finset.range b)) a
⊢ fixedLengthDigits hb 1 = Finset.image (fun (x : ℕ) ↦ [x]) (Finset.range b)

Tactic:
ext
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
a : List ℕ
h :
  ((∃ (a_1 : ℕ), a = [a_1]) ∧ ∀ x ∈ a, x < b) ↔
    Membership.mem (γ := Finset (List ℕ)) (Finset.image (fun (x : ℕ) ↦ [x]) (Finset.range b)) a
⊢ a ∈ fixedLengthDigits hb 1 ↔
    Membership.mem (γ := Finset (List ℕ)) (Finset.image (fun (x : ℕ) ↦ [x]) (Finset.range b)) a

Tactic:
rw [mem_fixedLengthDigits_iff, List.length_eq_one_iff]

Premises used: List.length_eq_one_iff, List.mem_fixedLengthDigits_iff
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
a : List ℕ
⊢ ((∃ (a_1 : ℕ), a = [a_1]) ∧ ∀ x ∈ a, x < b) ↔
    Membership.mem (γ := Finset (List ℕ)) (Finset.image (fun (x : ℕ) ↦ [x]) (Finset.range b)) a

Tactic:
grind
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l : ℕ
rw : (Finset.range (b ^ l)).card = b ^ l
rw₁ rw₂ : b ^ l = b ^ l
⊢ (fixedLengthDigits hb l).card = b ^ l

Tactic:
rw [Set.BijOn.finsetCard_eq (ofDigits b) (bijOn_ofDigits' hb l), Finset.card_range]

Premises used: Nat.ofDigits, Finset.card_range, Nat.bijOn_ofDigits', Set.BijOn.finsetCard_eq
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l d : ℕ
L : List ℕ
hL : L ∈ consFixedLengthDigits hb l d
obtain : ∀ w ∈ fixedLengthDigits hb l, ∀ (hL : d :: w ∈ consFixedLengthDigits hb l d), d :: w ≠ []
⊢ L ≠ []

Tactic:
obtain ⟨_, _, rfl⟩ := Finset.mem_image.mp hL

Premises used: Finset.mem_image, Iff.mp, rfl
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l d : ℕ
w : List ℕ
left : w ∈ fixedLengthDigits hb l
hL : d :: w ∈ consFixedLengthDigits hb l d
⊢ d :: w ≠ []

Tactic:
cons_ne_nil d _

Premises used: List.cons_ne_nil
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l d : ℕ
w : List ℕ
left : w ∈ fixedLengthDigits hb l
hL : d :: w ∈ consFixedLengthDigits hb l d
⊢ d :: w ≠ []

Tactic:
exact cons_ne_nil d _

Premises used: List.cons_ne_nil
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
l d : ℕ
L : List ℕ
hL : L ∈ consFixedLengthDigits hb l d
obtain : ∀ w ∈ fixedLengthDigits hb l, ∀ (hL : d :: w ∈ consFixedLengthDigits hb l d), (d :: w).head ⋯ = d
⊢ L.head ⋯ = d

Tactic:
obtain ⟨_, _, rfl⟩ := Finset.mem_image.mp hL

Premises used: Finset.mem_image, Iff.mp, rfl