bump to nightly-2023-04-09-02

mathlib commit leanprover-community/mathlib@284fdd2

Mathbin/AlgebraicTopology/SimplexCategory.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Scott Morrison, Adam Topaz
 
 ! This file was ported from Lean 3 source module algebraic_topology.simplex_category
-! leanprover-community/mathlib commit e8ac6315bcfcbaf2d19a046719c3b553206dac75
+! leanprover-community/mathlib commit 19cb3751e5e9b3d97adb51023949c50c13b5fdfd
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -16,6 +16,9 @@ import Mathbin.CategoryTheory.Functor.ReflectsIsomorphisms
 
 /-! # The simplex category
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We construct a skeletal model of the simplex category, with objects `ℕ` and the
 morphism `n ⟶ m` being the monotone maps from `fin (n+1)` to `fin (m+1)`.
 

Mathbin/Analysis/Analytic/Inverse.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 
 ! This file was ported from Lean 3 source module analysis.analytic.inverse
-! leanprover-community/mathlib commit ce11c3c2a285bbe6937e26d9792fda4e51f3fe1a
+! leanprover-community/mathlib commit 284fdd2962e67d2932fa3a79ce19fcf92d38e228
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -191,7 +191,6 @@ theorem rightInv_coeff_one (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[
     p.right_inv i 1 = (continuousMultilinearCurryFin1 𝕜 F E).symm i.symm := by rw [right_inv]
 #align formal_multilinear_series.right_inv_coeff_one FormalMultilinearSeries.rightInv_coeff_one
 
-/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `congrm #[[expr i.symm.to_continuous_linear_map.comp_continuous_multilinear_map (p.comp (λ k, _) _)]] -/
 /-- The right inverse does not depend on the zeroth coefficient of a formal multilinear
 series. -/
 theorem rightInv_removeZero (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) :
@@ -204,8 +203,7 @@ theorem rightInv_removeZero (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[
   · simp only [right_inv_coeff_one]
   simp only [right_inv, neg_inj]
   rw [remove_zero_comp_of_pos _ _ (add_pos_of_nonneg_of_pos n.zero_le zero_lt_two)]
-  trace
-    "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:73:14: unsupported tactic `congrm #[[expr i.symm.to_continuous_linear_map.comp_continuous_multilinear_map (p.comp (λ k, _) _)]]"
+  congr 2 with k
   by_cases hk : k < n + 2 <;> simp [hk, IH]
 #align formal_multilinear_series.right_inv_remove_zero FormalMultilinearSeries.rightInv_removeZero
 

Mathbin/Analysis/Calculus/ContDiffDef.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 
 ! This file was ported from Lean 3 source module analysis.calculus.cont_diff_def
-! leanprover-community/mathlib commit dd6388c44e6f6b4547070b887c5905d5cfe6c9f8
+! leanprover-community/mathlib commit 284fdd2962e67d2932fa3a79ce19fcf92d38e228
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -613,6 +613,7 @@ theorem contDiffWithinAt_succ_iff_hasFderivWithinAt {n : ℕ} :
             ((p' y 0) 0) z
         unfold_coes
         congr
+        decide
       · convert(Hp'.mono (inter_subset_left v u)).congr fun x hx => Hp'.zero_eq x hx.1
         · ext (x y)
           change p' x 0 (init (@snoc 0 (fun i : Fin 1 => E) 0 y)) y = p' x 0 0 y

Mathbin/Analysis/Hofer.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot
 
 ! This file was ported from Lean 3 source module analysis.hofer
-! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982
+! leanprover-community/mathlib commit 19cb3751e5e9b3d97adb51023949c50c13b5fdfd
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.Analysis.SpecificLimits.Basic
 /-!
 # Hofer's lemma
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This is an elementary lemma about complete metric spaces. It is motivated by an
 application to the bubbling-off analysis for holomorphic curves in symplectic topology.
 We are *very* far away from having these applications, but the proof here is a nice

Mathbin/Analysis/InnerProductSpace/Symmetric.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Moritz Doll, Frédéric Dupuis, Heather Macbeth
 
 ! This file was ported from Lean 3 source module analysis.inner_product_space.symmetric
-! leanprover-community/mathlib commit 46b633fd842bef9469441c0209906f6dddd2b4f5
+! leanprover-community/mathlib commit 36172d6661e181c215108035483dbbeabd62942e
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -172,5 +172,41 @@ theorem isSymmetric_iff_inner_map_self_real (T : V →ₗ[ℂ] V) :
 
 end Complex
 
+/-- Polarization identity for symmetric linear maps.
+See `inner_map_polarization` for the complex version without the symmetric assumption. -/
+theorem IsSymmetric.inner_map_polarization {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (x y : E) :
+    ⟪T x, y⟫ =
+      (⟪T (x + y), x + y⟫ - ⟪T (x - y), x - y⟫ - i * ⟪T (x + (i : 𝕜) • y), x + (i : 𝕜) • y⟫ +
+          i * ⟪T (x - (i : 𝕜) • y), x - (i : 𝕜) • y⟫) /
+        4 :=
+  by
+  rcases@I_mul_I_ax 𝕜 _ with (h | h)
+  · simp_rw [h, MulZeroClass.zero_mul, sub_zero, add_zero, map_add, map_sub, inner_add_left,
+      inner_add_right, inner_sub_left, inner_sub_right, hT x, ← inner_conj_symm x (T y)]
+    suffices (re ⟪T y, x⟫ : 𝕜) = ⟪T y, x⟫
+      by
+      rw [eq_conj_iff_re.mpr this]
+      ring_nf
+    · rw [← re_add_im ⟪T y, x⟫]
+      simp_rw [h, MulZeroClass.mul_zero, add_zero]
+      norm_cast
+  · simp_rw [map_add, map_sub, inner_add_left, inner_add_right, inner_sub_left, inner_sub_right,
+      LinearMap.map_smul, inner_smul_left, inner_smul_right, IsROrC.conj_i, mul_add, mul_sub,
+      sub_sub, ← mul_assoc, mul_neg, h, neg_neg, one_mul, neg_one_mul]
+    ring
+#align linear_map.is_symmetric.inner_map_polarization LinearMap.IsSymmetric.inner_map_polarization
+
+/-- A symmetric linear map `T` is zero if and only if `⟪T x, x⟫_ℝ = 0` for all `x`.
+See `inner_map_self_eq_zero` for the complex version without the symmetric assumption. -/
+theorem IsSymmetric.inner_map_eq_zero {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) :
+    (∀ x, ⟪T x, x⟫ = 0) ↔ T = 0 :=
+  by
+  simp_rw [LinearMap.ext_iff, zero_apply]
+  refine' ⟨fun h x => _, fun h => by simp_rw [h, inner_zero_left, forall_const]⟩
+  rw [← @inner_self_eq_zero 𝕜, hT.inner_map_polarization]
+  simp_rw [h _]
+  ring
+#align linear_map.is_symmetric.inner_map_eq_zero LinearMap.IsSymmetric.inner_map_eq_zero
+
 end LinearMap
 

Mathbin/Analysis/Normed/Group/Pointwise.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Yaël Dillies
 
 ! This file was ported from Lean 3 source module analysis.normed.group.pointwise
-! leanprover-community/mathlib commit f2ce6086713c78a7f880485f7917ea547a215982
+! leanprover-community/mathlib commit 19cb3751e5e9b3d97adb51023949c50c13b5fdfd
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Topology.MetricSpace.HausdorffDistance
 /-!
 # Properties of pointwise addition of sets in normed groups
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We explore the relationships between pointwise addition of sets in normed groups, and the norm.
 Notably, we show that the sum of bounded sets remain bounded.
 -/

Mathbin/Analysis/NormedSpace/Multilinear.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 
 ! This file was ported from Lean 3 source module analysis.normed_space.multilinear
-! leanprover-community/mathlib commit ce11c3c2a285bbe6937e26d9792fda4e51f3fe1a
+! leanprover-community/mathlib commit 284fdd2962e67d2932fa3a79ce19fcf92d38e228
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -937,7 +937,7 @@ theorem mkPiField_apply (z : G) (m : ι → 𝕜) :
 
 theorem mkPiField_apply_one_eq_self (f : ContinuousMultilinearMap 𝕜 (fun i : ι => 𝕜) G) :
     ContinuousMultilinearMap.mkPiField 𝕜 ι (f fun i => 1) = f :=
-  toMultilinearMap_inj f.toMultilinearMap.mkPiRing_apply_one_eq_self
+  toMultilinearMap_injective f.toMultilinearMap.mkPiRing_apply_one_eq_self
 #align continuous_multilinear_map.mk_pi_field_apply_one_eq_self ContinuousMultilinearMap.mkPiField_apply_one_eq_self
 
 @[simp]
@@ -950,7 +950,7 @@ theorem mkPiField_eq_iff {z₁ z₂ : G} :
     ContinuousMultilinearMap.mkPiField 𝕜 ι z₁ = ContinuousMultilinearMap.mkPiField 𝕜 ι z₂ ↔
       z₁ = z₂ :=
   by
-  rw [← to_multilinear_map_inj.eq_iff]
+  rw [← to_multilinear_map_injective.eq_iff]
   exact MultilinearMap.mkPiRing_eq_iff
 #align continuous_multilinear_map.mk_pi_field_eq_iff ContinuousMultilinearMap.mkPiField_eq_iff
 
@@ -1437,7 +1437,7 @@ theorem ContinuousLinearMap.curry_uncurryLeft
 @[simp]
 theorem ContinuousMultilinearMap.uncurry_curryLeft (f : ContinuousMultilinearMap 𝕜 Ei G) :
     f.curryLeft.uncurryLeft = f :=
-  ContinuousMultilinearMap.toMultilinearMap_inj <| f.toMultilinearMap.uncurry_curryLeft
+  ContinuousMultilinearMap.toMultilinearMap_injective <| f.toMultilinearMap.uncurry_curryLeft
 #align continuous_multilinear_map.uncurry_curry_left ContinuousMultilinearMap.uncurry_curryLeft
 
 variable (𝕜 Ei G)

Mathbin/Analysis/SpecificLimits/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Johannes Hölzl, Yury G. Kudryashov, Patrick Massot
 
 ! This file was ported from Lean 3 source module analysis.specific_limits.basic
-! leanprover-community/mathlib commit 57ac39bd365c2f80589a700f9fbb664d3a1a30c2
+! leanprover-community/mathlib commit 19cb3751e5e9b3d97adb51023949c50c13b5fdfd
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -17,6 +17,9 @@ import Mathbin.Topology.Algebra.Algebra
 /-!
 # A collection of specific limit computations
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file, by design, is independent of `normed_space` in the import hierarchy.  It contains
 important specific limit computations in metric spaces, in ordered rings/fields, and in specific
 instances of these such as `ℝ`, `ℝ≥0` and `ℝ≥0∞`.

Mathbin/CategoryTheory/Category/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Stephen Morgan, Scott Morrison, Johannes Hölzl, Reid Barton
 
 ! This file was ported from Lean 3 source module category_theory.category.basic
-! leanprover-community/mathlib commit 448144f7ae193a8990cb7473c9e9a01990f64ac7
+! leanprover-community/mathlib commit 2efd2423f8d25fa57cf7a179f5d8652ab4d0df44
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -98,8 +98,10 @@ infixr:80
   " ≫ " =>-- type as \b1
   CategoryStruct.comp
 
-#print CategoryTheory.Category /-
 -- type as \gg
+initialize_simps_projections CategoryStruct (-to_quiver_hom)
+
+#print CategoryTheory.Category /-
 /-- The typeclass `category C` describes morphisms associated to objects of type `C`.
 The universe levels of the objects and morphisms are unconstrained, and will often need to be
 specified explicitly, as `category.{v} C`. (See also `large_category` and `small_category`.)
@@ -150,8 +152,8 @@ section
 
 variable {C : Type u} [Category.{v} C] {X Y Z : C}
 
-initialize_simps_projections category (to_category_struct_to_quiver_hom → Hom,
-  to_category_struct_comp → comp, to_category_struct_id → id, -toCategoryStruct)
+initialize_simps_projections category (to_category_struct_comp → comp, to_category_struct_id → id,
+  -toCategoryStruct)
 
 #print CategoryTheory.eq_whisker /-
 /-- postcompose an equation between morphisms by another morphism -/

Mathbin/CategoryTheory/FinCategory.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 
 ! This file was ported from Lean 3 source module category_theory.fin_category
-! leanprover-community/mathlib commit 3dadefa3f544b1db6214777fe47910739b54c66a
+! leanprover-community/mathlib commit 2efd2423f8d25fa57cf7a179f5d8652ab4d0df44
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -104,7 +104,7 @@ abbrev AsType : Type :=
 #align category_theory.fin_category.as_type CategoryTheory.FinCategory.AsType
 
 #print CategoryTheory.FinCategory.categoryAsType /-
-@[simps (config := lemmasOnly) hom id comp]
+@[simps (config := lemmasOnly) id comp]
 noncomputable instance categoryAsType : SmallCategory (AsType α)
     where
   hom i j := Fin (Fintype.card (@Quiver.Hom (ObjAsType α) _ i j))
@@ -113,7 +113,7 @@ noncomputable instance categoryAsType : SmallCategory (AsType α)
 #align category_theory.fin_category.category_as_type CategoryTheory.FinCategory.categoryAsType
 -/
 
-attribute [local simp] category_as_type_hom category_as_type_id category_as_type_comp
+attribute [local simp] category_as_type_id category_as_type_comp
 
 #print CategoryTheory.FinCategory.asTypeToObjAsType /-
 /-- The "identity" functor from `as_type α` to `obj_as_type α`. -/

Mathbin/CategoryTheory/Groupoid.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Reid Barton, Scott Morrison, David Wärn
 
 ! This file was ported from Lean 3 source module category_theory.groupoid
-! leanprover-community/mathlib commit e97cf15cd1aec9bd5c193b2ffac5a6dc9118912b
+! leanprover-community/mathlib commit 2efd2423f8d25fa57cf7a179f5d8652ab4d0df44
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -56,6 +56,10 @@ restate_axiom groupoid.inv_comp'
 
 restate_axiom groupoid.comp_inv'
 
+initialize_simps_projections Groupoid (-to_category_to_category_struct_to_quiver_hom,
+  to_category_to_category_struct_comp → comp, to_category_to_category_struct_id → id,
+  -to_category_to_category_struct, -toCategory)
+
 #print CategoryTheory.LargeGroupoid /-
 /-- A `large_groupoid` is a groupoid
 where the objects live in `Type (u+1)` while the morphisms live in `Type u`.

Mathbin/CategoryTheory/Idempotents/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 
 ! This file was ported from Lean 3 source module category_theory.idempotents.basic
-! leanprover-community/mathlib commit 3a061790136d13594ec10c7c90d202335ac5d854
+! leanprover-community/mathlib commit 19cb3751e5e9b3d97adb51023949c50c13b5fdfd
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.CategoryTheory.Abelian.Basic
 /-!
 # Idempotent complete categories
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we define the notion of idempotent complete categories
 (also known as Karoubian categories, or pseudoabelian in the case of
 preadditive categories).

Mathbin/CategoryTheory/Idempotents/FunctorCategories.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 
 ! This file was ported from Lean 3 source module category_theory.idempotents.functor_categories
-! leanprover-community/mathlib commit 31019c2504b17f85af7e0577585fad996935a317
+! leanprover-community/mathlib commit 19cb3751e5e9b3d97adb51023949c50c13b5fdfd
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.CategoryTheory.Idempotents.Karoubi
 /-!
 # Idempotent completeness and functor categories
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define an instance `functor_category_is_idempotent_complete` expressing
 that a functor category `J ⥤ C` is idempotent complete when the target category `C` is.
 

Mathbin/CategoryTheory/Idempotents/FunctorExtension.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 
 ! This file was ported from Lean 3 source module category_theory.idempotents.functor_extension
-! leanprover-community/mathlib commit 5f68029a863bdf76029fa0f7a519e6163c14152e
+! leanprover-community/mathlib commit 19cb3751e5e9b3d97adb51023949c50c13b5fdfd
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.CategoryTheory.Idempotents.Karoubi
 /-!
 # Extension of functors to the idempotent completion
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we construct an extension `functor_extension₁`
 of functors `C ⥤ karoubi D` to functors `karoubi C ⥤ karoubi D`. This results in an
 equivalence `karoubi_universal₁ C D : (C ⥤ karoubi D) ≌ (karoubi C ⥤ karoubi D)`.

Mathbin/CategoryTheory/Idempotents/Karoubi.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 
 ! This file was ported from Lean 3 source module category_theory.idempotents.karoubi
-! leanprover-community/mathlib commit 200eda15d8ff5669854ff6bcc10aaf37cb70498f
+! leanprover-community/mathlib commit 19cb3751e5e9b3d97adb51023949c50c13b5fdfd
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.CategoryTheory.Equivalence
 /-!
 # The Karoubi envelope of a category
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we define the Karoubi envelope `karoubi C` of a category `C`.
 
 ## Main constructions and definitions

Mathbin/CategoryTheory/Idempotents/KaroubiKaroubi.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 
 ! This file was ported from Lean 3 source module category_theory.idempotents.karoubi_karoubi
-! leanprover-community/mathlib commit 31019c2504b17f85af7e0577585fad996935a317
+! leanprover-community/mathlib commit 19cb3751e5e9b3d97adb51023949c50c13b5fdfd
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.CategoryTheory.Idempotents.Karoubi
 /-!
 # Idempotence of the Karoubi envelope
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we construct the equivalence of categories
 `karoubi_karoubi.equivalence C : karoubi C ≌ karoubi (karoubi C)` for any category `C`.
 

Mathbin/CategoryTheory/Monoidal/Braided.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 
 ! This file was ported from Lean 3 source module category_theory.monoidal.braided
-! leanprover-community/mathlib commit c9c9fa15fec7ca18e9ec97306fb8764bfe988a7e
+! leanprover-community/mathlib commit 2efd2423f8d25fa57cf7a179f5d8652ab4d0df44
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -330,6 +330,9 @@ restate_axiom symmetric_category.symmetry'
 
 attribute [simp, reassoc.1] symmetric_category.symmetry
 
+initialize_simps_projections SymmetricCategory (to_braided_category_braiding → braiding,
+  -toBraidedCategory)
+
 variable (C : Type u₁) [Category.{v₁} C] [MonoidalCategory C] [BraidedCategory C]
 
 variable (D : Type u₂) [Category.{v₂} D] [MonoidalCategory D] [BraidedCategory D]