Help with proof about lists

Stream: lean4

[Jesse Slater]

I am having a lot of trouble proving this:

example (xs : List α) (i : Nat) (leq : i ≤ xs.length):
  (xs.take i) ++ (xs.reverse.take (xs.length - i)).reverse = xs := by
    sorry

I have tried induction on both i and xs, but I have never been able to prove
List.reverse (List.take (List.length xs) (List.reverse xs)) = xs
How should I proceed?

[Trebor Huang]

If you have proved that reverse is an involution, then taking reverse on both sides you only need to prove take xs.length xs.reverse = xs.reverse

[Trebor Huang]

Then with take xs.length xs = xs and xs.reverse.length = xs.length you should be able to conclude the proof

[Jesse Slater]

I have tried that approach, but I have not been able to make the proof come together. I am very new at this, so I am probably making some simple error in approach, but I did not make that work.

[Wojciech Nawrocki]

Hi @Jesse Slater , here is one way you could do it:

theorem List.take_length (l : List α) : l.take l.length = l := by
  induction l with
  | nil => rfl
  | cons x xs ih =>
    simp [take, length, ih]

theorem reverse_lemma (l : List α) : (l.reverse.take l.length).reverse = l := by
  conv => rhs; rw [← List.reverse_reverse l]
  apply congrArg
  rw [← List.length_reverse l]
  apply List.take_length