# Zulip Chat Archive

## 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