-- Mathlib/Data/Nat/Digits.lean
theorem digits_ofDigits (b : ℕ) (h : 1 < b) (L : List ℕ) (w₁ : ∀ l ∈ L, l < b)
    (w₂ : ∀ h : L ≠ [], L.getLast h ≠ 0) : digits b (ofDigits b L) = L

Proof state:
case cons.w₁
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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

Tactic:
apply w₁

Result:
case cons.w₁.a
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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 ∈ d :: L

Proof state:
b : ℕ
h : 1 < b
L : List ℕ
w₁ : ∀ l ∈ L, l < b
w₂ : ∀ (h : L ≠ []), L.getLast h ≠ 0
⊢ b.digits (ofDigits b L) = L

Tactic:
induction' L with d L ih

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

case cons
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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

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

Tactic:
convert w₂

Result:
no goals

Proof state:
case neg
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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

Tactic:
right

Result:
case neg.h
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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

Proof state:
case cons.hxb
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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

Tactic:
exact w₁ d (List.mem_cons_self _ _)

Result:
no goals

Proof state:
case neg.h
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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
⊢ L.getLast h' ∈ L

Tactic:
exact List.getLast_mem h'

Result:
no goals

Proof state:
case cons
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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

Tactic:
rw [digits_add b h]

Result:
case cons
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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

case cons.hxb
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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

case cons.hxy
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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

Proof state:
case cons.w₁.a
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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 ∈ d :: L

Tactic:
exact List.mem_cons_of_mem _ m

Result:
no goals

Proof state:
case neg.h
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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

Tactic:
refine digits_zero_of_eq_zero h.ne_bot w₂ _ ?_

Result:
case neg.h
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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

Proof state:
case nil
b : ℕ
h : 1 < b
w₁ : ∀ l ∈ [], l < b
w₂ : ∀ (h : [] ≠ []), [].getLast h ≠ 0
⊢ b.digits (ofDigits b []) = []

Tactic:
dsimp [ofDigits]

Result:
case nil
b : ℕ
h : 1 < b
w₁ : ∀ l ∈ [], l < b
w₂ : ∀ (h : [] ≠ []), [].getLast h ≠ 0
⊢ b.digits 0 = []

Proof state:
case cons.w₂
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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 ≠ []), L.getLast h ≠ 0

Tactic:
intro h

Result:
case cons.w₂
b : ℕ
h✝ : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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 ≠ []
⊢ L.getLast h ≠ 0

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

Tactic:
intro l m

Result:
case cons.w₁
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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

Proof state:
case neg.h
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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

Tactic:
contrapose! w₂

Result:
case neg.h
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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

Proof state:
case pos.h
b : ℕ
h : 1 < b
d : ℕ
ih : (∀ l ∈ [], l < b) → (∀ (h : [] ≠ []), [].getLast h ≠ 0) → b.digits (ofDigits b []) = []
w₁ : ∀ l ∈ [d], l < b
w₂ : [d].getLast ⋯ ≠ 0
⊢ d ≠ 0

Tactic:
simpa using w₂

Result:
no goals

Proof state:
case cons.hxy
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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

Tactic:
by_cases h' : L = []

Result:
case pos
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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

case neg
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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

Proof state:
case nil
b : ℕ
h : 1 < b
w₁ : ∀ l ∈ [], l < b
w₂ : ∀ (h : [] ≠ []), [].getLast h ≠ 0
⊢ b.digits 0 = []

Tactic:
simp

Result:
no goals

Proof state:
case cons.w₂
b : ℕ
h✝ : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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 ≠ []
⊢ L.getLast h ≠ 0

Tactic:
rw [List.getLast_cons h] at w₂

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

Proof state:
case neg.h
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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

Tactic:
rw [List.getLast_cons h']

Result:
case neg.h
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (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
⊢ L.getLast h' ∈ L