update mathlib

dwrensha · Dec 9, 2023 · 2581bb7 · 2581bb7
1 parent 07c0ae5
commit 2581bb7
Show file tree

Hide file tree

Showing 5 changed files with 9 additions and 10 deletions.
diff --git a/Compfiles/Imo1989P5.lean b/Compfiles/Imo1989P5.lean
@@ -169,7 +169,7 @@ problem imo1989_p5 (n : ℕ) : ∃ m, ∀ j < n, ¬IsPrimePow (m + j) := by
   let ci : List ChinesePair :=
     List.ofFn (fun x : Fin n ↦ have hx0: ↑x < List.length l := by
                                  rw [hll, Nat.two_mul]
-                                 exact Nat.lt_add_right _ n n x.2
+                                 exact Nat.lt_add_right n x.2
                                have hx1: ↑x + n < List.length l := by
                                  rw [hll, Nat.two_mul]
                                  exact Nat.add_lt_add_right x.2 n
@@ -186,7 +186,7 @@ problem imo1989_p5 (n : ℕ) : ∃ m, ∀ j < n, ¬IsPrimePow (m + j) := by
            (hl _ (List.get_mem _ _ _)).1
            (hl _ (List.get_mem _ _ _)).1
      · exact lemma3 l hld (LT.lt.ne hij)
-     · have hijn : i < j + n := Nat.lt_add_right _ _ n hij
+     · have hijn : i < j + n := Nat.lt_add_right n hij
        exact lemma3 l hld (Fin.ne_of_vne (LT.lt.ne hijn))
      · have hijn' := calc j < n := j.prop
                           _ ≤ i + n := Nat.le_add_left _ _
@@ -211,7 +211,7 @@ problem imo1989_p5 (n : ℕ) : ∃ m, ∀ j < n, ¬IsPrimePow (m + j) := by
   have hcil : ci.length = n := by aesop
   have hj1 : j < ci.length := by rwa [hcil]
   have hj2 : j < l.length := by rw [hll, Nat.two_mul]
-                                exact Nat.lt_add_right j n n hj
+                                exact Nat.lt_add_right n hj
   have hj3 : j + n < l.length := by rw [hll, Nat.two_mul]
                                     exact Nat.add_lt_add_right hj n
   have h1 := hm (ci.get ⟨j, hj1⟩) (List.get_mem _ _ _)

diff --git a/Compfiles/Usa1998P3.lean b/Compfiles/Usa1998P3.lean
@@ -121,8 +121,7 @@ lemma lemma2 (f : ℕ → ℝ) :
             · exact Nat.ne_of_gt hx
             · exact Nat.lt.base (n + 1)
           · obtain ⟨hy1, hy2⟩ := hy
-            use hy1
-            exact Nat.lt_add_right y (Nat.succ n) 1 hy2
+            exact ⟨hy1, Nat.lt_add_right 1 hy2⟩
       rw [h7, Finset.prod_insert h7']
       ring
     rw [h3]

diff --git a/Compfiles/Usa2022P4.lean b/Compfiles/Usa2022P4.lean
@@ -67,7 +67,7 @@ problem usa2022_p4 (p q : ℕ) :
               a^2 + q = p := ha
               _ < p * q := h2
               _ = b^2 + q := hb.symm
-    have h4 : a^2 < b^2 := (Nat.add_lt_add_iff_right q (a ^ 2) (b ^ 2)).mp h3
+    have h4 : a^2 < b^2 := Nat.add_lt_add_iff_right.mp h3
     exact lt_of_pow_lt_pow' 2 h4
   have hba' : 0 < b - a := Nat.sub_pos_of_lt hba
 

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "baf6defee1fe881ae535519c0776f37f6ef08603",
+   "rev": "dbb4045860667f0d09669dbfb524b6e7b0ca3aca",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,10 +49,10 @@
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "62d6feffc19793121b8a8cf373cd86be552e941e",
+   "rev": "8fe6d2da03600766a6037b326e18901334ccc4d4",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "62d6feffc19793121b8a8cf373cd86be552e941e",
+   "inputRev": "8fe6d2da03600766a6037b326e18901334ccc4d4",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "compfiles",

diff --git a/lakefile.lean b/lakefile.lean
@@ -25,4 +25,4 @@ lean_exe checkSolution where
   root := `scripts.checkSolution
   supportInterpreter := true
 
-require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "62d6feffc19793121b8a8cf373cd86be552e941e"
+require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "8fe6d2da03600766a6037b326e18901334ccc4d4"