awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Count (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
a b : ℕ
h : count p a < count p b
⊢ ∃ x ∈ Set.Ico a b, p x
have obtain : ∀ (k : ℕ) (h : count p a < count p (a + k + 1)), ∃ x ∈ Set.Ico a (a + k + 1), p x
Tactic: obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt (lt_of_count_lt_count h)
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Data.Nat.Count (hypothesis)
Goal:
p : ℕ → Prop
inst : DecidablePred p
a k : ℕ
h : count p a < count p (a + k + 1)
⊢ ∃ x ∈ Set.Ico a (a + k + 1), p x
have h₁ : 0 < count (fun (k : ℕ) ↦ p (a + k)) (k + 1)
Tactic: rw [add_assoc, count_add, Nat.lt_add_right_iff_pos] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Count (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
a k : ℕ
h : 0 < count (fun (k : ℕ) ↦ p (a + k)) (k + 1)
⊢ ∃ x ∈ Set.Ico a (a + k + 1), p x
have obtain : ∀ (t : ℕ) (ht : t < k + 1) (hp : p (a + t)), ∃ x ∈ Set.Ico a (a + k + 1), p x
Tactic: obtain ⟨t, ht, hp⟩ := count_ne_iff_exists.mp h.ne'
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
h : 2 ≤ b
n : ℕ
w : 0 < n
⊢ b.digitsAux h n = n % b :: b.digitsAux h (n / b)
have zero : ∀ (w : LT.lt (α := ℕ) 0 0), b.digitsAux h 0 = 0 % b :: b.digitsAux h (0 / b)
Tactic: cases n
Cleared hypotheses: n, w
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
h : 2 ≤ b
n : ℕ
w : 0 < n
zero : ∀ (w : LT.lt (α := ℕ) 0 0), b.digitsAux h 0 = 0 % b :: b.digitsAux h (0 / b)
⊢ b.digitsAux h n = n % b :: b.digitsAux h (n / b)
have succ : ∀ (n : ℕ) (w : 0 < n + 1), b.digitsAux h (n + 1) = (n + 1) % b :: b.digitsAux h ((n + 1) / b)
Tactic: cases n
Cleared hypotheses: n, w
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
h : 2 ≤ b
n : ℕ
w : 0 < n + 1
⊢ b.digitsAux h (n + 1) = (n + 1) % b :: b.digitsAux h ((n + 1) / b)
have succ : (n + 1) % b :: b.digitsAux h ((n + 1) / b) = (n + 1) % b :: b.digitsAux h ((n + 1) / b)
Tactic: rw [digitsAux]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
⊢ b.digits 0 = []
have zero : digits 0 0 = []
Tactic: rcases b with (_ | ⟨_ | ⟨_⟩⟩)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
zero : digits 0 0 = []
⊢ b.digits 0 = []
have succ : (HAdd.hAdd (α := ℕ) 0 1).digits 0 = []
Tactic: rcases b with (_ | ⟨_ | ⟨_⟩⟩)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
zero : digits 0 0 = []
succ : (HAdd.hAdd (α := ℕ) 0 1).digits 0 = []
⊢ b.digits 0 = []
have succ₁ : ∀ (n : ℕ), (n + 1 + 1).digits 0 = []
Tactic: rcases b with (_ | ⟨_ | ⟨_⟩⟩)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
n b : ℕ
hb : 2 ≤ b
hn : 0 < n
⊢ b.digits n = n % b :: b.digits (n / b)
have rw : (b - 2 + 2).digits n = n % (b - 2 + 2) :: (b - 2 + 2).digits (n / (b - 2 + 2))
Tactic: rw [Nat.eq_add_of_sub_eq hb rfl, Nat.eq_add_of_sub_eq hn rfl, Nat.digits_add_two_add_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
n b : ℕ
hb : 2 ≤ b
hn : 0 < n
rw : (b - 2 + 2).digits n = n % (b - 2 + 2) :: (b - 2 + 2).digits (n / (b - 2 + 2))
⊢ b.digits n = n % b :: b.digits (n / b)
have rw₁ : (b - 2 + 2).digits (n - succ 0 + succ 0) =
  (n - succ 0 + succ 0) % (b - 2 + 2) :: (b - 2 + 2).digits ((n - succ 0 + succ 0) / (b - 2 + 2))
Tactic: rw [Nat.eq_add_of_sub_eq hb rfl, Nat.eq_add_of_sub_eq hn rfl, Nat.digits_add_two_add_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
n b : ℕ
hb : 2 ≤ b
hn : 0 < n
rw : (b - 2 + 2).digits n = n % (b - 2 + 2) :: (b - 2 + 2).digits (n / (b - 2 + 2))
rw₁ :
  (b - 2 + 2).digits (n - succ 0 + succ 0) =
    (n - succ 0 + succ 0) % (b - 2 + 2) :: (b - 2 + 2).digits ((n - succ 0 + succ 0) / (b - 2 + 2))
⊢ b.digits n = n % b :: b.digits (n / b)
have rw₂ : (n - succ 0 + 1) % (b - 2 + 2) :: (b - 2 + 2).digits ((n - succ 0 + 1) / (b - 2 + 2)) =
  (n - succ 0 + succ 0) % (b - 2 + 2) :: (b - 2 + 2).digits ((n - succ 0 + succ 0) / (b - 2 + 2))
Tactic: rw [Nat.eq_add_of_sub_eq hb rfl, Nat.eq_add_of_sub_eq hn rfl, Nat.digits_add_two_add_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b x : ℕ
hx : x ≠ 0
hxb : x < b
⊢ b.digits x = [x]
have rcases : ∀ (x : ℕ) (hx : x.succ ≠ 0) (hxb : x.succ < b), b.digits x.succ = [x.succ]
Tactic: rcases exists_eq_succ_of_ne_zero hx with ⟨x, rfl⟩
Cleared hypotheses: x, hx, hxb
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b x : ℕ
hx : x.succ ≠ 0
hxb : x.succ < b
⊢ b.digits x.succ = [x.succ]
have rcases : ∀ (b : ℕ) (hxb : x.succ < b + succ 1), (b + succ 1).digits x.succ = [x.succ]
Tactic: rcases Nat.exists_eq_add_of_le' ((Nat.le_add_left 1 x).trans_lt hxb) with ⟨b, rfl⟩
Cleared hypotheses: b, hxb
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
x : ℕ
hx : x.succ ≠ 0
b : ℕ
hxb : x.succ < b + succ 1
⊢ (b + succ 1).digits x.succ = [x.succ]
have rw : (x + 1) % (b + 2) :: (b + 2).digits ((x + 1) / (b + 2)) = [x.succ]
Tactic: rw [digits_add_two_add_one, div_eq_of_lt hxb, digits_zero, mod_eq_of_lt hxb]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
x : ℕ
hx : x.succ ≠ 0
b : ℕ
hxb : x.succ < b + succ 1
rw : (x + 1) % (b + 2) :: (b + 2).digits ((x + 1) / (b + 2)) = [x.succ]
⊢ (b + succ 1).digits x.succ = [x.succ]
have rw₁ : (x + 1) % (b + 2) :: (b + 2).digits 0 = [x.succ]
Tactic: rw [digits_add_two_add_one, div_eq_of_lt hxb, digits_zero, mod_eq_of_lt hxb]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
x : ℕ
hx : x.succ ≠ 0
b : ℕ
hxb : x.succ < b + succ 1
rw : (x + 1) % (b + 2) :: (b + 2).digits ((x + 1) / (b + 2)) = [x.succ]
rw₁ : (x + 1) % (b + 2) :: (b + 2).digits 0 = [x.succ]
⊢ (b + succ 1).digits x.succ = [x.succ]
have rw₂ : [(x + 1) % (b + 2)] = [x.succ]
Tactic: rw [digits_add_two_add_one, div_eq_of_lt hxb, digits_zero, mod_eq_of_lt hxb]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
x : ℕ
hx : x.succ ≠ 0
b : ℕ
hxb : x.succ < b + succ 1
rw : (x + 1) % (b + 2) :: (b + 2).digits ((x + 1) / (b + 2)) = [x.succ]
rw₁ : (x + 1) % (b + 2) :: (b + 2).digits 0 = [x.succ]
rw₂ : [(x + 1) % (b + 2)] = [x.succ]
⊢ (b + succ 1).digits x.succ = [x.succ]
have rw₃ : [x.succ] = [x.succ]
Tactic: rw [digits_add_two_add_one, div_eq_of_lt hxb, digits_zero, mod_eq_of_lt hxb]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
h : 1 < b
x y : ℕ
hxb : x < b
hxy : x ≠ 0 ∨ y ≠ 0
⊢ b.digits (x + b * y) = x :: b.digits y
have rcases : ∀ (b : ℕ) (h : 1 < b + 2) (hxb : x < b + 2), (b + 2).digits (x + (b + 2) * y) = x :: (b + 2).digits y
Tactic: rcases Nat.exists_eq_add_of_le' h with ⟨b, rfl : _ = _ + 2⟩
Cleared hypotheses: b, h, hxb
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
x y : ℕ
hxy : x ≠ 0 ∨ y ≠ 0
b : ℕ
h : 1 < b + 2
hxb : x < b + 2
⊢ (b + 2).digits (x + (b + 2) * y) = x :: (b + 2).digits y
have zero : ∀ (hxy : x ≠ 0 ∨ Ne (α := ℕ) 0 0), (b + 2).digits (x + (b + 2) * 0) = x :: (b + 2).digits 0
Tactic: cases y
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
x y : ℕ
hxy : x ≠ 0 ∨ y ≠ 0
b : ℕ
h : 1 < b + 2
hxb : x < b + 2
zero : ∀ (hxy : x ≠ 0 ∨ Ne (α := ℕ) 0 0), (b + 2).digits (x + (b + 2) * 0) = x :: (b + 2).digits 0
⊢ (b + 2).digits (x + (b + 2) * y) = x :: (b + 2).digits y
have succ : ∀ (n : ℕ) (hxy : x ≠ 0 ∨ n + 1 ≠ 0), (b + 2).digits (x + (b + 2) * (n + 1)) = x :: (b + 2).digits (n + 1)
Tactic: cases y
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
x b : ℕ
h : 1 < b + 2
hxb : x < b + 2
n : ℕ
hxy : x ≠ 0 ∨ n + 1 ≠ 0
⊢ (b + 2).digitsAux ⋯ (x + (b + 2) * (n + 1)) = x :: (b + 2).digitsAux ⋯ (n + 1)
have succ : (x + (b + 2) * (n + 1)) % (b + 2) :: (b + 2).digitsAux sorry ((x + (b + 2) * (n + 1)) / (b + 2)) =
  x :: (b + 2).digitsAux sorry (n + 1)
Tactic: rw [digitsAux_def]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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)
⊢ (b + 2).digitsAux ⋯ (x + (b + 2) * (n + 1)) = x :: (b + 2).digitsAux ⋯ (n + 1)
have succ₁ : 0 < x + (b + 2) * (n + 1)
Tactic: rw [digitsAux_def]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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) :: (b + 2).digitsAux ⋯ ((x + (b + 2) * (n + 1)) / (b + 2)) =
    x :: (b + 2).digitsAux ⋯ (n + 1)
have succ : (x + (b + 2) * (n + 1)) % (b + 2) = x
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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
⊢ (x + (b + 2) * (n + 1)) % (b + 2) :: (b + 2).digitsAux ⋯ ((x + (b + 2) * (n + 1)) / (b + 2)) =
    x :: (b + 2).digitsAux ⋯ (n + 1)
have succ₁ : (x + (b + 2) * (n + 1)) / (b + 2) = n + 1
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
α : Type u_1
inst : Semiring α
b : α
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)
have cons : (↑d : α) + b * ofDigits b L = (↑d : α) + b * List.foldr (fun (x : ℕ) (y : α) ↦ (↑x : α) + b * y) 0 L
Tactic: dsimp [ofDigits]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
α : Type u_1
inst : Semiring α
b : α
d : ℕ
L : List ℕ
ih : ofDigits b L = 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
have 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
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
α : Type u_1
inst : Semiring α
b : α
L : List ℕ
⊢ ofDigits b L = List.foldr (fun (x : ℕ) (y : α) ↦ (↑x : α) + b * y) 0 L
have nil : ofDigits b [] = List.foldr (fun (x : ℕ) (y : α) ↦ (↑x : α) + b * y) 0 []
Tactic: induction L with
  | nil => rfl
  | cons d L ih => dsimp [ofDigits]; rw [ih]
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
α : Type u_1
inst : Semiring α
b : α
L : List ℕ
nil : ofDigits b [] = List.foldr (fun (x : ℕ) (y : α) ↦ (↑x : α) + b * y) 0 []
⊢ ofDigits b L = List.foldr (fun (x : ℕ) (y : α) ↦ (↑x : α) + b * y) 0 L
have 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)
Tactic: induction L with
  | nil => rfl
  | cons d L ih => dsimp [ofDigits]; rw [ih]
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
l2 : List ℕ
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
have cons : (↑hd : ℕ) + b * (ofDigits b tl + b ^ tl.length * ofDigits b l2) =
  (↑hd : ℕ) + b * ofDigits b tl + b * b ^ tl.length * ofDigits b l2
Tactic: rw [ofDigits, List.cons_append, ofDigits, IH, List.length_cons, pow_succ']
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
l1 l2 : List ℕ
⊢ ofDigits b (l1 ++ l2) = ofDigits b l1 + b ^ l1.length * ofDigits b l2
have nil : ofDigits b ([] ++ l2) = ofDigits b [] + b ^ List.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
Cleared hypotheses: l1
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
l1 l2 : List ℕ
nil : ofDigits b ([] ++ l2) = ofDigits b [] + b ^ List.length (α := ℕ) [] * ofDigits b l2
⊢ ofDigits b (l1 ++ l2) = ofDigits b l1 + b ^ l1.length * ofDigits b l2
have 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
Tactic: induction l1 with
  | nil => simp [ofDigits]
  | cons hd tl IH =>
    rw [ofDigits, List.cons_append, ofDigits, IH, List.length_cons, pow_succ']
    ring
Cleared hypotheses: l1
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
l : List ℕ
⊢ ofDigits b (l ++ [0]) = ofDigits b l
have rw : ofDigits b l + b ^ l.length * ofDigits b [0] = ofDigits b l
Tactic: rw [ofDigits_append, ofDigits_singleton, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
l : List ℕ
rw : ofDigits b l + b ^ l.length * ofDigits b [0] = ofDigits b l
⊢ ofDigits b (l ++ [0]) = ofDigits b l
have rw₁ : ofDigits b l + b ^ l.length * 0 = ofDigits b l
Tactic: rw [ofDigits_append, ofDigits_singleton, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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
⊢ ofDigits b (l ++ [0]) = ofDigits b l
have rw₂ : ofDigits b l + 0 = ofDigits b l
Tactic: rw [ofDigits_append, ofDigits_singleton, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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
⊢ ofDigits b (l ++ [0]) = ofDigits b l
have rw₃ : ofDigits b l = ofDigits b l
Tactic: rw [ofDigits_append, ofDigits_singleton, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b k : ℕ
⊢ ofDigits b (List.replicate k 0) = 0
have zero : ofDigits b (List.replicate 0 0) = 0
Tactic: induction k with
  | zero => rfl
  | succ k ih => simp [List.replicate, ofDigits_cons, ih]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b k : ℕ
zero : ofDigits b (List.replicate 0 0) = 0
⊢ ofDigits b (List.replicate k 0) = 0
have succ : ∀ (k : ℕ) (ih : ofDigits b (List.replicate k 0) = 0), ofDigits b (List.replicate (k + 1) 0) = 0
Tactic: induction k with
  | zero => rfl
  | succ k ih => simp [List.replicate, ofDigits_cons, ih]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b k : ℕ
l : List ℕ
⊢ ofDigits b (l ++ List.replicate k 0) = ofDigits b l
have rw : ofDigits b l + b ^ l.length * ofDigits b (List.replicate k 0) = ofDigits b l
Tactic: rw [ofDigits_append]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
l : List ℕ
d : ℕ
⊢ ofDigits b (d :: l).reverse = ofDigits b l.reverse + b ^ l.length * d
have simp : ofDigits b (l.reverse ++ [d]) = ofDigits b l.reverse + b ^ l.length * d
Tactic: simp only [List.reverse_cons]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
b : ℕ
l : List ℕ
d : ℕ
⊢ ofDigits b (l.reverse ++ [d]) = ofDigits b l.reverse + b ^ l.length * d
have rw : ofDigits b l.reverse + b ^ l.reverse.length * ofDigits b [d] = ofDigits b l.reverse + b ^ l.length * d
Tactic: rw [ofDigits_append]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
α : Type u_1
inst : Semiring α
b 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))
have cons : (↑(d + b * ofDigits b L) : α) = (↑d : α) + HMul.hMul (α := α) (↑b : α) (ofDigits (↑b : α) L)
Tactic: dsimp [ofDigits]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
α : Type u_1
inst : Semiring α
b d : ℕ
L : List ℕ
ih : Eq.{u_1 + 1} (α := α) (↑(ofDigits b L) : α) (ofDigits (↑b : α) L)
⊢ (↑(d + b * ofDigits b L) : α) = (↑d : α) + HMul.hMul (α := α) (↑b : α) (ofDigits (↑b : α) L)
have cons : (↑d : α) + HMul.hMul (α := α) (↑b : α) (↑(ofDigits b L) : α) =
  (↑d : α) + HMul.hMul (α := α) (↑b : α) (ofDigits (↑b : α) L)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
α : Type u_1
inst : Semiring α
b d : ℕ
L : List ℕ
ih : Eq.{u_1 + 1} (α := α) (↑(ofDigits b L) : α) (ofDigits (↑b : α) L)
⊢ (↑d : α) + HMul.hMul (α := α) (↑b : α) (↑(ofDigits b L) : α) =
    (↑d : α) + HMul.hMul (α := α) (↑b : α) (ofDigits (↑b : α) L)
have cons : (↑d : α) + HMul.hMul (α := α) (↑b : α) (ofDigits (↑b : α) L) =
  (↑d : α) + HMul.hMul (α := α) (↑b : α) (ofDigits (↑b : α) L)
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
α : Type u_1
inst : Semiring α
b : ℕ
L : List ℕ
⊢ Eq.{u_1 + 1} (α := α) (↑(ofDigits b L) : α) (ofDigits (↑b : α) L)
have nil : Eq.{u_1 + 1} (α := α) (↑(ofDigits b []) : α) (ofDigits (↑b : α) [])
Tactic: induction L with
  | nil => simp [ofDigits]
  | cons d L ih => dsimp [ofDigits]; push_cast; rw [ih]
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
Goal:
α : Type u_1
inst : Semiring α
b : ℕ
L : List ℕ
nil : Eq.{u_1 + 1} (α := α) (↑(ofDigits b []) : α) (ofDigits (↑b : α) [])
⊢ Eq.{u_1 + 1} (α := α) (↑(ofDigits b L) : α) (ofDigits (↑b : α) L)
have 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))
Tactic: induction L with
  | nil => simp [ofDigits]
  | cons d L ih => dsimp [ofDigits]; push_cast; rw [ih]
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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
⊢ b.digits (ofDigits b (d :: L)) = d :: L
have cons : b.digits (d + b * ofDigits b L) = d :: L
Tactic: dsimp [ofDigits]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (hypothesis)
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
⊢ b.digits (d + b * ofDigits b L) = d :: L
have w₃ : (d :: L).getLast sorry ≠ 0
Tactic: replace w₂ := w₂ (by simp)
Cleared hypotheses: w₂
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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
⊢ b.digits (d + b * ofDigits b L) = d :: L
have cons : d :: b.digits (ofDigits b L) = d :: L
Tactic: rw [digits_add b h]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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
⊢ b.digits (d + b * ofDigits b L) = d :: L
have cons₁ : d < b
Tactic: rw [digits_add b h]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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
⊢ b.digits (d + b * ofDigits b L) = d :: L
have cons₂ : d ≠ 0 ∨ ofDigits b L ≠ 0
Tactic: rw [digits_add b h]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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.digits (ofDigits b L) = d :: L
have cons : ∀ l ∈ L, l < b
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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
⊢ d :: b.digits (ofDigits b L) = d :: L
have cons₁ : ∀ (h : L ≠ []), L.getLast h ≠ 0
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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 < b
have cons : l ∈ d :: L
Tactic: apply w₁
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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 ≠ 0 ∨ ofDigits b L ≠ 0
have pos : ∀ (h' : L = []), d ≠ 0 ∨ ofDigits b L ≠ 0
Tactic: by_cases h' : L = []
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0
have neg : ∀ (h' : ¬L = []), d ≠ 0 ∨ ofDigits b L ≠ 0
Tactic: by_cases h' : L = []
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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 = []
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0
have 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 sorry ≠ 0), d ≠ 0 ∨ ofDigits b [] ≠ 0
Tactic: rcases h' with rfl
Cleared hypotheses: L, ih, w₁, w₂, h'
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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 ∨ ofDigits b [] ≠ 0
have pos : d ≠ 0
Tactic: left
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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 = []
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0
have neg : ofDigits b L ≠ 0
Tactic: right
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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 = []
⊢ ofDigits b L ≠ 0
have neg : ∀ (w₂ : ofDigits b L = 0), (d :: L).getLast sorry = 0
Tactic: contrapose w₂
Cleared hypotheses: w₂
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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
have neg : (d :: L).getLast sorry ∈ L
Tactic: refine digits_zero_of_eq_zero h.ne_bot w₂ _ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Digits.Defs (goal)
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 ⋯ ∈ L
have neg : L.getLast h' ∈ L
Tactic: rw [List.getLast_cons h']