Bump Lean+Mathlib

MIL/C02_Basics/S03_Using_Theorems_and_Lemmas.lean

@@ -171,7 +171,7 @@ TEXT. -/
 -- QUOTE:
 #check (exp_le_exp : exp a ≤ exp b ↔ a ≤ b)
 #check (exp_lt_exp : exp a < exp b ↔ a < b)
-#check (log_le_log : 0 < a → 0 < b → (log a ≤ log b ↔ a ≤ b))
+#check (log_le_log : 0 < a → a ≤ b → log a ≤ log b)
 #check (log_lt_log : 0 < a → a < b → log a < log b)
 #check (add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d)
 #check (add_le_add_left : a ≤ b → ∀ c, c + a ≤ c + b)
@@ -188,7 +188,7 @@ TEXT. -/
 -- QUOTE.
 
 /- TEXT:
-Some of the theorems, ``exp_le_exp``, ``exp_lt_exp``, and ``log_le_log``
+Some of the theorems, ``exp_le_exp``, ``exp_lt_exp``
 use a *bi-implication*, which represents the
 phrase "if and only if."
 (You can type it in VS Code with ``\lr`` of ``\iff``).
@@ -240,8 +240,7 @@ example : (0 : ℝ) < 1 := by norm_num
 
 example (h : a ≤ b) : log (1 + exp a) ≤ log (1 + exp b) := by
   have h₀ : 0 < 1 + exp a := by sorry
-  have h₁ : 0 < 1 + exp b := by sorry
-  apply (log_le_log h₀ h₁).mpr
+  apply log_le_log h₀
   sorry
 -- QUOTE.
 
@@ -260,8 +259,7 @@ example (h₀ : d ≤ e) : c + exp (a + d) ≤ c + exp (a + e) := by
 
 example (h : a ≤ b) : log (1 + exp a) ≤ log (1 + exp b) := by
   have h₀ : 0 < 1 + exp a := by linarith [exp_pos a]
-  have h₁ : 0 < 1 + exp b := by linarith [exp_pos b]
-  apply (log_le_log h₀ h₁).mpr
+  apply log_le_log h₀
   apply add_le_add_left (exp_le_exp.mpr h)
 
 -- SOLUTION.

MIL/C10_Differential_Calculus/S02_Differential_Calculus_in_Normed_Spaces.lean

@@ -1,8 +1,8 @@
 import MIL.Common
 import Mathlib.Analysis.NormedSpace.BanachSteinhaus
 import Mathlib.Analysis.NormedSpace.FiniteDimension
-import Mathlib.Analysis.Calculus.Inverse
-import Mathlib.Analysis.Calculus.ContDiff.Basic
+import Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
+import Mathlib.Analysis.Calculus.ContDiff.IsROrC
 import Mathlib.Analysis.Calculus.FDeriv.Prod
 
 
@@ -300,7 +300,7 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCom
 
 example (f : E → F) (f' : E →L[𝕜] F) (x₀ : E) :
     HasFDerivAt f f' x₀ ↔ (fun x ↦ f x - f x₀ - f' (x - x₀)) =o[𝓝 x₀] fun x ↦ x - x₀ :=
-  Iff.rfl
+  hasFDerivAtFilter_iff_isLittleO ..
 
 example (f : E → F) (f' : E →L[𝕜] F) (x₀ : E) (hff' : HasFDerivAt f f' x₀) : fderiv 𝕜 f x₀ = f' :=
   hff'.fderiv

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "9e37a01f8590f81ace095b56710db694b5bf8ca0",
+   "rev": "ee49cf8fada1bf5a15592c399a925c401848227f",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "3141402ba5a5f0372d2378fd75a481bc79a74ecf",
+   "rev": "69404390bdc1de946bf0a2e51b1a69f308e56d7a",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,10 +31,10 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "909febc72b4f64628f8d35cd0554f8a90b6e0749",
+   "rev": "31d41415d5782a196999d4fd8eeaef3cae386a5f",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.23",
+   "inputRev": "v0.0.24",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "19096ec3fc6f290dc088f7f3ffd6318d4a0bd93d",
+   "rev": "623cc31f4dd18f45cd1a9901104271f1ba6328c1",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.4.0-rc1
+leanprover/lean4:v4.5.0-rc1