Theorem: Imo2000P2.schur (Compfiles/Imo2000P2.lean)

State before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
wlog Hcb : c ≤ b with h1
State after:
case inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
h1 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
              a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hcb : ¬c ≤ b
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c

a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c

State before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
wlog Hba : b ≤ a with h2
State after:
case inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
                a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hba : ¬b ≤ a
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c

a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c

State before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
have h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) =
          (a - b) * (a * (a - c) - b * (b - c)) := by ring
State after:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c

State before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ (a - b) * (a * (a - c) - b * (b - c))
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
rw [← h5] at h6
State after:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c

State before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
have h12 : 0 ≤ (c - a) * (c - b) := by nlinarith only [Hba, Hcb]
State after:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
h12 : 0 ≤ (c - a) * (c - b)
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c

State before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
h12 : 0 ≤ (c - a) * (c - b)
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
have h13 : 0 ≤ c * (c - a) * (c - b) := by nlinarith only [hc, h12]
State after:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
h12 : 0 ≤ (c - a) * (c - b)
h13 : 0 ≤ c * (c - a) * (c - b)
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c

State before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
h12 : 0 ≤ (c - a) * (c - b)
h13 : 0 ≤ c * (c - a) * (c - b)
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
linarith
State after:
no goals

State before:
case inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
h1 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
              a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hcb : ¬c ≤ b
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
have h3 : b ≤ c := le_of_not_le Hcb
State after:
case inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
h1 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
              a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hcb : ¬c ≤ b
h3 : b ≤ c
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c

State before:
case inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
h1 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
              a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hcb : ¬c ≤ b
h3 : b ≤ c
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
linarith [h1 a c b ha hc hb h3]
State after:
no goals

State before:
case inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
                a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hba : ¬b ≤ a
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
have h4 : a ≤ b := le_of_not_le Hba
State after:
case inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
                a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hba : ¬b ≤ a
h4 : a ≤ b
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c

State before:
case inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
                a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hba : ¬b ≤ a
h4 : a ≤ b
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
obtain hca | hac : c ≤ a ∨ a ≤ c := le_total c a
State after:
case inr.inl
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
                a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hba : ¬b ≤ a
h4 : a ≤ b
hca : c ≤ a
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c

case inr.inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
                a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hba : ¬b ≤ a
h4 : a ≤ b
hac : a ≤ c
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c

State before:
case inr.inl
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
                a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hba : ¬b ≤ a
h4 : a ≤ b
hca : c ≤ a
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
have := h2 b a c hb ha hc hca h4
State after:
case inr.inl
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
                a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hba : ¬b ≤ a
h4 : a ≤ b
hca : c ≤ a
this : b ^ 2 * a + b ^ 2 * c + a ^ 2 * b + a ^ 2 * c + c ^ 2 * b + c ^ 2 * a ≤ b ^ 3 + a ^ 3 + c ^ 3 + 3 * b * a * c
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c

State before:
case inr.inl
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
                a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hba : ¬b ≤ a
h4 : a ≤ b
hca : c ≤ a
this : b ^ 2 * a + b ^ 2 * c + a ^ 2 * b + a ^ 2 * c + c ^ 2 * b + c ^ 2 * a ≤ b ^ 3 + a ^ 3 + c ^ 3 + 3 * b * a * c
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
linarith only [this]
State after:
no goals

State before:
case inr.inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
                a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hba : ¬b ≤ a
h4 : a ≤ b
hac : a ≤ c
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
have := h2 b c a hb hc ha hac Hcb
State after:
case inr.inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
                a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hba : ¬b ≤ a
h4 : a ≤ b
hac : a ≤ c
this : b ^ 2 * c + b ^ 2 * a + c ^ 2 * b + c ^ 2 * a + a ^ 2 * b + a ^ 2 * c ≤ b ^ 3 + c ^ 3 + a ^ 3 + 3 * b * c * a
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c

State before:
case inr.inr
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
h2 :
  ∀ (a b c : ℝ),
    0 ≤ a →
      0 ≤ b →
        0 ≤ c →
          c ≤ b →
            b ≤ a →
              a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤
                a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Hba : ¬b ≤ a
h4 : a ≤ b
hac : a ≤ c
this : b ^ 2 * c + b ^ 2 * a + c ^ 2 * b + c ^ 2 * a + a ^ 2 * b + a ^ 2 * c ≤ b ^ 3 + c ^ 3 + a ^ 3 + 3 * b * c * a
⊢ a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b ≤ a ^ 3 + b ^ 3 + c ^ 3 + 3 * a * b * c
Tactic:
linarith only [this]
State after:
no goals

State before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
⊢ a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
Tactic:
ring
State after:
no goals

State before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
⊢ 0 ≤ (a - b) * (a * (a - c) - b * (b - c))
Tactic:
apply mul_nonneg
State after:
case ha
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
⊢ 0 ≤ a - b

case hb
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
⊢ 0 ≤ a * (a - c) - b * (b - c)

State before:
case ha
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
⊢ 0 ≤ a - b
Tactic:
exact sub_nonneg_of_le Hba
State after:
no goals

State before:
case hb
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
⊢ 0 ≤ a * (a - c) - b * (b - c)
Tactic:
nlinarith
State after:
no goals

State before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
⊢ 0 ≤ (c - a) * (c - b)
Tactic:
nlinarith only [Hba, Hcb]
State after:
no goals

State before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
h5 : a * (a - b) * (a - c) + b * (b - a) * (b - c) = (a - b) * (a * (a - c) - b * (b - c))
h6 : 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c)
h12 : 0 ≤ (c - a) * (c - b)
⊢ 0 ≤ c * (c - a) * (c - b)
Tactic:
nlinarith only [hc, h12]
State after:
no goals