Theorem: Imo1962P2.lemma2 (Compfiles/Imo1962P2.lean)

State before:
x : ℝ
hx4 : 0 ≤ 3 - x
hx5 : 0 ≤ x + 1
⊢ √(3 - x) ^ 2 - 2 * √(3 - x) * √(x + 1) + √(x + 1) ^ 2 = 3 - x - 2 * √(3 - x) * √(x + 1) + (x + 1)
Tactic:
rw [Real.sq_sqrt hx4, add_left_cancel_iff, Real.sq_sqrt hx5]
State after:
no goals

State before:
x : ℝ
hx4 : 0 ≤ 3 - x
hx5 : 0 ≤ x + 1
⊢ 3 - x - 2 * √(3 - x) * √(x + 1) + (x + 1) = 4 - 2 * (√(3 - x) * √(x + 1))
Tactic:
ring
State after:
no goals

State before:
x : ℝ
hx4 : 0 ≤ 3 - x
hx5 : 0 ≤ x + 1
⊢ 4 - 2 * (√(3 - x) * √(x + 1)) = 4 - 2 * √((3 - x) * (x + 1))
Tactic:
rw[←Real.sqrt_mul hx4]
State after:
no goals