LeanAgent Proofs

MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean

@@ -177,7 +177,7 @@ TEXT. -/
 -- Prove these:
 -- QUOTE:
 theorem add_neg_cancel_right (a b : R) : a + b + -b = a := by
-  sorry
+  simp
 -- QUOTE.
 
 -- SOLUTIONS:
@@ -189,10 +189,10 @@ Use these to prove the following:
 TEXT. -/
 -- QUOTE:
 theorem add_left_cancel {a b c : R} (h : a + b = a + c) : b = c := by
-  sorry
+  simpa using h
 
 theorem add_right_cancel {a b c : R} (h : a + b = c + b) : a = c := by
-  sorry
+  simpa using h
 -- QUOTE.
 
 -- SOLUTIONS:
@@ -277,7 +277,7 @@ so the following theorem also requires some work.
 TEXT. -/
 -- QUOTE:
 theorem zero_mul (a : R) : 0 * a = 0 := by
-  sorry
+  rw [MulZeroClass.zero_mul]
 -- QUOTE.
 
 -- SOLUTIONS:
@@ -293,17 +293,19 @@ established in this section.
 TEXT. -/
 -- QUOTE:
 theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b := by
-  sorry
+  rw [add_eq_zero_iff_eq_neg] at h
+  simp [h]
 
 theorem eq_neg_of_add_eq_zero {a b : R} (h : a + b = 0) : a = -b := by
-  sorry
+  rw [eq_neg_iff_add_eq_zero]
+  exact h
 
 theorem neg_zero : (-0 : R) = 0 := by
   apply neg_eq_of_add_eq_zero
   rw [add_zero]
 
 theorem neg_neg (a : R) : - -a = a := by
-  sorry
+  simp
 -- QUOTE.
 
 -- SOLUTIONS:
@@ -380,7 +382,7 @@ variable {R : Type*} [Ring R]
 -- EXAMPLES:
 -- QUOTE:
 theorem self_sub (a : R) : a - a = 0 := by
-  sorry
+  simp
 -- QUOTE.
 
 -- SOLUTIONS:
@@ -405,7 +407,8 @@ theorem one_add_one_eq_two : 1 + 1 = (2 : R) := by
 
 -- EXAMPLES:
 theorem two_mul (a : R) : 2 * a = a + a := by
-  sorry
+  rw [← one_add_one_eq_two]
+  simp [add_mul]
 -- QUOTE.
 
 -- SOLUTIONS:
@@ -466,13 +469,13 @@ namespace MyGroup
 -- EXAMPLES:
 -- QUOTE:
 theorem mul_right_inv (a : G) : a * a⁻¹ = 1 := by
-  sorry
+  simp
 
 theorem mul_one (a : G) : a * 1 = a := by
-  sorry
+  simp
 
 theorem mul_inv_rev (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by
-  sorry
+  simp
 -- QUOTE.
 
 -- SOLUTIONS:

MIL/C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean

@@ -240,10 +240,10 @@ using only those axioms:
 TEXT. -/
 -- QUOTE:
 theorem absorb1 : x ⊓ (x ⊔ y) = x := by
-  sorry
+  simp
 
 theorem absorb2 : x ⊔ x ⊓ y = x := by
-  sorry
+  simp
 -- QUOTE.
 
 -- SOLUTIONS:

MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean

@@ -98,8 +98,7 @@ TEXT. -/
 -- QUOTE:
 theorem my_lemma3 :
     ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by
-  intro x y ε epos ele1 xlt ylt
-  sorry
+  apply C03S01.my_lemma
 -- QUOTE.
 
 /- TEXT:
@@ -504,7 +503,7 @@ example : s ⊆ s := by
 theorem Subset.refl : s ⊆ s := fun x xs ↦ xs
 
 theorem Subset.trans : r ⊆ s → s ⊆ t → r ⊆ t := by
-  sorry
+  exact Set.Subset.trans
 -- QUOTE.
 
 -- SOLUTIONS:

MIL/C03_Logic/S04_Conjunction_and_Iff.lean

@@ -243,9 +243,8 @@ We suggest proving an auxiliary lemma using
 ``linarith``, ``pow_two_nonneg``, and ``pow_eq_zero``.
 TEXT. -/
 -- QUOTE:
-theorem aux {x y : ℝ} (h : x ^ 2 + y ^ 2 = 0) : x = 0 :=
-  have h' : x ^ 2 = 0 := by sorry
-  pow_eq_zero h'
+theorem aux {x y : ℝ} (h : x ^ 2 + y ^ 2 = 0) : x = 0 := by
+  nlinarith
 
 example (x y : ℝ) : x ^ 2 + y ^ 2 = 0 ↔ x = 0 ∧ y = 0 :=
   sorry

MIL/C03_Logic/S05_Disjunction.lean

@@ -155,13 +155,14 @@ namespace MyAbs
 
 -- EXAMPLES:
 theorem le_abs_self (x : ℝ) : x ≤ |x| := by
-  sorry
+  rw [le_abs]
+  simp
 
 theorem neg_le_abs_self (x : ℝ) : -x ≤ |x| := by
-  sorry
+  simpa using C03S05.MyAbs.le_abs_self (-x)
 
 theorem abs_add (x y : ℝ) : |x + y| ≤ |x| + |y| := by
-  sorry
+  apply abs_add_le
 -- QUOTE.
 
 -- SOLUTIONS:
@@ -194,7 +195,8 @@ theorem lt_abs : x < |y| ↔ x < y ∨ x < -y := by
   sorry
 
 theorem abs_lt : |x| < y ↔ -y < x ∧ x < y := by
-  sorry
+  cases x
+  exact abs_lt
 -- QUOTE.
 
 -- SOLUTIONS: