proving pi >= 0

Stream: new members

[Mii Nguyen]

I'm trying to prove 0 ≤ r^2 * pi. Here is my work

lemma pi_r_sq_pos (r : ℝ) (H: 0 ≤ r): 0 ≤ r^2 * pi :=
have r^2 ≥ 0, from pow_nonneg H 2,
have pi >  0, from pi_pos,
begin
    apply mul_nonneg,
end

I have to prove that pi ≥ 0 instead of pi > 0, but I still stuck in it.
Would someone help me with this? Thank you.

[Patrick Massot]

apply mul_nonneg ; linarith

[Mii Nguyen]

what is the role of linarith in this case? @Patrick Massot

[Patrick Massot]

The role of linarith is to blast away stupid equality and inequality problems

[Patrick Massot]

But you can also be explicit of course:

lemma pi_r_sq_pos (r : ℝ) (H: 0 ≤ r): 0 ≤ r^2 * pi :=
have r^2 ≥ 0, from pow_nonneg H 2,
have pi >  0, from pi_pos,
mul_nonneg ‹r^2 ≥ 0› (le_of_lt ‹0 < pi›)

[Patrick Massot]

But in this case, the mathlib style is to be concise (because the result is trivial and wouldn't be even stated on paper):

lemma pi_r_sq_pos (r : ℝ) (H: 0 ≤ r): 0 ≤ r^2 * pi :=
mul_nonneg (pow_nonneg H 2) (le_of_lt pi_pos)

[Mii Nguyen]

Would you explain the different of ‹ › and ( )? The first is for , say, exact argument and the second is for function? @Patrick Massot

[Mii Nguyen]

I can find the informations of it in which chapter of the book?

[Patrick Massot]

https://leanprover.github.io/logic_and_proof/propositional_logic_in_lean.html#additional-syntax

[Mii Nguyen]

Thank you @Patrick Massot

[Patrick Massot]

or https://leanprover.github.io/theorem_proving_in_lean/quantifiers_and_equality.html#more-on-the-proof-language

[Kevin Buzzard]

le_of_lt is a proof that if a < b then a <= b; this is the answer to your original question, and it's in Patrick's code.

[Kevin Buzzard]

You can guess it because you want to prove _ <= _ which is called le, and it's the conclusion, so le_of, and then you write le_of and hit things like ctrl-space until VS Code tells you the things it knows which have "le_of" in, and then you find it.