--- Título: (a+b)(a-b) = a^2-b^2 Autor: José A. Alonso --- Demostrar con Lean4 que si a y b son números reales, entonces

   (a + b) * (a - b) = a^2 - b^2

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (a b : ℝ)

example : (a + b) * (a - b) = a^2 - b^2 :=
sorry

Demostración en lenguaje natural [mathjax] Por la siguiente cadena de igualdades: \begin{align} (a + b)(a - b) &= a(a - b) + b(a - b) &&\text{[por la distributiva]} \\ &= (aa - ab) + b(a - b) &&\text{[por la distributiva]} \\ &= (a^2 - ab) + b(a - b) &&\text{[por def. de cuadrado]} \\ &= (a^2 - ab) + (ba - bb) &&\text{[por la distributiva]} \\ &= (a^2 - ab) + (ba - b^2) &&\text{[por def. de cuadrado]} \\ &= (a^2 + -(ab)) + (ba - b^2) &&\text{[por def. de resta]} \\ &= a^2 + (-(ab) + (ba - b^2)) &&\text{[por la asociativa]} \\ &= a^2 + (-(ab) + (ba + -b^2)) &&\text{[por def. de resta]} \\ &= a^2 + ((-(ab) + ba) + -b^2) &&\text{[por la asociativa]} \\ &= a^2 + ((-(ab) + ab) + -b^2) &&\text{[por la conmutativa]} \\ &= a^2 + (0 + -b^2) &&\text{[por def. de opuesto]} \\ &= (a^2 + 0) + -b^2 &&\text{[por asociativa]} \\ &= a^2 + -b^2 &&\text{[por def. de cero]} \\ &= a^2 - b^2 &&\text{[por def. de resta]} \end{align} Demostraciones con Lean

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (a b : ℝ)

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

example : (a + b) * (a - b) = a^2 - b^2 :=
calc
  (a + b) * (a - b)
    = a * (a - b) + b * (a - b)         := by rw [add_mul]
  _ = (a * a - a * b) + b * (a - b)     := by rw [mul_sub]
  _ = (a^2 - a * b) + b * (a - b)       := by rw [← pow_two]
  _ = (a^2 - a * b) + (b * a - b * b)   := by rw [mul_sub]
  _ = (a^2 - a * b) + (b * a - b^2)     := by rw [← pow_two]
  _ = (a^2 + -(a * b)) + (b * a - b^2)  := by ring
  _ = a^2 + (-(a * b) + (b * a - b^2))  := by rw [add_assoc]
  _ = a^2 + (-(a * b) + (b * a + -b^2)) := by ring
  _ = a^2 + ((-(a * b) + b * a) + -b^2) := by rw [← add_assoc
                                              (-(a * b)) (b * a) (-b^2)]
  _ = a^2 + ((-(a * b) + a * b) + -b^2) := by rw [mul_comm]
  _ = a^2 + (0 + -b^2)                  := by rw [neg_add_self (a * b)]
  _ = (a^2 + 0) + -b^2                  := by rw [← add_assoc]
  _ = a^2 + -b^2                        := by rw [add_zero]
  _ = a^2 - b^2                         := by linarith

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

example : (a + b) * (a - b) = a^2 - b^2 :=
calc
  (a + b) * (a - b)
    = a * (a - b) + b * (a - b)         := by ring
  _ = (a * a - a * b) + b * (a - b)     := by ring
  _ = (a^2 - a * b) + b * (a - b)       := by ring
  _ = (a^2 - a * b) + (b * a - b * b)   := by ring
  _ = (a^2 - a * b) + (b * a - b^2)     := by ring
  _ = (a^2 + -(a * b)) + (b * a - b^2)  := by ring
  _ = a^2 + (-(a * b) + (b * a - b^2))  := by ring
  _ = a^2 + (-(a * b) + (b * a + -b^2)) := by ring
  _ = a^2 + ((-(a * b) + b * a) + -b^2) := by ring
  _ = a^2 + ((-(a * b) + a * b) + -b^2) := by ring
  _ = a^2 + (0 + -b^2)                  := by ring
  _ = (a^2 + 0) + -b^2                  := by ring
  _ = a^2 + -b^2                        := by ring
  _ = a^2 - b^2                         := by ring

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

example : (a + b) * (a - b) = a^2 - b^2 :=
by ring

-- 4ª demostración (por reescritura usando el lema anterior)
-- =========================================================

-- El lema anterior es
lemma aux : (a + b) * (c + d) = a * c + a * d + b * c + b * d :=
by ring

-- La demostración es
example : (a + b) * (a - b) = a^2 - b^2 :=
by
  rw [sub_eq_add_neg]
  rw [aux]
  rw [mul_neg]
  rw [add_assoc (a * a)]
  rw [mul_comm b a]
  rw [neg_add_self]
  rw [add_zero]
  rw [← pow_two]
  rw [mul_neg]
  rw [← pow_two]
  rw [← sub_eq_add_neg]

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

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