bump to nightly-2023-03-30-06

mathlib commit leanprover-community/mathlib@b685f50

Mathbin/GroupTheory/GroupAction/Pi.lean

@@ -354,7 +354,7 @@ section Extend
 lean 3 declaration is
   forall {R : Type.{u1}} {α : Type.{u2}} {β : Type.{u3}} {γ : Type.{u4}} [_inst_1 : SMul.{u1, u4} R γ] (r : R) (f : α -> β) (g : α -> γ) (e : β -> γ), Eq.{max (succ u3) (succ u4)} (β -> γ) (Function.extend.{succ u2, succ u3, succ u4} α β γ f (SMul.smul.{u1, max u2 u4} R (α -> γ) (Function.hasSMul.{u2, u1, u4} α R γ _inst_1) r g) (SMul.smul.{u1, max u3 u4} R (β -> γ) (Function.hasSMul.{u3, u1, u4} β R γ _inst_1) r e)) (SMul.smul.{u1, max u3 u4} R (β -> γ) (Function.hasSMul.{u3, u1, u4} β R γ _inst_1) r (Function.extend.{succ u2, succ u3, succ u4} α β γ f g e))
 but is expected to have type
-  forall {R : Type.{u4}} {α : Type.{u3}} {β : Type.{u2}} {γ : Type.{u1}} [_inst_1 : SMul.{u4, u1} R γ] (r : R) (f : α -> β) (g : α -> γ) (e : β -> γ), Eq.{max (succ u2) (succ u1)} (β -> γ) (Function.extend.{succ u3, succ u2, succ u1} α β γ f (HSMul.hSMul.{u4, max u3 u1, max u3 u1} R (α -> γ) (α -> γ) (instHSMul.{u4, max u3 u1} R (α -> γ) (Pi.instSMul.{u3, u1, u4} α R (fun (a._@.Mathlib.GroupTheory.GroupAction.Pi._hyg.2657 : α) => γ) (fun (i : α) => _inst_1))) r g) (HSMul.hSMul.{u4, max u2 u1, max u2 u1} R (β -> γ) (β -> γ) (instHSMul.{u4, max u2 u1} R (β -> γ) (Pi.instSMul.{u2, u1, u4} β R (fun (a._@.Mathlib.GroupTheory.GroupAction.Pi._hyg.2660 : β) => γ) (fun (i : β) => _inst_1))) r e)) (HSMul.hSMul.{u4, max u2 u1, max u2 u1} R (β -> γ) (β -> γ) (instHSMul.{u4, max u2 u1} R (β -> γ) (Pi.instSMul.{u2, u1, u4} β R (fun (a._@.Mathlib.Logic.Function.Basic._hyg.7459 : β) => γ) (fun (i : β) => _inst_1))) r (Function.extend.{succ u3, succ u2, succ u1} α β γ f g e))
+  forall {R : Type.{u4}} {α : Type.{u3}} {β : Type.{u2}} {γ : Type.{u1}} [_inst_1 : SMul.{u4, u1} R γ] (r : R) (f : α -> β) (g : α -> γ) (e : β -> γ), Eq.{max (succ u2) (succ u1)} (β -> γ) (Function.extend.{succ u3, succ u2, succ u1} α β γ f (HSMul.hSMul.{u4, max u3 u1, max u3 u1} R (α -> γ) (α -> γ) (instHSMul.{u4, max u3 u1} R (α -> γ) (Pi.instSMul.{u3, u1, u4} α R (fun (a._@.Mathlib.GroupTheory.GroupAction.Pi._hyg.2657 : α) => γ) (fun (i : α) => _inst_1))) r g) (HSMul.hSMul.{u4, max u2 u1, max u2 u1} R (β -> γ) (β -> γ) (instHSMul.{u4, max u2 u1} R (β -> γ) (Pi.instSMul.{u2, u1, u4} β R (fun (a._@.Mathlib.GroupTheory.GroupAction.Pi._hyg.2660 : β) => γ) (fun (i : β) => _inst_1))) r e)) (HSMul.hSMul.{u4, max u2 u1, max u2 u1} R (β -> γ) (β -> γ) (instHSMul.{u4, max u2 u1} R (β -> γ) (Pi.instSMul.{u2, u1, u4} β R (fun (a._@.Mathlib.Logic.Function.Basic._hyg.7460 : β) => γ) (fun (i : β) => _inst_1))) r (Function.extend.{succ u3, succ u2, succ u1} α β γ f g e))
 Case conversion may be inaccurate. Consider using '#align function.extend_smul Function.extend_smulₓ'. -/
 @[to_additive]
 theorem Function.extend_smul {R α β γ : Type _} [SMul R γ] (r : R) (f : α → β) (g : α → γ)

Mathbin/Logic/Function/Basic.lean

@@ -271,7 +271,7 @@ theorem Injective.of_comp_iff' (f : α → β) {g : γ → α} (hg : Bijective g
 lean 3 declaration is
   forall {α : Sort.{u1}} {β : Sort.{u2}} {γ : Sort.{u3}} {g : β -> γ}, (Function.Injective.{u2, u3} β γ g) -> (Function.Injective.{imax u1 u2, imax u1 u3} (α -> β) (α -> γ) (Function.comp.{u1, u2, u3} α β γ g))
 but is expected to have type
-  forall {α : Sort.{u1}} {β : Sort.{u3}} {γ : Sort.{u2}} {g : β -> γ}, (Function.Injective.{u3, u2} β γ g) -> (Function.Injective.{imax u1 u3, imax u1 u2} (α -> β) (α -> γ) ((fun (x._@.Mathlib.Logic.Function.Basic._hyg.1113 : β -> γ) (x._@.Mathlib.Logic.Function.Basic._hyg.1115 : α -> β) => Function.comp.{u1, u3, u2} α β γ x._@.Mathlib.Logic.Function.Basic._hyg.1113 x._@.Mathlib.Logic.Function.Basic._hyg.1115) g))
+  forall {α : Sort.{u1}} {β : Sort.{u3}} {γ : Sort.{u2}} {g : β -> γ}, (Function.Injective.{u3, u2} β γ g) -> (Function.Injective.{imax u1 u3, imax u1 u2} (α -> β) (α -> γ) ((fun (x._@.Mathlib.Logic.Function.Basic._hyg.1114 : β -> γ) (x._@.Mathlib.Logic.Function.Basic._hyg.1116 : α -> β) => Function.comp.{u1, u3, u2} α β γ x._@.Mathlib.Logic.Function.Basic._hyg.1114 x._@.Mathlib.Logic.Function.Basic._hyg.1116) g))
 Case conversion may be inaccurate. Consider using '#align function.injective.comp_left Function.Injective.comp_leftₓ'. -/
 /-- Composition by an injective function on the left is itself injective. -/
 theorem Injective.comp_left {g : β → γ} (hg : Function.Injective g) :
@@ -1716,7 +1716,7 @@ def Set.piecewise {α : Type u} {β : α → Sort v} (s : Set α) (f g : ∀ i,
 lean 3 declaration is
   forall {α : Sort.{u1}} {C : α -> Sort.{u2}} {a : α} {a' : α} (h : Eq.{u1} α a a'), Function.Bijective.{u2, u2} (C a) (C a') (Eq.recOn.{u2, u1} α a C a' h)
 but is expected to have type
-  forall {α : Sort.{u2}} {C : α -> Sort.{u1}} {a : α} {a' : α} (h : Eq.{u2} α a a'), Function.Bijective.{u1, u1} (C a) (C a') (fun (x._@.Mathlib.Logic.Function.Basic._hyg.10798 : C a) => Eq.ndrec.{u1, u2} α a C x._@.Mathlib.Logic.Function.Basic._hyg.10798 a' h)
+  forall {α : Sort.{u2}} {C : α -> Sort.{u1}} {a : α} {a' : α} (h : Eq.{u2} α a a'), Function.Bijective.{u1, u1} (C a) (C a') (fun (x._@.Mathlib.Logic.Function.Basic._hyg.10802 : C a) => Eq.ndrec.{u1, u2} α a C x._@.Mathlib.Logic.Function.Basic._hyg.10802 a' h)
 Case conversion may be inaccurate. Consider using '#align eq_rec_on_bijective eq_rec_on_bijectiveₓ'. -/
 theorem eq_rec_on_bijective {α : Sort _} {C : α → Sort _} :
     ∀ {a a' : α} (h : a = a'), Function.Bijective (@Eq.recOn _ _ C _ h)
@@ -1768,7 +1768,7 @@ theorem cast_inj {α β : Type _} (h : α = β) {x y : α} : cast h x = cast h y
 lean 3 declaration is
   forall {α : Sort.{u2}} {β : Sort.{u3}} {γ : β -> Sort.{u1}} {f : α -> β} {g : β -> α} (h : Function.LeftInverse.{u2, u3} α β g f) (C : forall (a : α), γ (f a)) (a : α), Eq.{u1} (γ (f a)) (Eq.ndrec.{u1, u3} β (f (g (f a))) γ (C (g (f a))) (f a) (congr_arg.{u2, u3} α β (g (f a)) a f (h a))) (C a)
 but is expected to have type
-  forall {α : Sort.{u2}} {β : Sort.{u1}} {γ : β -> Sort.{u3}} {f : α -> β} {g : β -> α} (h : Function.LeftInverse.{u2, u1} α β g f) (C : forall (a : α), γ (f a)) (a : α), Eq.{u3} (γ (f a)) (Eq.rec.{u3, u1} β (f (g (f a))) (fun (x : β) (x._@.Mathlib.Logic.Function.Basic._hyg.11127 : Eq.{u1} β (f (g (f a))) x) => γ x) (C (g (f a))) (f a) (congr_arg.{u2, u1} α β (g (f a)) a f (h a))) (C a)
+  forall {α : Sort.{u2}} {β : Sort.{u1}} {γ : β -> Sort.{u3}} {f : α -> β} {g : β -> α} (h : Function.LeftInverse.{u2, u1} α β g f) (C : forall (a : α), γ (f a)) (a : α), Eq.{u3} (γ (f a)) (Eq.rec.{u3, u1} β (f (g (f a))) (fun (x : β) (x._@.Mathlib.Logic.Function.Basic._hyg.11131 : Eq.{u1} β (f (g (f a))) x) => γ x) (C (g (f a))) (f a) (congr_arg.{u2, u1} α β (g (f a)) a f (h a))) (C a)
 Case conversion may be inaccurate. Consider using '#align function.left_inverse.eq_rec_eq Function.LeftInverse.eq_rec_eqₓ'. -/
 theorem Function.LeftInverse.eq_rec_eq {α β : Sort _} {γ : β → Sort v} {f : α → β} {g : β → α}
     (h : Function.LeftInverse g f) (C : ∀ a : α, γ (f a)) (a : α) :
@@ -1780,7 +1780,7 @@ theorem Function.LeftInverse.eq_rec_eq {α β : Sort _} {γ : β → Sort v} {f
 lean 3 declaration is
   forall {α : Sort.{u2}} {β : Sort.{u3}} {γ : β -> Sort.{u1}} {f : α -> β} {g : β -> α} (h : Function.LeftInverse.{u2, u3} α β g f) (C : forall (a : α), γ (f a)) (a : α), Eq.{u1} (γ (f a)) (Eq.recOn.{u1, u3} β (f (g (f a))) γ (f a) (congr_arg.{u2, u3} α β (g (f a)) a f (h a)) (C (g (f a)))) (C a)
 but is expected to have type
-  forall {α : Sort.{u2}} {β : Sort.{u1}} {γ : β -> Sort.{u3}} {f : α -> β} {g : β -> α} (h : Function.LeftInverse.{u2, u1} α β g f) (C : forall (a : α), γ (f a)) (a : α), Eq.{u3} (γ (f a)) (Eq.recOn.{u3, u1} β (f (g (f a))) (fun (x : β) (x._@.Mathlib.Logic.Function.Basic._hyg.11243 : Eq.{u1} β (f (g (f a))) x) => γ x) (f a) (congr_arg.{u2, u1} α β (g (f a)) a f (h a)) (C (g (f a)))) (C a)
+  forall {α : Sort.{u2}} {β : Sort.{u1}} {γ : β -> Sort.{u3}} {f : α -> β} {g : β -> α} (h : Function.LeftInverse.{u2, u1} α β g f) (C : forall (a : α), γ (f a)) (a : α), Eq.{u3} (γ (f a)) (Eq.recOn.{u3, u1} β (f (g (f a))) (fun (x : β) (x._@.Mathlib.Logic.Function.Basic._hyg.11247 : Eq.{u1} β (f (g (f a))) x) => γ x) (f a) (congr_arg.{u2, u1} α β (g (f a)) a f (h a)) (C (g (f a)))) (C a)
 Case conversion may be inaccurate. Consider using '#align function.left_inverse.eq_rec_on_eq Function.LeftInverse.eq_rec_on_eqₓ'. -/
 theorem Function.LeftInverse.eq_rec_on_eq {α β : Sort _} {γ : β → Sort v} {f : α → β} {g : β → α}
     (h : Function.LeftInverse g f) (C : ∀ a : α, γ (f a)) (a : α) :

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "8e663bd0869e714df9b9b2ba5a14136984d5153d",
+    "rev": "ba5bd03226df584593b34a3f16d80774aabfcb37",
     "name": "lean3port",
-    "inputRev?": "8e663bd0869e714df9b9b2ba5a14136984d5153d"}},
+    "inputRev?": "ba5bd03226df584593b34a3f16d80774aabfcb37"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "876c5e34e838b8bb3119b477132ed8204f65cb2c",
+    "rev": "67bb1670eb367d3073d64c94ed0f2d688083d627",
     "name": "mathlib",
-    "inputRev?": "876c5e34e838b8bb3119b477132ed8204f65cb2c"}},
+    "inputRev?": "67bb1670eb367d3073d64c94ed0f2d688083d627"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

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-03-30-04"
+def tag : String := "nightly-2023-03-30-06"
 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"@"8e663bd0869e714df9b9b2ba5a14136984d5153d"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"ba5bd03226df584593b34a3f16d80774aabfcb37"
 
 @[default_target]
 lean_lib Mathbin where