Demostrar con Lean4 que si \(G\) es un grupo y \(a, b, c \u2208 G\) tales que \(a\u00b7b = a\u00b7c\), entonces \(b = c\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Algebra.Group.Basic\n\nvariable {G : Type} [Group G]\nvariable {a b c : G}\n\nexample\n (h: a * b = a * c)\n : b = c :=\nsorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Por la siguiente cadena de igualdades
\n\begin{align}
\n b &= 1\u00b7b &&\text{[porque \(1\) es neutro]} \\
\n &= (a\u207b\u00b9\u00b7a)\u00b7b &&\text{[porque \(a\u207b\u00b9\) es el inverso de \(a\)]} \\
\n &= a\u207b\u00b9\u00b7(a\u00b7b) &&\text{[por la asociativa]} \\
\n &= a\u207b\u00b9\u00b7(a\u00b7c) &&\text{[por la hip\u00f3tesis]} \\
\n &= (a\u207b\u00b9\u00b7a)\u00b7c &&\text{[por la asociativa]} \\
\n &= 1\u00b7c &&\text{[porque \(a\u207b\u00b9\) es el inverso de \(a\)]} \\
\n &= c &&\text{[porque 1 es neutro]}
\n\end{align}<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Algebra.Group.Basic\n\nvariable {G : Type} [Group G]\nvariable {a b c : G}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h: a * b = a * c)\n : b = c :=\ncalc b = 1 * b := (one_mul b).symm\n _ = (a\u207b\u00b9 * a) * b := congrArg (. * b) (inv_mul_self a).symm\n _ = a\u207b\u00b9 * (a * b) := mul_assoc a\u207b\u00b9 a b\n _ = a\u207b\u00b9 * (a * c) := congrArg (a\u207b\u00b9 * .) h\n _ = (a\u207b\u00b9 * a) * c := (mul_assoc a\u207b\u00b9 a c).symm\n _ = 1 * c := congrArg (. * c) (inv_mul_self a)\n _ = c := one_mul c\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h: a * b = a * c)\n : b = c :=\ncalc b = 1 * b := by rw [one_mul]\n _ = (a\u207b\u00b9 * a) * b := by rw [inv_mul_self]\n _ = a\u207b\u00b9 * (a * b) := by rw [mul_assoc]\n _ = a\u207b\u00b9 * (a * c) := by rw [h]\n _ = (a\u207b\u00b9 * a) * c := by rw [mul_assoc]\n _ = 1 * c := by rw [inv_mul_self]\n _ = c := by rw [one_mul]\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h: a * b = a * c)\n : b = c :=\ncalc b = 1 * b := by simp\n _ = (a\u207b\u00b9 * a) * b := by simp\n _ = a\u207b\u00b9 * (a * b) := by simp\n _ = a\u207b\u00b9 * (a * c) := by simp [h]\n _ = (a\u207b\u00b9 * a) * c := by simp\n _ = 1 * c := by simp\n _ = c := by simp\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h: a * b = a * c)\n : b = c :=\ncalc b = a\u207b\u00b9 * (a * b) := by simp\n _ = a\u207b\u00b9 * (a * c) := by simp [h]\n _ = c := by simp\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h: a * b = a * c)\n : b = c :=\nmul_left_cancel h\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h: a * b = a * c)\n : b = c :=\nby aesop\n\n-- Lemas usados\n-- ============\n\n-- #check (inv_mul_self a : a\u207b\u00b9 * a = 1)\n-- #check (mul_assoc a b c : (a * b) * c = a * (b * c))\n-- #check (mul_left_cancel : a * b = a * c \u2192 b = c)\n-- #check (one_mul a : 1 * a = a)\n<\/pre>\n