awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
rw : ofDigits b' (b'.digits n) % b = 0 ↔ b ∣ ofDigits 1 (b'.digits n)
rw₁ : ofDigits b' (b'.digits n) % b = 0 ↔ ofDigits 1 (b'.digits n) % b = 0
rw₂ : ofDigits (b' % b) (b'.digits n) % b = 0 ↔ ofDigits 1 (b'.digits n) % b = 0
rw₃ rw₄ : ofDigits 1 (b'.digits n) % b = 0 ↔ ofDigits 1 (b'.digits n) % b = 0
⊢ b ∣ ofDigits b' (b'.digits n) ↔ b ∣ ofDigits 1 (b'.digits n)

Tactic:
rw [Nat.dvd_iff_mod_eq_zero, Nat.dvd_iff_mod_eq_zero, ofDigits_mod, h]

Premises used: Nat.ofDigits_mod, Nat.dvd_iff_mod_eq_zero
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
b b' : ℕ
c : ℤ
h : (↑b : ℤ) ∣ (↑b' : ℤ) - c
n : ℕ
rw : Dvd.dvd (α := ℤ) (↑b : ℤ) (↑n : ℤ) ↔ (↑b : ℤ) ∣ ofDigits c (b'.digits n)
⊢ b ∣ n ↔ (↑b : ℤ) ∣ ofDigits c (b'.digits n)

Tactic:
rw [← Int.natCast_dvd_natCast]

Premises used: Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
b b' : ℕ
c : ℤ
h : (↑b : ℤ) ∣ (↑b' : ℤ) - c
n : ℕ
⊢ Dvd.dvd (α := ℤ) (↑b : ℤ) (↑n : ℤ) ↔ (↑b : ℤ) ∣ ofDigits c (b'.digits n)

Tactic:
dvd_iff_dvd_of_dvd_sub (zmodeq_ofDigits_digits b b' c (Int.modEq_iff_dvd.2 h).symm _).symm.dvd

Premises used: Iff.mpr, Int.ModEq.symm, Int.modEq_iff_dvd, Int.ModEq.dvd, dvd_iff_dvd_of_dvd_sub, Nat.zmodeq_ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
b b' : ℕ
c : ℤ
h : (↑b : ℤ) ∣ (↑b' : ℤ) - c
n : ℕ
⊢ Dvd.dvd (α := ℤ) (↑b : ℤ) (↑n : ℤ) ↔ (↑b : ℤ) ∣ ofDigits c (b'.digits n)

Tactic:
exact
    dvd_iff_dvd_of_dvd_sub (zmodeq_ofDigits_digits b b' c (Int.modEq_iff_dvd.2 h).symm _).symm.dvd

Premises used: Iff.mpr, Int.ModEq.symm, Int.modEq_iff_dvd, Int.ModEq.dvd, dvd_iff_dvd_of_dvd_sub, Nat.zmodeq_ofDigits_digits
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
n : ℕ
⊢ (↑11 : ℤ) ∣ HSub.hSub (α := ℤ) (↑10 : ℤ) (-1)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
n : ℕ
⊢ 11 ∣ n ↔ Dvd.dvd (α := ℤ) (↑11 : ℤ) (ofDigits (-1) (digits 10 n))

Tactic:
have t := dvd_iff_dvd_ofDigits 11 10 (-1 : ℤ) (by simp) n
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
n : ℕ
t : 11 ∣ n ↔ Dvd.dvd (α := ℤ) (↑11 : ℤ) (ofDigits (-1) (digits 10 n))
⊢ 11 ∣ n ↔ Dvd.dvd (α := ℤ) (↑11 : ℤ) (List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)))

Tactic:
rw [ofDigits_neg_one] at t

Premises used: Nat.ofDigits_neg_one
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
n : ℕ
t : 11 ∣ n ↔ Dvd.dvd (α := ℤ) (↑11 : ℤ) (List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)))
⊢ 11 ∣ n ↔ Dvd.dvd (α := ℤ) 11 (List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)))

Tactic:
t
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
n : ℕ
t : 11 ∣ n ↔ Dvd.dvd (α := ℤ) (↑11 : ℤ) (List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)))
⊢ 11 ∣ n ↔ Dvd.dvd (α := ℤ) 11 (List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)))

Tactic:
exact t
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
n : ℕ
p : (digits 10 n).Palindrome
h : Even (digits 10 n).length
dig : List ℤ := List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)
rwa rwa₁ rwa₂ rwa₃ : Even (digits 10 n).length
⊢ Even dig.length

Tactic:
rwa [List.length_map]

Premises used: List.length_map
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
n : ℕ
p : (digits 10 n).Palindrome
h : Even (digits 10 n).length
dig : List ℤ := List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)
⊢ Even dig.length

Tactic:
replace h : Even dig.length := by rwa [List.length_map]
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)
h : Even dig.length
⊢ 11 ∣ n

Tactic:
eleven_dvd_iff.2 ⟨0, (?_ : dig.alternatingSum = 0)⟩

Premises used: Iff.mpr, Exists.intro, OfNat.ofNat, Nat.eleven_dvd_iff
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)
h : Even dig.length
refine : dig.alternatingSum = 0
⊢ 11 ∣ n

Tactic:
refine eleven_dvd_iff.2 ⟨0, (?_ : dig.alternatingSum = 0)⟩

Premises used: Iff.mpr, Exists.intro, OfNat.ofNat, Nat.eleven_dvd_iff
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)
h : Even dig.length
⊢ dig.reverse.alternatingSum = HPow.hPow (α := ℤ) (-1) (dig.length + 1) • dig.alternatingSum

Tactic:
have := dig.alternatingSum_reverse
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)
h : Even dig.length
this : dig.reverse.alternatingSum = HPow.hPow (α := ℤ) (-1) (dig.length + 1) • dig.alternatingSum
⊢ List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)) = -dig.alternatingSum

Tactic:
rw [(p.map _).reverse_eq, _root_.pow_succ', h.neg_one_pow, mul_one, neg_one_zsmul] at this

Premises used: Even.neg_one_pow, List.Palindrome.reverse_eq, List.Palindrome.map, mul_one, pow_succ', neg_one_zsmul
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)
h : Even dig.length
this : List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)) = -dig.alternatingSum
⊢ dig.alternatingSum = 0

Tactic:
eq_zero_of_neg_eq this.symm

Premises used: eq_zero_of_neg_eq, Eq.symm
-- Module: Mathlib.Data.Nat.Digits.Div
Goal:
n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)
h : Even dig.length
this : List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)) = -dig.alternatingSum
⊢ dig.alternatingSum = 0

Tactic:
exact eq_zero_of_neg_eq this.symm

Premises used: eq_zero_of_neg_eq, Eq.symm
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
l : List ℕ
this :
  Eq (α := List ℕ) (List.zipWith (fun (a i : ℕ) ↦ a * b ^ (i + 1)) l (List.range l.length))
    (List.zipWith (fun (a i : ℕ) ↦ b * (a * b ^ i)) l (List.range l.length))
⊢ List.sum (List.zipWith (fun (a i : ℕ) ↦ a * b ^ (i + 1)) l (List.range l.length)) =
    b * List.sum (List.zipWith (fun (a i : ℕ) ↦ a * b ^ i) l (List.range l.length))

Tactic:
simp [this]
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
l : List ℕ
a :
  Eq (α := List ℕ) (List.zipWith (fun (a i : ℕ) ↦ a * b ^ (i + 1)) l (List.range l.length))
    (List.zipWith (fun (a i : ℕ) ↦ b * (a * b ^ i)) l (List.range l.length))
⊢ List.sum (List.zipWith (fun (a i : ℕ) ↦ a * b ^ (i + 1)) l (List.range l.length)) =
    b * List.sum (List.zipWith (fun (a i : ℕ) ↦ a * b ^ i) l (List.range l.length))

Tactic:
suffices
    l.zipWith (fun a i : ℕ => a * b ^ (i + 1)) (List.range l.length) =
      l.zipWith (fun a i => b * (a * b ^ i)) (List.range l.length)
    by simp [this]
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
l : List ℕ
e_f : Eq (α := ℕ → ℕ → ℕ) (fun (a i : ℕ) ↦ a * b ^ (i + 1)) fun (a i : ℕ) ↦ b * (a * b ^ i)
⊢ Eq (α := List ℕ) (List.zipWith (fun (a i : ℕ) ↦ a * b ^ (i + 1)) l (List.range l.length))
    (List.zipWith (fun (a i : ℕ) ↦ b * (a * b ^ i)) l (List.range l.length))

Tactic:
congr
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
l : List ℕ
e_f : ∀ (x x_1 : ℕ), x * b ^ (x_1 + 1) = b * (x * b ^ x_1)
⊢ Eq (α := ℕ → ℕ → ℕ) (fun (a i : ℕ) ↦ a * b ^ (i + 1)) fun (a i : ℕ) ↦ b * (a * b ^ i)

Tactic:
ext
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
l : List ℕ
x x_1 : ℕ
⊢ x * b ^ (x_1 + 1) = b * (x * b ^ x_1)

Tactic:
ring
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
L : List ℕ
rw :
  Eq (α := ℕ) (List.foldr (fun (x y : ℕ) ↦ (↑x : ℕ) + b * y) 0 L)
    (List.sum
      (List.zipWith
        (Function.curry fun (x : ℕ × ℕ) ↦
          match (motive := ℕ × ℕ → ℕ) x with
          | (a, i) => a * b ^ i)
        L (List.range L.length)))
⊢ ofDigits b L = List.sum (List.mapIdx (fun (i a : ℕ) ↦ a * b ^ i) L)

Tactic:
rw [List.mapIdx_eq_zipIdx_map, List.zipIdx_eq_zip_range', List.map_zip_eq_zipWith,
    ofDigits_eq_foldr, ← List.range_eq_range']

Premises used: Nat.ofDigits_eq_foldr, List.zipIdx_eq_zip_range', List.map_zip_eq_zipWith, List.range_eq_range', List.mapIdx_eq_zipIdx_map
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
⊢ Eq (α := ℕ) (List.foldr (fun (x y : ℕ) ↦ (↑x : ℕ) + b * y) 0 [])
    (List.sum
      (List.zipWith (α := ℕ)
        (Function.curry fun (x : ℕ × ℕ) ↦
          match (motive := ℕ × ℕ → ℕ) x with
          | (a, i) => a * b ^ i)
        [] (List.range (List.length (α := ℕ) []))))

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b hd : ℕ
tl : List ℕ
hl :
  Eq (α := ℕ) (List.foldr (fun (x y : ℕ) ↦ (↑x : ℕ) + b * y) 0 tl)
    (List.sum
      (List.zipWith
        (Function.curry fun (x : ℕ × ℕ) ↦
          match (motive := ℕ × ℕ → ℕ) x with
          | (a, i) => a * b ^ i)
        tl (List.range tl.length)))
⊢ Eq (α := ℕ) (List.foldr (fun (x y : ℕ) ↦ (↑x : ℕ) + b * y) 0 (hd :: tl))
    (List.sum
      (List.zipWith
        (Function.curry fun (x : ℕ × ℕ) ↦
          match (motive := ℕ × ℕ → ℕ) x with
          | (a, i) => a * b ^ i)
        (hd :: tl) (List.range (hd :: tl).length)))

Tactic:
simpa [List.range_succ_eq_map, List.zipWith_map_right, ofDigits_eq_sum_mapIdx_aux] using
      Or.inl hl

Premises used: Nat.ofDigits_eq_sum_mapIdx_aux, List.zipWith_map_right, List.range_succ_eq_map, Or.inl
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
L : List ℕ
nil :
  Eq (α := ℕ) (List.foldr (fun (x y : ℕ) ↦ (↑x : ℕ) + b * y) 0 [])
    (List.sum
      (List.zipWith (α := ℕ)
        (Function.curry fun (x : ℕ × ℕ) ↦
          match (motive := ℕ × ℕ → ℕ) x with
          | (a, i) => a * b ^ i)
        [] (List.range (List.length (α := ℕ) []))))
cons :
  ∀ (hd : ℕ) (tl : List ℕ)
    (hl :
      Eq (α := ℕ) (List.foldr (fun (x y : ℕ) ↦ (↑x : ℕ) + b * y) 0 tl)
        (List.sum
          (List.zipWith
            (Function.curry fun (x : ℕ × ℕ) ↦
              match (motive := ℕ × ℕ → ℕ) x with
              | (a, i) => a * b ^ i)
            tl (List.range tl.length)))),
    Eq (α := ℕ) (List.foldr (fun (x y : ℕ) ↦ (↑x : ℕ) + b * y) 0 (hd :: tl))
      (List.sum
        (List.zipWith
          (Function.curry fun (x : ℕ × ℕ) ↦
            match (motive := ℕ × ℕ → ℕ) x with
            | (a, i) => a * b ^ i)
          (hd :: tl) (List.range (hd :: tl).length)))
⊢ Eq (α := ℕ) (List.foldr (fun (x y : ℕ) ↦ (↑x : ℕ) + b * y) 0 L)
    (List.sum
      (List.zipWith
        (Function.curry fun (x : ℕ × ℕ) ↦
          match (motive := ℕ × ℕ → ℕ) x with
          | (a, i) => a * b ^ i)
        L (List.range L.length)))

Tactic:
induction L with
  | nil => simp
  | cons hd tl hl =>
    simpa [List.range_succ_eq_map, List.zipWith_map_right, ofDigits_eq_sum_mapIdx_aux] using
      Or.inl hl

Premises used: Nat.ofDigits_eq_sum_mapIdx_aux, List.zipWith_map_right, List.range_succ_eq_map
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
h :
  ∀ (n : ℕ) (IH : ∀ m < n, ∀ (hn : m ≠ 0), (b.digits m).length = log b m + 1) (hn : n ≠ 0),
    (b.digits n).length = log b n + 1
⊢ (b.digits n).length = log b n + 1

Tactic:
induction n using Nat.strong_induction_on with | _ n IH
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, ∀ (hn : m ≠ 0), (b.digits m).length = log b m + 1
hn : n ≠ 0
h : (b.digits (n / b)).length + 1 = log b n + 1
⊢ (b.digits n).length = log b n + 1

Tactic:
rw [digits_eq_cons_digits_div hb hn, List.length]

Premises used: Nat.digits_eq_cons_digits_div, List.length
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, ∀ (hn : m ≠ 0), (b.digits m).length = log b m + 1
hn : n ≠ 0
pos : ∀ (h : n / b = 0), (b.digits (n / b)).length + 1 = log b n + 1
neg : ∀ (h : ¬n / b = 0), (b.digits (n / b)).length + 1 = log b n + 1
⊢ (b.digits (n / b)).length + 1 = log b n + 1

Tactic:
by_cases h : n / b = 0
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, ∀ (hn : m ≠ 0), (b.digits m).length = log b m + 1
hn : n ≠ 0
h : n / b = 0
pos : n < b ∨ b ≤ 1
⊢ (b.digits (n / b)).length + 1 = log b n + 1

Tactic:
simp [h]
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, ∀ (hn : m ≠ 0), (b.digits m).length = log b m + 1
hn : n ≠ 0
h : n / b = 0
⊢ n < b ∨ b ≤ 1

Tactic:
aesop
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, ∀ (hn : m ≠ 0), (b.digits m).length = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
⊢ n / b < n

Tactic:
have : n / b < n := div_lt_self (Nat.pos_of_ne_zero hn) hb
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, ∀ (hn : m ≠ 0), (b.digits m).length = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
this : n / b < n
neg : 1 ≤ log b n
⊢ (b.digits (n / b)).length + 1 = log b n + 1

Tactic:
rw [IH _ this h, log_div_base, tsub_add_cancel_of_le]

Premises used: tsub_add_cancel_of_le, Nat.log_div_base
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, ∀ (hn : m ≠ 0), (b.digits m).length = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
this : n / b < n
⊢ 1 ≤ log b n

Tactic:
Nat.succ_le_of_lt (log_pos hb ?_)

Premises used: Nat.succ_le_of_lt, Nat.log_pos
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, ∀ (hn : m ≠ 0), (b.digits m).length = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
this : n / b < n
neg : b ≤ n
⊢ 1 ≤ log b n

Tactic:
refine Nat.succ_le_of_lt (log_pos hb ?_)

Premises used: Nat.succ_le_of_lt, Nat.log_pos
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, ∀ (hn : m ≠ 0), (b.digits m).length = log b m + 1
hn : n ≠ 0
h : ¬n / b = 0
this : n / b < n
neg : ∀ (h : n < b), n / b = 0
⊢ b ≤ n

Tactic:
contrapose! h
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, ∀ (hn : m ≠ 0), (b.digits m).length = log b m + 1
hn : n ≠ 0
this : n / b < n
h : n < b
⊢ n / b = 0

Tactic:
div_eq_of_lt h

Premises used: Nat.div_eq_of_lt
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b : ℕ
hb : 1 < b
n : ℕ
IH : ∀ m < n, ∀ (hn : m ≠ 0), (b.digits m).length = log b m + 1
hn : n ≠ 0
this : n / b < n
h : n < b
⊢ n / b = 0

Tactic:
exact div_eq_of_lt h

Premises used: Nat.div_eq_of_lt
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b k : ℕ
hb : 1 < b
n : ℕ
pos : ∀ (h : n = 0), (b.digits n).length ≤ k ↔ n < b ^ k
neg : ∀ (h : ¬n = 0), (b.digits n).length ≤ k ↔ n < b ^ k
⊢ (b.digits n).length ≤ k ↔ n < b ^ k

Tactic:
by_cases h : n = 0
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b k : ℕ
hb : 1 < b
n : ℕ
h : n = 0
⊢ 0 < b ^ k

Tactic:
positivity
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b k : ℕ
hb : 1 < b
n : ℕ
h : n = 0
⊢ 0 < b ^ k

Tactic:
have : 0 < b ^ k := by positivity
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b k : ℕ
hb : 1 < b
n : ℕ
h : n = 0
this : 0 < b ^ k
⊢ (b.digits n).length ≤ k ↔ n < b ^ k

Tactic:
simpa [h]
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b k : ℕ
hb : 1 < b
n : ℕ
h : ¬n = 0
neg : log b n + 1 ≤ k ↔ log b n < k
⊢ (b.digits n).length ≤ k ↔ n < b ^ k

Tactic:
rw [length_digits b n hb h, ← log_lt_iff_lt_pow hb h]

Premises used: Nat.log_lt_iff_lt_pow, Nat.length_digits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b k : ℕ
hb : 1 < b
n : ℕ
h : ¬n = 0
⊢ log b n + 1 ≤ k ↔ log b n < k

Tactic:
add_one_le_iff

Premises used: Nat.add_one_le_iff
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b k : ℕ
hb : 1 < b
n : ℕ
h : ¬n = 0
⊢ log b n + 1 ≤ k ↔ log b n < k

Tactic:
exact add_one_le_iff

Premises used: Nat.add_one_le_iff
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b k : ℕ
hb : 1 < b
n : ℕ
contrapose! : (b.digits n).length ≤ k ↔ n < b ^ k
⊢ k < (b.digits n).length ↔ b ^ k ≤ n

Tactic:
contrapose!
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b k : ℕ
hb : 1 < b
n : ℕ
⊢ (b.digits n).length ≤ k ↔ n < b ^ k

Tactic:
digits_length_le_iff hb n

Premises used: Nat.digits_length_le_iff
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b k : ℕ
hb : 1 < b
n : ℕ
⊢ (b.digits n).length ≤ k ↔ n < b ^ k

Tactic:
exact digits_length_le_iff hb n

Premises used: Nat.digits_length_le_iff
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b m : ℕ
hm : m ≠ 0
zero : (digits 0 m).getLast ⋯ ≠ 0
succ : ((HAdd.hAdd (α := ℕ) 0 1).digits m).getLast ⋯ ≠ 0
succ₁ : ∀ (b : ℕ), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
⊢ (b.digits m).getLast ⋯ ≠ 0

Tactic:
rcases b with (_ | _ | b)
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
m : ℕ
hm : m ≠ 0
zero : ∀ (hm : Ne (α := ℕ) 0 0), (digits 0 0).getLast ⋯ ≠ 0
zero₁ : ∀ (n : ℕ) (hm : n + 1 ≠ 0), (digits 0 (n + 1)).getLast ⋯ ≠ 0
⊢ (digits 0 m).getLast ⋯ ≠ 0

Tactic:
cases m
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
hm : Ne (α := ℕ) 0 0
⊢ (digits 0 0).getLast ⋯ ≠ 0

Tactic:
cases hm rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
n : ℕ
hm : n + 1 ≠ 0
⊢ (digits 0 (n + 1)).getLast ⋯ ≠ 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
m : ℕ
hm : m ≠ 0
⊢ ((HAdd.hAdd (α := ℕ) 0 1).digits m).getLast ⋯ ≠ 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
m : ℕ
hm : m ≠ 0
b : ℕ
succ : ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
⊢ ((b + 1 + 1).digits m).getLast ⋯ ≠ 0

Tactic:
revert hm
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
⊢ ∀ (hm : n ≠ 0), ((b + 1 + 1).digits n).getLast ⋯ ≠ 0

Tactic:
?_
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
m b : ℕ
succ :
  ∀ (n : ℕ) (IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0) (hm : n ≠ 0),
    ((b + 1 + 1).digits n).getLast ⋯ ≠ 0
⊢ ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0

Tactic:
induction m using Nat.strongRecOn with | ind n IH => ?_
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
pos : ∀ (hnb : n < b + 2), ((b + 1 + 1).digits n).getLast ⋯ ≠ 0
neg : ∀ (hnb : b + 2 ≤ n), ((b + 1 + 1).digits n).getLast ⋯ ≠ 0
⊢ ((b + 1 + 1).digits n).getLast ⋯ ≠ 0

Tactic:
by_cases! hnb : n < b + 2
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : n < b + 2
⊢ ((b + 1 + 1).digits n).getLast ⋯ ≠ 0

Tactic:
simpa only [digits_of_lt (b + 2) n hn hnb]

Premises used: HAdd.hAdd, Nat.digits_of_lt, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : b + 2 ≤ n
neg : ((b + 2).digits (n / (b + 2))).getLast ⋯ ≠ 0
neg₁ : (b + 2).digits (n / (b + 2)) ≠ []
⊢ ((b + 1 + 1).digits n).getLast ⋯ ≠ 0

Tactic:
rw [digits_getLast n (le_add_left 2 b)]

Premises used: Nat.le_add_left, OfNat.ofNat, Nat.digits_getLast
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : b + 2 ≤ n
⊢ ((b + 2).digits (n / (b + 2))).getLast ⋯ ≠ 0

Tactic:
IH _ (Nat.div_lt_self hn.bot_lt (one_lt_succ_succ b)) ?_

Premises used: Nat.one_lt_succ_succ, Nat.div_lt_self, Ne.bot_lt
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : b + 2 ≤ n
neg : 0 < n / b.succ.succ
⊢ n / b.succ.succ ≠ 0

Tactic:
rw [← pos_iff_ne_zero]

Premises used: pos_iff_ne_zero
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : b + 2 ≤ n
⊢ 0 < n / b.succ.succ

Tactic:
Nat.div_pos hnb (zero_lt_succ (succ b))

Premises used: Nat.zero_lt_succ, Nat.div_pos, Nat.succ
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b n : ℕ
IH : ∀ m < n, ∀ (hm : m ≠ 0), ((b + 1 + 1).digits m).getLast ⋯ ≠ 0
hn : n ≠ 0
hnb : b + 2 ≤ n
⊢ 0 < n / b.succ.succ

Tactic:
exact Nat.div_pos hnb (zero_lt_succ (succ b))

Premises used: Nat.zero_lt_succ, Nat.div_pos, Nat.succ
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b m n : ℕ
hb : 0 < b
inl :
  ∀ (hb : 0 < succ 0),
    (succ 0).digits n ++ (succ 0).digits m = (succ 0).digits (n + succ 0 ^ ((succ 0).digits n).length * m)
inr : ∀ (hb : succ 0 < b), b.digits n ++ b.digits m = b.digits (n + b ^ (b.digits n).length * m)
⊢ b.digits n ++ b.digits m = b.digits (n + b ^ (b.digits n).length * m)

Tactic:
rcases eq_or_lt_of_le (Nat.succ_le_of_lt hb) with (rfl | hb)

Premises used: Nat.succ_le_of_lt, eq_or_lt_of_le, rfl
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
m n : ℕ
hb : 0 < succ 0
⊢ (succ 0).digits n ++ (succ 0).digits m = (succ 0).digits (n + succ 0 ^ ((succ 0).digits n).length * m)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b m n : ℕ
hb_1 : 0 < b
hb : succ 0 < b
inr : b.digits n ++ b.digits m = b.digits (ofDigits b (b.digits n ++ b.digits m))
⊢ b.digits n ++ b.digits m = b.digits (n + b ^ (b.digits n).length * m)

Tactic:
rw [← ofDigits_digits_append_digits]

Premises used: Nat.ofDigits_digits_append_digits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b m n : ℕ
hb_1 : 0 < b
hb : succ 0 < b
⊢ b.digits n ++ b.digits m = b.digits (ofDigits b (b.digits n ++ b.digits m))

Tactic:
(digits_ofDigits b hb _ (fun l hl => ?_) (fun h_append => ?_)).symm

Premises used: Nat.digits_ofDigits, Eq.symm
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b m n : ℕ
hb_1 : 0 < b
hb : succ 0 < b
inr : ∀ (l : ℕ) (hl : l ∈ b.digits n ++ b.digits m), l < b
inr₁ : ∀ (h_append : b.digits n ++ b.digits m ≠ []), (b.digits n ++ b.digits m).getLast h_append ≠ 0
⊢ b.digits n ++ b.digits m = b.digits (ofDigits b (b.digits n ++ b.digits m))

Tactic:
refine (digits_ofDigits b hb _ (fun l hl => ?_) (fun h_append => ?_)).symm

Premises used: Nat.digits_ofDigits, Eq.symm
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b m n : ℕ
hb_1 : 0 < b
hb : succ 0 < b
l : ℕ
hl : l ∈ b.digits n ++ b.digits m
inr : ∀ (h : l ∈ b.digits n), l < b
inr₁ : ∀ (h : l ∈ b.digits m), l < b
⊢ l < b

Tactic:
rcases (List.mem_append.mp hl) with (h | h)

Premises used: List.mem_append, Iff.mp
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b m n : ℕ
hb_1 : 0 < b
hb : succ 0 < b
l : ℕ
hl : l ∈ b.digits n ++ b.digits m
h : l ∈ b.digits n
⊢ l < b

Tactic:
digits_lt_base hb h

Premises used: Nat.digits_lt_base
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b m n : ℕ
hb_1 : 0 < b
hb : succ 0 < b
l : ℕ
hl : l ∈ b.digits n ++ b.digits m
h : l ∈ b.digits n
⊢ l < b

Tactic:
exact digits_lt_base hb h

Premises used: Nat.digits_lt_base
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b m n : ℕ
hb_1 : 0 < b
hb : succ 0 < b
l : ℕ
hl : l ∈ b.digits n ++ b.digits m
h : l ∈ b.digits m
⊢ l < b

Tactic:
digits_lt_base hb h

Premises used: Nat.digits_lt_base
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b m n : ℕ
hb_1 : 0 < b
hb : succ 0 < b
l : ℕ
hl : l ∈ b.digits n ++ b.digits m
h : l ∈ b.digits m
⊢ l < b

Tactic:
exact digits_lt_base hb h

Premises used: Nat.digits_lt_base
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b m n : ℕ
hb_1 : 0 < b
hb : succ 0 < b
h_append : b.digits n ++ b.digits m ≠ []
pos : ∀ (h : b.digits m = []), (b.digits n ++ b.digits m).getLast h_append ≠ 0
neg : ∀ (h : ¬b.digits m = []), (b.digits n ++ b.digits m).getLast h_append ≠ 0
⊢ (b.digits n ++ b.digits m).getLast h_append ≠ 0

Tactic:
by_cases h : digits b m = []

Premises used: Nat.digits
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b m n : ℕ
hb_1 : 0 < b
hb : succ 0 < b
h_append : b.digits n ++ b.digits m ≠ []
h : b.digits m = []
pos : ∀ (h_append_1 : b.digits n ≠ []), (b.digits n).getLast ⋯ ≠ 0
⊢ (b.digits n ++ b.digits m).getLast h_append ≠ 0

Tactic:
simp only [h, List.append_nil] at h_append ⊢

Premises used: List.append_nil
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b m n : ℕ
hb_1 : 0 < b
hb : succ 0 < b
h_append_1 : b.digits n ++ b.digits m ≠ []
h : b.digits m = []
h_append : b.digits n ≠ []
⊢ (b.digits n).getLast ⋯ ≠ 0

Tactic:
getLast_digit_ne_zero b <| digits_ne_nil_iff_ne_zero.mp h_append

Premises used: Nat.getLast_digit_ne_zero, Nat.digits_ne_nil_iff_ne_zero, Iff.mp
-- Module: Mathlib.Data.Nat.Digits.Lemmas
Goal:
b m n : ℕ
hb_1 : 0 < b
hb : succ 0 < b
h_append_1 : b.digits n ++ b.digits m ≠ []
h : b.digits m = []
h_append : b.digits n ≠ []
⊢ (b.digits n).getLast ⋯ ≠ 0

Tactic:
exact getLast_digit_ne_zero b <| digits_ne_nil_iff_ne_zero.mp h_append

Premises used: Nat.getLast_digit_ne_zero, Nat.digits_ne_nil_iff_ne_zero, Iff.mp