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

State before:
a b c : ℝ
⊢ |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| =
    |(a - b) * (b - c) * (c - a) * -(a + b + c)|
Tactic:
ring_nf
State after:
no goals

State before:
a b c : ℝ
⊢ a - b + (b - c) + (c - a) = 0
Tactic:
ring
State after:
no goals

State before:
a b c : ℝ
⊢ √2 / 32 * ((a - b) ^ 2 + (b - c) ^ 2 + (c - a) ^ 2 + (-(a + b + c)) ^ 2) ^ 2 =
    9 * √2 / 32 * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
Tactic:
ring
State after:
no goals