# Zulip Chat Archive

## Stream: new members

### Topic: function on product

#### Nicolò Cavalleri (Jun 18 2020 at 12:02):

Is there somewhere in Mathlib where I can find very primitive results on functions such that fxg \comp hxe = (f \comp h) x (g \comp e) where all functions have different domains and codomains exept from the obvious ones which need to be equal to make the equation work? It's not hard to prove it by myself but it would be cool to know if all these results are in Mathlib as I cannot really locate them. (I know the product function is written in Lean with λ abstraction but it was too long to write it with lean notation)

#### Scott Morrison (Jun 18 2020 at 12:08):

Do you know how to use `library_search`

?

#### Scott Morrison (Jun 18 2020 at 12:10):

There are four strategies for finding statements in mathlib:

- learn the #naming scheme
- use
`library_search`

(sometime it helps to write a separate`example`

with the statement you're after) - ask here
- meander around in the source code!

#### Jalex Stark (Jun 18 2020 at 13:32):

I think following those more-or-less in order is good. In particular, by the time, you get to 3, you'll have an `example`

that you can post with your question.

#### Kevin Buzzard (Jun 18 2020 at 13:34):

@Nicolò Cavalleri I would encourage you to formalise your questions (i.e. actually post a piece of working code with a `sorry`

and say "what is this precise function called"). If you do that, you get much more efficient answers, and often, using `library_search`

, you can even find out the answers yourself.

#### Nicolò Cavalleri (Jun 18 2020 at 14:40):

I am looking in Mathlib for lemmas of the kind:

```
lemma comp_of_prod_eq_prod_of_comp {A : Type*} {B : Type*} {C : Type*} {D : Type*} {E : Type*} {F : Type*}
(f : A → B) (g : C → D) (h : B → E) (k : D → F) :
(λ x : B × D, (h x.fst, k x.snd)) ∘ (λ x : A × C, (f x.fst, g x.snd)) = (λ x : A × C, ((h ∘ f) x.fst, (k ∘ g) x.snd)) :=
by refine rfl
```

library_search suggests refine rfl, but that is a tactic and does not point anywhere in mathlib. I am also wondering if there is a convenient notation for product of functions such as `(λ x : A × C, (f x.fst, g x.snd))`

#### Kenny Lau (Jun 18 2020 at 14:42):

`rfl`

means "this is true by definition"

#### Kevin Buzzard (Jun 18 2020 at 14:46):

Not everything which is true by definition has a name in mathlib

#### Kevin Buzzard (Jun 18 2020 at 14:47):

Product function -- good question!

#### Nicolò Cavalleri (Jun 18 2020 at 14:51):

Does also `refine rfl`

mean it is true by definition? The point is that if the goal is the rhs of = in the above lemma, exact lhs seems not to work, even if this is a simplification of my lemma so I am not entirely sure. That is why I needed to write the lemma separately

#### Bryan Gin-ge Chen (Jun 18 2020 at 14:52):

You should be able to replace `by refine rfl`

with just `rfl`

. `refine`

without any underscores just does the same thing as `exact`

.

#### Scott Morrison (Jun 18 2020 at 14:53):

This probably counts as a bug in`library_search`

that it doesn't just print `rfl`

here...

#### Scott Morrison (Jun 18 2020 at 14:54):

I should also have `library_search`

defer the `solve_by_elim`

round until after the "only unfold `reducible`

stuff" round...

#### Bryan Gin-ge Chen (Jun 18 2020 at 14:54):

Sometimes you have to use `change`

to change the goal into something defeq before Lean will accept a proof of that via `exact`

.

#### Johan Commelin (Jun 18 2020 at 14:54):

Scott Morrison said:

This probably counts as a bug in

`library_search`

that it doesn't just print`rfl`

here...

Well... then "Try this" would also have to replace the `by`

...

#### Nicolò Cavalleri (Jun 18 2020 at 17:13):

What if I wanted to define `(λ x : A × C, (f x.fst, g x.snd))`

to be `f.prod g`

? I think I could probably do it but I am a bit lost on what would be the standard way to do it

#### Johan Commelin (Jun 18 2020 at 17:19):

@Nicolò Cavalleri This is "difficult" to achieve, because functions are such a basic notion that there is no good dot notation for them at the moment.

#### Johan Commelin (Jun 18 2020 at 17:19):

You could get `function.prod f g`

though

#### Nicolò Cavalleri (Jun 18 2020 at 17:22):

Johan Commelin said:

You could get

`function.prod f g`

though

Are you suggesting to define `function.prod`

? Or does it exist already? (In case my Lean says it does not exist!)

#### Patrick Massot (Jun 18 2020 at 17:36):

This is `prod.map`

.

#### Johan Commelin (Jun 18 2020 at 17:39):

Aah, I didn't pay attention to the maths...

#### Johan Commelin (Jun 18 2020 at 17:41):

@Nicolò Cavalleri `function.prod`

(following current [informal?] naming conventions) would mean `f : A → B`

, `g : A → C`

, and then `function.prod f g : A → B × C`

, the natural map `\lam x, (f x, g x)`

.

#### Johan Commelin (Jun 18 2020 at 17:41):

I think `prod.map`

, which is what you want, already exists in mathlib.

Last updated: May 09 2021 at 19:11 UTC