--- Título: Las funciones f(x,y) = (x + y)² y g(x,y) = x² + 2xy + y² son iguales Autor: José A. Alonso --- [mathjax] Demostrar con Lean4 que las funciones \\(f(x,y) = (x + y)²\\) y \\(g(x,y) = x² + 2xy + y\\)² son iguales. Para ello, completar la siguiente teoría de Lean4:

import  Mathlib.Data.Real.Basic

example : (fun x y : ℝ ↦ (x + y)^2) = (fun x y : ℝ ↦ x^2 + 2*x*y + y^2) :=
by sorry

1. Demostraciones con Lean4

import  Mathlib.Data.Real.Basic

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

example : (fun x y : ℝ ↦ (x + y)^2) = (fun x y : ℝ ↦ x^2 + 2*x*y + y^2) :=
by
  ext u v
  -- u v : ℝ
  -- ⊢ (u + v) ^ 2 = u ^ 2 + 2 * u * v + v ^ 2
  ring

-- Comentario: La táctica ext transforma las conclusiones de la forma
-- (fun x ↦ f x) = (fun x ↦ g x) en f x = g x.

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

example : (fun x y : ℝ ↦ (x + y)^2) = (fun x y : ℝ ↦ x^2 + 2*x*y + y^2) :=
by { ext ; ring }

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

Referencias

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