Sea G un grupo y a,b,c \u2208 G. Demostrar que si a * b = a* c, entonces b = c.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport algebra.group.basic\n\nuniverse u\nvariables {G : Type u} [group G]\nvariables {a b c : G}\n\nexample\n (h: a * b = a * c)\n : b = c :=\nsorry\n<\/pre>\n[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n
\r\nimport algebra.group.basic\r\n\r\nuniverse u\r\nvariables {G : Type u} [group G]\r\nvariables {a b c : G}\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h: a * b = a * c)\r\n : b = c :=\r\ncalc b = 1 * b : (one_mul b).symm\r\n ... = (a\u207b\u00b9 * a) * b : congr_arg (* b) (inv_mul_self a).symm\r\n ... = a\u207b\u00b9 * (a * b) : mul_assoc a\u207b\u00b9 a b\r\n ... = a\u207b\u00b9 * (a * c) : congr_arg ((*) a\u207b\u00b9) h\r\n ... = (a\u207b\u00b9 * a) * c : (mul_assoc a\u207b\u00b9 a c).symm\r\n ... = 1 * c : congr_arg (* c) (inv_mul_self a)\r\n ... = c : one_mul c\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h: a * b = a * c)\r\n : b = c :=\r\ncalc b = 1 * b : by rw one_mul\r\n ... = (a\u207b\u00b9 * a) * b : by rw inv_mul_self\r\n ... = a\u207b\u00b9 * (a * b) : by rw mul_assoc\r\n ... = a\u207b\u00b9 * (a * c) : by rw h\r\n ... = (a\u207b\u00b9 * a) * c : by rw mul_assoc\r\n ... = 1 * c : by rw inv_mul_self\r\n ... = c : by rw one_mul\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h: a * b = a * c)\r\n : b = c :=\r\ncalc b = 1 * b : by simp\r\n ... = (a\u207b\u00b9 * a) * b : by simp\r\n ... = a\u207b\u00b9 * (a * b) : by simp\r\n ... = a\u207b\u00b9 * (a * c) : by simp [h]\r\n ... = (a\u207b\u00b9 * a) * c : by simp\r\n ... = 1 * c : by simp\r\n ... = c : by simp\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h: a * b = a * c)\r\n : b = c :=\r\ncalc b = a\u207b\u00b9 * (a * b) : by simp\r\n ... = a\u207b\u00b9 * (a * c) : by simp [h]\r\n ... = c : by simp\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h: a * b = a * c)\r\n : b = c :=\r\nbegin\r\n have h1 : a\u207b\u00b9 * (a * b) = a\u207b\u00b9 * (a * c),\r\n { by finish [h] },\r\n have h2 : (a\u207b\u00b9 * a) * b = (a\u207b\u00b9 * a) * c,\r\n { by finish },\r\n have h3 : 1 * b = 1 * c,\r\n { by finish },\r\n have h3 : b = c,\r\n { by finish },\r\n exact h3,\r\nend\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h: a * b = a * c)\r\n : b = c :=\r\nbegin\r\n have : a\u207b\u00b9 * (a * b) = a\u207b\u00b9 * (a * c),\r\n { by finish [h] },\r\n have h2 : (a\u207b\u00b9 * a) * b = (a\u207b\u00b9 * a) * c,\r\n { by finish },\r\n have h3 : 1 * b = 1 * c,\r\n { by finish },\r\n have h3 : b = c,\r\n { by finish },\r\n exact h3,\r\nend\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h: a * b = a * c)\r\n : b = c :=\r\nbegin\r\n have h1 : a\u207b\u00b9 * (a * b) = a\u207b\u00b9 * (a * c),\r\n { congr, exact h, },\r\n have h2 : (a\u207b\u00b9 * a) * b = (a\u207b\u00b9 * a) * c,\r\n { simp only [h1, mul_assoc], },\r\n have h3 : 1 * b = 1 * c,\r\n { simp only [h2, (inv_mul_self a).symm], },\r\n rw one_mul at h3,\r\n rw one_mul at h3,\r\n exact h3,\r\nend\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h: a * b = a * c)\r\n : b = c :=\r\nmul_left_cancel h\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h: a * b = a * c)\r\n : b = c :=\r\nby finish\r\n<\/pre>\n