Proving functions are equal

Stream: new members

[Devon Richards]

I was playing around with lean trying to familiarize myself with it so I decided to try and define finite sequences and some operations on them. I defined finite_sequence (n : nat) (\alpha : Type u) as fin n \to \alpha. Then I defined initial_segment s m which is the sequence of the first m elements of s, and concat s t which is the sequence made by the elements of s followed by the elements of t.
Now I'm trying to prove that \forall (s t : finite_sequence n \alpha), s = initial_segment (concat s t) and I'm having trouble figuring out how to prove it in Lean. The outline of the proof in my head is to show that \forall i, s i = (initial_segment (concat s t)) i. Do I need to restate the theorem in that form or is there some good way to prove them equal otherwise without needing to simplify the definitions till they're definitionaly equal? I was wanting to treat the sequences as concrete objects not functions so the equality without the explicit parameter seemed much more aesthetically appealing.

[Hanting Zhang]

To "prove things are equal by proving their parts are equal," i.e. extensionality, you use the ext tactic (tactic#ext). Although this is general advice and I'm not completely sure it will work for your case.

[Chris Hughes]

funext is the theorem you need. The ext tactic is one way of automatically applying funext

[Devon Richards]

Thank you, that was exactly what I wanted.