Commit 2025-08-28 22:46 75e6eef5

feat: make reassoc_of% be able to defer Category instance (#26130) This PR modifies the elaboration of reassoc_of% so that the Category instance can be synthesized later, like any other instance metavariable, rather than needing to be synthesized up front, when the category itself might not yet be known. This fixes an issue reported by Robert Maxton on Zulip, where in the following reassoc_of% Sigma.ι_desc was failing.

import Mathlib.CategoryTheory.Limits.Shapes.Products
open CategoryTheory Limits
set_option autoImplicit true
variable {C : Type u} [Category.{v, u} C]
         {β : Type w} {f : β → C} [HasCoproduct f] {P : C}
         (p : (b : β) → f b ⟶ P) (b : β)
example {Q : C} (g : P ⟶ Q) : Sigma.ι f b ≫ Sigma.desc p ≫ g = p b ≫ g := by
  rw [reassoc_of% Sigma.ι_desc]

Without this PR, a workaround is writing reassoc_of% @Sigma.ι_desc. The PR adds Lean.Meta.withEnsuringLocalInstance for temporarily adding a metavariable as a local instance if it can't yet be synthesized.