Sea \(M\) un monoide y \(a, b \u2208 M\) tales que \(ab = 1\). Demostrar con Lean4 que \(a = 1\) si y s\u00f3lo si \(b = 1\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Algebra.Group.Basic\n\nvariable {M : Type} [Monoid M]\nvariable {a b : M}\n\nexample\n (h : a * b = 1)\n : a = 1 \u2194 b = 1 :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Demostraremos las dos implicaciones.<\/p>\n
(\u27f9) Supongamos que \(a = 1\). Entonces,
\n\begin{align}
\n b &= 1\u00b7b &&\text{[por neutro por la izquierda]} \\
\n &= a\u00b7b &&\text{[por supuesto]} \\
\n &= 1 &&\text{[por hip\u00f3tesis]}
\n\end{align}<\/p>\n
(\u27f8) Supongamos que \(b = 1\). Entonces,
\n\begin{align}
\n a &= a\u00b71 &&\text{[por neutro por la derecha]} \\
\n &= a\u00b7b &&\text{[por supuesto]} \\
\n &= 1 &&\text{[por hip\u00f3tesis]}
\n\end{align}<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Algebra.Group.Basic\n\nvariable {M : Type} [Monoid M]\nvariable {a b : M}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : a * b = 1)\n : a = 1 \u2194 b = 1 :=\nby\n constructor\n . -- \u22a2 a = 1 \u2192 b = 1\n intro a1\n -- a1 : a = 1\n -- \u22a2 b = 1\n calc b = 1 * b := (one_mul b).symm\n _ = a * b := congrArg (. * b) a1.symm\n _ = 1 := h\n . -- \u22a2 b = 1 \u2192 a = 1\n intro b1\n -- b1 : b = 1\n -- \u22a2 a = 1\n calc a = a * 1 := (mul_one a).symm\n _ = a * b := congrArg (a * .) b1.symm\n _ = 1 := h\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : a * b = 1)\n : a = 1 \u2194 b = 1 :=\nby\n constructor\n . -- \u22a2 a = 1 \u2192 b = 1\n intro a1\n -- a1 : a = 1\n -- \u22a2 b = 1\n rw [a1] at h\n -- h : 1 * b = 1\n rw [one_mul] at h\n -- h : b = 1\n exact h\n . -- \u22a2 b = 1 \u2192 a = 1\n intro b1\n -- b1 : b = 1\n -- \u22a2 a = 1\n rw [b1] at h\n -- h : a * 1 = 1\n rw [mul_one] at h\n -- h : a = 1\n exact h\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : a * b = 1)\n : a = 1 \u2194 b = 1 :=\nby\n constructor\n . -- \u22a2 a = 1 \u2192 b = 1\n rintro rfl\n -- h : 1 * b = 1\n simpa using h\n . -- \u22a2 b = 1 \u2192 a = 1\n rintro rfl\n -- h : a * 1 = 1\n simpa using h\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : a * b = 1)\n : a = 1 \u2194 b = 1 :=\nby constructor <;> (rintro rfl; simpa using h)\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : a * b = 1)\n : a = 1 \u2194 b = 1 :=\neq_one_iff_eq_one_of_mul_eq_one h\n\n-- Lemas usados\n-- ============\n\n-- #check (eq_one_iff_eq_one_of_mul_eq_one : a * b = 1 \u2192 (a = 1 \u2194 b = 1))\n-- #check (mul_one a : a * 1 = a)\n-- #check (one_mul a : 1 * a = a)\n<\/pre>\n