Merge branch 'master' into MR-covariant-derivatives

Author: grunweg

Archive/Imo/Imo2024Q3.lean

@@ -876,7 +876,7 @@ lemma p_le_two_mul_k {n : ℕ} (hn : N' a N + 2 < n) (hs : Small a (a n)) : p a
     convert Finset.exists_ne_map_eq_of_card_lt_of_maps_to (t := Finset.Icc 1 (k a)) ?_ ?_
     · simp
     · rintro i -
-      simp [Finset.mem_Icc]
+      simp
       rw [← Small, hc.small_apply_add_two_mul_iff_small i (by omega)]
       simp [hs, hc.one_le_apply]
   have hs' : Small a (a (n + 2 * x)) := by rwa [hc.small_apply_add_two_mul_iff_small x (by omega)]

Mathlib.lean

@@ -1585,6 +1585,7 @@ import Mathlib.Analysis.InnerProductSpace.Dual
 import Mathlib.Analysis.InnerProductSpace.EuclideanDist
 import Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
 import Mathlib.Analysis.InnerProductSpace.JointEigenspace
+import Mathlib.Analysis.InnerProductSpace.Laplacian
 import Mathlib.Analysis.InnerProductSpace.LaxMilgram
 import Mathlib.Analysis.InnerProductSpace.LinearMap
 import Mathlib.Analysis.InnerProductSpace.LinearPMap
@@ -2280,6 +2281,7 @@ import Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
 import Mathlib.CategoryTheory.Limits.Shapes.KernelPair
 import Mathlib.CategoryTheory.Limits.Shapes.Kernels
 import Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
+import Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
 import Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
 import Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
 import Mathlib.CategoryTheory.Limits.Shapes.PiProd
@@ -2403,6 +2405,8 @@ import Mathlib.CategoryTheory.Monoidal.DayConvolution
 import Mathlib.CategoryTheory.Monoidal.Discrete
 import Mathlib.CategoryTheory.Monoidal.End
 import Mathlib.CategoryTheory.Monoidal.ExternalProduct
+import Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
+import Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension
 import Mathlib.CategoryTheory.Monoidal.Free.Basic
 import Mathlib.CategoryTheory.Monoidal.Free.Coherence
 import Mathlib.CategoryTheory.Monoidal.Functor
@@ -3683,6 +3687,7 @@ import Mathlib.Geometry.Manifold.DerivationBundle
 import Mathlib.Geometry.Manifold.Diffeomorph
 import Mathlib.Geometry.Manifold.Elaborators
 import Mathlib.Geometry.Manifold.GroupLieAlgebra
+import Mathlib.Geometry.Manifold.Instances.Icc
 import Mathlib.Geometry.Manifold.Instances.Real
 import Mathlib.Geometry.Manifold.Instances.Sphere
 import Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
@@ -3716,6 +3721,7 @@ import Mathlib.Geometry.Manifold.VectorBundle.Hom
 import Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
 import Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
 import Mathlib.Geometry.Manifold.VectorBundle.Pullback
+import Mathlib.Geometry.Manifold.VectorBundle.Riemannian
 import Mathlib.Geometry.Manifold.VectorBundle.SmoothSection
 import Mathlib.Geometry.Manifold.VectorBundle.Tangent
 import Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
@@ -4752,6 +4758,7 @@ import Mathlib.Order.Category.Preord
 import Mathlib.Order.Category.Semilat
 import Mathlib.Order.Chain
 import Mathlib.Order.Circular
+import Mathlib.Order.Circular.ZMod
 import Mathlib.Order.Closure
 import Mathlib.Order.Cofinal
 import Mathlib.Order.CompactlyGenerated.Basic

Mathlib/Algebra/Algebra/Subalgebra/Directed.lean

@@ -44,7 +44,7 @@ variable (K)
 it on each subalgebra, and proving that it agrees on the intersection of subalgebras. -/
 noncomputable def iSupLift (dir : Directed (· ≤ ·) K) (f : ∀ i, K i →ₐ[R] B)
     (hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h))
-    (T : Subalgebra R A) (hT : T = iSup K): ↥T →ₐ[R] B :=
+    (T : Subalgebra R A) (hT : T = iSup K) : ↥T →ₐ[R] B :=
   { toFun := Set.iUnionLift (fun i => ↑(K i)) (fun i x => f i x)
         (fun i j x hxi hxj => by
           let ⟨k, hik, hjk⟩ := dir i j

Mathlib/Algebra/BigOperators/Finsupp/Fin.lean

@@ -23,7 +23,7 @@ lemma sum_cons [AddCommMonoid M] (n : ℕ) (σ : Fin n →₀ M) (i : M) :
   exact Fin.sum_cons i σ
 
 lemma sum_cons' [Zero M] [AddCommMonoid N] (n : ℕ) (σ : Fin n →₀ M) (i : M)
-    (f : Fin (n+1) → M → N) (h : ∀ x, f x 0 = 0) :
+    (f : Fin (n + 1) → M → N) (h : ∀ x, f x 0 = 0) :
     (sum (Finsupp.cons i σ) f) = f 0 i + sum σ (Fin.tail f) := by
   rw [sum_fintype _ _ (fun _ => by apply h), sum_fintype _ _ (fun _ => by apply h)]
   simp_rw [Fin.sum_univ_succ, cons_zero, cons_succ]

Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

@@ -212,7 +212,7 @@ variable {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M}
 
 @[to_additive]
 lemma prod_of_injOn (e : ι → κ) (he : Set.InjOn e s) (hest : Set.MapsTo e s t)
-    (h' : ∀ i ∈ t, i ∉ e '' s → g i = 1) (h : ∀ i ∈ s, f i = g (e i))  :
+    (h' : ∀ i ∈ t, i ∉ e '' s → g i = 1) (h : ∀ i ∈ s, f i = g (e i)) :
     ∏ i ∈ s, f i = ∏ j ∈ t, g j := by
   classical
   exact (prod_nbij e (fun a ↦ mem_image_of_mem e) he (by simp [Set.surjOn_image]) h).trans <|

Mathlib/Algebra/BrauerGroup/Defs.lean

@@ -84,7 +84,7 @@ end IsBrauerEquivalent
 variable (K)
 
 /-- `CSA` equipped with Brauer Equivalence is indeed a setoid. -/
-def Brauer.CSA_Setoid: Setoid (CSA K) where
+def Brauer.CSA_Setoid : Setoid (CSA K) where
   r := IsBrauerEquivalent
   iseqv := IsBrauerEquivalent.is_eqv
 

Mathlib/Algebra/Category/AlgCat/Limits.lean

@@ -109,20 +109,20 @@ def limitConeIsLimit : IsLimit (limitCone.{v, w} F) := by
     simp only [Functor.mapCone_π_app, forget_map, map_one, Pi.one_apply]
   · intro x y
     ext j
-    simp only [Functor.comp_obj, forget_obj, Equiv.toFun_as_coe, Functor.mapCone_pt,
+    simp only [Functor.comp_obj, forget_obj, Functor.mapCone_pt,
       Functor.mapCone_π_app, forget_map, Equiv.symm_apply_apply,
-      Types.Small.limitCone_pt, equivShrink_symm_mul]
+      Types.Small.limitCone_pt, equivShrink_symm_mul, EquivLike.coe_apply]
     apply map_mul
   · ext j
-    simp only [Functor.comp_obj, forget_obj, Equiv.toFun_as_coe, Functor.mapCone_pt,
+    simp only [Functor.comp_obj, forget_obj, Functor.mapCone_pt,
       Functor.mapCone_π_app, forget_map, Equiv.symm_apply_apply,
-      equivShrink_symm_zero]
+      equivShrink_symm_zero, EquivLike.coe_apply]
     apply map_zero
   · intro x y
     ext j
-    simp only [Functor.comp_obj, forget_obj, Equiv.toFun_as_coe, Functor.mapCone_pt,
+    simp only [Functor.comp_obj, forget_obj, Functor.mapCone_pt,
       Functor.mapCone_π_app, forget_map, Equiv.symm_apply_apply,
-      Types.Small.limitCone_pt, equivShrink_symm_add]
+      Types.Small.limitCone_pt, equivShrink_symm_add, EquivLike.coe_apply]
     apply map_add
   · intro r
     simp only [Equiv.algebraMap_def, Equiv.symm_symm]

Mathlib/Algebra/Category/ModuleCat/ExteriorPower.lean

@@ -40,7 +40,7 @@ namespace AlternatingMap
 variable {M : ModuleCat.{v} R} {N : ModuleCat.{max u v} R} {n : ℕ}
 
 @[ext]
-lemma ext {φ φ' : M.AlternatingMap N n} (h : ∀ (x : Fin n → M), φ x = φ' x ) :
+lemma ext {φ φ' : M.AlternatingMap N n} (h : ∀ (x : Fin n → M), φ x = φ' x) :
     φ = φ' :=
   _root_.AlternatingMap.ext h
 

Mathlib/Algebra/Category/ModuleCat/Presheaf/Free.lean

@@ -85,7 +85,7 @@ noncomputable def freeHomEquiv : (freeObj F ⟶ G) ≃ (F ⟶ G.presheaf ⋙ for
 
 lemma free_hom_ext {ψ ψ' : freeObj F ⟶ G}
     (h : freeAdjunctionUnit R F ≫ Functor.whiskerRight ((toPresheaf _).map ψ) _ =
-      freeAdjunctionUnit R F ≫ Functor.whiskerRight ((toPresheaf _).map ψ') _ ) : ψ = ψ' :=
+      freeAdjunctionUnit R F ≫ Functor.whiskerRight ((toPresheaf _).map ψ') _) : ψ = ψ' :=
   freeHomEquiv.injective h
 
 variable (R) in

Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean

@@ -85,7 +85,7 @@ abbrev ofHom {X Y : Type v}
     (f : X →L[R] Y) : of R X ⟶ of R Y :=
   ConcreteCategory.ofHom f
 
-@[simp] lemma hom_ofHom  {X Y : Type v}
+@[simp] lemma hom_ofHom {X Y : Type v}
     [AddCommGroup X] [Module R X] [TopologicalSpace X] [ContinuousAdd X] [ContinuousSMul R X]
     [AddCommGroup Y] [Module R Y] [TopologicalSpace Y] [ContinuousAdd Y] [ContinuousSMul R Y]
     (f : X →L[R] Y) :