--- Título: 3 divide al máximo común divisor de 6 y 15. Autor: José A. Alonso --- [mathjax] Demostrar con Lean4 que 3 divide al máximo común divisor de 6 y 15. Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Real.Basic
import Mathlib.Data.Nat.GCD.Basic

open Nat

example : 3 ∣ gcd 6 15 :=
by sorry

Demostración en lenguaje natural Se usará el siguiente lema \\[ (∀ k, m, n ∈ ℕ)[k ∣ \gcd(m, n) ↔ k ∣ m ∧ k ∣ n] \\] Por el lema, \\[ 3 ∣ \gcd(6, 15) \\] se reduce a \\[ 3 ∣ 6 ∧ 3 ∣ 15 \\] que se verifican fácilmente. Demostraciones con Lean4

import Mathlib.Data.Real.Basic
import Mathlib.Data.Nat.GCD.Basic

open Nat

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

example : 3 ∣ gcd 6 15 :=
by
  rw [dvd_gcd_iff]
  -- ⊢ 3 ∣ 6 ∧ 3 ∣ 15
  constructor
  . -- 3 ∣ 6
    norm_num
  . -- ⊢ 3 ∣ 15
    norm_num

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

example : 3 ∣ gcd 6 15 :=
by
  rw [dvd_gcd_iff]
  -- ⊢ 3 ∣ 6 ∧ 3 ∣ 15
  constructor <;> norm_num

-- Lemas usados
-- ============

-- variable (k m n : ℕ)
-- #check (dvd_gcd_iff : k ∣ gcd m n ↔ k ∣ m ∧ k ∣ n)

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

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