--- Título: En ℝ, -y > x² + 1 ⊢ y > 0 ∨ y < -1. Autor: José A. Alonso --- [mathjax] Demostrar con Lean4 que en \\(ℝ\\), \\[ -y > x² + 1 ⊢ y > 0 ∨ y < -1 \\] Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Real.Basic
variable {x y : ℝ}

example
  (h : -y > x^2 + 1)
  : y > 0 ∨ y < -1 :=
by sorry

Demostración en lenguaje natural Usaremos los siguientes lemas \\begin{align} &(∀ b, c ∈ ℝ)[b ≤ c → ∀ (a : ℝ), b + a ≤ c + a)] \\tag{L1} \\\\ &(∀ a ∈ ℝ)[0 ≤ a²] \\tag{L2} \\\\ &(∀ a ∈ ℝ)[0 + a = a] \\tag{L3} \\\\ &(∀ a, b ∈ ℝ)[a < -b ↔ b < -a] \\tag{L4} \\end{align} Se tiene \\begin{align} -y &> x^2 + 1 &&\\text{[por la hipótesis]} \\\\ &≥ 0 + 1 &&\\text{[por L1 y L2]} \\\\ &= 1 &&\\text{[por L3]} \\end{align} Por tanto, \\[ -y > 1 \\] y, aplicando el lema L4, se tiene \\[ y < -1 \\] Como se verifica la segunda parte de la diyunción, se verifica la disyunción. Demostraciones con Lean4

import Mathlib.Data.Real.Basic
variable {x y : ℝ}

-- 1ª demostración
-- ===============

example
  (h : -y > x^2 + 1)
  : y > 0 ∨ y < -1 :=
by
  have h1 : -y > 1 := by
    calc -y > x^2 + 1 := by exact h
          _ ≥ 0 + 1   := add_le_add_right (pow_two_nonneg x) 1
          _ = 1       := zero_add 1
  have h2: y < -1 := lt_neg.mp h1
  show y > 0 ∨ y < -1
  exact Or.inr h2

-- 2ª demostración
-- ===============

example
  (h : -y > x^2 + 1)
  : y > 0 ∨ y < -1 :=
by
  have h1 : -y > 1 := by linarith [pow_two_nonneg x]
  have h2: y < -1 := lt_neg.mp h1
  show y > 0 ∨ y < -1
  exact Or.inr h2

-- 3ª demostración
-- ===============

example
  (h : -y > x^2 + 1)
  : y > 0 ∨ y < -1 :=
by
  have h1: y < -1 := by linarith [pow_two_nonneg x]
  show y > 0 ∨ y < -1
  exact Or.inr h1

-- 4ª demostración
-- ===============

example
  (h : -y > x^2 + 1)
  : y > 0 ∨ y < -1 :=
by
  right
  -- ⊢ y < -1
  linarith [pow_two_nonneg x]

-- 5ª demostración
-- ===============

example
  (h : -y > x^2 + 1)
  : y > 0 ∨ y < -1 :=
by { right ; linarith [pow_two_nonneg x] }

-- Lemas usados
-- ============

-- variable (a b c : ℝ)
-- #check (add_le_add_right : b ≤ c → ∀ (a : ℝ),  b + a ≤ c + a)
-- #check (lt_neg : a < -b ↔ b < -a)
-- #check (pow_two_nonneg a : 0 ≤ a ^ 2)
-- #check (zero_add a : 0 + a = a)

Demostraciones interactivas Se puede interactuar con las demostraciones anteriores en Lean 4 Web. Referencias

J. Avigad y P. Massot. Mathematics in Lean, p. 39.