awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b f : ℕ
zero :
  ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore 0 n l1).length = (b.toDigitsCore 0 n l2).length
⊢ ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
have zero₁ : ∀ (n : ℕ) (l1 l2 : List Char) (hlen : l1.length = l2.length), l1.length = l2.length
Tactic: induction f with (simp only [Nat.toDigitsCore]; intro n l1 l2 hlen)
  | zero => assumption
  | succ f ih =>
    if hx : n / b = 0 then
      simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]
    else
      simp only [hx, if_false]
      specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2)
      simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih
      exact ih trivial
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b f : ℕ
zero :
  ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore 0 n l1).length = (b.toDigitsCore 0 n l2).length
zero₁ : ∀ (n : ℕ) (l1 l2 : List Char) (hlen : l1.length = l2.length), l1.length = l2.length
⊢ ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
have succ : ∀ (f : ℕ)
  (ih :
    ∀ (n : ℕ) (l1 l2 : List Char),
      l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length)
  (n : ℕ) (l1 l2 : List Char),
  l1.length = l2.length → (b.toDigitsCore (f + 1) n l1).length = (b.toDigitsCore (f + 1) n l2).length
Tactic: induction f with (simp only [Nat.toDigitsCore]; intro n l1 l2 hlen)
  | zero => assumption
  | succ f ih =>
    if hx : n / b = 0 then
      simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]
    else
      simp only [hx, if_false]
      specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2)
      simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih
      exact ih trivial
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b f : ℕ
zero :
  ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore 0 n l1).length = (b.toDigitsCore 0 n l2).length
zero₁ : ∀ (n : ℕ) (l1 l2 : List Char) (hlen : l1.length = l2.length), l1.length = l2.length
succ :
  ∀ (f : ℕ)
    (ih :
      ∀ (n : ℕ) (l1 l2 : List Char),
        l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length)
    (n : ℕ) (l1 l2 : List Char),
    l1.length = l2.length → (b.toDigitsCore (f + 1) n l1).length = (b.toDigitsCore (f + 1) n l2).length
⊢ ∀ (n : ℕ) (l1 l2 : List Char), l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length
have succ₁ : ∀ (f : ℕ)
  (ih :
    ∀ (n : ℕ) (l1 l2 : List Char),
      l1.length = l2.length → (b.toDigitsCore f n l1).length = (b.toDigitsCore f n l2).length)
  (n : ℕ) (l1 l2 : List Char) (hlen : l1.length = l2.length),
  (if n / b = 0 then (n % b).digitChar :: l1 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l1)).length =
    (if n / b = 0 then (n % b).digitChar :: l2 else b.toDigitsCore f (n / b) ((n % b).digitChar :: l2)).length
Tactic: induction f with (simp only [Nat.toDigitsCore]; intro n l1 l2 hlen)
  | zero => assumption
  | succ f ih =>
    if hx : n / b = 0 then
      simp only [hx, if_true, List.length, congrArg (fun l ↦ l + 1) hlen]
    else
      simp only [hx, if_false]
      specialize ih (n / b) (Nat.digitChar (n % b) :: l1) (Nat.digitChar (n % b) :: l2)
      simp only [List.length, congrArg (fun l ↦ l + 1) hlen] at ih
      exact ih trivial
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b f : ℕ
⊢ ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
have succ : ∀ (f : ℕ)
  (ih :
    ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1)
  (n : ℕ) (c : Char) (tl : List Char),
  (b.toDigitsCore (f + 1) n (c :: tl)).length = (b.toDigitsCore (f + 1) n tl).length + 1
Tactic: induction f with (intro n c tl; simp only [Nat.toDigitsCore, List.length])
  | succ f ih =>
    grind
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b f : ℕ
succ :
  ∀ (f : ℕ)
    (ih :
      ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1)
    (n : ℕ) (c : Char) (tl : List Char),
    (b.toDigitsCore (f + 1) n (c :: tl)).length = (b.toDigitsCore (f + 1) n tl).length + 1
⊢ ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
have succ₁ : ∀ (f : ℕ)
  (ih :
    ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1)
  (n : ℕ) (c : Char) (tl : List Char),
  (if n / b = 0 then (n % b).digitChar :: c :: tl else b.toDigitsCore f (n / b) ((n % b).digitChar :: c :: tl)).length =
    (if n / b = 0 then (n % b).digitChar :: tl else b.toDigitsCore f (n / b) ((n % b).digitChar :: tl)).length + 1
Tactic: induction f with (intro n c tl; simp only [Nat.toDigitsCore, List.length])
  | succ f ih =>
    grind
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b f : ℕ
succ :
  ∀ (f : ℕ)
    (ih :
      ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1)
    (n : ℕ) (c : Char) (tl : List Char),
    (b.toDigitsCore (f + 1) n (c :: tl)).length = (b.toDigitsCore (f + 1) n tl).length + 1
succ₁ :
  ∀ (f : ℕ)
    (ih :
      ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1)
    (n : ℕ) (c : Char) (tl : List Char),
    (if n / b = 0 then (n % b).digitChar :: c :: tl
        else b.toDigitsCore f (n / b) ((n % b).digitChar :: c :: tl)).length =
      (if n / b = 0 then (n % b).digitChar :: tl else b.toDigitsCore f (n / b) ((n % b).digitChar :: tl)).length + 1
⊢ ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore f n (c :: tl)).length = (b.toDigitsCore f n tl).length + 1
have zero : ∀ (n : ℕ) (c : Char) (tl : List Char), (b.toDigitsCore 0 n (c :: tl)).length = (b.toDigitsCore 0 n tl).length + 1
Tactic: induction f with (intro n c tl; simp only [Nat.toDigitsCore, List.length])
  | succ f ih =>
    grind
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
n b e : ℕ
h_b_pos : 0 < b
⊢ n < b ^ e.succ → n / b < b ^ e
have simp : n < b ^ e * b → n / b < b ^ e
Tactic: simp only [Nat.pow_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (hypothesis)
Goal:
b f : ℕ
ih : ∀ (n e : ℕ) (h_e_pos : 0 < e) (hlt : n < b ^ e), (b.toDigitsCore f n []).length ≤ e
n : ℕ
h_e_pos : 0 < HAdd.hAdd (α := ℕ) 0 1
hlt : n < b ^ HAdd.hAdd (α := ℕ) 0 1
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤
    HAdd.hAdd (α := ℕ) 0 1
have hlt₁ : n < b
Tactic: rw [zero_add, pow_one] at hlt
Cleared hypotheses: hlt
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (hypothesis)
Goal:
b f : ℕ
ih : ∀ (n e : ℕ) (h_e_pos : 0 < e) (hlt : n < b ^ e), (b.toDigitsCore f n []).length ≤ e
n e : ℕ
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1 + 1
have ih₁ : (b.toDigitsCore f (n / b) []).length ≤ e + 1
Tactic: specialize ih (n / b) _ (add_one_pos e) (Nat.div_lt_of_lt_mul <| by rwa [← pow_add_one'])
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b f n e : ℕ
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
ih : (b.toDigitsCore f (n / b) []).length ≤ e + 1
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1 + 1
have pos : n / b = 0 → [(n % b).digitChar].length ≤ e + 1 + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b f n e : ℕ
h_e_pos : 0 < e + 1 + 1
hlt : n < b ^ (e + 1 + 1)
ih : (b.toDigitsCore f (n / b) []).length ≤ e + 1
pos : n / b = 0 → [(n % b).digitChar].length ≤ e + 1 + 1
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1 + 1
have neg : ¬n / b = 0 → (b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1 + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b f : ℕ
ih : ∀ (n e : ℕ) (h_e_pos : 0 < e) (hlt : n < b ^ e), (b.toDigitsCore f n []).length ≤ e
n e : ℕ
h_e_pos : 0 < e + 1
hlt : n < b ^ (e + 1)
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1
have succ : ∀ (h_e_pos : 0 < HAdd.hAdd (α := ℕ) 0 1) (hlt : n < b ^ HAdd.hAdd (α := ℕ) 0 1),
  (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤
    HAdd.hAdd (α := ℕ) 0 1
Tactic: cases e with
      | zero =>
        rw [zero_add, pow_one] at hlt
        simp [Nat.div_eq_of_lt hlt]
      | succ e =>
        specialize ih (n / b) _ (add_one_pos e) (Nat.div_lt_of_lt_mul <| by rwa [← pow_add_one'])
        split_ifs
        · simp
        · simp only [toDigitsCore_lens_eq b f (n / b) (Nat.digitChar <| n % b),
            Nat.succ_le_succ_iff, ih]
Cleared hypotheses: e, h_e_pos, hlt
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b f : ℕ
ih : ∀ (n e : ℕ) (h_e_pos : 0 < e) (hlt : n < b ^ e), (b.toDigitsCore f n []).length ≤ e
n e : ℕ
h_e_pos : 0 < e + 1
hlt : n < b ^ (e + 1)
succ :
  ∀ (h_e_pos : 0 < HAdd.hAdd (α := ℕ) 0 1) (hlt : n < b ^ HAdd.hAdd (α := ℕ) 0 1),
    (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤
      HAdd.hAdd (α := ℕ) 0 1
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1
have succ₁ : ∀ (e : ℕ) (h_e_pos : 0 < e + 1 + 1) (hlt : n < b ^ (e + 1 + 1)),
  (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1 + 1
Tactic: cases e with
      | zero =>
        rw [zero_add, pow_one] at hlt
        simp [Nat.div_eq_of_lt hlt]
      | succ e =>
        specialize ih (n / b) _ (add_one_pos e) (Nat.div_lt_of_lt_mul <| by rwa [← pow_add_one'])
        split_ifs
        · simp
        · simp only [toDigitsCore_lens_eq b f (n / b) (Nat.digitChar <| n % b),
            Nat.succ_le_succ_iff, ih]
Cleared hypotheses: e, h_e_pos, hlt
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b f : ℕ
ih : ∀ (n e : ℕ) (h_e_pos : 0 < e) (hlt : n < b ^ e), (b.toDigitsCore f n []).length ≤ e
n e : ℕ
h_e_pos : 0 < e
hlt : n < b ^ e
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e
have succ : ∀ (h_e_pos : LT.lt (α := ℕ) 0 0) (hlt : n < HPow.hPow (β := ℕ) b 0),
  (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ 0
Tactic: cases e with
    | zero => exact False.elim (Nat.lt_irrefl 0 h_e_pos)
    | succ e =>
      cases e with
      | zero =>
        rw [zero_add, pow_one] at hlt
        simp [Nat.div_eq_of_lt hlt]
      | succ e =>
        specialize ih (n / b) _ (add_one_pos e) (Nat.div_lt_of_lt_mul <| by rwa [← pow_add_one'])
        split_ifs
        · simp
        · simp only [toDigitsCore_lens_eq b f (n / b) (Nat.digitChar <| n % b),
            Nat.succ_le_succ_iff, ih]
Cleared hypotheses: e, h_e_pos, hlt
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b f : ℕ
ih : ∀ (n e : ℕ) (h_e_pos : 0 < e) (hlt : n < b ^ e), (b.toDigitsCore f n []).length ≤ e
n e : ℕ
h_e_pos : 0 < e
hlt : n < b ^ e
succ :
  ∀ (h_e_pos : LT.lt (α := ℕ) 0 0) (hlt : n < HPow.hPow (β := ℕ) b 0),
    (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ 0
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e
have succ₁ : ∀ (e : ℕ) (h_e_pos : 0 < e + 1) (hlt : n < b ^ (e + 1)),
  (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1
Tactic: cases e with
    | zero => exact False.elim (Nat.lt_irrefl 0 h_e_pos)
    | succ e =>
      cases e with
      | zero =>
        rw [zero_add, pow_one] at hlt
        simp [Nat.div_eq_of_lt hlt]
      | succ e =>
        specialize ih (n / b) _ (add_one_pos e) (Nat.div_lt_of_lt_mul <| by rwa [← pow_add_one'])
        split_ifs
        · simp
        · simp only [toDigitsCore_lens_eq b f (n / b) (Nat.digitChar <| n % b),
            Nat.succ_le_succ_iff, ih]
Cleared hypotheses: e, h_e_pos, hlt
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b f n e : ℕ
h_e_pos : 0 < e
hlt : n < b ^ e
⊢ (b.toDigitsCore f n []).length ≤ e
have zero : ∀ (n e : ℕ) (h_e_pos : 0 < e) (hlt : n < b ^ e), (b.toDigitsCore 0 n []).length ≤ e
Tactic: induction f generalizing n e hlt h_e_pos with
  | zero => simp only [toDigitsCore, List.length, zero_le]
  | succ f ih =>
    simp only [toDigitsCore]
    cases e with
    | zero => exact False.elim (Nat.lt_irrefl 0 h_e_pos)
    | succ e =>
      cases e with
      | zero =>
        rw [zero_add, pow_one] at hlt
        simp [Nat.div_eq_of_lt hlt]
      | succ e =>
        specialize ih (n / b) _ (add_one_pos e) (Nat.div_lt_of_lt_mul <| by rwa [← pow_add_one'])
        split_ifs
        · simp
        · simp only [toDigitsCore_lens_eq b f (n / b) (Nat.digitChar <| n % b),
            Nat.succ_le_succ_iff, ih]
Cleared hypotheses: f, n, e, h_e_pos, hlt
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b f n e : ℕ
h_e_pos : 0 < e
hlt : n < b ^ e
zero : ∀ (n e : ℕ) (h_e_pos : 0 < e) (hlt : n < b ^ e), (b.toDigitsCore 0 n []).length ≤ e
⊢ (b.toDigitsCore f n []).length ≤ e
have succ : ∀ (f : ℕ) (ih : ∀ (n e : ℕ) (h_e_pos : 0 < e) (hlt : n < b ^ e), (b.toDigitsCore f n []).length ≤ e) (n e : ℕ)
  (h_e_pos : 0 < e) (hlt : n < b ^ e), (b.toDigitsCore (f + 1) n []).length ≤ e
Tactic: induction f generalizing n e hlt h_e_pos with
  | zero => simp only [toDigitsCore, List.length, zero_le]
  | succ f ih =>
    simp only [toDigitsCore]
    cases e with
    | zero => exact False.elim (Nat.lt_irrefl 0 h_e_pos)
    | succ e =>
      cases e with
      | zero =>
        rw [zero_add, pow_one] at hlt
        simp [Nat.div_eq_of_lt hlt]
      | succ e =>
        specialize ih (n / b) _ (add_one_pos e) (Nat.div_lt_of_lt_mul <| by rwa [← pow_add_one'])
        split_ifs
        · simp
        · simp only [toDigitsCore_lens_eq b f (n / b) (Nat.digitChar <| n % b),
            Nat.succ_le_succ_iff, ih]
Cleared hypotheses: f, n, e, h_e_pos, hlt
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Div (hypothesis)
Goal:
n : ℕ
⊢ (↑n : ℤ) ≡ List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)) [ZMOD 11]
have t : (↑n : ℤ) ≡ ofDigits (-1) (digits 10 n) [ZMOD (↑11 : ℤ)]
Tactic: have t := zmodeq_ofDigits_digits 11 10 (-1 : ℤ) (by unfold Int.ModEq; rfl) n
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Div (goal)
Goal:
n : ℕ
t : (↑n : ℤ) ≡ ofDigits (-1) (digits 10 n) [ZMOD (↑11 : ℤ)]
⊢ (↑n : ℤ) ≡ List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)) [ZMOD 11]
have rwa : ∀ (t : (↑n : ℤ) ≡ List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)) [ZMOD (↑11 : ℤ)]),
  (↑n : ℤ) ≡ List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)) [ZMOD 11]
Tactic: rwa [ofDigits_neg_one] at t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Div (goal)
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ n ↔ b ∣ (b'.digits n).sum
have rw : b ∣ n ↔ b ∣ ofDigits 1 (b'.digits n)
Tactic: rw [← ofDigits_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Div (goal)
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
| b ∣ n
have rw : b ∣ ofDigits b' (b'.digits n)
Tactic: rw [← ofDigits_digits b' n]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Div (goal)
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ n ↔ b ∣ ofDigits 1 (b'.digits n)
have conv_lhs : b ∣ ofDigits b' (b'.digits n) ↔ b ∣ ofDigits 1 (b'.digits n)
Tactic: conv_lhs => rw [← ofDigits_digits b' n]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Div (goal)
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ ofDigits b' (b'.digits n) ↔ b ∣ ofDigits 1 (b'.digits n)
have rw : ofDigits b' (b'.digits n) % b = 0 ↔ b ∣ ofDigits 1 (b'.digits n)
Tactic: rw [Nat.dvd_iff_mod_eq_zero, Nat.dvd_iff_mod_eq_zero, ofDigits_mod, h]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Div (goal)
Goal:
b b' : ℕ
h : b' % b = 1
n : ℕ
rw : ofDigits b' (b'.digits n) % b = 0 ↔ b ∣ ofDigits 1 (b'.digits n)
⊢ b ∣ ofDigits b' (b'.digits n) ↔ b ∣ ofDigits 1 (b'.digits n)
have rw₁ : ofDigits b' (b'.digits n) % b = 0 ↔ ofDigits 1 (b'.digits n) % b = 0
Tactic: rw [Nat.dvd_iff_mod_eq_zero, Nat.dvd_iff_mod_eq_zero, ofDigits_mod, h]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Div (goal)
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
⊢ b ∣ ofDigits b' (b'.digits n) ↔ b ∣ ofDigits 1 (b'.digits n)
have rw₂ : ofDigits (b' % b) (b'.digits n) % b = 0 ↔ ofDigits 1 (b'.digits n) % b = 0
Tactic: rw [Nat.dvd_iff_mod_eq_zero, Nat.dvd_iff_mod_eq_zero, ofDigits_mod, h]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Div (goal)
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
⊢ b ∣ ofDigits b' (b'.digits n) ↔ b ∣ ofDigits 1 (b'.digits n)
have rw₃ : ofDigits 1 (b'.digits n) % b = 0 ↔ ofDigits 1 (b'.digits n) % b = 0
Tactic: rw [Nat.dvd_iff_mod_eq_zero, Nat.dvd_iff_mod_eq_zero, ofDigits_mod, h]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Div (goal)
Goal:
b b' : ℕ
c : ℤ
h : (↑b : ℤ) ∣ (↑b' : ℤ) - c
n : ℕ
⊢ b ∣ n ↔ (↑b : ℤ) ∣ ofDigits c (b'.digits n)
have rw : Dvd.dvd (α := ℤ) (↑b : ℤ) (↑n : ℤ) ↔ (↑b : ℤ) ∣ ofDigits c (b'.digits n)
Tactic: rw [← Int.natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Div (hypothesis)
Goal:
n : ℕ
⊢ 11 ∣ n ↔ Dvd.dvd (α := ℤ) 11 (List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)))
have t : 11 ∣ n ↔ Dvd.dvd (α := ℤ) (↑11 : ℤ) (ofDigits (-1) (digits 10 n))
Tactic: have t := dvd_iff_dvd_ofDigits 11 10 (-1 : ℤ) (by simp) n
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Div (hypothesis)
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)))
have t₁ : 11 ∣ n ↔ Dvd.dvd (α := ℤ) (↑11 : ℤ) (List.alternatingSum (List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)))
Tactic: rw [ofDigits_neg_one] at t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Div (hypothesis)
Goal:
n : ℕ
p : (digits 10 n).Palindrome
h : Even (digits 10 n).length
dig : List ℤ := List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)
⊢ 11 ∣ n
have h₁ : Even dig.length
Tactic: replace h : Even dig.length := by rwa [List.length_map]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Div (goal)
Goal:
n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)
h : Even dig.length
⊢ 11 ∣ n
have refine : dig.alternatingSum = 0
Tactic: refine eleven_dvd_iff.2 ⟨0, (?_ : dig.alternatingSum = 0)⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Div (hypothesis)
Goal:
n : ℕ
p : (digits 10 n).Palindrome
dig : List ℤ := List.map (fun (n : ℕ) ↦ (↑n : ℤ)) (digits 10 n)
h : Even dig.length
⊢ dig.alternatingSum = 0
have this : dig.reverse.alternatingSum = HPow.hPow (α := ℤ) (-1) (dig.length + 1) • dig.alternatingSum
Tactic: have := dig.alternatingSum_reverse
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Div (hypothesis)
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
⊢ dig.alternatingSum = 0
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
l : List ℕ
⊢ 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))
have 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))
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]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
l : List ℕ
⊢ 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))
have e_f : Eq (α := ℕ → ℕ → ℕ) (fun (a i : ℕ) ↦ a * b ^ (i + 1)) fun (a i : ℕ) ↦ b * (a * b ^ i)
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
l : List ℕ
⊢ Eq (α := ℕ → ℕ → ℕ) (fun (a i : ℕ) ↦ a * b ^ (i + 1)) fun (a i : ℕ) ↦ b * (a * b ^ i)
have e_f : ∀ (x x_1 : ℕ), x * b ^ (x_1 + 1) = b * (x * b ^ x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
L : List ℕ
⊢ ofDigits b L = List.sum (List.mapIdx (fun (i a : ℕ) ↦ a * b ^ i) L)
have 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)))
Tactic: rw [List.mapIdx_eq_zipIdx_map, List.zipIdx_eq_zip_range', List.map_zip_eq_zipWith,
    ofDigits_eq_foldr, ← List.range_eq_range']
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Lemmas (goal)
Goal:
b : ℕ
L : List ℕ
⊢ 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)))
have 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 (α := ℕ) []))))
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
Cleared hypotheses: L