Demostrar con Lean4 que si \(M\) es un monoide conmutativo y \(x, y, z \u2208 M\) tales que \(x\u00b7y = 1\) y \(x\u00b7z = 1\), entonces \(y = z\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Algebra.Group.Basic\n\nvariable {M : Type} [CommMonoid M]\nvariable {x y z : M}\n\nexample\n (hy : x * y = 1)\n (hz : x * z = 1)\n : y = z :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Por la siguiente cadena de igualdades
\n\begin{align}
\n y &= 1\u00b7y &&\text{[por neutro a la izquierda]} \\
\n &= (x\u00b7z)\u00b7y &&\text{[por hip\u00f3tesis]} \\
\n &= (z\u00b7x)\u00b7y &&\text{[por la conmutativa]} \\
\n &= z\u00b7(x\u00b7y) &&\text{[por la asociativa]} \\
\n &= z\u00b71 &&\text{[por hip\u00f3tesis]} \\
\n &= z &&\text{[por neutro a la derecha]}
\n\end{align}<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Algebra.Group.Basic\n\nvariable {M : Type} [CommMonoid M]\nvariable {x y z : M}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (hy : x * y = 1)\n (hz : x * z = 1)\n : y = z :=\ncalc y = 1 * y := (one_mul y).symm\n _ = (x * z) * y := congrArg (. * y) hz.symm\n _ = (z * x) * y := congrArg (. * y) (mul_comm x z)\n _ = z * (x * y) := mul_assoc z x y\n _ = z * 1 := congrArg (z * .) hy\n _ = z := mul_one z\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (hy : x * y = 1)\n (hz : x * z = 1)\n : y = z :=\ncalc y = 1 * y := by simp only [one_mul]\n _ = (x * z) * y := by simp only [hz]\n _ = (z * x) * y := by simp only [mul_comm]\n _ = z * (x * y) := by simp only [mul_assoc]\n _ = z * 1 := by simp only [hy]\n _ = z := by simp only [mul_one]\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (hy : x * y = 1)\n (hz : x * z = 1)\n : y = z :=\ncalc y = 1 * y := by simp\n _ = (x * z) * y := by simp [hz]\n _ = (z * x) * y := by simp [mul_comm]\n _ = z * (x * y) := by simp [mul_assoc]\n _ = z * 1 := by simp [hy]\n _ = z := by simp\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (hy : x * y = 1)\n (hz : x * z = 1)\n : y = z :=\nby\n apply left_inv_eq_right_inv _ hz\n -- \u22a2 y * x = 1\n rw [mul_comm]\n -- \u22a2 x * y = 1\n exact hy\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (hy : x * y = 1)\n (hz : x * z = 1)\n : y = z :=\ninv_unique hy hz\n\n-- Lemas usados\n-- ============\n\n-- #check (inv_unique : x * y = 1 \u2192 x * z = 1 \u2192 y = z)\n-- #check (left_inv_eq_right_inv : y * x = 1 \u2192 x * z = 1 \u2192 y = z)\n-- #check (mul_assoc x y z : (x * y) * z = x * (y * z))\n-- #check (mul_comm x y : x * y = y * x)\n-- #check (mul_one x : x * 1 = x)\n-- #check (one_mul x : 1 * x = x)\n<\/pre>\n