Find out where sorryAx is coming from?

Stream: lean4

[Malvin Gattinger]

Can I get the information that the sorryAx comes from catchMe in an automated way?

def isNice : Nat → Bool := fun n => decide (n > 5)

@[simp]
theorem catchMe : isNice 23 := sorry

theorem complicated : n = 23 → isNice n := fun hyp => by rw [hyp]; simp

#print axioms complicated
-- 'complicated' depends on axioms: [sorryAx, propext]

[Eric Rodriguez]

I think Mario made such a thing, maybe in lean3

[Riccardo Brasca]

@Floris van Doorn wrote this for Lean3

[Floris van Doorn]

Yes, here: mathlib#16911. Feel free to port/rewrite.