bump to nightly-2023-04-06-18

mathlib commit leanprover-community/mathlib@06a655b

Mathbin/Data/Multiset/Basic.lean

@@ -4836,10 +4836,12 @@ def Pairwise (r : α → α → Prop) (m : Multiset α) : Prop :=
 #align multiset.pairwise Multiset.Pairwise
 -/
 
+#print Multiset.pairwise_zero /-
 @[simp]
 theorem pairwise_zero (r : α → α → Prop) : Multiset.Pairwise r 0 :=
   ⟨[], rfl, List.Pairwise.nil⟩
 #align multiset.pairwise_zero Multiset.pairwise_zero
+-/
 
 #print Multiset.pairwise_coe_iff /-
 theorem pairwise_coe_iff {r : α → α → Prop} {l : List α} :

Mathbin/RingTheory/QuotientNoetherian.lean

@@ -16,8 +16,10 @@ import Mathbin.RingTheory.QuotientNilpotent
 -/
 
 
+#print Ideal.Quotient.isNoetherianRing /-
 instance Ideal.Quotient.isNoetherianRing {R : Type _} [CommRing R] [h : IsNoetherianRing R]
     (I : Ideal R) : IsNoetherianRing (R ⧸ I) :=
   isNoetherianRing_iff.mpr <| isNoetherian_of_tower R <| Submodule.Quotient.isNoetherian _
 #align ideal.quotient.is_noetherian_ring Ideal.Quotient.isNoetherianRing
+-/
 

Mathbin/Topology/Algebra/Module/Simple.lean

@@ -26,6 +26,12 @@ variable {R : Type u} {M : Type v} {N : Type w} [Ring R] [TopologicalSpace R] [T
   [AddCommGroup M] [AddCommGroup N] [Module R M] [ContinuousSMul R M] [Module R N] [ContinuousAdd M]
   [IsSimpleModule R N]
 
+/- warning: linear_map.is_closed_or_dense_ker -> LinearMap.isClosed_or_dense_ker is a dubious translation:
+lean 3 declaration is
+  forall {R : Type.{u1}} {M : Type.{u2}} {N : Type.{u3}} [_inst_1 : Ring.{u1} R] [_inst_2 : TopologicalSpace.{u1} R] [_inst_3 : TopologicalSpace.{u2} M] [_inst_4 : AddCommGroup.{u2} M] [_inst_5 : AddCommGroup.{u3} N] [_inst_6 : Module.{u1, u2} R M (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4)] [_inst_7 : ContinuousSMul.{u1, u2} R M (SMulZeroClass.toHasSmul.{u1, u2} R M (AddZeroClass.toHasZero.{u2} M (AddMonoid.toAddZeroClass.{u2} M (AddCommMonoid.toAddMonoid.{u2} M (AddCommGroup.toAddCommMonoid.{u2} M _inst_4)))) (SMulWithZero.toSmulZeroClass.{u1, u2} R M (MulZeroClass.toHasZero.{u1} R (MulZeroOneClass.toMulZeroClass.{u1} R (MonoidWithZero.toMulZeroOneClass.{u1} R (Semiring.toMonoidWithZero.{u1} R (Ring.toSemiring.{u1} R _inst_1))))) (AddZeroClass.toHasZero.{u2} M (AddMonoid.toAddZeroClass.{u2} M (AddCommMonoid.toAddMonoid.{u2} M (AddCommGroup.toAddCommMonoid.{u2} M _inst_4)))) (MulActionWithZero.toSMulWithZero.{u1, u2} R M (Semiring.toMonoidWithZero.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (AddZeroClass.toHasZero.{u2} M (AddMonoid.toAddZeroClass.{u2} M (AddCommMonoid.toAddMonoid.{u2} M (AddCommGroup.toAddCommMonoid.{u2} M _inst_4)))) (Module.toMulActionWithZero.{u1, u2} R M (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) _inst_6)))) _inst_2 _inst_3] [_inst_8 : Module.{u1, u3} R N (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} N _inst_5)] [_inst_9 : ContinuousAdd.{u2} M _inst_3 (AddZeroClass.toHasAdd.{u2} M (AddMonoid.toAddZeroClass.{u2} M (SubNegMonoid.toAddMonoid.{u2} M (AddGroup.toSubNegMonoid.{u2} M (AddCommGroup.toAddGroup.{u2} M _inst_4)))))] [_inst_10 : IsSimpleModule.{u1, u3} R _inst_1 N _inst_5 _inst_8] (l : LinearMap.{u1, u1, u2, u3} R R (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) M N (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) (AddCommGroup.toAddCommMonoid.{u3} N _inst_5) _inst_6 _inst_8), Or (IsClosed.{u2} M _inst_3 ((fun (a : Type.{u2}) (b : Type.{u2}) [self : HasLiftT.{succ u2, succ u2} a b] => self.0) (Submodule.{u1, u2} R M (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) _inst_6) (Set.{u2} M) (HasLiftT.mk.{succ u2, succ u2} (Submodule.{u1, u2} R M (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) _inst_6) (Set.{u2} M) (CoeTCₓ.coe.{succ u2, succ u2} (Submodule.{u1, u2} R M (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) _inst_6) (Set.{u2} M) (SetLike.Set.hasCoeT.{u2, u2} (Submodule.{u1, u2} R M (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) _inst_6) M (Submodule.setLike.{u1, u2} R M (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) _inst_6)))) (LinearMap.ker.{u1, u1, u2, u3, max u2 u3} R R M N (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) (AddCommGroup.toAddCommMonoid.{u3} N _inst_5) _inst_6 _inst_8 (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) (LinearMap.{u1, u1, u2, u3} R R (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) M N (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) (AddCommGroup.toAddCommMonoid.{u3} N _inst_5) _inst_6 _inst_8) (LinearMap.semilinearMapClass.{u1, u1, u2, u3} R R M N (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) (AddCommGroup.toAddCommMonoid.{u3} N _inst_5) _inst_6 _inst_8 (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1)))) l))) (Dense.{u2} M _inst_3 ((fun (a : Type.{u2}) (b : Type.{u2}) [self : HasLiftT.{succ u2, succ u2} a b] => self.0) (Submodule.{u1, u2} R M (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) _inst_6) (Set.{u2} M) (HasLiftT.mk.{succ u2, succ u2} (Submodule.{u1, u2} R M (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) _inst_6) (Set.{u2} M) (CoeTCₓ.coe.{succ u2, succ u2} (Submodule.{u1, u2} R M (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) _inst_6) (Set.{u2} M) (SetLike.Set.hasCoeT.{u2, u2} (Submodule.{u1, u2} R M (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) _inst_6) M (Submodule.setLike.{u1, u2} R M (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) _inst_6)))) (LinearMap.ker.{u1, u1, u2, u3, max u2 u3} R R M N (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) (AddCommGroup.toAddCommMonoid.{u3} N _inst_5) _inst_6 _inst_8 (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) (LinearMap.{u1, u1, u2, u3} R R (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1))) M N (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) (AddCommGroup.toAddCommMonoid.{u3} N _inst_5) _inst_6 _inst_8) (LinearMap.semilinearMapClass.{u1, u1, u2, u3} R R M N (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) (AddCommGroup.toAddCommMonoid.{u3} N _inst_5) _inst_6 _inst_8 (RingHom.id.{u1} R (Semiring.toNonAssocSemiring.{u1} R (Ring.toSemiring.{u1} R _inst_1)))) l)))
+but is expected to have type
+  forall {R : Type.{u1}} {M : Type.{u2}} {N : Type.{u3}} [_inst_1 : Ring.{u1} R] [_inst_2 : TopologicalSpace.{u1} R] [_inst_3 : TopologicalSpace.{u2} M] [_inst_4 : AddCommGroup.{u2} M] [_inst_5 : AddCommGroup.{u3} N] [_inst_6 : Module.{u1, u2} R M (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4)] [_inst_7 : ContinuousSMul.{u1, u2} R M (SMulZeroClass.toSMul.{u1, u2} R M (NegZeroClass.toZero.{u2} M (SubNegZeroMonoid.toNegZeroClass.{u2} M (SubtractionMonoid.toSubNegZeroMonoid.{u2} M (SubtractionCommMonoid.toSubtractionMonoid.{u2} M (AddCommGroup.toDivisionAddCommMonoid.{u2} M _inst_4))))) (SMulWithZero.toSMulZeroClass.{u1, u2} R M (MonoidWithZero.toZero.{u1} R (Semiring.toMonoidWithZero.{u1} R (Ring.toSemiring.{u1} R _inst_1))) (NegZeroClass.toZero.{u2} M (SubNegZeroMonoid.toNegZeroClass.{u2} M (SubtractionMonoid.toSubNegZeroMonoid.{u2} M (SubtractionCommMonoid.toSubtractionMonoid.{u2} M (AddCommGroup.toDivisionAddCommMonoid.{u2} M _inst_4))))) (MulActionWithZero.toSMulWithZero.{u1, u2} R M (Semiring.toMonoidWithZero.{u1} R (Ring.toSemiring.{u1} R _inst_1)) (NegZeroClass.toZero.{u2} M (SubNegZeroMonoid.toNegZeroClass.{u2} M (SubtractionMonoid.toSubNegZeroMonoid.{u2} M (SubtractionCommMonoid.toSubtractionMonoid.{u2} M (AddCommGroup.toDivisionAddCommMonoid.{u2} M _inst_4))))) (Module.toMulActionWithZero.{u1, u2} R M (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) _inst_6)))) _inst_2 _inst_3] [_inst_8 : Module.{u1, u3} R N (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u3} N _inst_5)] [_inst_9 : ContinuousAdd.{u2} M _inst_3 (AddZeroClass.toAdd.{u2} M (AddMonoid.toAddZeroClass.{u2} M (SubNegMonoid.toAddMonoid.{u2} M (AddGroup.toSubNegMonoid.{u2} M (AddCommGroup.toAddGroup.{u2} M _inst_4)))))] [_inst_10 : IsSimpleModule.{u1, u3} R _inst_1 N _inst_5 _inst_8] (l : LinearMap.{u1, u1, u2, u3} R R (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (RingHom.id.{u1} R (NonAssocRing.toNonAssocSemiring.{u1} R (Ring.toNonAssocRing.{u1} R _inst_1))) M N (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) (AddCommGroup.toAddCommMonoid.{u3} N _inst_5) _inst_6 _inst_8), Or (IsClosed.{u2} M _inst_3 (SetLike.coe.{u2, u2} (Submodule.{u1, u2} R M (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) _inst_6) M (Submodule.setLike.{u1, u2} R M (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) _inst_6) (LinearMap.ker.{u1, u1, u2, u3, max u2 u3} R R M N (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) (AddCommGroup.toAddCommMonoid.{u3} N _inst_5) _inst_6 _inst_8 (RingHom.id.{u1} R (NonAssocRing.toNonAssocSemiring.{u1} R (Ring.toNonAssocRing.{u1} R _inst_1))) (LinearMap.{u1, u1, u2, u3} R R (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (RingHom.id.{u1} R (NonAssocRing.toNonAssocSemiring.{u1} R (Ring.toNonAssocRing.{u1} R _inst_1))) M N (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) (AddCommGroup.toAddCommMonoid.{u3} N _inst_5) _inst_6 _inst_8) (LinearMap.instSemilinearMapClassLinearMap.{u1, u1, u2, u3} R R M N (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) (AddCommGroup.toAddCommMonoid.{u3} N _inst_5) _inst_6 _inst_8 (RingHom.id.{u1} R (NonAssocRing.toNonAssocSemiring.{u1} R (Ring.toNonAssocRing.{u1} R _inst_1)))) l))) (Dense.{u2} M _inst_3 (SetLike.coe.{u2, u2} (Submodule.{u1, u2} R M (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) _inst_6) M (Submodule.setLike.{u1, u2} R M (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) _inst_6) (LinearMap.ker.{u1, u1, u2, u3, max u2 u3} R R M N (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) (AddCommGroup.toAddCommMonoid.{u3} N _inst_5) _inst_6 _inst_8 (RingHom.id.{u1} R (NonAssocRing.toNonAssocSemiring.{u1} R (Ring.toNonAssocRing.{u1} R _inst_1))) (LinearMap.{u1, u1, u2, u3} R R (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (RingHom.id.{u1} R (NonAssocRing.toNonAssocSemiring.{u1} R (Ring.toNonAssocRing.{u1} R _inst_1))) M N (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) (AddCommGroup.toAddCommMonoid.{u3} N _inst_5) _inst_6 _inst_8) (LinearMap.instSemilinearMapClassLinearMap.{u1, u1, u2, u3} R R M N (Ring.toSemiring.{u1} R _inst_1) (Ring.toSemiring.{u1} R _inst_1) (AddCommGroup.toAddCommMonoid.{u2} M _inst_4) (AddCommGroup.toAddCommMonoid.{u3} N _inst_5) _inst_6 _inst_8 (RingHom.id.{u1} R (NonAssocRing.toNonAssocSemiring.{u1} R (Ring.toNonAssocRing.{u1} R _inst_1)))) l)))
+Case conversion may be inaccurate. Consider using '#align linear_map.is_closed_or_dense_ker LinearMap.isClosed_or_dense_kerₓ'. -/
 /-- The kernel of a linear map taking values in a simple module over the base ring is closed or
 dense. Applies, e.g., to the case when `R = N` is a division ring. -/
 theorem LinearMap.isClosed_or_dense_ker (l : M →ₗ[R] N) :

Mathbin/Topology/Algebra/UniformFilterBasis.lean

@@ -30,18 +30,28 @@ namespace AddGroupFilterBasis
 
 variable {G : Type _} [AddCommGroup G] (B : AddGroupFilterBasis G)
 
+#print AddGroupFilterBasis.uniformSpace /-
 /-- The uniform space structure associated to an abelian group filter basis via the associated
 topological abelian group structure. -/
 protected def uniformSpace : UniformSpace G :=
   @TopologicalAddGroup.toUniformSpace G _ B.topology B.isTopologicalAddGroup
 #align add_group_filter_basis.uniform_space AddGroupFilterBasis.uniformSpace
+-/
 
+#print AddGroupFilterBasis.uniformAddGroup /-
 /-- The uniform space structure associated to an abelian group filter basis via the associated
 topological abelian group structure is compatible with its group structure. -/
 protected theorem uniformAddGroup : @UniformAddGroup G B.UniformSpace _ :=
   @comm_topologicalAddGroup_is_uniform G _ B.topology B.isTopologicalAddGroup
 #align add_group_filter_basis.uniform_add_group AddGroupFilterBasis.uniformAddGroup
+-/
 
+/- warning: add_group_filter_basis.cauchy_iff -> AddGroupFilterBasis.cauchy_iff is a dubious translation:
+lean 3 declaration is
+  forall {G : Type.{u1}} [_inst_1 : AddCommGroup.{u1} G] (B : AddGroupFilterBasis.{u1} G (AddCommGroup.toAddGroup.{u1} G _inst_1)) {F : Filter.{u1} G}, Iff (Cauchy.{u1} G (AddGroupFilterBasis.uniformSpace.{u1} G _inst_1 B) F) (And (Filter.NeBot.{u1} G F) (forall (U : Set.{u1} G), (Membership.Mem.{u1, u1} (Set.{u1} G) (AddGroupFilterBasis.{u1} G (AddCommGroup.toAddGroup.{u1} G _inst_1)) (AddGroupFilterBasis.hasMem.{u1} G (AddCommGroup.toAddGroup.{u1} G _inst_1)) U B) -> (Exists.{succ u1} (Set.{u1} G) (fun (M : Set.{u1} G) => Exists.{0} (Membership.Mem.{u1, u1} (Set.{u1} G) (Filter.{u1} G) (Filter.hasMem.{u1} G) M F) (fun (H : Membership.Mem.{u1, u1} (Set.{u1} G) (Filter.{u1} G) (Filter.hasMem.{u1} G) M F) => forall (x : G), (Membership.Mem.{u1, u1} G (Set.{u1} G) (Set.hasMem.{u1} G) x M) -> (forall (y : G), (Membership.Mem.{u1, u1} G (Set.{u1} G) (Set.hasMem.{u1} G) y M) -> (Membership.Mem.{u1, u1} G (Set.{u1} G) (Set.hasMem.{u1} G) (HSub.hSub.{u1, u1, u1} G G G (instHSub.{u1} G (SubNegMonoid.toHasSub.{u1} G (AddGroup.toSubNegMonoid.{u1} G (AddCommGroup.toAddGroup.{u1} G _inst_1)))) y x) U)))))))
+but is expected to have type
+  forall {G : Type.{u1}} [_inst_1 : AddCommGroup.{u1} G] (B : AddGroupFilterBasis.{u1} G (AddCommGroup.toAddGroup.{u1} G _inst_1)) {F : Filter.{u1} G}, Iff (Cauchy.{u1} G (AddGroupFilterBasis.uniformSpace.{u1} G _inst_1 B) F) (And (Filter.NeBot.{u1} G F) (forall (U : Set.{u1} G), (Membership.mem.{u1, u1} (Set.{u1} G) (AddGroupFilterBasis.{u1} G (AddCommGroup.toAddGroup.{u1} G _inst_1)) (AddGroupFilterBasis.instMembershipSetAddGroupFilterBasis.{u1} G (AddCommGroup.toAddGroup.{u1} G _inst_1)) U B) -> (Exists.{succ u1} (Set.{u1} G) (fun (M : Set.{u1} G) => And (Membership.mem.{u1, u1} (Set.{u1} G) (Filter.{u1} G) (instMembershipSetFilter.{u1} G) M F) (forall (x : G), (Membership.mem.{u1, u1} G (Set.{u1} G) (Set.instMembershipSet.{u1} G) x M) -> (forall (y : G), (Membership.mem.{u1, u1} G (Set.{u1} G) (Set.instMembershipSet.{u1} G) y M) -> (Membership.mem.{u1, u1} G (Set.{u1} G) (Set.instMembershipSet.{u1} G) (HSub.hSub.{u1, u1, u1} G G G (instHSub.{u1} G (SubNegMonoid.toSub.{u1} G (AddGroup.toSubNegMonoid.{u1} G (AddCommGroup.toAddGroup.{u1} G _inst_1)))) y x) U)))))))
+Case conversion may be inaccurate. Consider using '#align add_group_filter_basis.cauchy_iff AddGroupFilterBasis.cauchy_iffₓ'. -/
 /- ./././Mathport/Syntax/Translate/Basic.lean:635:2: warning: expanding binder collection (x y «expr ∈ » M) -/
 /- ./././Mathport/Syntax/Translate/Basic.lean:635:2: warning: expanding binder collection (x y «expr ∈ » M) -/
 theorem cauchy_iff {F : Filter G} :

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "34fd1cd4d80765166ce16a3af30272f36ca073d0",
+    "rev": "a78f761a6b966a183b80825070abdb3b43e8940b",
     "name": "lean3port",
-    "inputRev?": "34fd1cd4d80765166ce16a3af30272f36ca073d0"}},
+    "inputRev?": "a78f761a6b966a183b80825070abdb3b43e8940b"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "37b23dab695396bee39b27841e2475e01df12874",
+    "rev": "da954ad14736d54850445a7710e2a7e796261a0b",
     "name": "mathlib",
-    "inputRev?": "37b23dab695396bee39b27841e2475e01df12874"}},
+    "inputRev?": "da954ad14736d54850445a7710e2a7e796261a0b"}},
   {"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-04-06-16"
+def tag : String := "nightly-2023-04-06-18"
 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"@"34fd1cd4d80765166ce16a3af30272f36ca073d0"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"a78f761a6b966a183b80825070abdb3b43e8940b"
 
 @[default_target]
 lean_lib Mathbin where