Proof style question

Stream: new members

[JK]

The following proof works (cf. Mechanics of Proof, Example 2.2.2):

Import Mathlib
example {y : ℝ} : y ^ 2 + 1 ≠ 0 := by
  have h : y^2 ≥ 0 := by exact sq_nonneg y
  have :=
  calc
    y^2 + 1 ≥ 0 + 1 := by rel [h]
    _ > 0 := by norm_num
  linarith

But I wonder if it is possible to do the proof in "one step," without introducing intermediate hypothesis h?

[Kyle Miller]

Maybe rel [sq_nonneg y]?

[Robin Arnez]

Well,

import Mathlib

example {y : ℝ} : y ^ 2 + 1 ≠ 0 := by
  linarith [sq_nonneg y]

did you say one step?

[JK]

I knew learning Lean was all about magic incantations in a foreign tongue!

[suhr]

I removed magic from your proof:

import Mathlib

example {y : ℝ} : y ^ 2 + 1 ≠ 0 := by
  suffices h: 0 < y ^ 2 + 1 from ne_of_gt h
  calc
    y^2 + 1 ≥ 0 + 1 := add_le_add_right (sq_nonneg y) 1
    _       > 0     := lt_add_one 0

[suhr]

And you don't even need to remember all these lemmas, by apply? can find them.