-- Mathlib/Data/Nat/Digits.lean
theorem ofDigits_digits (b n : ℕ) : ofDigits b (digits b n) = n

Proof state:
case succ.zero.succ
n : ℕ
ih : ofDigits 1 (digits 1 n) = n
⊢ ofDigits 1 (digits 1 (n + 1)) = n + 1

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

Result:
no goals

Proof state:
case zero.succ
n : ℕ
⊢ ofDigits 0 (digits 0 (n + 1)) = n + 1

Tactic:
simp

Result:
no goals

Proof state:
b n : ℕ
⊢ ofDigits b (b.digits n) = n

Tactic:
rcases b with - | b

Result:
case zero
n : ℕ
⊢ ofDigits 0 (digits 0 n) = n

case succ
n b : ℕ
⊢ ofDigits (b + 1) ((b + 1).digits n) = n

Proof state:
case succ.succ.ind.succ
b n✝ : ℕ
h : ∀ m < n✝ + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((n✝ + 1) % (b + 2) :: (b + 2).digits ((n✝ + 1) / (b + 2))) = n✝ + 1

Tactic:
dsimp [ofDigits]

Result:
case succ.succ.ind.succ
b n✝ : ℕ
h : ∀ m < n✝ + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ (n✝ + 1) % (b + 2) + (b + 1 + 1) * ofDigits (b + 1 + 1) ((b + 2).digits ((n✝ + 1) / (b + 2))) = n✝ + 1

Proof state:
case succ.zero.zero

⊢ ofDigits (0 + 1) ((0 + 1).digits 0) = 0

Tactic:
rfl

Result:
no goals

Proof state:
case succ.succ.ind
b n : ℕ
h : ∀ m < n, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits n) = n

Tactic:
cases n

Result:
case succ.succ.ind.zero
b : ℕ
h : ∀ m < 0, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits 0) = 0

case succ.succ.ind.succ
b n✝ : ℕ
h : ∀ m < n✝ + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits (n✝ + 1)) = n✝ + 1

Proof state:
case zero
n : ℕ
⊢ ofDigits 0 (digits 0 n) = n

Tactic:
rcases n with - | n

Result:
case zero.zero

⊢ ofDigits 0 (digits 0 0) = 0

case zero.succ
n : ℕ
⊢ ofDigits 0 (digits 0 (n + 1)) = n + 1

Proof state:
case succ.succ.ind.zero
b : ℕ
h : ∀ m < 0, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) [] = 0

Tactic:
rfl

Result:
no goals

Proof state:
case zero.zero

⊢ ofDigits 0 (digits 0 0) = 0

Tactic:
rfl

Result:
no goals

Proof state:
case succ.succ.ind.succ
b n✝ : ℕ
h : ∀ m < n✝ + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ (n✝ + 1) % (b + 2) + (b + 1 + 1) * ((n✝ + 1) / (b + 2)) = n✝ + 1

Tactic:
rw [Nat.mod_add_div]

Result:
no goals

Proof state:
case succ.succ.ind.succ
b n✝ : ℕ
h : ∀ m < n✝ + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits (n✝ + 1)) = n✝ + 1

Tactic:
simp only [Nat.succ_eq_add_one, digits_add_two_add_one]

Result:
case succ.succ.ind.succ
b n✝ : ℕ
h : ∀ m < n✝ + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((n✝ + 1) % (b + 2) :: (b + 2).digits ((n✝ + 1) / (b + 2))) = n✝ + 1

Proof state:
case succ.zero
n : ℕ
⊢ ofDigits (0 + 1) ((0 + 1).digits n) = n

Tactic:
induction' n with n ih

Result:
case succ.zero.zero

⊢ ofDigits (0 + 1) ((0 + 1).digits 0) = 0

case succ.zero.succ
n : ℕ
ih : ofDigits (0 + 1) ((0 + 1).digits n) = n
⊢ ofDigits (0 + 1) ((0 + 1).digits (n + 1)) = n + 1

Proof state:
case succ.succ.ind.zero
b : ℕ
h : ∀ m < 0, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits 0) = 0

Tactic:
rw [digits_zero]

Result:
case succ.succ.ind.zero
b : ℕ
h : ∀ m < 0, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) [] = 0

Proof state:
case succ.zero.succ
n : ℕ
ih : ofDigits (0 + 1) ((0 + 1).digits n) = n
⊢ ofDigits (0 + 1) ((0 + 1).digits (n + 1)) = n + 1

Tactic:
rw [Nat.zero_add] at ih ⊢

Result:
case succ.zero.succ
n : ℕ
ih : ofDigits 1 (digits 1 n) = n
⊢ ofDigits 1 (digits 1 (n + 1)) = n + 1

Proof state:
case succ.succ.ind.succ
b n✝ : ℕ
h : ∀ m < n✝ + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ (n✝ + 1) % (b + 2) + (b + 1 + 1) * ofDigits (b + 1 + 1) ((b + 2).digits ((n✝ + 1) / (b + 2))) = n✝ + 1

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

Result:
case succ.succ.ind.succ
b n✝ : ℕ
h : ∀ m < n✝ + 1, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ (n✝ + 1) % (b + 2) + (b + 1 + 1) * ((n✝ + 1) / (b + 2)) = n✝ + 1

Proof state:
case succ.succ
n b : ℕ
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits n) = n

Tactic:
induction n using Nat.strongRecOn with | ind n h => ?_

Result:
case succ.succ.ind
b n : ℕ
h : ∀ m < n, ofDigits (b + 1 + 1) ((b + 1 + 1).digits m) = m
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits n) = n

Proof state:
case succ
n b : ℕ
⊢ ofDigits (b + 1) ((b + 1).digits n) = n

Tactic:
rcases b with - | b

Result:
case succ.zero
n : ℕ
⊢ ofDigits (0 + 1) ((0 + 1).digits n) = n

case succ.succ
n b : ℕ
⊢ ofDigits (b + 1 + 1) ((b + 1 + 1).digits n) = n