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

State before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
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 → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hcb : ¬c ≤ b
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)

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

State before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
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 → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hba : ¬b ≤ a
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)

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

State before:
a b c : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hc : 0 ≤ c
Hcb : c ≤ b
Hba : b ≤ a
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
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))
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)

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))
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
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)
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)

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 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
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)
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)

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 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
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)
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)

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)
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
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 → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hcb : ¬c ≤ b
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
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 → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hcb : ¬c ≤ b
h3 : b ≤ c
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)

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 → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hcb : ¬c ≤ b
h3 : b ≤ c
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Tactic:
linarith [h1 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 → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hba : ¬b ≤ a
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
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 → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hba : ¬b ≤ a
h4 : a ≤ b
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)

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 → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hba : ¬b ≤ a
h4 : a ≤ b
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
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 → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hba : ¬b ≤ a
h4 : a ≤ b
hca : c ≤ a
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)

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 → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hba : ¬b ≤ a
h4 : a ≤ b
hac : a ≤ c
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)

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 → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hba : ¬b ≤ a
h4 : a ≤ b
hca : c ≤ a
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Tactic:
have := h2 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 → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hba : ¬b ≤ a
h4 : a ≤ b
hca : c ≤ a
this : 0 ≤ b * (b - a) * (b - c) + a * (a - b) * (a - c) + c * (c - b) * (c - a)
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)

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 → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hba : ¬b ≤ a
h4 : a ≤ b
hca : c ≤ a
this : 0 ≤ b * (b - a) * (b - c) + a * (a - b) * (a - c) + c * (c - b) * (c - a)
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
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 → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hba : ¬b ≤ a
h4 : a ≤ b
hac : a ≤ c
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Tactic:
have := h2 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 → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hba : ¬b ≤ a
h4 : a ≤ b
hac : a ≤ c
this : 0 ≤ b * (b - c) * (b - a) + c * (c - b) * (c - a) + a * (a - b) * (a - c)
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)

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 → 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
Hba : ¬b ≤ a
h4 : a ≤ b
hac : a ≤ c
this : 0 ≤ b * (b - c) * (b - a) + c * (c - b) * (c - a) + a * (a - b) * (a - c)
⊢ 0 ≤ a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b)
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