issue with a lemma involving `unitNatIso`

Stream: new members

[Rida Hamadani]

The following lemma is giving me trouble in a bigger proof:

import Mathlib

open CategoryTheory MonoidalCategory MonoidalClosed SimplicialCategory

namespace SSet

noncomputable instance : MonoidalClosed SSet where
  closed A := {
    rightAdj := (sHomFunctor _).obj ⟨A⟩
    adj := FunctorToTypes.adj _
  }

noncomputable instance : Closed (𝟙_ SSet) := closed (𝟙_ SSet)

lemma curry_snd_unitNatIso_inv_app (X Y : SSet) (f : X ⟶ Y) :
    curry (CartesianMonoidalCategory.snd (𝟙_ SSet) X ≫ f) ≫ unitNatIso.inv.app Y = f := by
  sorry

end SSet

What is puzzling is how when we replace the second instance with:

instance : Closed (𝟙_ SSet) := unitClosed

then rfl closes the goal, however, in the project I'm working in (infinity-cosmos), the first instance is the one the lemma takes automatically, and rfl doesn't do anything anymore.

How can I solve this issue?

[Joël Riou]

I cannot answer specifically, but I have shown certain similar compatibilities. Usually, I would try various "tricks":

• pre/post-compose with the inverse of an isomorphism (here, I may try postcomposing with unitNatIso.hom.app Y);
• use (un)curry_injective and the various naturality lemmas;
• (un)apply a bijection like ((ihom X).obj Y) _⦋0⦌ ≃ (X ⟶ Y) (see https://github.com/joelriou/topcat-model-category/blob/master/TopCatModelCategory/SSet/Monoidal.lean#L169 which may depend on an out of date mathlib, before the chosen finite products refactor)
• try rfl at any stage.

If all of this fail, I would try to see if there are missing equational lemmas (e.g. for unitNatIso?).

[Rida Hamadani]

Thanks, post-composing fixed the issue! Here is the proof:

lemma curry_snd_unitNatIso_inv_app {X Y : SSet.{u}} (f : X ⟶ Y) :
    curry (CartesianMonoidalCategory.snd (𝟙_ SSet) X ≫ f) ≫ unitNatIso.inv.app Y = f := by
  rw [← Iso.app_inv, Iso.comp_inv_eq, Iso.app_hom, unitNatIso]
  simp only [Functor.id_obj, conjugateIsoEquiv_apply_hom, conjugateEquiv_apply_app,
    curriedTensor_obj_obj, ihom.ihom_adjunction_unit, leftUnitorNatIso_hom_app,
    ihom.coev_naturality_assoc, id_whiskerLeft, Functor.map_comp, Category.assoc,
    Iso.map_inv_hom_id_assoc]
  rfl

[Rida Hamadani]

But I'm curious about why the difference in instances would cause such an issue, I'd appreciate any insight into that as well.

[Joël Riou]

It is likely that at least one of the lemmas in the simp list is not a rfl equality. Syntactically, it seems that the statement curry_snd_unitNatIso_inv_app may hold in more general cartesian closed monoidal categories, in which case it is very unlikely we could prove it by rfl. That the chosen product and the internal hom in the category of functor to types have nice formulas makes it so that some proofs can be done by rfl (but we can consider we are lucky when this happens).