a(be)_eq_c(df).md

Título	Autor
Si ab = cd y e = f, entonces a(be) = c(df)	José A. Alonso

Demostrar con Lean4 que si ab = cd y e = f, entonces a(be) = c(df)

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

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

example
  (a b c d e f : ℝ)
  (h1 : a * b = c * d)
  (h2 : e = f)
  : a * (b * e) = c * (d * f) :=
by sorry

Demostración en leguaje natural

[mathjax] Por la siguiente cadena de igualdades \begin{align} a(be) &= a(bf) &&\text{[por la segunda hipótesis]} \ &= (ab)f &&\text{[por la asociativa]} \ &= (cd)f &&\text{[por la primera hipótesis]} \ &= c(df) &&\text{[por la asociativa]} \end{align}

Demostraciones con Lean

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

-- 1ª demostración
example
  (a b c d e f : ℝ)
  (h1 : a * b = c * d)
  (h2 : e = f)
  : a * (b * e) = c * (d * f) :=
calc
  a * (b * e)
    = a * (b * f) := by rw [h2]
  _ = (a * b) * f := by rw [←mul_assoc]
  _ = (c * d) * f := by rw [h1]
  _ = c * (d * f) := by rw [mul_assoc]

-- 2ª demostración
example
  (a b c d e f : ℝ)
  (h1 : a * b = c * d)
  (h2 : e = f)
  : a * (b * e) = c * (d * f) :=
by
  rw [h2]
  rw [←mul_assoc]
  rw [h1]
  rw [mul_assoc]

-- 3ª demostración
example
  (a b c d e f : ℝ)
  (h1 : a * b = c * d)
  (h2 : e = f)
  : a * (b * e) = c * (d * f) :=
by
  simp [*, ←mul_assoc]

Demostraciones interactivas

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

Referencias

• J. Avigad y P. Massot. Mathematics in Lean, p. 6.