-- Mathlib/Data/List/Induction.lean
theorem bidirectionalRec_cons_append {motive : List α → Sort*}
    (nil : motive []) (singleton : ∀ a : α, motive [a])
    (cons_append : ∀ (a : α) (l : List α) (b : α), motive l → motive (a :: (l ++ [b])))
    (a : α) (l : List α) (b : α) :
    bidirectionalRec nil singleton cons_append (a :: (l ++ [b])) =
      cons_append a l b (bidirectionalRec nil singleton cons_append l)

Proof state:
case cons
α : Type u_1
motive : List α → Sort u_2
nil : motive []
singleton : (a : α) → motive [a]
cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))
a b x : α
xs : List α
⊢ (match a :: (x :: xs ++ [b]) with
    | [] => nil
    | [a] => singleton a
    | a :: b :: l =>
      let l' := (b :: l).dropLast;
      let b' := (b :: l).getLast ⋯;
      cast ⋯ (cons_append a l' b' (bidirectionalRec nil singleton cons_append l'))) =
    cons_append a (x :: xs) b (bidirectionalRec nil singleton cons_append (x :: xs))

Tactic:
simp only [List.cons_append]

Result:
case cons
α : Type u_1
motive : List α → Sort u_2
nil : motive []
singleton : (a : α) → motive [a]
cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))
a b x : α
xs : List α
⊢ cast ⋯
      (cons_append a (x :: (xs ++ [b])).dropLast ((x :: (xs ++ [b])).getLast ⋯)
        (bidirectionalRec nil singleton cons_append (x :: (xs ++ [b])).dropLast)) =
    cons_append a (x :: xs) b (bidirectionalRec nil singleton cons_append (x :: xs))

Proof state:
case nil
α : Type u_1
motive : List α → Sort u_2
nil : motive []
singleton : (a : α) → motive [a]
cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))
a b : α
⊢ (match a :: ([] ++ [b]) with
    | [] => nil
    | [a] => singleton a
    | a :: b :: l =>
      let l' := (b :: l).dropLast;
      let b' := (b :: l).getLast ⋯;
      cast ⋯ (cons_append a l' b' (bidirectionalRec nil singleton cons_append l'))) =
    cons_append a [] b (bidirectionalRec nil singleton cons_append [])

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
motive : List α → Sort u_2
nil : motive []
singleton : (a : α) → motive [a]
cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))
a b x : α
xs ys init : List α
hinit : init = ys
last : α
hlast : last = b
⊢ a :: (ys ++ [b]) = a :: (init ++ [last])

Tactic:
simp [hinit, hlast]

Result:
no goals

Proof state:
α : Type u_1
motive : List α → Sort u_2
nil : motive []
singleton : (a : α) → motive [a]
cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))
a b x : α
xs : List α
this :
  ∀ (ys init : List α) (hinit : init = ys) (last : α) (hlast : last = b),
    cons_append a init last (bidirectionalRec nil singleton cons_append init) =
      cast ⋯ (cons_append a ys b (bidirectionalRec nil singleton cons_append ys))
⊢ cast ⋯
      (cons_append a (x :: xs ++ [b]).dropLast ((x :: xs ++ [b]).getLast ⋯)
        (bidirectionalRec nil singleton cons_append (x :: xs ++ [b]).dropLast)) =
    cons_append a (x :: xs) b (bidirectionalRec nil singleton cons_append (x :: xs))

Tactic:
rw [this (x :: xs) _ (by rw [dropLast_append_cons, dropLast_single, append_nil]) _ (by simp)]

Result:
α : Type u_1
motive : List α → Sort u_2
nil : motive []
singleton : (a : α) → motive [a]
cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))
a b x : α
xs : List α
this :
  ∀ (ys init : List α) (hinit : init = ys) (last : α) (hlast : last = b),
    cons_append a init last (bidirectionalRec nil singleton cons_append init) =
      cast ⋯ (cons_append a ys b (bidirectionalRec nil singleton cons_append ys))
⊢ cast ⋯ (cast ⋯ (cons_append a (x :: xs) b (bidirectionalRec nil singleton cons_append (x :: xs)))) =
    cons_append a (x :: xs) b (bidirectionalRec nil singleton cons_append (x :: xs))