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

1. learn the #naming scheme
2. use library_search (sometime it helps to write a separate example with the statement you're after)
4. 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 inlibrary_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 inlibrary_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