Diagnosis: downstream failures from [reducible_proj] Functor.obj in mathlib

Context: after the lean4 fix in leanprover/lean4#13562 routing the [reducible_proj] bump through reduceProj? (so simp, grind canon, cbv, vcgen and unfoldProjInst? all honour the attribute, not just whnfCore's .proj arm), enabling attribute [reducible_proj] Functor.obj in mathlib (commit a8aa749971f on the lean-pr-testing-13562 branch) produces a substantial wave of build failures across Mathlib.CategoryTheory.* and its dependents.

This is a triage / diagnosis writeup. Done in collaboration with Claude Opus 4.7 (1M context) on 2026-05-12.

The underlying mechanism

[reducible_proj] Functor.obj makes Functor.obj <structure-with-unfoldable-body> X reduce one extra step at low transparency. Concretely: when grind canon, simp's whnf, aesop's safe-rule matcher, @[simps]'s elaborator, or simps!'s signature generator processes a goal term containing (F⋙G).obj X or (Functor.id C).obj X or (uncurry.obj x).obj y, the projection now fires.

The reduction is uneven: it fires for the structure-projection head but not for the surrounding context (Functor.map is not [reducible_proj], so (F⋙G).map f stays as-is; Functor.comp F G is not in ctor form unless we unfold, but its .obj projection now does, so types reduce while terms don't). The result is partially-reduced goals whose pattern-matching profile no longer matches what mathlib lemmas, simp sets, and aesop safe rules were tuned for.

Six failure categories

A. naturality aesop default tactic fails

Most common, e.g. Currying.lean:93,141,147; many NatIso.ofComponents callsites.

Example goal after aesop's safe rules:

x.map f ≫ (NatIso.ofComponents (fun _ ↦ Iso.refl ((x.obj Y).obj _)) ⋯).hom =
(NatIso.ofComponents (fun _ ↦ Iso.refl ((x.obj X).obj _)) ⋯).hom ≫
  { obj := fun X ↦ (x.obj X.1).obj X.2, map := … }.curryObj.map f

The structure literal on the RHS is uncurry.obj x exposed by [reducible_proj]. Previously the term was (uncurry ⋙ curry).obj x — opaque, and aesop recognised the naturality square pattern. Now half of it is in literal form, half symbolic; aesop's pattern matcher gives up.

B. simp goal not closed

Examples: Yoneda.lean:775,802,972,….

simp [yonedaEquiv_comp] leaves yonedaEquiv (yonedaEquiv.symm x ≫ f) = (ConcreteCategory.hom (f.app (op X))) x. The simp lemmas were calibrated against unreduced Functor.obj forms; the reduced form's normal form is different, so the closing step never fires.

C. @[simps!]-generated lemmas have kernel type mismatches

Example: Yoneda.lean:1308 for FullyFaithful.homNatIso.

@[simps] runs at elaboration time, capturing the elaborated form of the projection chain. With [reducible_proj], some of those captured types have reduced; when the kernel checks the auto-generated lemma later (without the bump active, or with a different elaboration choice), the signatures don't match.

D. Pattern-not-found rewrites

Examples: Yoneda.lean:987,1114,1218.

rw [...] against the pattern ?m = ?m in a goal where the LHS still has ((uliftYoneda.op ⋙ coyoneda).obj X).map f but the bump has fired in a subterm. The rewrite tactic uses syntactic pattern matching after limited normalisation; the goal post-bump no longer presents the expected pattern.

E. "No goals to be solved" / stuck tactics

Examples: Quotient.lean:272; Yoneda.lean:989,1116,1220.

In Quotient.lean:

dsimp [lift, Functor]
congr  -- "No goals to be solved"

dsimp plus [reducible_proj] now closes the goal that previously needed congr. The fix is mechanical (drop the now-redundant tactic) but the file fails to build until it's removed.

F. Instance synthesis failure

Example: Topology.Category.TopCat.Basic.lean:188.

Instance resolution sees the constructed TopCat term in a partially-reduced form that doesn't match the expected class-head shape. Probably narrowable to "some implicit arg got reduced via [reducible_proj] and now instance resolution can't unify".

Where the id_obj case sits in this taxonomy

The error I patched in commit 6f96b69e21f on lean-pr-testing-13562,

Mathlib/CategoryTheory/Functor/Basic.lean:94:8: invalid pattern, (non-forbidden) application expected
  #0

is special among the failures — it's the only one where grind's pattern generator itself rejects the lemma. All other failures are proofs / tactics that used to succeed but no longer do because the goal shape changed. id_obj is genuinely now redundant (the LHS reduces definitionally to the RHS, so the lemma is trivially True modulo [reducible_proj]), so dropping @[grind =] is the right fix.

Reproduction notes

• Toolchain: leanprover/lean4-pr-releases:pr-release-13562-b5854c5 (the rebased PR head).
• Mathlib branch: lean-pr-testing-13562 at commit 6f96b69e21f (which has the toolchain pin and the two narrow fixes for id_obj and hcomp._proof_3).
• Reproduce: lake build Mathlib.CategoryTheory.Functor.Currying or lake build Mathlib.CategoryTheory.Yoneda from a checkout pinned to that commit.
• Files known to currently fail at the top level of Mathlib/CategoryTheory/: Functor.Currying, Yoneda, Quotient, and dependents thereof. Topology.Category.TopCat.Basic is the nearest non-CategoryTheory failure.