Bump Lean and Mathlib

FLT/ForMathlib/ActionTopology.lean

@@ -216,16 +216,14 @@ theorem iso (e : A ≃L[R] B) : IsActionTopology R B where
     constructor
     · rintro ⟨σ, ⟨hσ1, hσ2⟩, rfl⟩
       refine ⟨?_, ?_⟩
-      · exact @induced_continuous_smul (f := @id R) (hf := continuous_id)
-          (g := g') (τA := σ) _ _ _ _ _
-      · exact @induced_continuous_add (h := h') σ _
+      · exact induced_continuous_smul (f := @id R) (hf := continuous_id) (g := g') (τA := σ)
+      · exact induced_continuous_add (h := h')
     · rintro ⟨h1, h2⟩
       use τ.induced e
       rw [induced_compose]
       refine ⟨⟨?_, ?_⟩, ?_⟩
-      · exact @induced_continuous_smul (f := @id R) (hf := continuous_id)
-          (g := g) (τA := τ) _ _ _ _ _
-      · exact @induced_continuous_add (h := h) τ _
+      · exact induced_continuous_smul (f := @id R) (hf := continuous_id) (g := g) (τA := τ)
+      · exact induced_continuous_add (h := h)
       · nth_rw 2 [← induced_id (t := τ)]
         simp
 
@@ -401,8 +399,8 @@ instance pi : IsActionTopology R (∀ i, A i) := by
   · infer_instance
   · case h_option X _ hind _ _ _ _ =>
     let e : Option X ≃ X ⊕ Unit := Equiv.optionEquivSumPUnit X
-    refine @iso (e := ContinuousLinearEquiv.piCongrLeft R A e.symm) _ _ _ _ _ ?_
-    refine @iso (e := (ContinuousLinearEquiv.sumPiEquivProdPi R X Unit _).symm) _ _ _ _ _ ?_
+    apply @iso (e := ContinuousLinearEquiv.piCongrLeft R A e.symm)
+    apply @iso (e := (ContinuousLinearEquiv.sumPiEquivProdPi R X Unit _).symm)
     refine @prod _ _ _ _ _ _ (_) (hind) _ _ _ (_) (?_)
     let φ : Unit → Option X := fun t ↦ e.symm (Sum.inr t)
     exact iso (ContinuousLinearEquiv.pUnitPiEquiv R (fun t ↦ A (φ t))).symm

FLT/MathlibExperiments/FrobeniusRiou.lean

@@ -750,7 +750,7 @@ theorem algebraic {A : Type*} [CommRing A] {B : Type*} [Nontrivial B] [CommRing
 theorem normal : Normal K L := by
   sorry
 
-open FiniteDimensional
+open Module
 
 theorem separableClosure_finiteDimensional : FiniteDimensional K (separableClosure K L) := sorry
 

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "34e690ec07f6f6375668adba5a16d0d723226c2c",
+   "rev": "daf1ed91789811cf6bbb7bf2f4dad6b3bad8fbf4",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
+   "rev": "2b2f6d7fbe9d917fc010e9054c1ce11774c9088b",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ff420521a0c098891f4f44ecda9dd7ff57b50bad",
+   "rev": "b20a88676fd00affb90cbc9f1ff004ae588103b3",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e285a7ade149c551c17a4b24f127e1ef782e4bb1",
+   "rev": "63a7d4a353f48f6c5f1bc19d0f018b0513cb370a",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "781beceb959c68b36d3d96205b3531e341879d2c",
+   "rev": "4b61d4abc1659f15ffda5ec24fdebc229d51d066",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "81d4159870a16f4ae3253172f5d203bfa004b8e0",
+   "rev": "bc87839ae48935a0ee4540e49e93e32ac671d5b7",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.12.0
+leanprover/lean4:v4.13.0-rc3