bump to nightly-2023-03-01-00

mathlib commit leanprover-community/mathlib3@9da1b35
leanprover-community · Mar 1, 2023 · bccc50c · bccc50c
1 parent 1fb1623
commit bccc50c
Show file tree

Hide file tree

Showing 10 changed files with 161 additions and 163 deletions.
diff --git a/Mathbin/Algebra/Group/Units.lean b/Mathbin/Algebra/Group/Units.lean
@@ -125,9 +125,9 @@ def [anonymous] (u : αˣ) : α :=
   ↑u⁻¹
 #align units.simps.coe_inv [anonymous]
 
-initialize_simps_projections Units (val → coe as_prefix, inv → coe_inv as_prefix)
+initialize_simps_projections Units (val → coe, as_prefix coe, inv → coe_inv, as_prefix coe_inv)
 
-initialize_simps_projections AddUnits (val → coe as_prefix, neg → coe_neg as_prefix)
+initialize_simps_projections AddUnits (val → coe, as_prefix coe, neg → coe_neg, as_prefix coe_neg)
 
 /- warning: units.coe_mk -> Units.val_mk is a dubious translation:
 lean 3 declaration is

diff --git a/Mathbin/Algebra/Module/Equiv.lean b/Mathbin/Algebra/Module/Equiv.lean
diff --git a/Mathbin/LinearAlgebra/AffineSpace/AffineEquiv.lean b/Mathbin/LinearAlgebra/AffineSpace/AffineEquiv.lean
@@ -214,7 +214,7 @@ def Simps.symmApply (e : P₁ ≃ᵃ[k] P₂) : P₂ → P₁ :=
 #align affine_equiv.simps.symm_apply AffineEquiv.Simps.symmApply
 
 initialize_simps_projections AffineEquiv (to_equiv_to_fun → apply, to_equiv_inv_fun → symm_apply,
-  linear → linear as_prefix, -toEquiv)
+  linear → linear, as_prefix linear, -toEquiv)
 
 protected theorem bijective (e : P₁ ≃ᵃ[k] P₂) : Bijective e :=
   e.toEquiv.Bijective

diff --git a/Mathbin/LinearAlgebra/Pi.lean b/Mathbin/LinearAlgebra/Pi.lean
diff --git a/Mathbin/Order/Heyting/Hom.lean b/Mathbin/Order/Heyting/Hom.lean
diff --git a/Mathbin/Order/Hom/Lattice.lean b/Mathbin/Order/Hom/Lattice.lean
diff --git a/Mathbin/Order/Ideal.lean b/Mathbin/Order/Ideal.lean
diff --git a/Mathbin/Tactic/Simps.lean b/Mathbin/Tactic/Simps.lean
@@ -116,13 +116,11 @@ unsafe instance : has_to_format parsed_projection_data :=
 
 end
 
-#print ProjectionRule /-
 /-- The type of rules that specify how metadata for projections in changes.
   See `initialize_simps_projection`. -/
 abbrev ProjectionRule :=
   Sum (Name × Name) Name × Bool
 #align projection_rule ProjectionRule
--/
 
 /-- The `@[_simps_str]` attribute specifies the preferred projections of the given structure,
 used by the `@[simps]` attribute.

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "232aaddfaaa7d23f96af916f60d521e4405b67dd",
+    "rev": "339fa1901df2c7f00338edf9590d8dff4f5a2974",
     "name": "lean3port",
-    "inputRev?": "232aaddfaaa7d23f96af916f60d521e4405b67dd"}},
+    "inputRev?": "339fa1901df2c7f00338edf9590d8dff4f5a2974"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "7b5ca5d34639cc7c0cbf129b4dedefb79fb84ec8",
+    "rev": "b21620a738bdb033f8e5b97ca769d89ae650bfbc",
     "name": "mathlib",
-    "inputRev?": "7b5ca5d34639cc7c0cbf129b4dedefb79fb84ec8"}},
+    "inputRev?": "b21620a738bdb033f8e5b97ca769d89ae650bfbc"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

diff --git a/lakefile.lean b/lakefile.lean
@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-02-28-22"
+def tag : String := "nightly-2023-03-01-00"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"232aaddfaaa7d23f96af916f60d521e4405b67dd"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"339fa1901df2c7f00338edf9590d8dff4f5a2974"
 
 @[default_target]
 lean_lib Mathbin where