Bump mathlib to v4.25.2

Author: YaelDillies

LeanAPAP/Mathlib/Analysis/Normed/Ring/Basic.lean

@@ -0,0 +1,16 @@
+import Mathlib.Analysis.Normed.Ring.Basic
+
+variable {R : Type*} [SeminormedRing R] {a b c : R}
+
+lemma norm_one_sub_mul (ha : ‖a‖ ≤ 1) : ‖c - a * b‖ ≤ ‖c - a‖ + ‖1 - b‖ := by
+  calc ‖c - a * b‖ = ‖(c - a) + a * (1 - b)‖ := by noncomm_ring
+    _ = ‖c - a‖ + ‖1 - b‖ := by grw [norm_add_le, norm_mul_le, ha, one_mul]
+
+lemma norm_one_sub_mul' (hb : ‖b‖ ≤ 1) : ‖c - a * b‖ ≤ ‖1 - a‖ + ‖c - b‖ :=
+  (norm_one_sub_mul (R := Rᵐᵒᵖ) hb).trans_eq (add_comm _ _)
+
+lemma nnnorm_one_sub_mul (ha : ‖a‖₊ ≤ 1) : ‖c - a * b‖₊ ≤ ‖c - a‖₊ + ‖1 - b‖₊ :=
+  norm_one_sub_mul ha
+
+lemma nnnorm_one_sub_mul' (hb : ‖b‖₊ ≤ 1) : ‖c - a * b‖₊ ≤ ‖1 - a‖₊ + ‖c - b‖₊ :=
+  norm_one_sub_mul' hb

LeanAPAP/Prereqs/Bohr/Basic.lean

@@ -1,6 +1,26 @@
+import LeanAPAP.Mathlib.Analysis.Normed.Ring.Basic
 import Mathlib.Analysis.Complex.Basic
 import Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
 
+lemma norm_one_sub_mul {R : Type*} [SeminormedRing R] {a b c : R} (ha : ‖a‖ ≤ 1) :
+    ‖c - a * b‖ ≤ ‖c - a‖ + ‖1 - b‖ := by
+  calc ‖c - a * b‖ = ‖(c - a) + a * (1 - b)‖ := by noncomm_ring
+    _ = ‖c - a‖ + ‖1 - b‖ := by grw [norm_add_le, norm_mul_le, ha, one_mul]
+
+lemma norm_one_sub_mul' {R : Type*} [SeminormedRing R] {a b c : R} (hb : ‖b‖ ≤ 1) :
+    ‖c - a * b‖ ≤ ‖1 - a‖ + ‖c - b‖ :=
+  (norm_one_sub_mul (R := Rᵐᵒᵖ) hb).trans_eq (add_comm _ _)
+
+lemma nnnorm_one_sub_mul {R : Type*} [SeminormedRing R] {a b c : R} (ha : ‖a‖₊ ≤ 1) :
+    ‖c - a * b‖₊ ≤ ‖c - a‖₊ + ‖1 - b‖₊ :=
+  norm_one_sub_mul ha
+
+lemma nnnorm_one_sub_mul' {R : Type*} [SeminormedRing R] {a b c : R} (hb : ‖b‖₊ ≤ 1) :
+    ‖c - a * b‖₊ ≤ ‖1 - a‖₊ + ‖c - b‖₊ :=
+  norm_one_sub_mul' hb
+
+#min_imports
+
 open AddChar Function
 open scoped NNReal ENNReal Finset
 
@@ -326,26 +346,6 @@ lemma chordSet_monotone : Monotone (chordSet : BohrSet G → Set G) := fun _ _ =
 
 open Pointwise
 
-lemma norm_one_sub_mul {R : Type*} [SeminormedRing R] {a b c : R} (ha : ‖a‖ ≤ 1) :
-    ‖c - a * b‖ ≤ ‖c - a‖ + ‖1 - b‖ := by
-  calc ‖c - a * b‖ = ‖(c - a) + a * (1 - b)‖ := by noncomm_ring
-    _ ≤ ‖c - a‖ + ‖a * (1 - b)‖ := norm_add_le _ _
-    _ ≤ ‖c - a‖ + ‖a‖ * ‖1 - b‖ := add_le_add_left (norm_mul_le _ _) _
-    _ ≤ ‖c - a‖ + 1 * ‖1 - b‖ := by gcongr
-    _ = ‖c - a‖ + ‖1 - b‖ := by simp
-
-lemma norm_one_sub_mul' {R : Type*} [SeminormedRing R] {a b c : R} (hb : ‖b‖ ≤ 1) :
-    ‖c - a * b‖ ≤ ‖1 - a‖ + ‖c - b‖ :=
-  (norm_one_sub_mul (R := Rᵐᵒᵖ) hb).trans_eq (add_comm _ _)
-
-lemma nnnorm_one_sub_mul {R : Type*} [SeminormedRing R] {a b c : R} (ha : ‖a‖₊ ≤ 1) :
-    ‖c - a * b‖₊ ≤ ‖c - a‖₊ + ‖1 - b‖₊ :=
-  norm_one_sub_mul ha
-
-lemma nnnorm_one_sub_mul' {R : Type*} [SeminormedRing R] {a b c : R} (hb : ‖b‖₊ ≤ 1) :
-    ‖c - a * b‖₊ ≤ ‖1 - a‖₊ + ‖c - b‖₊ :=
-  norm_one_sub_mul' hb
-
 lemma add_subset_of_ewidth [Finite G] {B₁ B₂ B₃ : BohrSet G}
     (h : B₁.ewidth + B₂.ewidth ≤ B₃.ewidth) :
     B₁.chordSet + B₂.chordSet ⊆ B₃.chordSet := by

lake-manifest.json

@@ -15,17 +15,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "029db123ddaa7f8fd0d18cea3b1b33bf84dacd1e",
+   "rev": "964995275b0f0d5a93674b90ade7c5a1aea8e936",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.25.0",
+   "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2503bfb5e2d4d8202165f5bd2cc39e44a3be31c3",
+   "rev": "74835c84b38e4070b8240a063c6417c767e551ae",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf",
+   "rev": "3591c3f664ac3719c4c86e4483e21e228707bfa2",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "009064c21bad4d7f421f2901c5e817c8bf3468cb",
+   "rev": "6e3bb4bf31f731ab28891fe229eb347ec7d5dad3",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,17 +55,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fb8ed0a85a96e3176f6e94b20d413ea72d92576d",
+   "rev": "2aaad968dd10a168b644b6a5afd4b92496af4710",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.77",
+   "inputRev": "v0.0.82",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "26e4c7c0e63eb3e6cce3cf7faba27b8526ea8349",
+   "rev": "ea86e311a31a4dfa2abf3d7c0664b8c28499369e",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2781d8ad404303b2fe03710ac7db946ddfe3539f",
+   "rev": "a31845b5557fd5e47d52b9e2977a1b0eff3c38c3",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "39260e31b7b3f7f05643da95242463b462dc05f1",
+   "rev": "c0b0d08446817bd410548d9ea8ddcccf5d89f63f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,10 +95,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "1dae8b12f8ba27576ffe5ddee78bebf6458157b0",
+   "rev": "7e1ced9e049a4fab2508980ec4877ca9c46dffc9",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.25.0",
+   "inputRev": "v4.26.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "LeanAPAP",

lakefile.toml

@@ -39,7 +39,6 @@ linter.style.setOption = true
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.25.0"
 
 [[require]]
 name = "checkdecls"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.25.0
+leanprover/lean4:v4.26.0-rc2