case zero
n✝ n : ℕ
⊢ ofDigits zero (digits zero n) = n

case succ
n✝ n b : ℕ
⊢ ofDigits (succ b) (digits (succ b) n) = n
n✝ b n : ℕ
⊢ ofDigits b (digits b n) = n
cases' b with b
case zero.zero
n : ℕ
⊢ ofDigits zero (digits zero zero) = zero

case zero.succ
n✝ n : ℕ
⊢ ofDigits zero (digits zero (succ n)) = succ n
case zero
n✝ n : ℕ
⊢ ofDigits zero (digits zero n) = n
cases' n with n
no goals
case zero.zero
n : ℕ
⊢ ofDigits zero (digits zero zero) = zero
rfl
case zero.succ
n✝ n : ℕ
⊢ ofDigits 0 [n + 1] = n + 1
case zero.succ
n✝ n : ℕ
⊢ ofDigits zero (digits zero (succ n)) = succ n
change ofDigits 0 [n + 1] = n + 1
no goals
case zero.succ
n✝ n : ℕ
⊢ ofDigits 0 [n + 1] = n + 1
dsimp [ofDigits]
case succ.zero
n✝ n : ℕ
⊢ ofDigits (succ zero) (digits (succ zero) n) = n

case succ.succ
n✝ n b : ℕ
⊢ ofDigits (succ (succ b)) (digits (succ (succ b)) n) = n
case succ
n✝ n b : ℕ
⊢ ofDigits (succ b) (digits (succ b) n) = n
cases' b with b
case succ.zero.zero
n : ℕ
⊢ ofDigits (succ zero) (digits (succ zero) zero) = zero

case succ.zero.succ
n✝ n : ℕ
ih : ofDigits (succ zero) (digits (succ zero) n) = n
⊢ ofDigits (succ zero) (digits (succ zero) (succ n)) = succ n
case succ.zero
n✝ n : ℕ
⊢ ofDigits (succ zero) (digits (succ zero) n) = n
induction' n with n ih
no goals
case succ.zero.zero
n : ℕ
⊢ ofDigits (succ zero) (digits (succ zero) zero) = zero
rfl
case succ.zero.succ
n✝ n : ℕ
ih : ofDigits 1 (digits 1 n) = n
⊢ ofDigits 1 (digits 1 (succ n)) = succ n
case succ.zero.succ
n✝ n : ℕ
ih : ofDigits (succ zero) (digits (succ zero) n) = n
⊢ ofDigits (succ zero) (digits (succ zero) (succ n)) = succ n
rw[show succ zero = 1 by rfl] at ih ⊢
no goals
case succ.zero.succ
n✝ n : ℕ
ih : ofDigits 1 (digits 1 n) = n
⊢ ofDigits 1 (digits 1 (succ n)) = succ n
simp only [ih, add_comm 1, ofDigits_one_cons, Nat.cast_id, digits_one_succ]
no goals
n✝ n : ℕ
ih : ofDigits 1 (digits 1 n) = n
⊢ succ zero = 1
rfl
n✝ n b : ℕ
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ), m < n → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m) →
      ofDigits (succ (succ b)) (digits (succ (succ b)) n) = n
case succ.succ
n✝ n b : ℕ
⊢ ofDigits (succ (succ b)) (digits (succ (succ b)) n) = n
apply Nat.strongInductionOn n _
n b : ℕ
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ), m < n → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m) →
      ofDigits (succ (succ b)) (digits (succ (succ b)) n) = n
n✝ n b : ℕ
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ), m < n → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m) →
      ofDigits (succ (succ b)) (digits (succ (succ b)) n) = n
clear n
n✝ b n : ℕ
h : ∀ (m : ℕ), m < n → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m
⊢ ofDigits (succ (succ b)) (digits (succ (succ b)) n) = n
n b : ℕ
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ), m < n → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m) →
      ofDigits (succ (succ b)) (digits (succ (succ b)) n) = n
intro n h
case zero
n b : ℕ
h : ∀ (m : ℕ), m < zero → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m
⊢ ofDigits (succ (succ b)) (digits (succ (succ b)) zero) = zero

case succ
n b n✝ : ℕ
h : ∀ (m : ℕ), m < succ n✝ → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m
⊢ ofDigits (succ (succ b)) (digits (succ (succ b)) (succ n✝)) = succ n✝
n✝ b n : ℕ
h : ∀ (m : ℕ), m < n → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m
⊢ ofDigits (succ (succ b)) (digits (succ (succ b)) n) = n
cases n
case zero
n b : ℕ
h : ∀ (m : ℕ), m < zero → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m
⊢ ofDigits (succ (succ b)) [] = zero
case zero
n b : ℕ
h : ∀ (m : ℕ), m < zero → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m
⊢ ofDigits (succ (succ b)) (digits (succ (succ b)) zero) = zero
rw [digits_zero]
no goals
case zero
n b : ℕ
h : ∀ (m : ℕ), m < zero → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m
⊢ ofDigits (succ (succ b)) [] = zero
rfl
case succ
n b n✝ : ℕ
h : ∀ (m : ℕ), m < succ n✝ → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m
⊢ ofDigits (b + 1 + 1) ((n✝ + 1) % (b + 2) :: digits (b + 2) ((n✝ + 1) / (b + 2))) = n✝ + 1
case succ
n b n✝ : ℕ
h : ∀ (m : ℕ), m < succ n✝ → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m
⊢ ofDigits (succ (succ b)) (digits (succ (succ b)) (succ n✝)) = succ n✝
simp only [Nat.succ_eq_add_one, digits_add_two_add_one]
case succ
n b n✝ : ℕ
h : ∀ (m : ℕ), m < succ n✝ → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m
⊢ (n✝ + 1) % (b + 2) + (b + 1 + 1) * ofDigits (b + 1 + 1) (digits (b + 2) ((n✝ + 1) / (b + 2))) = n✝ + 1
case succ
n b n✝ : ℕ
h : ∀ (m : ℕ), m < succ n✝ → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m
⊢ ofDigits (b + 1 + 1) ((n✝ + 1) % (b + 2) :: digits (b + 2) ((n✝ + 1) / (b + 2))) = n✝ + 1
dsimp [ofDigits]
case succ
n b n✝ : ℕ
h : ∀ (m : ℕ), m < succ n✝ → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m
⊢ (n✝ + 1) % (b + 2) + (b + 1 + 1) * ((n✝ + 1) / (b + 2)) = n✝ + 1
case succ
n b n✝ : ℕ
h : ∀ (m : ℕ), m < succ n✝ → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m
⊢ (n✝ + 1) % (b + 2) + (b + 1 + 1) * ofDigits (b + 1 + 1) (digits (b + 2) ((n✝ + 1) / (b + 2))) = n✝ + 1
rw [h _ (Nat.div_lt_self' _ b)]
no goals
case succ
n b n✝ : ℕ
h : ∀ (m : ℕ), m < succ n✝ → ofDigits (succ (succ b)) (digits (succ (succ b)) m) = m
⊢ (n✝ + 1) % (b + 2) + (b + 1 + 1) * ((n✝ + 1) / (b + 2)) = n✝ + 1
rw [Nat.mod_add_div]