Beginner question about a simple proof

Stream: new members

[Marc Lelarge]

Hi,
is there a simple explanation why the following proof seems to work, i.e. Tactic state: No goals (with an error message: unknown identifier 'foo'):

import Mathlib

theorem easy (x : ℝ) (hx: x>0) : (x ^ 2 + 1) / x ≥ 2 := by
  apply (foo (by positivity))

Thanks!

[Filippo A. E. Nuccio]

When there is an error message (like the one concerning the non-existing foo) the other messages (like No goals) are unreliable. But this is a VSCode/Infoview thing, not any suggestion that you've actually proven the result. You can try by replacing the proof with an arbitrary nonsensical sequence of characters:

import Mathlib

theorem easy (x : ℝ) (hx: x>0) : (x ^ 2 + 1) / x ≥ 2 := by
  apply cdos

[Marc Lelarge]

Thanks a lot @Filippo A. E. Nuccio