--- Título: Si x, y, z ∈ ℕ, entonces x divide a yxz Autor: José A. Alonso --- [mathjax] Demostrar con Lean4 que si $x, y, z ∈ ℕ$, entonces $x$ divide a $yxz$. Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Real.Basic
variable (x y z : ℕ)

example : x ∣ y * x * z :=
by sorry

Demostración en lenguaje natural Por la transitividad de la divisibilidad aplicada a las relaciones \begin{align} x &\mid yx \\\\ yx &\mid yxz \end{align} Demostraciones con Lean4

import Mathlib.Data.Real.Basic
variable (x y z : ℕ)

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

example : x ∣ y * x * z :=
by
  have h1 : x ∣ y * x :=
    dvd_mul_left x y
  have h2 : (y * x) ∣ (y * x * z) :=
    dvd_mul_right (y * x) z
  show x ∣ y * x * z
  exact dvd_trans h1 h2

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

example : x ∣ y * x * z :=
dvd_trans (dvd_mul_left x y) (dvd_mul_right (y * x) z)

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

example : x ∣ y * x * z :=
by
  apply dvd_mul_of_dvd_left
  apply dvd_mul_left


-- Los lemas utilizados son:
#check (dvd_mul_left x y : x ∣ y * x)
#check (dvd_mul_right x y : x ∣ x * y)
#check (dvd_trans : x ∣ y → y ∣ z → x ∣ z)

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

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