# Zulip Chat Archive

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