Update Sun Sep 8 01:18:07 EDT 2024

PolyrithTutorial/03_Nonsingularity_of_Curves/02ProjectiveCurves.lean

@@ -31,7 +31,7 @@ example {x y z : K} (h : MvPolynomial.eval ![x, y, z] (klein K) = 0)
   have h₀ := hdz 0
   have h₁ := hdz 1
   have h₂ := hdz 2
-  simp at h h₀ h₁ h₂
+  simp [map_ofNat] at h h₀ h₁ h₂
   ext i
   fin_cases i <;> dsimp
   · polyrith
@@ -50,7 +50,6 @@ projective hypersurface in Kℙ². -/
 abbrev weierstrass : MvPolynomial (Fin 3) K :=
   -X 2 * X 1 ^ 2 + X 0 ^ 3 + C p * X 0 * X 2 ^ 2 + C q * X 2 ^ 3
 
-set_option maxHeartbeats 500000 in
 /-- A Weierstrass-form elliptic curve with nonzero discriminant `27 * q ^ 2 + 4 * p ^ 3` is
 nonsingular. -/
 example {x y z : K} (disc : 27 * q ^ 2 + 4 * p ^ 3 ≠ 0)
@@ -60,7 +59,7 @@ example {x y z : K} (disc : 27 * q ^ 2 + 4 * p ^ 3 ≠ 0)
   have h₀ := hdz 0
   have h₁ := hdz 1
   have h₂ := hdz 2
-  simp at h h₀ h₁ h₂
+  simp [map_ofNat] at h h₀ h₁ h₂
   ext i
   fin_cases i <;> dsimp
   · sorry

PolyrithTutorial/03_Nonsingularity_of_Curves/solutions/Solutions02ProjectiveCurves.lean

@@ -29,7 +29,7 @@ example {x y z : K} (h : MvPolynomial.eval ![x, y, z] (klein K) = 0)
   have h₀ := hdz 0
   have h₁ := hdz 1
   have h₂ := hdz 2
-  simp at h h₀ h₁ h₂
+  simp [map_ofNat] at h h₀ h₁ h₂
   ext i
   fin_cases i <;> dsimp
   · linear_combination (exp := 6)
@@ -51,7 +51,6 @@ projective hypersurface in Kℙ². -/
 abbrev weierstrass : MvPolynomial (Fin 3) K :=
   -X 2 * X 1 ^ 2 + X 0 ^ 3 + C p * X 0 * X 2 ^ 2 + C q * X 2 ^ 3
 
-set_option maxHeartbeats 500000 in
 /-- A Weierstrass-form elliptic curve with nonzero discriminant `27 * q ^ 2 + 4 * p ^ 3` is
 nonsingular. -/
 example {x y z : K} (disc : 27 * q ^ 2 + 4 * p ^ 3 ≠ 0)
@@ -61,7 +60,7 @@ example {x y z : K} (disc : 27 * q ^ 2 + 4 * p ^ 3 ≠ 0)
   have h₀ := hdz 0
   have h₁ := hdz 1
   have h₂ := hdz 2
-  simp at h h₀ h₁ h₂
+  simp [map_ofNat] at h h₀ h₁ h₂
   ext i
   fin_cases i <;> dsimp
   all_goals apply mul_left_cancel₀ disc

PolyrithTutorial/04_Combining_Tactics/02Sphere.lean

@@ -4,7 +4,7 @@ Adapted from mathlib, released under Apache 2.0 license as described in that rep
 Authors: Heather Macbeth
 -/
 import Mathlib.Data.Real.Basic
-import Mathlib.GroupTheory.GroupAction.Prod
+import Mathlib.Algebra.Group.Action.Prod
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.Polyrith
 

PolyrithTutorial/04_Combining_Tactics/solutions/Solutions02Sphere.lean

@@ -4,7 +4,7 @@ Adapted from mathlib, released under Apache 2.0 license as described in that rep
 Authors: Heather Macbeth
 -/
 import Mathlib.Data.Real.Basic
-import Mathlib.GroupTheory.GroupAction.Prod
+import Mathlib.Algebra.Group.Action.Prod
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.Polyrith
 

html/02_Using_Polyrith.html

@@ -141,7 +141,7 @@
 above proof, and state them in Lean with those input values.  See the broken proof below for the
 basic idea.</p>
 <p>There is one subtlety. It will happen that the same natural number appears as the index of the
-sequence <cite>T</cite>, but in more than one way.  For example, in the setup below, both <code class="docutils literal notranslate"><span class="pre">k</span> <span class="pre">*</span> <span class="pre">37</span></code> and
+sequence <code class="docutils literal notranslate"><span class="pre">T</span></code>, but in more than one way.  For example, in the setup below, both <code class="docutils literal notranslate"><span class="pre">k</span> <span class="pre">*</span> <span class="pre">37</span></code> and
 <code class="docutils literal notranslate"><span class="pre">37</span> <span class="pre">*</span> <span class="pre">k</span></code> appear as indices.  This prevents <code class="docutils literal notranslate"><span class="pre">polyrith</span></code> from parsing <code class="docutils literal notranslate"><span class="pre">T</span> <span class="pre">(k</span> <span class="pre">*</span> <span class="pre">37)</span></code> and
 <code class="docutils literal notranslate"><span class="pre">T</span> <span class="pre">(37</span> <span class="pre">*</span> <span class="pre">k)</span></code> as the same token.  So, before running <code class="docutils literal notranslate"><span class="pre">polyrith</span></code>, normalize all indices by
 running <code class="docutils literal notranslate"><span class="pre">ring_nf</span></code> (&#8220;ring normal form&#8221;) simultaneously on all the hypotheses you care about and on

html/03_Nonsingularity_of_Curves.html

@@ -217,7 +217,7 @@
 <span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">h&#8320;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">hdz</span><span class="w"> </span><span class="mi">0</span>
 <span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">h&#8321;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">hdz</span><span class="w"> </span><span class="mi">1</span>
 <span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">h&#8322;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">hdz</span><span class="w"> </span><span class="mi">2</span>
-<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="n">h&#8320;</span><span class="w"> </span><span class="n">h&#8321;</span><span class="w"> </span><span class="n">h&#8322;</span>
+<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">map_ofNat</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="n">h&#8320;</span><span class="w"> </span><span class="n">h&#8321;</span><span class="w"> </span><span class="n">h&#8322;</span>
 <span class="w">  </span><span class="n">ext</span><span class="w"> </span><span class="n">i</span>
 <span class="w">  </span><span class="n">fin_cases</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">dsimp</span>
 <span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">polyrith</span>
@@ -267,8 +267,7 @@
 If you like, you can get shorter <code class="docutils literal notranslate"><span class="pre">polyrith</span></code> certificates at the cost of more setup.
 The polynomials <span class="math notranslate nohighlight">\((27q^2+4p^3)x^4\)</span>, <span class="math notranslate nohighlight">\((27q^2+4p^3)y^3\)</span> and <span class="math notranslate nohighlight">\((27q^2+4p^3)z^5\)</span> are all in the ideal as well,
 and you can reduce the problem to these three goals by some initial work with the lemmas <code class="docutils literal notranslate"><span class="pre">pow_eq_zero</span></code> and <code class="docutils literal notranslate"><span class="pre">mul_left_cancel&#8320;</span></code>.</p>
-<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">set_option</span><span class="w"> </span><span class="n">maxHeartbeats</span><span class="w"> </span><span class="mi">500000</span><span class="w"> </span><span class="k">in</span>
-<span class="sd">/-- A Weierstrass-form elliptic curve with nonzero discriminant `27 * q ^ 2 + 4 * p ^ 3` is</span>
+<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="sd">/-- A Weierstrass-form elliptic curve with nonzero discriminant `27 * q ^ 2 + 4 * p ^ 3` is</span>
 <span class="sd">nonsingular. -/</span>
 <span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">K</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">disc</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">27</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">q</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span>
 <span class="w">    </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MvPolynomial.eval</span><span class="w"> </span><span class="bp">!</span><span class="o">[</span><span class="n">x</span><span class="o">,</span><span class="w"> </span><span class="n">y</span><span class="o">,</span><span class="w"> </span><span class="n">z</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">weierstrass</span><span class="w"> </span><span class="n">K</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="n">q</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span>
@@ -277,7 +276,7 @@
 <span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">h&#8320;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">hdz</span><span class="w"> </span><span class="mi">0</span>
 <span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">h&#8321;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">hdz</span><span class="w"> </span><span class="mi">1</span>
 <span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">h&#8322;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">hdz</span><span class="w"> </span><span class="mi">2</span>
-<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="n">h&#8320;</span><span class="w"> </span><span class="n">h&#8321;</span><span class="w"> </span><span class="n">h&#8322;</span>
+<span class="w">  </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="n">map_ofNat</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="n">h&#8320;</span><span class="w"> </span><span class="n">h&#8321;</span><span class="w"> </span><span class="n">h&#8322;</span>
 <span class="w">  </span><span class="n">ext</span><span class="w"> </span><span class="n">i</span>
 <span class="w">  </span><span class="n">fin_cases</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&lt;;&gt;</span><span class="w"> </span><span class="n">dsimp</span>
 <span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="gr">sorry</span>

lake-manifest.json

@@ -1,10 +1,11 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "60d622c124cebcecc000853cdae93f4251f4beb5",
+   "scope": "leanprover-community",
+   "rev": "9c6c2d647e57b2b7a0b42dd8080c698bd33a1b6f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +14,8 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6",
+   "scope": "leanprover-community",
+   "rev": "9d0bdd07bdfe53383567509348b1fe917fc08de4",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +24,8 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "bbb5ab510fd407350094422ee230c15ab7323769",
+   "scope": "leanprover-community",
+   "rev": "deb279eb7be16848d0bc8387f80d6e41bcdbe738",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,25 +34,28 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
+   "scope": "leanprover-community",
+   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.36",
+   "inputRev": "v0.0.41",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
+   "scope": "",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph.git",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "b167323652ab59a5d1b91e906ca4172d1c0474b7",
+   "scope": "leanprover-community",
+   "rev": "1ef0b288623337cb37edd1222b9c26b4b77c6620",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,10 +64,11 @@
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "8932a3d688d2bbf500429c4c888de4181086aad5",
+   "scope": "",
+   "rev": "20c73142afa995ac9c8fb80a9bb585a55ca38308",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "8932a3d688d2bbf500429c4c888de4181086aad5",
+   "inputRev": "v4.11.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "«polyrith-tutorial»",

lakefile.lean

@@ -11,4 +11,4 @@ lean_lib PolyrithTutorial {
   -- add library configuration options here
 }
 
-require mathlib from git "https://github.com/leanprover-community/mathlib4" @ s!"8932a3d688d2bbf500429c4c888de4181086aad5"
+require mathlib from git "https://github.com/leanprover-community/mathlib4" @ s!"v{Lean.versionString}"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.8.0-rc2
+leanprover/lean4:v4.11.0