case zero
n m : ℕ
hm : m ≠ 0
⊢ List.getLast (digits zero m) (_ : digits zero m ≠ []) ≠ 0

case succ.zero
n m : ℕ
hm : m ≠ 0
⊢ List.getLast (digits (succ zero) m) (_ : digits (succ zero) m ≠ []) ≠ 0

case succ.succ
n m : ℕ
hm : m ≠ 0
b : ℕ
⊢ List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
n b m : ℕ
hm : m ≠ 0
⊢ List.getLast (digits b m) (_ : digits b m ≠ []) ≠ 0
rcases b with (_ | _ | b)
case succ.succ
n m b : ℕ
⊢ ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
case succ.succ
n m : ℕ
hm : m ≠ 0
b : ℕ
⊢ List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
revert hm
case succ.succ
n m b : ℕ
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ),
        m < n → ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0) →
      ∀ (hm : n ≠ 0), List.getLast (digits (succ (succ b)) n) (_ : digits (succ (succ b)) n ≠ []) ≠ 0
case succ.succ
n m b : ℕ
⊢ ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
apply Nat.strongInductionOn m
case succ.succ
n✝ m b n : ℕ
IH : ∀ (m : ℕ), m < n → ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
hn : n ≠ 0
⊢ List.getLast (digits (succ (succ b)) n) (_ : digits (succ (succ b)) n ≠ []) ≠ 0
case succ.succ
n m b : ℕ
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ),
        m < n → ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0) →
      ∀ (hm : n ≠ 0), List.getLast (digits (succ (succ b)) n) (_ : digits (succ (succ b)) n ≠ []) ≠ 0
intro n IH hn
case pos
n✝ m b n : ℕ
IH : ∀ (m : ℕ), m < n → ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
hn : n ≠ 0
hnb : n < b + 2
⊢ List.getLast (digits (succ (succ b)) n) (_ : digits (succ (succ b)) n ≠ []) ≠ 0

case neg
n✝ m b n : ℕ
IH : ∀ (m : ℕ), m < n → ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ List.getLast (digits (succ (succ b)) n) (_ : digits (succ (succ b)) n ≠ []) ≠ 0
case succ.succ
n✝ m b n : ℕ
IH : ∀ (m : ℕ), m < n → ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
hn : n ≠ 0
⊢ List.getLast (digits (succ (succ b)) n) (_ : digits (succ (succ b)) n ≠ []) ≠ 0
by_cases hnb : n < b + 2
case zero.zero
n : ℕ
hm : zero ≠ 0
⊢ List.getLast (digits zero zero) (_ : digits zero zero ≠ []) ≠ 0

case zero.succ
n n✝ : ℕ
hm : succ n✝ ≠ 0
⊢ List.getLast (digits zero (succ n✝)) (_ : digits zero (succ n✝) ≠ []) ≠ 0
case zero
n m : ℕ
hm : m ≠ 0
⊢ List.getLast (digits zero m) (_ : digits zero m ≠ []) ≠ 0
cases m
no goals
case zero.zero
n : ℕ
hm : zero ≠ 0
⊢ List.getLast (digits zero zero) (_ : digits zero zero ≠ []) ≠ 0
cases hm rfl
no goals
case zero.succ
n n✝ : ℕ
hm : succ n✝ ≠ 0
⊢ List.getLast (digits zero (succ n✝)) (_ : digits zero (succ n✝) ≠ []) ≠ 0
simp
case succ.zero.zero
n : ℕ
hm : zero ≠ 0
⊢ List.getLast (digits (succ zero) zero) (_ : digits (succ zero) zero ≠ []) ≠ 0

case succ.zero.succ
n n✝ : ℕ
hm : succ n✝ ≠ 0
⊢ List.getLast (digits (succ zero) (succ n✝)) (_ : digits (succ zero) (succ n✝) ≠ []) ≠ 0
case succ.zero
n m : ℕ
hm : m ≠ 0
⊢ List.getLast (digits (succ zero) m) (_ : digits (succ zero) m ≠ []) ≠ 0
cases m
case succ.zero.succ
n m : ℕ
hm : succ m ≠ 0
⊢ List.getLast (digits (succ zero) (succ m)) (_ : digits (succ zero) (succ m) ≠ []) ≠ 0
case succ.zero.succ
n n✝ : ℕ
hm : succ n✝ ≠ 0
⊢ List.getLast (digits (succ zero) (succ n✝)) (_ : digits (succ zero) (succ n✝) ≠ []) ≠ 0
rename ℕ => m
case succ.zero.succ
n m : ℕ
hm : succ m ≠ 0
this : ∀ (v : ℕ), List.getLast (digits (succ zero) (succ v)) (_ : ¬1 :: List.replicate v 1 = []) = 1
⊢ List.getLast (digits (succ zero) (succ m)) (_ : digits (succ zero) (succ m) ≠ []) ≠ 0
case succ.zero.succ
n m : ℕ
hm : succ m ≠ 0
⊢ List.getLast (digits (succ zero) (succ m)) (_ : digits (succ zero) (succ m) ≠ []) ≠ 0
have : ∀ v, List.getLast (digits (succ zero) (succ v)) (by simp [digits, digitsAux1]) = 1 := by
  intros v; induction v <;> simp; assumption
no goals
case succ.zero.succ
n m : ℕ
hm : succ m ≠ 0
this : ∀ (v : ℕ), List.getLast (digits (succ zero) (succ v)) (_ : ¬1 :: List.replicate v 1 = []) = 1
⊢ List.getLast (digits (succ zero) (succ m)) (_ : digits (succ zero) (succ m) ≠ []) ≠ 0
simp only [digits_one, List.getLast_replicate_succ m 1, this]
no goals
case succ.zero.zero
n : ℕ
hm : zero ≠ 0
⊢ List.getLast (digits (succ zero) zero) (_ : digits (succ zero) zero ≠ []) ≠ 0
cases hm rfl
no goals
n m : ℕ
hm : succ m ≠ 0
v : ℕ
⊢ digits (succ zero) (succ v) ≠ []
simp [digits, digitsAux1]
n m : ℕ
hm : succ m ≠ 0
v : ℕ
⊢ List.getLast (digits (succ zero) (succ v)) (_ : ¬1 :: List.replicate v 1 = []) = 1
n m : ℕ
hm : succ m ≠ 0
⊢ ∀ (v : ℕ), List.getLast (digits (succ zero) (succ v)) (_ : ¬1 :: List.replicate v 1 = []) = 1
intros v
case succ
n m : ℕ
hm : succ m ≠ 0
n✝ : ℕ
n_ih✝ : List.getLast (digits (succ zero) (succ n✝)) (_ : ¬1 :: List.replicate n✝ 1 = []) = 1
⊢ List.getLast (digits (succ 0) (succ (succ n✝))) (_ : ¬1 :: List.replicate (succ n✝) 1 = []) = 1
n m : ℕ
hm : succ m ≠ 0
v : ℕ
⊢ List.getLast (digits (succ zero) (succ v)) (_ : ¬1 :: List.replicate v 1 = []) = 1
induction v <;> simp
no goals
case succ
n m : ℕ
hm : succ m ≠ 0
n✝ : ℕ
n_ih✝ : List.getLast (digits (succ zero) (succ n✝)) (_ : ¬1 :: List.replicate n✝ 1 = []) = 1
⊢ List.getLast (digits (succ 0) (succ (succ n✝))) (_ : ¬1 :: List.replicate (succ n✝) 1 = []) = 1
assumption
no goals
case pos
n✝ m b n : ℕ
IH : ∀ (m : ℕ), m < n → ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
hn : n ≠ 0
hnb : n < b + 2
⊢ List.getLast (digits (succ (succ b)) n) (_ : digits (succ (succ b)) n ≠ []) ≠ 0
simpa only [digits_of_lt (b + 2) n hn hnb]
case neg
n✝ m b n : ℕ
IH : ∀ (m : ℕ), m < n → ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ List.getLast (digits (b + 2) (n / (b + 2))) ?neg.q✝ ≠ 0

case neg.q
n✝ m b n : ℕ
IH : ∀ (m : ℕ), m < n → ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ digits (b + 2) (n / (b + 2)) ≠ []
case neg
n✝ m b n : ℕ
IH : ∀ (m : ℕ), m < n → ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ List.getLast (digits (succ (succ b)) n) (_ : digits (succ (succ b)) n ≠ []) ≠ 0
rw [digits_getLast n (le_add_left 2 b)]
case neg
n✝ m b n : ℕ
IH : ∀ (m : ℕ), m < n → ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ n / succ (succ b) ≠ 0
case neg
n✝ m b n : ℕ
IH : ∀ (m : ℕ), m < n → ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ List.getLast (digits (b + 2) (n / (b + 2))) ?neg.q✝ ≠ 0

case neg.q
n✝ m b n : ℕ
IH : ∀ (m : ℕ), m < n → ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ digits (b + 2) (n / (b + 2)) ≠ []
refine' IH _ (Nat.div_lt_self hn.bot_lt (one_lt_succ_succ b)) _
case neg
n✝ m b n : ℕ
IH : ∀ (m : ℕ), m < n → ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ 0 < n / succ (succ b)
case neg
n✝ m b n : ℕ
IH : ∀ (m : ℕ), m < n → ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ n / succ (succ b) ≠ 0
rw [← pos_iff_ne_zero]
no goals
case neg
n✝ m b n : ℕ
IH : ∀ (m : ℕ), m < n → ∀ (hm : m ≠ 0), List.getLast (digits (succ (succ b)) m) (_ : digits (succ (succ b)) m ≠ []) ≠ 0
hn : n ≠ 0
hnb : ¬n < b + 2
⊢ 0 < n / succ (succ b)
exact Nat.div_pos (le_of_not_lt hnb) (zero_lt_succ (succ b))