--- Título: (a + b)(a + b) = aa + 2ab + bb Autor: José A. Alonso --- Demostrar con Lean4 que si a y b son números reales, entonces 
   (a + b) * (a + b) = a * a + 2 * (a * b) + b * b
Para ello, completar la siguiente teoría de Lean4: 
import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (a b c : ℝ)

example :
  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
sorry
Demostración en lenguaje natural [mathjax] Por la siguiente cadena de igualdades \begin{align} (a + b)(a + b) &= (a + b)a + (a + b)b &&\text{[por la distributiva]} \\ &= aa + ba + (a + b)b &&\text{[por la distributiva]} \\ &= aa + ba + (ab + bb) &&\text{[por la distributiva]} \\ &= aa + ba + ab + bb &&\text{[por la asociativa]} \\ &= aa + (ba + ab) + bb &&\text{[por la asociativa]} \\ &= aa + (ab + ab) + bb &&\text{[por la conmutativa]} \\ &= aa + 2(ab) + bb &&\text{[por def. de doble]} \\ \end{align} Demostraciones con Lean4 
import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (a b c : ℝ)

-- 1ª demostración
example :
  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
calc
  (a + b) * (a + b)
    = (a + b) * a + (a + b) * b       := by rw [mul_add]
  _ = a * a + b * a + (a + b) * b     := by rw [add_mul]
  _ = a * a + b * a + (a * b + b * b) := by rw [add_mul]
  _ = a * a + b * a + a * b + b * b   := by rw [←add_assoc]
  _ = a * a + (b * a + a * b) + b * b := by rw [add_assoc (a * a)]
  _ = a * a + (a * b + a * b) + b * b := by rw [mul_comm b a]
  _ = a * a + 2 * (a * b) + b * b     := by rw [←two_mul]

-- 2ª demostración
example :
  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
calc
  (a + b) * (a + b)
    = a * a + b * a + (a * b + b * b) := by rw [mul_add, add_mul, add_mul]
  _ = a * a + (b * a + a * b) + b * b := by rw [←add_assoc, add_assoc (a * a)]
  _ = a * a + 2 * (a * b) + b * b     := by rw [mul_comm b a, ←two_mul]

-- 3ª demostración
example :
  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
calc
  (a + b) * (a + b)
    = a * a + b * a + (a * b + b * b) := by ring
  _ = a * a + (b * a + a * b) + b * b := by ring
  _ = a * a + 2 * (a * b) + b * b     := by ring

-- 4ª demostración
example :
  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
by ring

-- 5ª demostración
example :
  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
by
  rw [mul_add]
  rw [add_mul]
  rw [add_mul]
  rw [←add_assoc]
  rw [add_assoc (a * a)]
  rw [mul_comm b a]
  rw [←two_mul]

-- 6ª demostración
example :
  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
by
  rw [mul_add, add_mul, add_mul]
  rw [←add_assoc, add_assoc (a * a)]
  rw [mul_comm b a, ←two_mul]

-- 7ª demostración
example :
  (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
by linarith
Demostraciones interactivas Se puede interactuar con las demostraciones anteriores en Lean 4 Web. Referencias