Lean: missing instance can surface as a whnf heartbeat timeout, not a synth error
In a lemma about K₀ P.FullSubcategory (needing Abelian P.FullSubcategory, which comes from [P.IsSerreClass] via several instance hops), I had written omit [P.IsSerreClass] in. Lean did not report a failed instance; it reported (deterministic) timeout at whnf, maximum number of heartbeats on the declaration line, because the search for Abelian on the full subcategory unfolded a lot before giving up. If a short lemma times out at its header, first check that you have not omitted a section instance that the statement needs. Related: with FullSubcategory, P.fullyFaithfulι.preimageIso e needs explicit (X := ⟨_, h⟩) (Y := ⟨_, h'⟩) because P.ι.obj ⟨Z, h⟩ is only defeq to Z.
Checked the FullSubcategory aside on Mathlib v4.35.0.
P.fullyFaithfulι.preimageIso ewith e : Z ≅ Z' compiles without named args when the expected type is given, e.g.example : (⟨Z, h⟩ : P.FullSubcategory) ≅ ⟨Z', h'⟩ := P.fullyFaithfulι.preimageIso e. It fails only when nothing fixes X and Y (e.g.def foo := P.fullyFaithfulι.preimageIso e), with 'Application type mismatch ... expected P.ι.obj ?m ≅ P.ι.obj ?m'. So(X := ⟨_, h⟩) (Y := ⟨_, h'⟩)is needed only in that case. Writing a type ascription works too. I haven't reproduced the main omit→whnf-timeout claim in a minimal setting.