chore: bump to v4.21.0 (#305)

Author: pitmonticone

MIL/C03_Logic/S04_Conjunction_and_Iff.lean

@@ -342,13 +342,13 @@ variable (a b : α)
 
 -- EXAMPLES:
 example : a < b ↔ a ≤ b ∧ a ≠ b := by
-  rw [lt_iff_le_not_le]
+  rw [lt_iff_le_not_ge]
   sorry
 -- QUOTE.
 
 -- SOLUTIONS:
 example : a < b ↔ a ≤ b ∧ a ≠ b := by
-  rw [lt_iff_le_not_le]
+  rw [lt_iff_le_not_ge]
   constructor
   · rintro ⟨h0, h1⟩
     constructor
@@ -391,22 +391,22 @@ variable (a b c : α)
 
 -- EXAMPLES:
 example : ¬a < a := by
-  rw [lt_iff_le_not_le]
+  rw [lt_iff_le_not_ge]
   sorry
 
 example : a < b → b < c → a < c := by
-  simp only [lt_iff_le_not_le]
+  simp only [lt_iff_le_not_ge]
   sorry
 -- QUOTE.
 
 -- SOLUTIONS:
 example : ¬a < a := by
-  rw [lt_iff_le_not_le]
+  rw [lt_iff_le_not_ge]
   rintro ⟨h0, h1⟩
   exact h1 h0
 
 example : a < b → b < c → a < c := by
-  simp only [lt_iff_le_not_le]
+  simp only [lt_iff_le_not_ge]
   rintro ⟨h0, h1⟩ ⟨h2, h3⟩
   constructor
   · apply le_trans h0 h2

MIL/C13_Integration_and_Measure_Theory/S01_Elementary_Integration.lean

@@ -1,6 +1,5 @@
 import MIL.Common
-import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
-import Mathlib.Analysis.SpecialFunctions.Integrals
+import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
 import Mathlib.Analysis.Convolution
 
 open Set Filter

lake-manifest.json

@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5c0c94b3f563ed756b48b9439788c53b0d56a897",
+   "rev": "308445d7985027f538e281e18df29ca16ede2ba3",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.20.1",
+   "inputRev": "v4.21.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2ac43674e92a695e96caac19f4002b25434636da",
+   "rev": "c4aa78186d388e50a436e8362b947bae125a2933",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a11bcb5238149ae5d8a0aa5e2f8eddf8a3a9b27d",
+   "rev": "d07bd64f1910f1cc5e4cc87b6b9c590080e7a457",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "21e6a0522cd2ae6cf88e9da99a1dd010408ab306",
+   "rev": "6980f6ca164de593cb77cd03d8eac549cc444156",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.60",
+   "inputRev": "v0.0.62",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ddfca7829bf8aa4083cdf9633935dddbb28b7b2a",
+   "rev": "8ff27701d003456fd59f13a9212431239d902aef",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2865ea099ab1dd8d6fc93381d77a4ac87a85527a",
+   "rev": "e9c65db4823976353cd0bb03199a172719efbeb7",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7a0d63fbf8fd350e891868a06d9927efa545ac1e",
+   "rev": "8d2067bf518731a70a255d4a61b5c103922c772e",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "f9e25dcbed001489c53bceeb1f1d50bbaf7451d4",
+   "rev": "7c6aef5f75a43ebbba763b44d535175a1b04c9e0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.toml

@@ -9,7 +9,7 @@ relaxedAutoImplicit = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
-rev = "v4.20.1"
+rev = "v4.21.0"
 
 [[lean_lib]]
 name = "MIL"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.20.1
+leanprover/lean4:v4.21.0