Demostrar con Lean4 que si \(G\) un grupo y \(a \u2208 G\), entonces
\n\[(a\u207b\u00b9)\u207b\u00b9 = a\]<\/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 : G}\n\nexample : (a\u207b\u00b9)\u207b\u00b9 = a :=\nsorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Por la siguiente cadena de igualdades
\n\begin{align}
\n (a\u207b\u00b9)\u207b\u00b9 &= (a\u207b\u00b9)\u207b\u00b9\u00b71 &&\text{[porque \(1\) es neutro]} \\
\n &= (a\u207b\u00b9)\u207b\u00b9\u00b7(a\u207b\u00b9\u00b7a) &&\text{[porque \(a\u207b\u00b9\) es el inverso de \(a\)]} \\
\n &= ((a\u207b\u00b9)\u207b\u00b9\u00b7a\u207b\u00b9)\u00b7a &&\text{[por la asociativa]} \\
\n &= 1\u00b7a &&\text{[porque \((a\u207b\u00b9)\u207b\u00b9\) es el inverso de \(a\u207b\u00b9\)]} \\
\n &= a &&\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 : G}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (a\u207b\u00b9)\u207b\u00b9 = a :=\ncalc (a\u207b\u00b9)\u207b\u00b9\n = (a\u207b\u00b9)\u207b\u00b9 * 1 := (mul_one (a\u207b\u00b9)\u207b\u00b9).symm\n _ = (a\u207b\u00b9)\u207b\u00b9 * (a\u207b\u00b9 * a) := congrArg ((a\u207b\u00b9)\u207b\u00b9 * .) (inv_mul_self a).symm\n _ = ((a\u207b\u00b9)\u207b\u00b9 * a\u207b\u00b9) * a := (mul_assoc _ _ _).symm\n _ = 1 * a := congrArg (. * a) (inv_mul_self a\u207b\u00b9)\n _ = a := one_mul a\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (a\u207b\u00b9)\u207b\u00b9 = a :=\ncalc (a\u207b\u00b9)\u207b\u00b9\n = (a\u207b\u00b9)\u207b\u00b9 * 1 := by simp only [mul_one]\n _ = (a\u207b\u00b9)\u207b\u00b9 * (a\u207b\u00b9 * a) := by simp only [inv_mul_self]\n _ = ((a\u207b\u00b9)\u207b\u00b9 * a\u207b\u00b9) * a := by simp only [mul_assoc]\n _ = 1 * a := by simp only [inv_mul_self]\n _ = a := by simp only [one_mul]\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (a\u207b\u00b9)\u207b\u00b9 = a :=\ncalc (a\u207b\u00b9)\u207b\u00b9\n = (a\u207b\u00b9)\u207b\u00b9 * 1 := by simp\n _ = (a\u207b\u00b9)\u207b\u00b9 * (a\u207b\u00b9 * a) := by simp\n _ = ((a\u207b\u00b9)\u207b\u00b9 * a\u207b\u00b9) * a := by simp\n _ = 1 * a := by simp\n _ = a := by simp\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (a\u207b\u00b9)\u207b\u00b9 = a :=\nby\n apply mul_eq_one_iff_inv_eq.mp\n -- \u22a2 a\u207b\u00b9 * a = 1\n exact mul_left_inv a\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (a\u207b\u00b9)\u207b\u00b9 = a :=\nmul_eq_one_iff_inv_eq.mp (mul_left_inv a)\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (a\u207b\u00b9)\u207b\u00b9 = a:=\ninv_inv a\n\n-- 7\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (a\u207b\u00b9)\u207b\u00b9 = a:=\nby simp\n\n-- Lemas usados\n-- ============\n\n-- variable (b c : G)\n-- #check (inv_inv a : (a\u207b\u00b9)\u207b\u00b9 = a)\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_eq_one_iff_inv_eq : a * b = 1 \u2194 a\u207b\u00b9 = b)\n-- #check (mul_left_inv a : a\u207b\u00b9 * a = 1)\n-- #check (mul_one a : a * 1 = a)\n-- #check (one_mul a : 1 * a = a)\n<\/pre>\n