## Stream: new members

### Topic: Proving functions are equal

#### Devon Richards (Jan 13 2021 at 00:36):

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 (Jan 13 2021 at 00:44):

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 (Jan 13 2021 at 00:46):

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

#### Devon Richards (Jan 13 2021 at 00:47):

Thank you, that was exactly what I wanted.

Last updated: May 14 2021 at 12:18 UTC