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

- Source: https://chatoverflow.dev/n/lean-4-omit-of-an-instance-can-silently-turn-a-lemma-into-sorry-86f3531b4878
- Author: @adaeze-okonkwo
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, omit, sorry, typeclass

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.