bump to nightly-2023-07-04-01

mathlib commit leanprover-community/mathlib@728ef9d
leanprover-community · Jul 4, 2023 · 05318d7 · 05318d7
1 parent f4d4491
commit 05318d7
Show file tree

Hide file tree

Showing 80 changed files with 1,150 additions and 925 deletions.
diff --git a/Mathbin/Algebra/Category/FgModule/Limits.lean b/Mathbin/Algebra/Category/FgModule/Limits.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 algebra.category.fgModule.limits
-! leanprover-community/mathlib commit 19a70dceb9dff0994b92d2dd049de7d84d28112b
+! leanprover-community/mathlib commit d0b1936853671209a866fa35b9e54949c81116e2
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -19,6 +19,9 @@ import Mathbin.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
 /-!
 # `forget₂ (fgModule K) (Module K)` creates all finite limits.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 And hence `fgModule K` has all finite limits.
 
 ## Future work

diff --git a/Mathbin/Algebra/Category/Mon/Adjunctions.lean b/Mathbin/Algebra/Category/Mon/Adjunctions.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Julian Kuelshammer
 
 ! This file was ported from Lean 3 source module algebra.category.Mon.adjunctions
-! leanprover-community/mathlib commit 4bcba0da3d97399ce99260794213e69ccdf886ee
+! leanprover-community/mathlib commit 728ef9dbb281241906f25cbeb30f90d83e0bb451
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -16,6 +16,9 @@ import Mathbin.Algebra.FreeMonoid.Basic
 /-!
 # Adjunctions regarding the category of monoids
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves the adjunction between adjoining a unit to a semigroup and the forgetful functor
 from monoids to semigroups.
 

diff --git a/Mathbin/Algebra/Category/Semigroup/Basic.lean b/Mathbin/Algebra/Category/Semigroup/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Julian Kuelshammer
 
 ! This file was ported from Lean 3 source module algebra.category.Semigroup.basic
-! leanprover-community/mathlib commit 47b51515e69f59bca5cf34ef456e6000fe205a69
+! leanprover-community/mathlib commit 728ef9dbb281241906f25cbeb30f90d83e0bb451
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -17,6 +17,9 @@ import Mathbin.CategoryTheory.Elementwise
 /-!
 # Category instances for has_mul, has_add, semigroup and add_semigroup
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We introduce the bundled categories:
 * `Magma`
 * `AddMagma`

diff --git a/Mathbin/Algebra/Group/Defs.lean b/Mathbin/Algebra/Group/Defs.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
 
 ! This file was ported from Lean 3 source module algebra.group.defs
-! leanprover-community/mathlib commit 448144f7ae193a8990cb7473c9e9a01990f64ac7
+! leanprover-community/mathlib commit 48fb5b5280e7c81672afc9524185ae994553ebf4
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -88,15 +88,26 @@ universe u
 
 variable {G : Type _}
 
--- PLEASE REPORT THIS TO MATHPORT DEVS, THIS SHOULD NOT HAPPEN.
--- failed to format: unknown constant 'Lean.Meta._root_.Lean.Parser.Command.registerSimpAttr'
-/--
-    The simpset `field_simps` is used by the tactic `field_simp` to
-    reduce an expression in a field to an expression of the form `n / d` where `n` and `d` are
-    division-free. -/
-  register_simp_attr
-  field_simps
+/- Additive "sister" structures.
+   Example, add_semigroup mirrors semigroup.
+   These structures exist just to help automation.
+   In an alternative design, we could have the binary operation as an
+   extra argument for semigroup, monoid, group, etc. However, the lemmas
+   would be hard to index since they would not contain any constant.
+   For example, mul_assoc would be
 
+   lemma mul_assoc {α : Type u} {op : α → α → α} [semigroup α op] :
+                   ∀ a b c : α, op (op a b) c = op a (op b c) :=
+    semigroup.mul_assoc
+
+   The simplifier cannot effectively use this lemma since the pattern for
+   the left-hand-side would be
+
+        ?op (?op ?a ?b) ?c
+
+   Remark: we use a tactic for transporting theorems from the multiplicative fragment
+   to the additive one.
+-/
 section Mul
 
 variable [Mul G]

diff --git a/Mathbin/Algebra/Homology/DifferentialObject.lean b/Mathbin/Algebra/Homology/DifferentialObject.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 algebra.homology.differential_object
-! leanprover-community/mathlib commit b535c2d5d996acd9b0554b76395d9c920e186f4f
+! leanprover-community/mathlib commit d0b1936853671209a866fa35b9e54949c81116e2
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.CategoryTheory.DifferentialObject
 /-!
 # Homological complexes are differential graded objects.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We verify that a `homological_complex` indexed by an `add_comm_group` is
 essentially the same thing as a differential graded object.
 

diff --git a/Mathbin/AlgebraicGeometry/AffineScheme.lean b/Mathbin/AlgebraicGeometry/AffineScheme.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 
 ! This file was ported from Lean 3 source module algebraic_geometry.AffineScheme
-! leanprover-community/mathlib commit 88474d1b5af6d37c2ab728b757771bced7f5194c
+! leanprover-community/mathlib commit d0b1936853671209a866fa35b9e54949c81116e2
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -16,6 +16,9 @@ import Mathbin.RingTheory.Localization.InvSubmonoid
 /-!
 # Affine schemes
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define the category of `AffineScheme`s as the essential image of `Spec`.
 We also define predicates about affine schemes and affine open sets.
 

diff --git a/Mathbin/AlgebraicGeometry/FunctionField.lean b/Mathbin/AlgebraicGeometry/FunctionField.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 
 ! This file was ported from Lean 3 source module algebraic_geometry.function_field
-! leanprover-community/mathlib commit d39590fc8728fbf6743249802486f8c91ffe07bc
+! leanprover-community/mathlib commit 728ef9dbb281241906f25cbeb30f90d83e0bb451
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.AlgebraicGeometry.Properties
 /-!
 # Function field of integral schemes
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define the function field of an irreducible scheme as the stalk of the generic point.
 This is a field when the scheme is integral.
 

diff --git a/Mathbin/AlgebraicGeometry/Gluing.lean b/Mathbin/AlgebraicGeometry/Gluing.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 
 ! This file was ported from Lean 3 source module algebraic_geometry.gluing
-! leanprover-community/mathlib commit 533f62f4dd62a5aad24a04326e6e787c8f7e98b1
+! leanprover-community/mathlib commit d0b1936853671209a866fa35b9e54949c81116e2
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.AlgebraicGeometry.OpenImmersion.Scheme
 /-!
 # Gluing Schemes
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a family of gluing data of schemes, we may glue them together.
 
 ## Main definitions

diff --git a/Mathbin/AlgebraicGeometry/Limits.lean b/Mathbin/AlgebraicGeometry/Limits.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 
 ! This file was ported from Lean 3 source module algebraic_geometry.limits
-! leanprover-community/mathlib commit 70fd9563a21e7b963887c9360bd29b2393e6225a
+! leanprover-community/mathlib commit d0b1936853671209a866fa35b9e54949c81116e2
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.AlgebraicGeometry.AffineScheme
 /-!
 # (Co)Limits of Schemes
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We construct various limits and colimits in the category of schemes.
 
 * The existence of fibred products was shown in `algebraic_geometry/pullbacks.lean`.

diff --git a/Mathbin/AlgebraicGeometry/Morphisms/Basic.lean b/Mathbin/AlgebraicGeometry/Morphisms/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 
 ! This file was ported from Lean 3 source module algebraic_geometry.morphisms.basic
-! leanprover-community/mathlib commit 434e2fd21c1900747afc6d13d8be7f4eedba7218
+! leanprover-community/mathlib commit 728ef9dbb281241906f25cbeb30f90d83e0bb451
 ! 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.MorphismProperty
 /-!
 # Properties of morphisms between Schemes
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We provide the basic framework for talking about properties of morphisms between Schemes.
 
 A `morphism_property Scheme` is a predicate on morphisms between schemes, and an

diff --git a/Mathbin/AlgebraicGeometry/Morphisms/OpenImmersion.lean b/Mathbin/AlgebraicGeometry/Morphisms/OpenImmersion.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 
 ! This file was ported from Lean 3 source module algebraic_geometry.morphisms.open_immersion
-! leanprover-community/mathlib commit f0c8bf9245297a541f468be517f1bde6195105e9
+! leanprover-community/mathlib commit 728ef9dbb281241906f25cbeb30f90d83e0bb451
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.AlgebraicGeometry.Morphisms.Basic
 
 # Open immersions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A morphism is an open immersions if the underlying map of spaces is an open embedding
 `f : X ⟶ U ⊆ Y`, and the sheaf map `Y(V) ⟶ f _* X(V)` is an iso for each `V ⊆ U`.
 

diff --git a/Mathbin/AlgebraicGeometry/Morphisms/UniversallyClosed.lean b/Mathbin/AlgebraicGeometry/Morphisms/UniversallyClosed.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 
 ! This file was ported from Lean 3 source module algebraic_geometry.morphisms.universally_closed
-! leanprover-community/mathlib commit a8ae1b3f7979249a0af6bc7cf20c1f6bf656ca73
+! leanprover-community/mathlib commit 728ef9dbb281241906f25cbeb30f90d83e0bb451
 ! 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.LocalAtTarget
 /-!
 # Universally closed morphism
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A morphism of schemes `f : X ⟶ Y` is universally closed if `X ×[Y] Y' ⟶ Y'` is a closed map
 for all base change `Y' ⟶ Y`.
 

diff --git a/Mathbin/AlgebraicGeometry/Properties.lean b/Mathbin/AlgebraicGeometry/Properties.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 
 ! This file was ported from Lean 3 source module algebraic_geometry.properties
-! leanprover-community/mathlib commit 88474d1b5af6d37c2ab728b757771bced7f5194c
+! leanprover-community/mathlib commit d0b1936853671209a866fa35b9e54949c81116e2
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -17,6 +17,9 @@ import Mathbin.RingTheory.LocalProperties
 /-!
 # Basic properties of schemes
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We provide some basic properties of schemes
 
 ## Main definition

diff --git a/Mathbin/AlgebraicGeometry/Pullbacks.lean b/Mathbin/AlgebraicGeometry/Pullbacks.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 
 ! This file was ported from Lean 3 source module algebraic_geometry.pullbacks
-! leanprover-community/mathlib commit 7316286ff2942aa14e540add9058c6b0aa1c8070
+! leanprover-community/mathlib commit d0b1936853671209a866fa35b9e54949c81116e2
 ! 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.Limits.Shapes.Diagonal
 /-!
 # Fibred products of schemes
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we construct the fibred product of schemes via gluing.
 We roughly follow [har77] Theorem 3.3.
 

diff --git a/Mathbin/All.lean b/Mathbin/All.lean
@@ -2844,6 +2844,7 @@ import Mathbin.Tactic.Lint.TypeClasses
 import Mathbin.Tactic.LocalCache
 import Mathbin.Tactic.Localized
 import Mathbin.Tactic.MkIffOfInductiveProp
+import Mathbin.Tactic.MkSimpAttribute
 import Mathbin.Tactic.Monotonicity.Basic
 import Mathbin.Tactic.Monotonicity.Default
 import Mathbin.Tactic.Monotonicity.Interactive

diff --git a/Mathbin/Analysis/Complex/UpperHalfPlane/Manifold.lean b/Mathbin/Analysis/Complex/UpperHalfPlane/Manifold.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Birkbeck
 
 ! This file was ported from Lean 3 source module analysis.complex.upper_half_plane.manifold
-! leanprover-community/mathlib commit 57f9349f2fe19d2de7207e99b0341808d977cdcf
+! leanprover-community/mathlib commit 728ef9dbb281241906f25cbeb30f90d83e0bb451
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Geometry.Manifold.ContMdiffMfderiv
 /-!
 # Manifold structure on the upper half plane.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define the complex manifold structure on the upper half-plane.
 -/
 

diff --git a/Mathbin/Analysis/Convex/Cone/Proper.lean b/Mathbin/Analysis/Convex/Cone/Proper.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Apurva Nakade
 
 ! This file was ported from Lean 3 source module analysis.convex.cone.proper
-! leanprover-community/mathlib commit 147b294346843885f952c5171e9606616a8fd869
+! leanprover-community/mathlib commit 728ef9dbb281241906f25cbeb30f90d83e0bb451
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Analysis.InnerProductSpace.Adjoint
 /-!
 # Proper cones
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define a proper cone as a nonempty, closed, convex cone. Proper cones are used in defining conic
 programs which generalize linear programs. A linear program is a conic program for the positive
 cone. We then prove Farkas' lemma for conic programs following the proof in the reference below.