## Stream: new members

### Topic: homs vs. functions

#### Joachim Breitner (Jan 12 2022 at 21:55):

More beginner questions, hope that’s ok. My goal is

⇑h2 ∘ ⇑h1 = id


but what I really want (to apply suitable lemmas) is what I can’t express better than

monoid_hom.comp h2 h1 = monoid_hom.id G


How do I go about this? Is there a way to apply this lemma (is_free_group.hom_ext) to the above goal and have lean somehow figure out that both sides are indeed homs?

#### Yakov Pechersky (Jan 12 2022 at 22:03):

mathlib has the style tendency to not use pointfree (comp) lemmas, but use fully applied lemmas. so often such goals are solved by using an extensionality lemma (or tactic) first

#### Yakov Pechersky (Jan 12 2022 at 22:04):

So in this case, you might have a proof of that lemma, let's say named H, and use congr_fun H _

#### Yakov Pechersky (Jan 12 2022 at 22:05):

A #mwe always helps to give concrete examples

#### Anne Baanen (Jan 12 2022 at 22:09):

I hope we already have docs#monoid_hom.coe_comp and docs#monoid_hom.coe_id (EDIT: no coe_id unfortunately), then you could do it as follows:

#### Anne Baanen (Jan 12 2022 at 22:13):

import algebra.group.hom

variables {M N : Type*} [monoid M] [monoid N]

@[simp] lemma monoid_hom.coe_id : ((monoid_hom.id M) : M → M) = id := rfl

example (h1 : M →* N) (h2 : N →* M) (h : monoid_hom.comp h2 h1 = monoid_hom.id M) :
(h2 ∘ h1 : M → M) = id :=
by rw [← monoid_hom.coe_comp, ← monoid_hom.coe_id, h]


#### Anne Baanen (Jan 12 2022 at 22:17):

Now in fact coe_comp and coe_id are true by definition, so you can actually cheat a bit and say:

example (h1 : M →* N) (h2 : N →* M) (h : monoid_hom.comp h2 h1 = monoid_hom.id M) :
(h2 ∘ h1 : M → M) = id :=
congr_arg (coe_fn : (M →* M) → (M → M)) h


where coe_fn is the name of the double uparrow ⇑ implicitly converting a hom to a function.

#### Joachim Breitner (Jan 12 2022 at 22:22):

That proof term works, thanks. At least the sorry is gone, and maybe I’ll learn how to do it more pretty later :)

Last updated: Dec 20 2023 at 11:08 UTC