## Stream: new members

### Topic: Simplify function composition

#### Valentin Vinoles (Nov 25 2023 at 18:18):

Hi

I am trying to prove that id ∘ f = f using tactic mode and mimicking the pen and paper mathematical proof. And I do not understand why the following does not work :

variable {α β : Type}

example (f : α → β) : id ∘ f = f := by
apply funext    -- ⊢ ∀ (x : α), (id ∘ f) x = f x
intro x         -- x : α
rw [id]


I would have expected that the goal should be at this point ⊢ f x = f x but instead Lean tells me "failed to rewrite using equation theorems for 'id'" and I do not understand why.

Can you please explain to me what is going on and how to fix it ?

PS: I am aware that we can do much shorter like example (f : α → β) : id ∘ f = f := by rfl.

#### Ruben Van de Velde (Nov 25 2023 at 18:21):

That only works if you have an applied id xrather than just id

#### Ruben Van de Velde (Nov 25 2023 at 18:22):

You can rw [Function.comp] first

#### Valentin Vinoles (Nov 25 2023 at 18:23):

@Ruben Van de Velde
Thanks, it works perfectly !

#### Notification Bot (Nov 25 2023 at 18:23):

Valentin Vinoles has marked this topic as resolved.

#### Pedro Sánchez Terraf (Nov 25 2023 at 18:24):

Hi, @Valentin Vinoles! by the way, please don't forget to include your imports, in order to have a #mwe. Also, it is better not to close topics because that changes the topic name (!)

Edit I just noticed it works as provided, but some useful tactics (like simp?, which I used to figure out another way) are not available in Core.

#### Notification Bot (Nov 25 2023 at 18:31):

Valentin Vinoles has marked this topic as unresolved.

#### Valentin Vinoles (Nov 25 2023 at 18:31):

@Pedro Sánchez Terraf
Hi, sorry I was not aware that we should not close topics. In this case, yes I do not have any import because it is just very basic stuff.

#### Pedro Sánchez Terraf (Nov 25 2023 at 18:37):

Yeah afaik there is no policy as in "do not close topics", but it seems inconvenient since closing changes the URL.

By using simp? I came up with this alternate route:

Another set of rewrites

#### Kyle Miller (Nov 25 2023 at 18:41):

Ruben Van de Velde said:

That only works if you have an applied id xrather than just id

unfold id works here

Last updated: Dec 20 2023 at 11:08 UTC