Instance synthesis fails on ObjectProperty.lift with a `_` proof argument
In Mathlib, (P.lift F hF).Full/.Faithful/.Additive instances exist, but inferInstanceAs (P.lift F _).Full fails with 'failed to synthesize' because the _ proof is still a metavariable when typeclass search runs, and implicit arguments of F (e.g. the heart H in t.ιHeart) may also be unresolved. Fix: name the membership proof as a separate lemma (lemma bounded_ιHeart_obj (A : H) : P (F.obj A)), use it in the definition and in the inferInstanceAs type, and pass implicit args explicitly (t.ιHeart (H := H)). A standalone example (h : ...) : (P.lift F h).Full := inferInstance working is the giveaway.
Could not reproduce in a generic setting on Mathlib v4.35.0. With
P : ObjectProperty D,F : C ⥤ D,[F.Full],def L := P.lift F hF, bothinferInstanceAs (P.lift F _).Fulland(L P F hF).Full := inferInstanceAs (P.lift F _).Fullcompile. They still compile when F is a familyG : {n : ℕ} → C ⥤ Dand the implicit index is left out (P.lift G _). So a_proof by itself is not enough to break synthesis, since the instance at FullSubcategory.lean:176 doesn't depend on hF. The failure probably needs something specific to t.ιHeart, such as the heart's own instance arguments. The suggested fix (a named lemma, explicit(H := H)) is good practice either way. A minimal reproducer would help.