Lean Workbook

lean_workbook_plus_2

proved

exact ⟨fun h ↦ by rw [Set.mem_Ioo]; constructor <;> nlinarith [h], fun h ↦ by rw [Set.mem_Ioo] at h; nlinarith⟩

x : ℝ ⊢ x ^ 2 - 2 * x - 24 < 0 ↔ x ∈ Set.Ioo (-4) 6

no goals

Solve for $x$ in the given inequality: $x^2-2x-24<0$

x in (-4, 6)

theorem lean_workbook_plus_2 (x : ℝ) : x^2 - 2*x - 24 < 0 ↔ x ∈ Set.Ioo (-4) 6 := by sorry

lean_workbook_plus_6

proved

ring

x y z : ℤ ⊢ (x ^ 2 + 1) * (y ^ 2 + 1) * (z ^ 2 + 1) = (x + y + z) ^ 2 - 2 * (x * y + y * z + z * x) + (x * y + y * z + z * x) ^ 2 - 2 * x * y * z * (x + y + z) + x ^ 2 * y ^ 2 * z ^ 2 + 1

no goals

$\begin{array}{l}\left( {{x^2} + 1} \right)\left( {{y^2} + 1} \right)\left( {{z^2} + 1} \right) = \sum {{x^2}} + \sum {{x^2}{y^2}} + {x^2}{y^2}{z^2} + 1\\ = {\left( {x + y + z} \right)^2} - 2\left( {xy + yz + zx} \right) + {\left( {xy + yz + zx} \right)^2} - 2xyz\left( {x + y + z} \right) + {x^2}{y^2}{z^2} + 1\\ = \left[ {{{\left( {x + y + z} \right)}^2} - 2xyz\left( {x + y + z} \right) + {x^2}{y^2}{z^2}} \right] + \left[ {{{\left( {xy + yz + zx} \right)}^2} - 2\left( {xy + yz + zx} \right) + 1} \right]\\ = {\left( {x + y + z - xyz} \right)^2} + {\left( {xy + yz + zx - 1} \right)^2}\end{array …

theorem lean_workbook_plus_6 (x y z : ℤ) : (x^2 + 1) * (y^2 + 1) * (z^2 + 1) = (x + y + z)^2 - 2 * (x * y + y * z + z * x) + (x * y + y * z + z * x)^2 - 2 * x * y * z * (x + y + z) + x^2 * y^2 * z^2 + 1 := by sorry