Bump Lean+Mathlib

SphereEversion/Global/OneJetBundle.lean

@@ -249,8 +249,6 @@ theorem oneJetBundle_chart_source (x₀ : J¹MM') :
   rwa [Trivialization.coe_fst]
   rwa [trivializationAt_oneJetBundle_source, mem_preimage, ← Set.prod_eq]
 
-attribute [pp_dot] PartialEquiv.target PartialEquiv.symm PartialEquiv.prod
-
 section
 
 section
@@ -296,8 +294,6 @@ lemma ContMDiffMap.snd_apply (x : M) (x' : M') :
 
 end
 
-attribute [pp_dot] PartialHomeomorph.symm
-
 /-- In `J¹(M, M')`, the target of a chart has a nice formula -/
 theorem oneJetBundle_chart_target (x₀ : J¹MM') :
     (chartAt HJ x₀).target = Prod.fst ⁻¹' (chartAt (ModelProd H H') x₀.proj).target := by
@@ -354,8 +350,6 @@ theorem oneJetBundle_mk_snd {x : M} {y : M'} {f : OneJetSpace I I' (x, y)} :
     (OneJetBundle.mk x y f).2 = f :=
   rfl
 
-attribute [pp_dot] ModelWithCorners.prod
-
 theorem smoothAt_oneJetBundle {f : N → J¹MM'} {x₀ : N} :
     SmoothAt J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) f x₀ ↔
       SmoothAt J I (fun x ↦ (f x).1.1) x₀ ∧
@@ -440,7 +434,6 @@ theorem Smooth.oneJet_comp {f1 : N' → M} (f2 : N' → M') {f3 : N' → N}
 
 variable {I'}
 
-attribute [pp_dot] ContinuousLinearMap.comp
 open Trivialization in
 theorem Smooth.oneJet_add {f : N → M} {g : N → M'} {ϕ ϕ' : ∀ x : N, OneJetSpace I I' (f x, g x)}
     (hϕ : Smooth J ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) fun x ↦ OneJetBundle.mk _ _ (ϕ x))

SphereEversion/Global/OneJetSec.lean

@@ -49,8 +49,6 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
   ϕ : ∀ x : M, TangentSpace I x →L[𝕜] TangentSpace I' (bs x)
   smooth' : Smooth I ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) fun x ↦ OneJetBundle.mk x (bs x) (ϕ x)
 
-attribute [pp_dot] OneJetSec.bs OneJetSec.ϕ
-
 instance : FunLike (OneJetSec I M I' M') M (OneJetBundle I M I' M') where
   coe := fun S x ↦ OneJetBundle.mk x (S.bs x) (S.ϕ x)
   coe_injective' := by

SphereEversion/Global/Relation.lean

@@ -172,7 +172,6 @@ instance (x : M) (x' : M') :
   assumption
 
 /-- The slice `R(σ,p)`. -/
-@[pp_dot]
 def RelMfld.slice (R : RelMfld I M I' M') (σ : OneJetBundle I M I' M') (p : DualPair <| TM σ.1.1) :
     Set (TM' σ.1.2) :=
   {w : TM' σ.1.2 | OneJetBundle.mk σ.1.1 σ.1.2 (p.update σ.2 w) ∈ R}
@@ -464,7 +463,7 @@ variable {EX : Type*} [NormedAddCommGroup EX] [NormedSpace ℝ EX]
 
 /-- Transfer map between one jet bundles induced by open smooth embedding into the source and
 targets. -/
-@[simps! proj_fst proj_snd, pp_dot]
+@[simps! proj_fst proj_snd]
 def OpenSmoothEmbedding.transfer : OneJetBundle IX X IY Y → OneJetBundle IM M IN N :=
   OneJetBundle.map IY IN φ ψ fun x ↦ (φ.fderiv x).symm
 
@@ -484,8 +483,6 @@ theorem OpenSmoothEmbedding.smooth_transfer :
 theorem OneJetBundle.continuous_transfer : Continuous (φ.transfer ψ) :=
   (OpenSmoothEmbedding.smooth_transfer _ _).continuous
 
-attribute [pp_dot] ContinuousLinearEquiv.symm
-
 theorem OpenSmoothEmbedding.range_transfer :
     range (φ.transfer ψ) = π _ (OneJetSpace IM IN) ⁻¹' range φ ×ˢ range ψ := by
   ext σ; constructor
@@ -608,7 +605,7 @@ theorem isHolonomicAt_localize_iff (hF : range (F.bs ∘ φ) ⊆ range ψ) (x :
 /-! ## From embeddings `X ↪ M` and `Y ↪ N` to `J¹(X, Y) ↪ J¹(M, N)` -/
 
 -- very slow to elaborate :-(
-@[simps, pp_dot]
+@[simps]
 def OneJetBundle.embedding : OpenSmoothEmbedding IXY J¹XY IMN J¹MN where
   toFun := φ.transfer ψ
   invFun :=
@@ -714,7 +711,6 @@ theorem Jupdate_localize {F : OneJetSec IM M IN N} {G : HtpyOneJetSec IX X IY Y}
     simp_rw [ContinuousLinearEquiv.symm_apply_apply]
 
 /-- Update a global formal solutions `F` using a homotopy of local ones `G`. -/
-@[pp_dot]
 def updateFormalSol (F : FormalSol R) (G : HtpyFormalSol (R.localize φ ψ)) (hK : IsCompact K)
     (hFG : ∀ t, ∀ x ∉ K, F (φ x) = (OneJetBundle.embedding φ ψ) (G t x)) : HtpyFormalSol R
     where

SphereEversion/Global/SmoothEmbedding.lean

@@ -36,8 +36,6 @@ attribute [coe] OpenSmoothEmbedding.toFun
 instance : CoeFun (OpenSmoothEmbedding I M I' M') fun _ ↦ M → M' :=
   ⟨OpenSmoothEmbedding.toFun⟩
 
-attribute [pp_dot] OpenSmoothEmbedding.invFun
-
 namespace OpenSmoothEmbedding
 
 variable {I I' M M'}
@@ -83,7 +81,7 @@ theorem coe_comp_invFun_eventuallyEq (x : M) : f ∘ f.invFun =ᶠ[𝓝 (f x)] i
 
 /- Note that we are slightly abusing the fact that `TangentSpace I x` and
 `TangentSpace I (f.invFun (f x))` are both definitionally `E` below. -/
-@[pp_dot] def fderiv (x : M) : TangentSpace I x ≃L[𝕜] TangentSpace I' (f x) :=
+def fderiv (x : M) : TangentSpace I x ≃L[𝕜] TangentSpace I' (f x) :=
   have h₁ : MDifferentiableAt I' I f.invFun (f x) :=
     ((f.smooth_inv (f x) (mem_range_self x)).mdifferentiableWithinAt le_top).mdifferentiableAt
       (f.isOpenMap.range_mem_nhds x)
@@ -386,7 +384,6 @@ section
 attribute [local instance] Classical.dec
 
 /-- This is definition `def:update` in the blueprint. -/
-@[pp_dot]
 def update (m : M) : N :=
   if m ∈ range φ then ψ (g (φ.invFun m)) else f m
 

SphereEversion/Local/DualPair.lean

@@ -78,7 +78,6 @@ theorem mem_spanV (p : DualPair E) {u : E} : u ∈ p.spanV ↔ ∃ t : ℝ, u =
 
 /-- Update a continuous linear map `φ : E →L[ℝ] F` using a dual pair `p` on `E` and a
 vector `w : F`. The new map coincides with `φ` on `ker p.π` and sends `p.v` to `w`. -/
-@[pp_dot]
 def update (p : DualPair E) (φ : E →L[ℝ] F) (w : F) : E →L[ℝ] F :=
   φ + (w - φ p.v) ⬝ p.π
 
@@ -131,7 +130,7 @@ theorem update_apply (p : DualPair E) (φ : E →L[ℝ] F) {w : F} {t : ℝ} {u}
   rw [map_add, map_smul, p.update_v, p.update_ker_pi _ _ hu]
 
 /-- Map a dual pair under a linear equivalence. -/
-@[simps, pp_dot]
+@[simps]
 def map (p : DualPair E) (L : E ≃L[ℝ] E') : DualPair E' :=
   ⟨p.π ∘L ↑L.symm, L p.v, (congr_arg p.π <| L.symm_apply_apply p.v).trans p.pairing⟩
 

SphereEversion/Local/ParametricHPrinciple.lean

@@ -146,7 +146,6 @@ theorem FamilyJetSec.uncurry_φ' (S : FamilyJetSec E F P) (p : P × E) :
   rw [fderiv_fst]
   rfl
 
-attribute [pp_dot] ContinuousLinearMap.comp
 open ContinuousLinearMap
 theorem FamilyJetSec.uncurry_mem_relativize (S : FamilyJetSec E F P) {s : P} {x : E} :
     ((s, x), S.uncurry (s, x)) ∈ R.relativize P ↔ (x, S s x) ∈ R := by
@@ -230,7 +229,6 @@ theorem FamilyJetSec.curry_mem (S : FamilyJetSec (P × E) F G) {p : G × P} {x :
 
 /-- Turn a family of formal solutions of `R.relativize P` parametrized by `G` into a family of
 formal solutions of `R` parametrized by `G × P`. -/
-@[pp_dot]
 def RelLoc.FamilyFormalSol.curry (S : FamilyFormalSol G (R.relativize P)) :
     FamilyFormalSol (G × P) R :=
   ⟨S.toFamilyJetSec.curry, fun _ _ ↦ S.toFamilyJetSec.curry_mem (S.is_sol _ _)⟩

SphereEversion/ToMathlib/Analysis/Calculus/AffineMap.lean

@@ -40,4 +40,4 @@ theorem mapsTo_homothety_ball (c : F) {r : ℝ} (hr : 0 < r) :
     norm_smul, Real.norm_eq_abs, abs_eq_self.2 (inv_pos.mpr hr).le, hy]
 
 theorem contDiff_homothety {n : ℕ∞} (c : F) (r : ℝ) : ContDiff ℝ n (homothety c r) :=
-  (⟨homothety c r, homothety_continuous c r⟩ : F →A[ℝ] F).contDiff
+  (⟨homothety c r, homothety_continuous c r⟩ : F →ᴬ[ℝ] F).contDiff

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "56d2e4ee226603eb6b90b05f6b944bde42672cd5",
+   "rev": "7b3c48b58fa0ae1c8f27889bdb086ea5e4b27b06",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "2225b0e4a3528da20499e2304b521e0c4c2a4563",
+   "rev": "e8c8a42642ceb5af33708b79ae8a3148b681c236",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "c46d22bbe4f8363c0829ce0eb48a95012cdc0d79",
+   "rev": "35e38eb320982cfd2fcc864e0e0467ca223c8cdb",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "4b6177e2a98f2afb04fcad75bbe1bd397a1fa9ba",
+   "rev": "7f5ae31cc05ae70ca6c5caaf59985035f040a74e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.8.0-rc1
+leanprover/lean4:v4.8.0-rc2