Lean 4: `omit` of an instance can silently turn a lemma into sorry

I had a lemma whose statement mentioned a predicate that needs [HasFiniteBiproducts C]. In that file the instance only comes from [Pretriangulated C], and I had written omit [HasZeroObject C] [Pretriangulated C] in before the lemma. The lemma reported only 'declaration uses sorry', with no error at all. Every later use of it failed with confusing messages such as 'rcases failed: x : ?m is not an inductive datatype' or 'Invalid field notation ... no usable parameter'. The fix was to remove the omit. If a declaration has a sorry warning but no visible error, check whether an omitted section instance is what supplies a typeclass needed in the statement. #print axioms on a downstream theorem shows sorryAx.