-- Mathlib/Data/Nat/Digits.lean
theorem digits_append_digits {b m n : ℕ} (hb : 0 < b) :
    digits b n ++ digits b m = digits b (n + b ^ (digits b n).length * m)

Proof state:
case neg
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
h_append : b.digits n ++ b.digits m ≠ []
h : ¬b.digits m = []
⊢ (b.digits n ++ b.digits m).getLast h_append ≠ 0

Tactic:
exact (List.getLast_append_of_right_ne_nil _ _ h) ▸
    (getLast_digit_ne_zero _ <| digits_ne_nil_iff_ne_zero.mp h)

Result:
no goals

Proof state:
case inr.refine_1
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
l : ℕ
hl : l ∈ b.digits n ++ b.digits m
⊢ l < b

Tactic:
rcases (List.mem_append.mp hl) with (h | h) <;> exact digits_lt_base hb h

Result:
no goals

Proof state:
case inl
m n : ℕ
hb : 0 < succ 0
⊢ (succ 0).digits n ++ (succ 0).digits m = (succ 0).digits (n + succ 0 ^ ((succ 0).digits n).length * m)

Tactic:
simp

Result:
no goals

Proof state:
case pos
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
h_append : b.digits n ++ b.digits m ≠ []
h : b.digits m = []
⊢ (b.digits n ++ b.digits m).getLast h_append ≠ 0

Tactic:
simp only [h, List.append_nil] at h_append ⊢

Result:
case pos
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
h_append✝ : b.digits n ++ b.digits m ≠ []
h : b.digits m = []
h_append : b.digits n ≠ []
⊢ (b.digits n).getLast ⋯ ≠ 0

Proof state:
case inr.refine_2
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
h_append : b.digits n ++ b.digits m ≠ []
⊢ (b.digits n ++ b.digits m).getLast h_append ≠ 0

Tactic:
by_cases h : digits b m = []

Result:
case pos
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
h_append : b.digits n ++ b.digits m ≠ []
h : b.digits m = []
⊢ (b.digits n ++ b.digits m).getLast h_append ≠ 0

case neg
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
h_append : b.digits n ++ b.digits m ≠ []
h : ¬b.digits m = []
⊢ (b.digits n ++ b.digits m).getLast h_append ≠ 0

Proof state:
case inr
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
⊢ b.digits n ++ b.digits m = b.digits (n + b ^ (b.digits n).length * m)

Tactic:
rw [← ofDigits_digits_append_digits]

Result:
case inr
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
⊢ b.digits n ++ b.digits m = b.digits (ofDigits b (b.digits n ++ b.digits m))

Proof state:
b m n : ℕ
hb : 0 < b
⊢ b.digits n ++ b.digits m = b.digits (n + b ^ (b.digits n).length * m)

Tactic:
rcases eq_or_lt_of_le (Nat.succ_le_of_lt hb) with (rfl | hb)

Result:
case inl
m n : ℕ
hb : 0 < succ 0
⊢ (succ 0).digits n ++ (succ 0).digits m = (succ 0).digits (n + succ 0 ^ ((succ 0).digits n).length * m)

case inr
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
⊢ b.digits n ++ b.digits m = b.digits (n + b ^ (b.digits n).length * m)

Proof state:
case inr
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
⊢ b.digits n ++ b.digits m = b.digits (ofDigits b (b.digits n ++ b.digits m))

Tactic:
refine (digits_ofDigits b hb _ (fun l hl => ?_) (fun h_append => ?_)).symm

Result:
case inr.refine_1
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
l : ℕ
hl : l ∈ b.digits n ++ b.digits m
⊢ l < b

case inr.refine_2
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
h_append : b.digits n ++ b.digits m ≠ []
⊢ (b.digits n ++ b.digits m).getLast h_append ≠ 0

Proof state:
case pos
b m n : ℕ
hb✝ : 0 < b
hb : succ 0 < b
h_append✝ : b.digits n ++ b.digits m ≠ []
h : b.digits m = []
h_append : b.digits n ≠ []
⊢ (b.digits n).getLast ⋯ ≠ 0

Tactic:
exact getLast_digit_ne_zero b <| digits_ne_nil_iff_ne_zero.mp h_append

Result:
no goals