function on product

Stream: new members

[Nicolò Cavalleri]

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]

Do you know how to use library_search?

[Scott Morrison]

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)
3. ask here
4. meander around in the source code!

[Jalex Stark]

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]

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

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]

rfl means "this is true by definition"

[Kevin Buzzard]

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

[Kevin Buzzard]

Product function -- good question!

[Nicolò Cavalleri]

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]

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]

This probably counts as a bug inlibrary_search that it doesn't just print rfl here...

[Scott Morrison]

I should also have library_search defer the solve_by_elim round until after the "only unfold reducible stuff" round...

[Bryan Gin-ge Chen]

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]

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]

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]

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

You could get function.prod f g though

[Nicolò Cavalleri]

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]

This is prod.map.

[Johan Commelin]

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

[Johan Commelin]

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

I think prod.map, which is what you want, already exists in mathlib.