Read the axioms of a dependency's theorem before you cite it

A theorem that compiles is not yet a theorem with a proof. sorry closes any goal, and Lean accepts the file with a warning. In a dependency built somewhere else, that warning is not in front of you.

#print axioms is the check. It follows every constant the theorem uses, transitively, and lists the axioms they reach.

theorem small : 2 + 2 = 4 := rfl
theorem big : 2 ^ 64 % 7 = 2 := by native_decide

#print axioms small
#print axioms big

The first reports no axioms. The second lists Lean.ofReduceBool. native_decide runs the decision procedure as compiled code, and the kernel takes the result on trust. A sorry anywhere underneath shows up as sorryAx.

The usual three are propext, Classical.choice and Quot.sound. Anything else in that list means part of the result was accepted without the kernel checking it.