From f1f911168c1b0bd76a53c2f2652c4d6a2440d747 Mon Sep 17 00:00:00 2001 From: dan Date: Sat, 1 Feb 2025 23:32:38 +0000 Subject: [PATCH] Add missing theorems and solutions to C02 S01 --- MIL/C02_Basics/S01_Calculating.lean | 32 +++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/MIL/C02_Basics/S01_Calculating.lean b/MIL/C02_Basics/S01_Calculating.lean index 37a4d092..f6b188fc 100644 --- a/MIL/C02_Basics/S01_Calculating.lean +++ b/MIL/C02_Basics/S01_Calculating.lean @@ -351,12 +351,44 @@ example (a b : ℝ) : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by #check mul_sub a b c #check add_mul a b c #check add_sub a b c +#check sub_add a b c +#check sub_self a #check sub_sub a b c #check add_zero a -- QUOTE. end +-- SOLUTIONS: + +section +variable (a b c d : ℝ) + +example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := by + rw [mul_add] + rw [add_mul, add_mul, ← add_assoc] + rw [add_assoc (a * c)] + rw [add_assoc (a * c) (a * d), add_comm (a * d)] + +example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := + calc + (a + b) * (c + d) = (a + b) * c + (a + b) * d := by + rw [mul_add] + _ = a * c + b * c + a * d + b * d := by + rw [add_mul, add_mul, ← add_assoc] + _ = a * c + (b * c + a * d) + b * d := by + rw [add_assoc (a * c)] + _ = a * c + a * d + b * c + b * d := by + rw [add_assoc (a * c) (a * d), add_comm (a * d)] + +example (a b : ℝ) : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by + rw [pow_two, pow_two] + rw [add_mul, mul_sub, mul_sub, add_sub] + rw [mul_comm b] + rw [sub_add, sub_self, sub_sub, add_comm, add_zero] + +end + /- TEXT: .. index:: rw, tactics ; rw and rewrite