-- Mathlib/Data/List/Induction.lean
theorem reverseRecOn_concat {motive : List α → Sort*} (x : α) (xs : List α) (nil : motive [])
    (append_singleton : ∀ (l : List α) (a : α), motive l → motive (l ++ [a])) :
    reverseRecOn (motive := motive) (xs ++ [x]) nil append_singleton =
      append_singleton _ _ (reverseRecOn (motive := motive) xs nil append_singleton)

Proof state:
case intro
α : Type u_1
motive : List α → Sort u_2
x : α
xs : List α
nil : motive []
append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])
ys : List α
hy : xs.reverse.reverse = ys
⊢ cast ⋯ (append_singleton xs.reverse.reverse x (reverseRecOn xs.reverse.reverse nil append_singleton)) =
    cast ⋯ (append_singleton ys x (reverseRecOn ys nil append_singleton))

Tactic:
subst ys

Result:
case intro
α : Type u_1
motive : List α → Sort u_2
x : α
xs : List α
nil : motive []
append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])
⊢ cast ⋯ (append_singleton xs.reverse.reverse x (reverseRecOn xs.reverse.reverse nil append_singleton)) =
    cast ⋯ (append_singleton xs.reverse.reverse x (reverseRecOn xs.reverse.reverse nil append_singleton))

Proof state:
α : Type u_1
motive : List α → Sort u_2
x : α
xs : List α
nil : motive []
append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])
this :
  ∀ (ys : List α) (h : xs.reverse.reverse = ys),
    reverseRecOn (xs ++ [x]) nil append_singleton =
      cast ⋯ (append_singleton ys x (reverseRecOn ys nil append_singleton))
⊢ reverseRecOn (xs ++ [x]) nil append_singleton = append_singleton xs x (reverseRecOn xs nil append_singleton)

Tactic:
exact this _ (reverse_reverse xs)

Result:
no goals

Proof state:
case h_1
α : Type u_1
motive : List α → Sort u_2
x : α
xs : List α
nil : motive []
append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])
ys : List α
hy : xs.reverse.reverse = ys
heq✝ : (xs ++ [x]).reverse = []
⊢ cast ⋯ nil = cast ⋯ (append_singleton ys x (reverseRecOn ys nil append_singleton))

case h_2
α : Type u_1
motive : List α → Sort u_2
x : α
xs : List α
nil : motive []
append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])
ys : List α
hy : xs.reverse.reverse = ys
head✝ : α
tail✝ : List α
heq✝ : (xs ++ [x]).reverse = head✝ :: tail✝
⊢ cast ⋯ (append_singleton tail✝.reverse head✝ (reverseRecOn tail✝.reverse nil append_singleton)) =
    cast ⋯ (append_singleton ys x (reverseRecOn ys nil append_singleton))

Tactic:
next h => simp at h

Result:
case h_2
α : Type u_1
motive : List α → Sort u_2
x : α
xs : List α
nil : motive []
append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])
ys : List α
hy : xs.reverse.reverse = ys
head✝ : α
tail✝ : List α
heq✝ : (xs ++ [x]).reverse = head✝ :: tail✝
⊢ cast ⋯ (append_singleton tail✝.reverse head✝ (reverseRecOn tail✝.reverse nil append_singleton)) =
    cast ⋯ (append_singleton ys x (reverseRecOn ys nil append_singleton))

Proof state:
α : Type u_1
motive : List α → Sort u_2
x : α
xs : List α
nil : motive []
append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])
ys : List α
hy : xs.reverse.reverse = ys
⊢ reverseRecOn (xs ++ [x]) nil append_singleton = cast ⋯ (append_singleton ys x (reverseRecOn ys nil append_singleton))

Tactic:
conv_lhs => unfold reverseRecOn

Result:
α : Type u_1
motive : List α → Sort u_2
x : α
xs : List α
nil : motive []
append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])
ys : List α
hy : xs.reverse.reverse = ys
⊢ (match h : (xs ++ [x]).reverse with
    | [] => cast ⋯ nil
    | head :: tail => cast ⋯ (append_singleton tail.reverse head (reverseRecOn tail.reverse nil append_singleton))) =
    cast ⋯ (append_singleton ys x (reverseRecOn ys nil append_singleton))