-- 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:
α : 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 α
h : xs.reverse.reverse = ys
⊢ motive (ys ++ [x]) = motive (xs ++ [x])

Tactic:
simp [(reverse_reverse _).symm.trans h]

Result:
no goals

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
head✝ : α
tail✝ : List α
⊢ ∀ (heq : x = head✝ ∧ xs.reverse = tail✝),
    cast ⋯ (append_singleton tail✝.reverse head✝ (reverseRecOn tail✝.reverse nil append_singleton)) =
      cast ⋯ (append_singleton ys x (reverseRecOn ys nil append_singleton))

Tactic:
rintro ⟨rfl, rfl⟩

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])
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))

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])
⊢ 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))

Tactic:
rfl

Result:
no goals

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
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:
simp only [reverse_append, reverse_cons, reverse_nil, nil_append, singleton_append, cons.injEq]

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
head✝ : α
tail✝ : List α
⊢ ∀ (heq : x = head✝ ∧ xs.reverse = 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
⊢ (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))

Tactic:
split

Result:
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))

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
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:
revert heq

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
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])
⊢ reverseRecOn (xs ++ [x]) nil append_singleton = append_singleton xs x (reverseRecOn xs nil append_singleton)

Tactic:
suffices ∀ ys (h : reverse (reverse xs) = ys),
    reverseRecOn (motive := motive) (xs ++ [x]) nil append_singleton =
      cast (by simp [(reverse_reverse _).symm.trans h])
        (append_singleton _ x (reverseRecOn (motive := motive) ys nil append_singleton)) by
  exact this _ (reverse_reverse xs)

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 α) (h : xs.reverse.reverse = ys),
    reverseRecOn (xs ++ [x]) nil append_singleton =
      cast ⋯ (append_singleton ys x (reverseRecOn ys nil append_singleton))

Proof state:
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 heq =>
  revert heq
  simp only [reverse_append, reverse_cons, reverse_nil, nil_append, singleton_append, cons.injEq]
  rintro ⟨rfl, rfl⟩
  subst ys
  rfl

Result:
no goals

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 α) (h : xs.reverse.reverse = ys),
    reverseRecOn (xs ++ [x]) nil append_singleton =
      cast ⋯ (append_singleton ys x (reverseRecOn ys nil append_singleton))

Tactic:
intros ys hy

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
⊢ reverseRecOn (xs ++ [x]) 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
h : (xs ++ [x]).reverse = []
⊢ cast ⋯ nil = cast ⋯ (append_singleton ys x (reverseRecOn ys nil append_singleton))

Tactic:
simp at h

Result:
no goals