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

State before:
x : ℝ
⊢ (15 / 8) ^ 2 - (3 - x) * (x + 1) = (x - (1 + √31 / 8)) * (x - (1 - √31 / 8))
Tactic:
have h1 : Real.sqrt 31 ^ 2 = 31 := Real.sq_sqrt (Nat.ofNat_nonneg _)
State after:
x : ℝ
h1 : √31 ^ 2 = 31
⊢ (15 / 8) ^ 2 - (3 - x) * (x + 1) = (x - (1 + √31 / 8)) * (x - (1 - √31 / 8))

State before:
x : ℝ
h1 : √31 ^ 2 = 31
⊢ (15 / 8) ^ 2 - (3 - x) * (x + 1) = (x - (1 + √31 / 8)) * (x - (1 - √31 / 8))
Tactic:
ring_nf
State after:
x : ℝ
h1 : √31 ^ 2 = 31
⊢ 33 / 64 - x * 2 + x ^ 2 = 1 - x * 2 + x ^ 2 + √31 ^ 2 * (-1 / 64)

State before:
x : ℝ
h1 : √31 ^ 2 = 31
⊢ 33 / 64 - x * 2 + x ^ 2 = 1 - x * 2 + x ^ 2 + √31 ^ 2 * (-1 / 64)
Tactic:
rw [h1]
State after:
x : ℝ
h1 : √31 ^ 2 = 31
⊢ 33 / 64 - x * 2 + x ^ 2 = 1 - x * 2 + x ^ 2 + 31 * (-1 / 64)

State before:
x : ℝ
h1 : √31 ^ 2 = 31
⊢ 33 / 64 - x * 2 + x ^ 2 = 1 - x * 2 + x ^ 2 + 31 * (-1 / 64)
Tactic:
ring
State after:
no goals