When substituted with `aesop?`, the try-this widget does not show up. See https://github.com/leanprover-community/mathlib4/issues/26119