case nil
n b : ℕ
h : 1 < b
L : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L → l < b
w₂✝ : ∀ (h : L ≠ []), List.getLast L h ≠ 0
w₁ : ∀ (l : ℕ), l ∈ [] → l < b
w₂ : ∀ (h : [] ≠ []), List.getLast [] h ≠ 0
⊢ digits b (ofDigits b []) = []

case cons
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : ∀ (h : d :: L ≠ []), List.getLast (d :: L) h ≠ 0
⊢ digits b (ofDigits b (d :: L)) = d :: L
n b : ℕ
h : 1 < b
L : List ℕ
w₁ : ∀ (l : ℕ), l ∈ L → l < b
w₂ : ∀ (h : L ≠ []), List.getLast L h ≠ 0
⊢ digits b (ofDigits b L) = L
induction' L with d L ih
case nil
n b : ℕ
h : 1 < b
L : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L → l < b
w₂✝ : ∀ (h : L ≠ []), List.getLast L h ≠ 0
w₁ : ∀ (l : ℕ), l ∈ [] → l < b
w₂ : ∀ (h : [] ≠ []), List.getLast [] h ≠ 0
⊢ digits b 0 = []
case nil
n b : ℕ
h : 1 < b
L : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L → l < b
w₂✝ : ∀ (h : L ≠ []), List.getLast L h ≠ 0
w₁ : ∀ (l : ℕ), l ∈ [] → l < b
w₂ : ∀ (h : [] ≠ []), List.getLast [] h ≠ 0
⊢ digits b (ofDigits b []) = []
dsimp [ofDigits]
no goals
case nil
n b : ℕ
h : 1 < b
L : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L → l < b
w₂✝ : ∀ (h : L ≠ []), List.getLast L h ≠ 0
w₁ : ∀ (l : ℕ), l ∈ [] → l < b
w₂ : ∀ (h : [] ≠ []), List.getLast [] h ≠ 0
⊢ digits b 0 = []
simp
case cons
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : ∀ (h : d :: L ≠ []), List.getLast (d :: L) h ≠ 0
⊢ digits b (d + b * ofDigits b L) = d :: L
case cons
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : ∀ (h : d :: L ≠ []), List.getLast (d :: L) h ≠ 0
⊢ digits b (ofDigits b (d :: L)) = d :: L
dsimp [ofDigits]
case cons
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
⊢ digits b (d + b * ofDigits b L) = d :: L
case cons
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : ∀ (h : d :: L ≠ []), List.getLast (d :: L) h ≠ 0
⊢ digits b (d + b * ofDigits b L) = d :: L
replace w₂ := w₂ (by simp)
case cons
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
⊢ d :: digits b (ofDigits b L) = d :: L

case cons.hxb
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
⊢ d < b

case cons.hxy
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0
case cons
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
⊢ digits b (d + b * ofDigits b L) = d :: L
rw [digits_add b h]
no goals
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : ∀ (h : d :: L ≠ []), List.getLast (d :: L) h ≠ 0
⊢ d :: L ≠ []
simp
case cons.w₁
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
⊢ ∀ (l : ℕ), l ∈ L → l < b

case cons.w₂
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
⊢ ∀ (h : L ≠ []), List.getLast L h ≠ 0
case cons
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
⊢ d :: digits b (ofDigits b L) = d :: L
rw [ih]
case cons.w₁
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
l : ℕ
m : l ∈ L
⊢ l < b
case cons.w₁
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
⊢ ∀ (l : ℕ), l ∈ L → l < b
intro l m
case cons.w₁.a
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
l : ℕ
m : l ∈ L
⊢ l ∈ d :: L
case cons.w₁
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
l : ℕ
m : l ∈ L
⊢ l < b
apply w₁
no goals
case cons.w₁.a
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
l : ℕ
m : l ∈ L
⊢ l ∈ d :: L
exact List.mem_cons_of_mem _ m
case cons.w₂
n b : ℕ
h✝ : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
h : L ≠ []
⊢ List.getLast L h ≠ 0
case cons.w₂
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
⊢ ∀ (h : L ≠ []), List.getLast L h ≠ 0
intro h
case cons.w₂
n b : ℕ
h✝ : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
h : L ≠ []
w₂ : List.getLast L h ≠ 0
⊢ List.getLast L h ≠ 0
case cons.w₂
n b : ℕ
h✝ : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
h : L ≠ []
⊢ List.getLast L h ≠ 0
rw [List.getLast_cons h] at w₂
no goals
case cons.w₂
n b : ℕ
h✝ : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
h : L ≠ []
w₂ : List.getLast L h ≠ 0
⊢ List.getLast L h ≠ 0
convert w₂
no goals
case cons.hxb
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
⊢ d < b
exact w₁ d (List.mem_cons_self _ _)
case pos
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
h' : L = []
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0

case neg
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
h' : ¬L = []
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0
case cons.hxy
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0
by_cases h' : L = []
case pos
n b : ℕ
h : 1 < b
L : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L → l < b
w₂✝ : ∀ (h : L ≠ []), List.getLast L h ≠ 0
d : ℕ
ih : (∀ (l : ℕ), l ∈ [] → l < b) → (∀ (h : [] ≠ []), List.getLast [] h ≠ 0) → digits b (ofDigits b []) = []
w₁ : ∀ (l : ℕ), l ∈ [d] → l < b
w₂ : List.getLast [d] (_ : ¬[d] = []) ≠ 0
⊢ d ≠ 0 ∨ ofDigits b [] ≠ 0
case pos
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
h' : L = []
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0
rcases h' with rfl
case pos.h
n b : ℕ
h : 1 < b
L : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L → l < b
w₂✝ : ∀ (h : L ≠ []), List.getLast L h ≠ 0
d : ℕ
ih : (∀ (l : ℕ), l ∈ [] → l < b) → (∀ (h : [] ≠ []), List.getLast [] h ≠ 0) → digits b (ofDigits b []) = []
w₁ : ∀ (l : ℕ), l ∈ [d] → l < b
w₂ : List.getLast [d] (_ : ¬[d] = []) ≠ 0
⊢ d ≠ 0
case pos
n b : ℕ
h : 1 < b
L : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L → l < b
w₂✝ : ∀ (h : L ≠ []), List.getLast L h ≠ 0
d : ℕ
ih : (∀ (l : ℕ), l ∈ [] → l < b) → (∀ (h : [] ≠ []), List.getLast [] h ≠ 0) → digits b (ofDigits b []) = []
w₁ : ∀ (l : ℕ), l ∈ [d] → l < b
w₂ : List.getLast [d] (_ : ¬[d] = []) ≠ 0
⊢ d ≠ 0 ∨ ofDigits b [] ≠ 0
left
no goals
case pos.h
n b : ℕ
h : 1 < b
L : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L → l < b
w₂✝ : ∀ (h : L ≠ []), List.getLast L h ≠ 0
d : ℕ
ih : (∀ (l : ℕ), l ∈ [] → l < b) → (∀ (h : [] ≠ []), List.getLast [] h ≠ 0) → digits b (ofDigits b []) = []
w₁ : ∀ (l : ℕ), l ∈ [d] → l < b
w₂ : List.getLast [d] (_ : ¬[d] = []) ≠ 0
⊢ d ≠ 0
simpa using w₂
case neg.h
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
h' : ¬L = []
⊢ ofDigits b L ≠ 0
case neg
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
h' : ¬L = []
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0
right
case neg.h
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
h' : ¬L = []
w₂ : ofDigits b L = 0
⊢ List.getLast (d :: L) (_ : ¬d :: L = []) = 0
case neg.h
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
w₂ : List.getLast (d :: L) (_ : ¬d :: L = []) ≠ 0
h' : ¬L = []
⊢ ofDigits b L ≠ 0
contrapose! w₂
case neg.h
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
h' : ¬L = []
w₂ : ofDigits b L = 0
⊢ List.getLast (d :: L) (_ : ¬d :: L = []) ∈ L
case neg.h
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
h' : ¬L = []
w₂ : ofDigits b L = 0
⊢ List.getLast (d :: L) (_ : ¬d :: L = []) = 0
refine' digits_zero_of_eq_zero h.ne_bot w₂ _ _
case neg.h
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
h' : ¬L = []
w₂ : ofDigits b L = 0
⊢ List.getLast L h' ∈ L
case neg.h
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
h' : ¬L = []
w₂ : ofDigits b L = 0
⊢ List.getLast (d :: L) (_ : ¬d :: L = []) ∈ L
rw [List.getLast_cons h']
no goals
case neg.h
n b : ℕ
h : 1 < b
L✝ : List ℕ
w₁✝ : ∀ (l : ℕ), l ∈ L✝ → l < b
w₂✝ : ∀ (h : L✝ ≠ []), List.getLast L✝ h ≠ 0
d : ℕ
L : List ℕ
ih : (∀ (l : ℕ), l ∈ L → l < b) → (∀ (h : L ≠ []), List.getLast L h ≠ 0) → digits b (ofDigits b L) = L
w₁ : ∀ (l : ℕ), l ∈ d :: L → l < b
h' : ¬L = []
w₂ : ofDigits b L = 0
⊢ List.getLast L h' ∈ L
exact List.getLast_mem h'