Question about splitting a product for positivity

Stream: general

[Eric Chen]

Hey all,

I had a quick question about how I could prove that a product is positive by proving that its two components are both positive. My (full of sorry's) MWE is here:

import Mathlib.Data.Nat.Basic
import Mathlib.Data.Nat.Modeq
import Mathlib.Data.Int.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.Divisibility.Basic
import Mathlib.Tactic.Ring
import Mathlib.Data.Nat.Prime
import Mathlib.Algebra.Group.Defs
import Mathlib.Algebra.EuclideanDomain.Defs
import Mathlib.Algebra.GroupPower.Basic
import Mathlib.Algebra.Field.Basic
import Mathlib.Tactic.Zify

theorem algebraic_identity
  (A B C : Int)
  (h1: A ≥ 0)
  (h2: B ≥ 0)
  (h3: C ≥ 0):
  A^3 + B^3 + C^3 - 3 * A * B * C ≥ 0:= by

  let b := B - A
  let c := C - A
  have imp1: A^3 + B^3 + C^3 - 3 * A * B * C = (b^2 - b * c + c^2) * (A + B + C) := by ring
  --We want to show by the sum of squares that this is always non-negative.
  rw[imp1]
  simp
  ring

  have identity (a b c : Int): - (a*b*c*3) +a^3 + b^3 + c^3  = (a+b+c) * (a^2+b^2+c^2-a*b-b*c-a*c):= by
    ring
  rw[identity]

  have pos1: B+A+C ≥ 0 := by
    positivity

  have pos2: A^2 + B^2 + C^2 - A*B - B*C - A*C >= 0 := by
    sorry

  sorry

Essentially, I want to use pos1 and pos2 to reason that their product is positive. However, I don't know exactly how I could integrate these two with positivity.

Thanks!

[Edward van de Meent]

Have you tried the linarith tactic? Also, maybe using the calc tactic might help.

[Ruben Van de Velde]

Can you take it from here?

theorem algebraic_identity
    (A B C : Int)
    (h1: A ≥ 0)
    (h2: B ≥ 0)
    (h3: C ≥ 0):
    A^3 + B^3 + C^3 - 3 * A * B * C ≥ 0 := by
  calc
    0 ≤ (A^2 + B^2 + C^2 - A*B - B*C - A*C) * (A + B + C) := mul_nonneg ?_ ?_
    _ = A^3 + B^3 + C^3 - 3 * A * B * C := by ring
  · sorry
  · sorry

[Eric Chen]

Yep, this solves it. Thank you so much!

In general, how does calc work? What do the underscores and question marks mean?

[Kim Morrison]

If you hover over calc the pop-up explains the basics. ?_ is a placeholder that gives a separate goal afterwards to provide that term (either in the calculation or a proof of a step).

[Eric Chen]

I see, thanks everyone!