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

Tactic:
simp

Result:
no goals

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 α
⊢ 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:
suffices ∀ (ys init : List α) (hinit : init = ys) (last : α) (hlast : last = b),
    (cons_append a init last
      (bidirectionalRec nil singleton cons_append init)) =
    cast (congr_arg motive <| by simp [hinit, hlast])
      (cons_append a ys b (bidirectionalRec nil singleton cons_append ys)) by
  rw [this (x :: xs) _ (by rw [dropLast_append_cons, dropLast_single, append_nil]) _ (by simp)]
  simp

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 α
⊢ ∀ (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))

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))
⊢ (x :: xs ++ [b]).dropLast = x :: xs

Tactic:
rw [dropLast_append_cons, dropLast_single, append_nil]

Result:
no goals

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 α
⊢ ∀ (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))

Tactic:
rintro ys init rfl last rfl

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 x : α
xs init : List α
last : α
⊢ cons_append a init last (bidirectionalRec nil singleton cons_append init) =
    cast ⋯ (cons_append a init last (bidirectionalRec nil singleton cons_append init))

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 x : α
xs init : List α
last : α
⊢ cons_append a init last (bidirectionalRec nil singleton cons_append init) =
    cast ⋯ (cons_append a init last (bidirectionalRec nil singleton cons_append init))

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 : α
l : List α
b : α
⊢ bidirectionalRec nil singleton cons_append (a :: (l ++ [b])) =
    cons_append a l b (bidirectionalRec nil singleton cons_append l)

Tactic:
conv_lhs => unfold bidirectionalRec

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 : α
l : List α
b : α
⊢ (match a :: (l ++ [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 l b (bidirectionalRec nil singleton cons_append l)

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 : α
l : List α
b : α
⊢ (match a :: (l ++ [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 l b (bidirectionalRec nil singleton cons_append l)

Tactic:
cases l with
| nil => rfl
| cons x xs =>
simp only [List.cons_append]
dsimp only [← List.cons_append]
suffices ∀ (ys init : List α) (hinit : init = ys) (last : α) (hlast : last = b),
    (cons_append a init last
      (bidirectionalRec nil singleton cons_append init)) =
    cast (congr_arg motive <| by simp [hinit, hlast])
      (cons_append a ys b (bidirectionalRec nil singleton cons_append ys)) by
  rw [this (x :: xs) _ (by rw [dropLast_append_cons, dropLast_single, append_nil]) _ (by simp)]
  simp
rintro ys init rfl last rfl
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 : 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))
⊢ (x :: xs ++ [b]).getLast ⋯ = b

Tactic:
simp

Result:
no goals

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 α
⊢ 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:
dsimp 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))