Simplify function composition

Stream: new members

[Valentin Vinoles]

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]

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

[Ruben Van de Velde]

You can rw [Function.comp] first

[Valentin Vinoles]

@Ruben Van de Velde
Thanks, it works perfectly !

[Notification Bot]

Valentin Vinoles has marked this topic as resolved.

[Pedro Sánchez Terraf]

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]

Valentin Vinoles has marked this topic as unresolved.

[Valentin Vinoles]

@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]

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

variable {α β : Type}

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

[Kyle Miller]

Ruben Van de Velde said:

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

unfold id works here