Theorem: Usa2001P3.usa2001_p3_lemma (Compfiles/Usa2001P3.lean)

State before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
⊢ a * b + b * c + c * a - a * b * c ≤ 2
Tactic:
have eq1 := calc
  (2 + a) * (2 - a) = 4 - a ^ 2 := by ring_nf
  _ = a ^ 2 + b ^ 2 + c ^ 2 + a * b * c - a ^ 2 := by rw [h]
  _ = (b ^ 2 + c ^ 2) + a * b * c := by ring_nf
  _ ≥ 2 * b * c + a * b * c := by rel [two_mul_le_add_sq b c]
  _ = (2 + a) * (b * c) := by ring_nf
State after:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
⊢ a * b + b * c + c * a - a * b * c ≤ 2

State before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
⊢ a * b + b * c + c * a - a * b * c ≤ 2
Tactic:
have a2gt0 : 2 + a > 0 := by linarith
State after:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
a2gt0 : 2 + a > 0
⊢ a * b + b * c + c * a - a * b * c ≤ 2

State before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
a2gt0 : 2 + a > 0
⊢ a * b + b * c + c * a - a * b * c ≤ 2
Tactic:
have bc := (mul_le_mul_left a2gt0).mp eq1
State after:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
a2gt0 : 2 + a > 0
bc : b * c ≤ 2 - a
⊢ a * b + b * c + c * a - a * b * c ≤ 2

State before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
a2gt0 : 2 + a > 0
bc : b * c ≤ 2 - a
⊢ a * b + b * c + c * a - a * b * c ≤ 2
Tactic:
calc
  a * b + b * c + c * a - a * b * c = a * b + b * c + a * c * (1 - b) := by ring_nf
  _ ≤ a * b + (2 - a) + a * c * (1 - b) := by gcongr
  _ = 2 - a * ((b - 1) * (c - 1)) := by ring_nf
  _ ≤ 2 - 0 := by gcongr; positivity
  _ = 2 := by norm_num
State after:
no goals

State before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
⊢ (2 + a) * (2 - a) = 4 - a ^ 2
Tactic:
ring_nf
State after:
no goals

State before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
⊢ 4 - a ^ 2 = a ^ 2 + b ^ 2 + c ^ 2 + a * b * c - a ^ 2
Tactic:
rw [h]
State after:
no goals

State before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
⊢ a ^ 2 + b ^ 2 + c ^ 2 + a * b * c - a ^ 2 = b ^ 2 + c ^ 2 + a * b * c
Tactic:
ring_nf
State after:
no goals

State before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
⊢ b ^ 2 + c ^ 2 + a * b * c ≥ 2 * b * c + a * b * c
Tactic:
rel [two_mul_le_add_sq b c]
State after:
no goals

State before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
⊢ 2 * b * c + a * b * c = (2 + a) * (b * c)
Tactic:
ring_nf
State after:
no goals

State before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
⊢ 2 + a > 0
Tactic:
linarith
State after:
no goals

State before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
a2gt0 : 2 + a > 0
bc : b * c ≤ 2 - a
⊢ a * b + b * c + c * a - a * b * c = a * b + b * c + a * c * (1 - b)
Tactic:
ring_nf
State after:
no goals

State before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
a2gt0 : 2 + a > 0
bc : b * c ≤ 2 - a
⊢ a * b + b * c + a * c * (1 - b) ≤ a * b + (2 - a) + a * c * (1 - b)
Tactic:
gcongr
State after:
no goals

State before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
a2gt0 : 2 + a > 0
bc : b * c ≤ 2 - a
⊢ a * b + (2 - a) + a * c * (1 - b) = 2 - a * ((b - 1) * (c - 1))
Tactic:
ring_nf
State after:
no goals

State before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
a2gt0 : 2 + a > 0
bc : b * c ≤ 2 - a
⊢ 2 - a * ((b - 1) * (c - 1)) ≤ 2 - 0
Tactic:
gcongr
State after:
case h
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
a2gt0 : 2 + a > 0
bc : b * c ≤ 2 - a
⊢ 0 ≤ a * ((b - 1) * (c - 1))

State before:
case h
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
a2gt0 : 2 + a > 0
bc : b * c ≤ 2 - a
⊢ 0 ≤ a * ((b - 1) * (c - 1))
Tactic:
positivity
State after:
no goals

State before:
a b c : ℝ
ha : 0 ≤ a
_hb : 0 ≤ b
_hc : 0 ≤ c
h : a ^ 2 + b ^ 2 + c ^ 2 + a * b * c = 4
hbc : (b - 1) * (c - 1) ≥ 0
eq1 : (2 + a) * (2 - a) ≥ (2 + a) * (b * c)
a2gt0 : 2 + a > 0
bc : b * c ≤ 2 - a
⊢ 2 - 0 = 2
Tactic:
norm_num
State after:
no goals