Demostrar con Lean4 que si ab = cd y e = f, entonces a(be) = c(df)<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\r\nimport Mathlib.Tactic\r\nimport Mathlib.Data.Real.Basic\r\n\r\nexample\r\n (a b c d e f : \u211d)\r\n (h1 : a * b = c * d)\r\n (h2 : e = f)\r\n : a * (b * e) = c * (d * f) :=\r\nby sorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en leguaje natural<\/b><\/p>\n
\nPor la siguiente cadena de igualdades
\n\\begin{align}
\n a(be)
\n &= a(bf) &&\\text{[por la segunda hip\u00f3tesis]} \\\\
\n &= (ab)f &&\\text{[por la asociativa]} \\\\
\n &= (cd)f &&\\text{[por la primera hip\u00f3tesis]} \\\\
\n &= c(df) &&\\text{[por la asociativa]}
\n\\end{align}<\/p>\n
Demostraciones con Lean<\/b><\/p>\n\r\nimport Mathlib.Tactic\r\nimport Mathlib.Data.Real.Basic\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample\r\n (a b c d e f : \u211d)\r\n (h1 : a * b = c * d)\r\n (h2 : e = f)\r\n : a * (b * e) = c * (d * f) :=\r\ncalc\r\n a * (b * e)\r\n = a * (b * f) := by rw [h2]\r\n _ = (a * b) * f := by rw [\u2190mul_assoc]\r\n _ = (c * d) * f := by rw [h1]\r\n _ = c * (d * f) := by rw [mul_assoc]\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample\r\n (a b c d e f : \u211d)\r\n (h1 : a * b = c * d)\r\n (h2 : e = f)\r\n : a * (b * e) = c * (d * f) :=\r\nby\r\n rw [h2]\r\n rw [\u2190mul_assoc]\r\n rw [h1]\r\n rw [mul_assoc]\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample\r\n (a b c d e f : \u211d)\r\n (h1 : a * b = c * d)\r\n (h2 : e = f)\r\n : a * (b * e) = c * (d * f) :=\r\nby\r\n simp [*, \u2190mul_assoc]\r\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n