# Zulip Chat Archive

## Stream: new members

### Topic: prod.map vs limits.prod.map

#### Jack J Garzella (Aug 02 2022 at 18:01):

Hello, I am yet again working on the thing discussed in #maths > Definition of presheaf of modules, and I believe I have reduced (a chunk of) the problem to showing a statement like the following:

MWE Lemma statement

I don't really know how one would go about comparing `prod.map`

and `limits.prod.map`

, does anyone know how to prove such at thing?

#### Jack J Garzella (Aug 02 2022 at 18:07):

Hmm, it seems I could also use advice on how to get code to properly highlight in a spoiler, if anyone knows.

#### Andrew Yang (Aug 02 2022 at 18:07):

I think `ext1`

could help? Or maybe docs#category_theory.limits.prod.hom_ext if `ext`

found the wrong lemma.

#### Andrew Yang (Aug 02 2022 at 18:09):

It should be

Spoiler

You can click the view source on the top right to see how I wrote it.

#### Jack J Garzella (Aug 02 2022 at 19:25):

Ok, I ended up proving the lemma! Thanks!

#### Adam Topaz (Aug 02 2022 at 19:32):

I suspect `by {ext1, simp}`

should close the goal. If not, then there are some simp lemmas missing.

#### Jack J Garzella (Aug 04 2022 at 01:09):

@Adam Topaz turns out, `by {ext1, simp}`

does not close it. I don't quite know how `ext1`

works, but it seems to focus on the first, goal, and since there are two (one for each projection), it doesn't seem to work. There also seem to be some lemmas missing, `simp`

doesn't even close the first goal.

#### Jack J Garzella (Aug 04 2022 at 01:11):

By using the strategy of "write a bunch of have statements that can be cleared by simp, and then use `simp?`

to turn them into things of the form `conv_lhs { simp only [...] }`

, I was able to come up with the following:

```
lemma prod_map_bpo_commutes (A B C D : Type u) (f : A ⟶ C) (g : B ⟶ D) :
as_hom (prod.map f g) ≫
(binary_product_iso C D).inv =
(binary_product_iso A B).inv ≫
limits.prod.map f g :=
begin
apply category_theory.limits.prod.hom_ext,
-- prod.fst, goal 1
apply funext, intros x,
conv_lhs {
simp only [category_theory.types_comp_apply,
category_theory.limits.types.binary_product_iso_inv_comp_fst_apply],
},
conv_rhs {
simp only [category_theory.limits.prod.map_fst,
category_theory.iso.cancel_iso_inv_left,
eq_self_iff_true,
category_theory.category.assoc],
simp only [category_theory.types_comp_apply,
eq_self_iff_true,
category_theory.limits.types.binary_product_iso_inv_comp_fst_apply]
},
refl,
-- prod.snd, goal 2
apply funext, intros x,
conv_lhs {
simp only [category_theory.types_comp_apply,
category_theory.limits.types.binary_product_iso_inv_comp_snd_apply],
},
conv_rhs {
simp only [category_theory.limits.prod.map_snd,
category_theory.iso.cancel_iso_inv_left,
eq_self_iff_true,
category_theory.category.assoc],
simp only [category_theory.types_comp_apply,
eq_self_iff_true,
category_theory.limits.types.binary_product_iso_inv_comp_snd_apply]
},
refl,
end
```

#### Mario Carneiro (Aug 04 2022 at 01:16):

you should use braces to delimit subgoals instead of comments

#### Adam Topaz (Aug 04 2022 at 01:46):

```
import category_theory.closed.cartesian
import category_theory.limits.types
import category_theory.limits.shapes.types
import category_theory.types
noncomputable theory
universes u v
open category_theory
-- open category_theory.limits
open category_theory.limits.types
open category_theory.concrete_category
instance : monoidal_category (Type u) :=
monoidal_of_has_finite_products (Type u)
@[simp, reassoc]
lemma fst_foo (A B : Type u) :
(binary_product_iso A B).inv ≫ limits.prod.fst = prod.fst :=
limits.prod.lift_fst _ _
@[simp, reassoc]
lemma snd_foo (A B : Type u) :
(binary_product_iso A B).inv ≫ limits.prod.snd = prod.snd :=
limits.prod.lift_snd _ _
lemma prod_map_bpo_commutes (A B C D : Type u) (f : A ⟶ C) (g : B ⟶ D) :
as_hom (prod.map f g) ≫
(binary_product_iso C D).inv =
(binary_product_iso A B).inv ≫
limits.prod.map f g :=
by { ext1; simpa }
```

#### Adam Topaz (Aug 04 2022 at 01:46):

not quite `ext1, simp`

, but close ;)

#### Jack J Garzella (Aug 04 2022 at 04:53):

When I change the final semicolon to a comma, Lean complains because there are two goals and only the first one gets solved. Can you explain why simp works when there is a semicolon, but if I change that to a comma it complains?

#### Jireh Loreaux (Aug 04 2022 at 05:03):

A semicolon means: apply the next tactic to *all* the goals. So, in your case, the tactic after the semicolon solves both goals, but when you change it to a comma, that last tactic only acts on the 1st goal (it solves it, but there's still one leftover).

Last updated: Dec 20 2023 at 11:08 UTC