Update Sun Dec 24 18:33:26 EST 2023

Math2001/02_Proofs_with_Structure/02_Invoking_Lemmas.lean

@@ -28,5 +28,5 @@ example {a b : ℝ} (h1 : a ^ 2 + b ^ 2 = 0) : a ^ 2 = 0 := by
 example {m : ℤ} (hm : m + 1 = 5) : 3 * m ≠ 6 := by
   sorry
 
-theorem problem2 {s : ℚ} (h1 : 3 * s ≤ -6) (h2 : 2 * s ≥ -4) : s = -2 := by
+example {s : ℚ} (h1 : 3 * s ≤ -6) (h2 : 2 * s ≥ -4) : s = -2 := by
   sorry

Math2001/03_Parity_and_Divisibility/04_Modular_Arithmetic_Calculations.lean

@@ -48,7 +48,7 @@ example {x : ℤ} : x ^ 3 ≡ x [ZMOD 3] := by
 example {n : ℤ} (hn : n ≡ 1 [ZMOD 3]) : n ^ 3 + 7 * n ≡ 2 [ZMOD 3] :=
   sorry
 
-theorem problem4 {a : ℤ} (ha : a ≡ 3 [ZMOD 4]) :
+example {a : ℤ} (ha : a ≡ 3 [ZMOD 4]) :
     a ^ 3 + 4 * a ^ 2 + 2 ≡ 1 [ZMOD 4] :=
   sorry
 
@@ -58,7 +58,7 @@ example (a b : ℤ) : (a + b) ^ 3 ≡ a ^ 3 + b ^ 3 [ZMOD 3] :=
 example : ∃ a : ℤ, 4 * a ≡ 1 [ZMOD 7] := by
   sorry
 
-theorem problem5 : ∃ k : ℤ, 5 * k ≡ 6 [ZMOD 8] := by
+example : ∃ k : ℤ, 5 * k ≡ 6 [ZMOD 8] := by
   sorry
 
 example (n : ℤ) : 5 * n ^ 2 + 3 * n + 7 ≡ 1 [ZMOD 2] := by

Math2001/04_Proofs_with_Structure_II/01_Forall_Implies.lean

@@ -86,7 +86,7 @@ example {n : ℤ} (hn : ∀ m, 1 ≤ m → m ≤ 5 → m ∣ n) : 15 ∣ n := by
 example : ∃ n : ℕ, ∀ m : ℕ, n ≤ m := by
   sorry
 
-theorem problem1 : ∃ a : ℝ, ∀ b : ℝ, ∃ c : ℝ, a + b < c := by
+example : ∃ a : ℝ, ∀ b : ℝ, ∃ c : ℝ, a + b < c := by
   sorry
 
 example : forall_sufficiently_large x : ℝ, x ^ 3 + 3 * x ≥ 7 * x ^ 2 + 12 := by

Math2001/04_Proofs_with_Structure_II/05_Proof_by_Contradiction.lean

@@ -135,7 +135,7 @@ example : Prime 79 := by
 /-! # Exercises -/
 
 
-theorem problem3 : ¬ (∃ t : ℝ, t ≤ 4 ∧ t ≥ 5) := by
+example : ¬ (∃ t : ℝ, t ≤ 4 ∧ t ≥ 5) := by
   sorry
 
 example : ¬ (∃ a : ℝ, a ^ 2 ≤ 8 ∧ a ^ 3 ≥ 30) := by

Math2001/Homework/hw0.lean

@@ -5,7 +5,11 @@ import AutograderLib
 
 attribute [-instance] Int.instDivInt_1 Int.instDivInt Nat.instDivNat
 
-/-! # Homework 0 -/
+/-! # Homework 0
+
+Don't forget to compare with the text version,
+https://hrmacbeth.github.io/math2001/Homework.html#homework-0
+for clearer statements and any special instructions. -/
 
 
 @[autograded 5]

Math2001/Homework/hw1.lean

@@ -5,7 +5,11 @@ import AutograderLib
 
 attribute [-instance] Int.instDivInt_1 Int.instDivInt Nat.instDivNat
 
-/-! # Homework 1 -/
+/-! # Homework 1
+
+Don't forget to compare with the text version,
+https://hrmacbeth.github.io/math2001/Homework.html#homework-1
+for clearer statements and any special instructions. -/
 
 
 @[autograded 5]

Math2001/Homework/hw2.lean

@@ -5,7 +5,11 @@ import AutograderLib
 
 attribute [-instance] Int.instDivInt_1 Int.instDivInt Nat.instDivNat
 
-/-! # Homework 2 -/
+/-! # Homework 2
+
+Don't forget to compare with the text version,
+https://hrmacbeth.github.io/math2001/Homework.html#homework-2
+for clearer statements and any special instructions. -/
 
 
 @[autograded 4]

html/02_Proofs_with_Structure.html

@@ -699,7 +699,7 @@ <h3><span class="section-number">2.2.4. </span>Exercises<a class="headerlink" hr
 <span class="math notranslate nohighlight">\(2s \ge -4\)</span>. Show that <span class="math notranslate nohighlight">\(s=-2\)</span>.</p>
 <p>You will probably use the lemma <code class="docutils literal notranslate"><span class="pre">le_antisymm</span></code>, stating if <span class="math notranslate nohighlight">\(x\le y\)</span> and
 <span class="math notranslate nohighlight">\(x\ge y\)</span> then <span class="math notranslate nohighlight">\(x = y\)</span>.</p>
-<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">problem2</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">&#8474;</span><span class="o">}</span> <span class="o">(</span><span class="n">h1</span> <span class="o">:</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">s</span> <span class="bp">&#8804;</span> <span class="bp">-</span><span class="mi">6</span><span class="o">)</span> <span class="o">(</span><span class="n">h2</span> <span class="o">:</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">s</span> <span class="bp">&#8805;</span> <span class="bp">-</span><span class="mi">4</span><span class="o">)</span> <span class="o">:</span> <span class="n">s</span> <span class="bp">=</span> <span class="bp">-</span><span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span>
+<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">s</span> <span class="o">:</span> <span class="n">&#8474;</span><span class="o">}</span> <span class="o">(</span><span class="n">h1</span> <span class="o">:</span> <span class="mi">3</span> <span class="bp">*</span> <span class="n">s</span> <span class="bp">&#8804;</span> <span class="bp">-</span><span class="mi">6</span><span class="o">)</span> <span class="o">(</span><span class="n">h2</span> <span class="o">:</span> <span class="mi">2</span> <span class="bp">*</span> <span class="n">s</span> <span class="bp">&#8805;</span> <span class="bp">-</span><span class="mi">4</span><span class="o">)</span> <span class="o">:</span> <span class="n">s</span> <span class="bp">=</span> <span class="bp">-</span><span class="mi">2</span> <span class="o">:=</span> <span class="kd">by</span>
   <span class="gr">sorry</span>
 </pre></div>
 </div>

html/03_Parity_and_Divisibility.html

@@ -1263,7 +1263,7 @@ <h3><span class="section-number">3.4.5. </span>Exercises<a class="headerlink" hr
 </li>
 <li><p>Let <span class="math notranslate nohighlight">\(a\)</span> be an integer for which <span class="math notranslate nohighlight">\(a\equiv 3\mod 4\)</span>.
 Show that <span class="math notranslate nohighlight">\(a^3+4a^2+2\equiv 1\mod 4\)</span>.</p>
-<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">problem4</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">ha</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="mi">3</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">4</span><span class="o">])</span> <span class="o">:</span>
+<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">{</span><span class="n">a</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">}</span> <span class="o">(</span><span class="n">ha</span> <span class="o">:</span> <span class="n">a</span> <span class="bp">&#8801;</span> <span class="mi">3</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">4</span><span class="o">])</span> <span class="o">:</span>
     <span class="n">a</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">+</span> <span class="mi">4</span> <span class="bp">*</span> <span class="n">a</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">+</span> <span class="mi">2</span> <span class="bp">&#8801;</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">4</span><span class="o">]</span> <span class="o">:=</span>
   <span class="gr">sorry</span>
 </pre></div>
@@ -1282,7 +1282,7 @@ <h3><span class="section-number">3.4.5. </span>Exercises<a class="headerlink" hr
 </div>
 </li>
 <li><p>Show that there exists an integer <span class="math notranslate nohighlight">\(k\)</span>, such that <span class="math notranslate nohighlight">\(5k\equiv 6\mod 8\)</span>.</p>
-<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">problem5</span> <span class="o">:</span> <span class="bp">&#8707;</span> <span class="n">k</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">,</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">k</span> <span class="bp">&#8801;</span> <span class="mi">6</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">8</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
+<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#8707;</span> <span class="n">k</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">,</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">k</span> <span class="bp">&#8801;</span> <span class="mi">6</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">8</span><span class="o">]</span> <span class="o">:=</span> <span class="kd">by</span>
   <span class="gr">sorry</span>
 </pre></div>
 </div>

html/04_Proofs_with_Structure_II.html

@@ -511,7 +511,7 @@ <h3><span class="section-number">4.1.10. </span>Exercises<a class="headerlink" h
 </li>
 <li><p>Show that there exists a real number <span class="math notranslate nohighlight">\(a\)</span>, such that for all real numbers <span class="math notranslate nohighlight">\(b\)</span>, there
 exists a real number <span class="math notranslate nohighlight">\(c\)</span>, such that <span class="math notranslate nohighlight">\(a + b &lt; c\)</span>.</p>
-<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">problem1</span> <span class="o">:</span> <span class="bp">&#8707;</span> <span class="n">a</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">,</span> <span class="bp">&#8704;</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">,</span> <span class="bp">&#8707;</span> <span class="n">c</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">,</span> <span class="n">a</span> <span class="bp">+</span> <span class="n">b</span> <span class="bp">&lt;</span> <span class="n">c</span> <span class="o">:=</span> <span class="kd">by</span>
+<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#8707;</span> <span class="n">a</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">,</span> <span class="bp">&#8704;</span> <span class="n">b</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">,</span> <span class="bp">&#8707;</span> <span class="n">c</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">,</span> <span class="n">a</span> <span class="bp">+</span> <span class="n">b</span> <span class="bp">&lt;</span> <span class="n">c</span> <span class="o">:=</span> <span class="kd">by</span>
   <span class="gr">sorry</span>
 </pre></div>
 </div>
@@ -1795,7 +1795,7 @@ <h3><span class="section-number">4.5.10. </span>Exercises<a class="headerlink" h
 <ol class="arabic">
 <li><p>Show that there does not exist a real number <span class="math notranslate nohighlight">\(t\)</span>, such that <span class="math notranslate nohighlight">\(t \le 4\)</span> and
 <span class="math notranslate nohighlight">\(t\geq 5\)</span>.</p>
-<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span> <span class="n">problem3</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="o">(</span><span class="bp">&#8707;</span> <span class="n">t</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">,</span> <span class="n">t</span> <span class="bp">&#8804;</span> <span class="mi">4</span> <span class="bp">&#8743;</span> <span class="n">t</span> <span class="bp">&#8805;</span> <span class="mi">5</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
+<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="o">(</span><span class="bp">&#8707;</span> <span class="n">t</span> <span class="o">:</span> <span class="n">&#8477;</span><span class="o">,</span> <span class="n">t</span> <span class="bp">&#8804;</span> <span class="mi">4</span> <span class="bp">&#8743;</span> <span class="n">t</span> <span class="bp">&#8805;</span> <span class="mi">5</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
   <span class="gr">sorry</span>
 </pre></div>
 </div>