!4#3836 CategoryTheory.Sites.CompatiblePlus

Stream: mathlib4

[Moritz Firsching]

In porting !4#3836, in 5 or so of the theorems "no applicable extensionality lemma found" , soext does not work anymore.
I looked in lean3 and figured out that in one of those writing

refine' Multiequalizer.hom_ext ((unop B).index (P ⋙ F)) ((J.diagram P X ⋙ F).map f ≫
          ((isLimitOfPreserves F
          (limit.isLimit ((unop B).index P).multicospan)).conePointUniqueUpToIso
          (limit.isLimit (((unop B).index P).multicospan ⋙ F)) ≪≫
          HasLimit.isoOfNatIso (GrothendieckTopology.Cover.multicospanComp F P (unop B)).symm).hom)
          (((isLimitOfPreserves F
          (limit.isLimit ((unop A).index P).multicospan)).conePointUniqueUpToIso
          (limit.isLimit (((unop A).index P).multicospan ⋙ F)) ≪≫
          HasLimit.isoOfNatIso (
          GrothendieckTopology.Cover.multicospanComp F P (unop A)).symm).hom ≫
          (J.diagram (P ⋙ F) X).map f)  (fun (a : ((unop B).index (P ⋙ F)).L) ↦ _)

fixes the theorem, but this seems awfully long for what has been "ext" before. Do I need to add a suitable extensionality lemma? If yes, which one would that be?

Another issue: plusFunctorWhiskerRightIso only works after setting maxHeartbeats to 400000
Help would be appreciated!

[Ruben Van de Velde]

I believe there's cases where we needed to add more ext lemmas

[Kevin Buzzard]

In the flat functor PR I found an ext failure where the missing lemma looked very pathological. Maybe we're better off writing an ext! tactic which emulates the lean 3 "try all ext lemmas and see which unify" approach?

[Moritz Firsching]

Having ext! sounds good to me.

[Moritz Firsching]

Ruben Van de Velde said:

I believe there's cases where we needed to add more ext lemmas

I don't know how to figure out which ext lemmas are needed here

[Adam Topaz]

Is the issue that a lemma like docs4#CategoryTheory.Limits.IsLimit.hom_ext not firing?

[Adam Topaz]

Well, it’s not firing because it’s not tagged with ext. but I think the lean3 version was… docs#category_theory.limits.is_limit.hom_ext

[Adam Topaz]

Hmm maybe not.

[Kevin Buzzard]

Does apply Multiequalizer.hom_ext work?

[Moritz Firsching]

yes, great, this worked at least for a few of the cases. Now there are two non-working ext left.

docs4#CategoryTheory.Limits.Multiequalizer.hom_ext seems to have the [ext] attribute. What is the reason that ext is not finding it?

[Kevin Buzzard]

Does it syntactically match? Lean 3 ext, if nothing syntactially matched, apparently just tried all ext lemmas to se if anything unified. Lean 4 has dropped this (although there have been suggestions of writing ext! which tries all ext lemmas, although I'm in no position to write this myself).

[Scott Morrison]

The problem wasn't really the exts, but just not following the proof in mathlib3. :-) An erw had mysteriously changed to an ineffective simp only, and there was a mistranslation of colim_map to colim_map (which unfortunately exists!) rather than colimMap.

[Scott Morrison]

@Moritz Firsching, if you want to review my change at https://github.com/leanprover-community/mathlib4/pull/3836/commits/5ae1b6ef51d294ec82b8b39c880e0a336be611f1, I think we can mark this awaiting-review.

[Moritz Firsching]

Done. Great fix!