Theorem: Imo2006P3.proof₂ (Compfiles/Imo2006P3.lean)

State before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
⊢ 9 * √2 / 32 ≤ M
Tactic:
set α := sqrt (2:ℝ)
State after:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
⊢ 9 * α / 32 ≤ M

State before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
⊢ 9 * α / 32 ≤ M
Tactic:
have hα : α ^ 2 = 2 := sq_sqrt (by norm_num)
State after:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
⊢ 9 * α / 32 ≤ M

State before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
⊢ 9 * α / 32 ≤ M
Tactic:
let a := 2 - 3 * α
State after:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
⊢ 9 * α / 32 ≤ M

State before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
⊢ 9 * α / 32 ≤ M
Tactic:
let c := 2 + 3 * α
State after:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 9 * α / 32 ≤ M

State before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 9 * α / 32 ≤ M
Tactic:
calc _ = 18 ^ 2 * 2 * α / 48 ^ 2 := by ring
  _ ≤ M := ?_
State after:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 18 ^ 2 * 2 * α / 48 ^ 2 ≤ M

State before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 18 ^ 2 * 2 * α / 48 ^ 2 ≤ M
Tactic:
rw [div_le_iff (by positivity)]
State after:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 18 ^ 2 * 2 * α ≤ M * 48 ^ 2

State before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 18 ^ 2 * 2 * α ≤ M * 48 ^ 2
Tactic:
calc 18 ^ 2 * 2 * α
    = 18 ^ 2 * α ^ 2 * α := by linear_combination -324 * α * hα
  _ = abs (-(18 ^ 2 * α ^ 2 * α)) := by rw [abs_neg, abs_of_nonneg]; positivity
  _ = |a * 2 * (a ^ 2 - 2 ^ 2) + 2 * c * (2 ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| := by ring_nf
  _ ≤ M * (a ^ 2 + 2 ^ 2 + c ^ 2) ^ 2 := by apply h
  _ = M * 48 ^ 2 := by linear_combination (324 * α ^ 2 + 1080) * M * hα
State after:
no goals

State before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
⊢ 0 ≤ 2
Tactic:
norm_num
State after:
no goals

State before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 9 * α / 32 = 18 ^ 2 * 2 * α / 48 ^ 2
Tactic:
ring
State after:
no goals

State before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 0 < 48 ^ 2
Tactic:
positivity
State after:
no goals

State before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 18 ^ 2 * 2 * α = 18 ^ 2 * α ^ 2 * α
Tactic:
linear_combination -324 * α * hα
State after:
no goals

State before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 18 ^ 2 * α ^ 2 * α = |(-(18 ^ 2 * α ^ 2 * α))|
Tactic:
rw [abs_neg, abs_of_nonneg]
State after:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 0 ≤ 18 ^ 2 * α ^ 2 * α

State before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 0 ≤ 18 ^ 2 * α ^ 2 * α
Tactic:
positivity
State after:
no goals

State before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ |(-(18 ^ 2 * α ^ 2 * α))| = |a * 2 * (a ^ 2 - 2 ^ 2) + 2 * c * (2 ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)|
Tactic:
ring_nf
State after:
no goals

State before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ |a * 2 * (a ^ 2 - 2 ^ 2) + 2 * c * (2 ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + 2 ^ 2 + c ^ 2) ^ 2
Tactic:
apply h
State after:
no goals

State before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ M * (a ^ 2 + 2 ^ 2 + c ^ 2) ^ 2 = M * 48 ^ 2
Tactic:
linear_combination (324 * α ^ 2 + 1080) * M * hα
State after:
no goals