bump to nightly-2023-04-25-12

mathlib commit leanprover-community/mathlib@2651125

Mathbin/CategoryTheory/Limits/Constructions/WeaklyInitial.lean

@@ -32,6 +32,7 @@ open Limits
 
 variable {C : Type u} [Category.{v} C]
 
+#print CategoryTheory.has_weakly_initial_of_weakly_initial_set_and_hasProducts /-
 /--
 If `C` has (small) products and a small weakly initial set of objects, then it has a weakly initial
 object.
@@ -40,7 +41,9 @@ theorem has_weakly_initial_of_weakly_initial_set_and_hasProducts [HasProducts.{v
     {B : ι → C} (hB : ∀ A : C, ∃ i, Nonempty (B i ⟶ A)) : ∃ T : C, ∀ X, Nonempty (T ⟶ X) :=
   ⟨∏ B, fun X => ⟨Pi.π _ _ ≫ (hB X).choose_spec.some⟩⟩
 #align category_theory.has_weakly_initial_of_weakly_initial_set_and_has_products CategoryTheory.has_weakly_initial_of_weakly_initial_set_and_hasProducts
+-/
 
+#print CategoryTheory.hasInitial_of_weakly_initial_and_hasWideEqualizers /-
 /-- If `C` has (small) wide equalizers and a weakly initial object, then it has an initial object.
 
 The initial object is constructed as the wide equalizer of all endomorphisms on the given weakly
@@ -69,6 +72,7 @@ theorem hasInitial_of_weakly_initial_and_hasWideEqualizers [HasWideEqualizers.{v
     apply equalizer.condition
   exact has_initial_of_unique (wide_equalizer (id : endos → endos))
 #align category_theory.has_initial_of_weakly_initial_and_has_wide_equalizers CategoryTheory.hasInitial_of_weakly_initial_and_hasWideEqualizers
+-/
 
 end CategoryTheory
 

Mathbin/CategoryTheory/Preadditive/Generator.lean

@@ -28,32 +28,46 @@ namespace CategoryTheory
 
 variable {C : Type u} [Category.{v} C] [Preadditive C]
 
+#print CategoryTheory.Preadditive.isSeparating_iff /-
 theorem Preadditive.isSeparating_iff (𝒢 : Set C) :
     IsSeparating 𝒢 ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ G ∈ 𝒢, ∀ (h : G ⟶ X), h ≫ f = 0) → f = 0 :=
   ⟨fun h𝒢 X Y f hf => h𝒢 _ _ (by simpa only [limits.comp_zero] using hf), fun h𝒢 X Y f g hfg =>
     sub_eq_zero.1 <| h𝒢 _ (by simpa only [preadditive.comp_sub, sub_eq_zero] using hfg)⟩
 #align category_theory.preadditive.is_separating_iff CategoryTheory.Preadditive.isSeparating_iff
+-/
 
+#print CategoryTheory.Preadditive.isCoseparating_iff /-
 theorem Preadditive.isCoseparating_iff (𝒢 : Set C) :
     IsCoseparating 𝒢 ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ G ∈ 𝒢, ∀ (h : Y ⟶ G), f ≫ h = 0) → f = 0 :=
   ⟨fun h𝒢 X Y f hf => h𝒢 _ _ (by simpa only [limits.zero_comp] using hf), fun h𝒢 X Y f g hfg =>
     sub_eq_zero.1 <| h𝒢 _ (by simpa only [preadditive.sub_comp, sub_eq_zero] using hfg)⟩
 #align category_theory.preadditive.is_coseparating_iff CategoryTheory.Preadditive.isCoseparating_iff
+-/
 
+#print CategoryTheory.Preadditive.isSeparator_iff /-
 theorem Preadditive.isSeparator_iff (G : C) :
     IsSeparator G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : G ⟶ X, h ≫ f = 0) → f = 0 :=
   ⟨fun hG X Y f hf => hG.def _ _ (by simpa only [limits.comp_zero] using hf), fun hG =>
     (isSeparator_def _).2 fun X Y f g hfg =>
       sub_eq_zero.1 <| hG _ (by simpa only [preadditive.comp_sub, sub_eq_zero] using hfg)⟩
 #align category_theory.preadditive.is_separator_iff CategoryTheory.Preadditive.isSeparator_iff
+-/
 
+#print CategoryTheory.Preadditive.isCoseparator_iff /-
 theorem Preadditive.isCoseparator_iff (G : C) :
     IsCoseparator G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : Y ⟶ G, f ≫ h = 0) → f = 0 :=
   ⟨fun hG X Y f hf => hG.def _ _ (by simpa only [limits.zero_comp] using hf), fun hG =>
     (isCoseparator_def _).2 fun X Y f g hfg =>
       sub_eq_zero.1 <| hG _ (by simpa only [preadditive.sub_comp, sub_eq_zero] using hfg)⟩
 #align category_theory.preadditive.is_coseparator_iff CategoryTheory.Preadditive.isCoseparator_iff
+-/
 
+/- warning: category_theory.is_separator_iff_faithful_preadditive_coyoneda -> CategoryTheory.isSeparator_iff_faithful_preadditiveCoyoneda is a dubious translation:
+lean 3 declaration is
+  forall {C : Type.{u2}} [_inst_1 : CategoryTheory.Category.{u1, u2} C] [_inst_2 : CategoryTheory.Preadditive.{u1, u2} C _inst_1] (G : C), Iff (CategoryTheory.IsSeparator.{u1, u2} C _inst_1 G) (CategoryTheory.Faithful.{u1, u1, u2, succ u1} C _inst_1 AddCommGroupCat.{u1} AddCommGroupCat.largeCategory.{u1} (CategoryTheory.Functor.obj.{u1, max u2 u1, u2, max u1 u2 (succ u1)} (Opposite.{succ u2} C) (CategoryTheory.Category.opposite.{u1, u2} C _inst_1) (CategoryTheory.Functor.{u1, u1, u2, succ u1} C _inst_1 AddCommGroupCat.{u1} AddCommGroupCat.largeCategory.{u1}) (CategoryTheory.Functor.category.{u1, u1, u2, succ u1} C _inst_1 AddCommGroupCat.{u1} AddCommGroupCat.largeCategory.{u1}) (CategoryTheory.preadditiveCoyoneda.{u1, u2} C _inst_1 _inst_2) (Opposite.op.{succ u2} C G)))
+but is expected to have type
+  forall {C : Type.{u2}} [_inst_1 : CategoryTheory.Category.{u1, u2} C] [_inst_2 : CategoryTheory.Preadditive.{u1, u2} C _inst_1] (G : C), Iff (CategoryTheory.IsSeparator.{u1, u2} C _inst_1 G) (CategoryTheory.Faithful.{u1, u1, u2, succ u1} C _inst_1 AddCommGroupCat.{u1} AddCommGroupCat.largeCategory.{u1} (Prefunctor.obj.{succ u1, max (succ u2) (succ u1), u2, max u2 (succ u1)} (Opposite.{succ u2} C) (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} (Opposite.{succ u2} C) (CategoryTheory.Category.toCategoryStruct.{u1, u2} (Opposite.{succ u2} C) (CategoryTheory.Category.opposite.{u1, u2} C _inst_1))) (CategoryTheory.Functor.{u1, u1, u2, succ u1} C _inst_1 AddCommGroupCat.{u1} AddCommGroupCat.largeCategory.{u1}) (CategoryTheory.CategoryStruct.toQuiver.{max u2 u1, max u2 (succ u1)} (CategoryTheory.Functor.{u1, u1, u2, succ u1} C _inst_1 AddCommGroupCat.{u1} AddCommGroupCat.largeCategory.{u1}) (CategoryTheory.Category.toCategoryStruct.{max u2 u1, max u2 (succ u1)} (CategoryTheory.Functor.{u1, u1, u2, succ u1} C _inst_1 AddCommGroupCat.{u1} AddCommGroupCat.largeCategory.{u1}) (CategoryTheory.Functor.category.{u1, u1, u2, succ u1} C _inst_1 AddCommGroupCat.{u1} AddCommGroupCat.largeCategory.{u1}))) (CategoryTheory.Functor.toPrefunctor.{u1, max u2 u1, u2, max u2 (succ u1)} (Opposite.{succ u2} C) (CategoryTheory.Category.opposite.{u1, u2} C _inst_1) (CategoryTheory.Functor.{u1, u1, u2, succ u1} C _inst_1 AddCommGroupCat.{u1} AddCommGroupCat.largeCategory.{u1}) (CategoryTheory.Functor.category.{u1, u1, u2, succ u1} C _inst_1 AddCommGroupCat.{u1} AddCommGroupCat.largeCategory.{u1}) (CategoryTheory.preadditiveCoyoneda.{u1, u2} C _inst_1 _inst_2)) (Opposite.op.{succ u2} C G)))
+Case conversion may be inaccurate. Consider using '#align category_theory.is_separator_iff_faithful_preadditive_coyoneda CategoryTheory.isSeparator_iff_faithful_preadditiveCoyonedaₓ'. -/
 theorem isSeparator_iff_faithful_preadditiveCoyoneda (G : C) :
     IsSeparator G ↔ Faithful (preadditiveCoyoneda.obj (op G)) :=
   by
@@ -62,13 +76,25 @@ theorem isSeparator_iff_faithful_preadditiveCoyoneda (G : C) :
   exact ⟨fun h => faithful.of_comp _ (forget AddCommGroupCat), fun h => faithful.comp _ _⟩
 #align category_theory.is_separator_iff_faithful_preadditive_coyoneda CategoryTheory.isSeparator_iff_faithful_preadditiveCoyoneda
 
+/- warning: category_theory.is_separator_iff_faithful_preadditive_coyoneda_obj -> CategoryTheory.isSeparator_iff_faithful_preadditiveCoyonedaObj is a dubious translation:
+lean 3 declaration is
+  forall {C : Type.{u2}} [_inst_1 : CategoryTheory.Category.{u1, u2} C] [_inst_2 : CategoryTheory.Preadditive.{u1, u2} C _inst_1] (G : C), Iff (CategoryTheory.IsSeparator.{u1, u2} C _inst_1 G) (CategoryTheory.Faithful.{u1, u1, u2, succ u1} C _inst_1 (ModuleCat.{u1, u1} (CategoryTheory.End.{u1, u2} (Opposite.{succ u2} C) (CategoryTheory.Category.toCategoryStruct.{u1, u2} (Opposite.{succ u2} C) (CategoryTheory.Category.opposite.{u1, u2} C _inst_1)) (Opposite.op.{succ u2} C G)) (CategoryTheory.Preadditive.CategoryTheory.End.ring.{u1, u2} (Opposite.{succ u2} C) (CategoryTheory.Category.opposite.{u1, u2} C _inst_1) (CategoryTheory.Opposite.preadditive.{u2, u1} C _inst_1 _inst_2) (Opposite.op.{succ u2} C G))) (ModuleCat.moduleCategory.{u1, u1} (CategoryTheory.End.{u1, u2} (Opposite.{succ u2} C) (CategoryTheory.Category.toCategoryStruct.{u1, u2} (Opposite.{succ u2} C) (CategoryTheory.Category.opposite.{u1, u2} C _inst_1)) (Opposite.op.{succ u2} C G)) (CategoryTheory.Preadditive.CategoryTheory.End.ring.{u1, u2} (Opposite.{succ u2} C) (CategoryTheory.Category.opposite.{u1, u2} C _inst_1) (CategoryTheory.Opposite.preadditive.{u2, u1} C _inst_1 _inst_2) (Opposite.op.{succ u2} C G))) (CategoryTheory.preadditiveCoyonedaObj.{u1, u2} C _inst_1 _inst_2 (Opposite.op.{succ u2} C G)))
+but is expected to have type
+  forall {C : Type.{u2}} [_inst_1 : CategoryTheory.Category.{u1, u2} C] [_inst_2 : CategoryTheory.Preadditive.{u1, u2} C _inst_1] (G : C), Iff (CategoryTheory.IsSeparator.{u1, u2} C _inst_1 G) (CategoryTheory.Faithful.{u1, u1, u2, succ u1} C _inst_1 (ModuleCat.{u1, u1} (CategoryTheory.End.{u1, u2} (Opposite.{succ u2} C) (CategoryTheory.Category.toCategoryStruct.{u1, u2} (Opposite.{succ u2} C) (CategoryTheory.Category.opposite.{u1, u2} C _inst_1)) (Opposite.op.{succ u2} C G)) (CategoryTheory.Preadditive.instRingEndToCategoryStruct.{u1, u2} (Opposite.{succ u2} C) (CategoryTheory.Category.opposite.{u1, u2} C _inst_1) (CategoryTheory.instPreadditiveOppositeOpposite.{u2, u1} C _inst_1 _inst_2) (Opposite.op.{succ u2} C G))) (ModuleCat.moduleCategory.{u1, u1} (CategoryTheory.End.{u1, u2} (Opposite.{succ u2} C) (CategoryTheory.Category.toCategoryStruct.{u1, u2} (Opposite.{succ u2} C) (CategoryTheory.Category.opposite.{u1, u2} C _inst_1)) (Opposite.op.{succ u2} C G)) (CategoryTheory.Preadditive.instRingEndToCategoryStruct.{u1, u2} (Opposite.{succ u2} C) (CategoryTheory.Category.opposite.{u1, u2} C _inst_1) (CategoryTheory.instPreadditiveOppositeOpposite.{u2, u1} C _inst_1 _inst_2) (Opposite.op.{succ u2} C G))) (CategoryTheory.preadditiveCoyonedaObj.{u1, u2} C _inst_1 _inst_2 (Opposite.op.{succ u2} C G)))
+Case conversion may be inaccurate. Consider using '#align category_theory.is_separator_iff_faithful_preadditive_coyoneda_obj CategoryTheory.isSeparator_iff_faithful_preadditiveCoyonedaObjₓ'. -/
 theorem isSeparator_iff_faithful_preadditiveCoyonedaObj (G : C) :
     IsSeparator G ↔ Faithful (preadditiveCoyonedaObj (op G)) :=
   by
   rw [is_separator_iff_faithful_preadditive_coyoneda, preadditive_coyoneda_obj_2]
   exact ⟨fun h => faithful.of_comp _ (forget₂ _ AddCommGroupCat.{v}), fun h => faithful.comp _ _⟩
 #align category_theory.is_separator_iff_faithful_preadditive_coyoneda_obj CategoryTheory.isSeparator_iff_faithful_preadditiveCoyonedaObj
 
+/- warning: category_theory.is_coseparator_iff_faithful_preadditive_yoneda -> CategoryTheory.isCoseparator_iff_faithful_preadditiveYoneda is a dubious translation:
+lean 3 declaration is
+  forall {C : Type.{u2}} [_inst_1 : CategoryTheory.Category.{u1, u2} C] [_inst_2 : CategoryTheory.Preadditive.{u1, u2} C _inst_1] (G : C), Iff (CategoryTheory.IsCoseparator.{u1, u2} C _inst_1 G) (CategoryTheory.Faithful.{u1, u1, u2, succ u1} (Opposite.{succ u2} C) (CategoryTheory.Category.opposite.{u1, u2} C _inst_1) AddCommGroupCat.{u1} AddCommGroupCat.largeCategory.{u1} (CategoryTheory.Functor.obj.{u1, max u2 u1, u2, max u1 u2 (succ u1)} C _inst_1 (CategoryTheory.Functor.{u1, u1, u2, succ u1} (Opposite.{succ u2} C) (CategoryTheory.Category.opposite.{u1, u2} C _inst_1) AddCommGroupCat.{u1} AddCommGroupCat.largeCategory.{u1}) (CategoryTheory.Functor.category.{u1, u1, u2, succ u1} (Opposite.{succ u2} C) (CategoryTheory.Category.opposite.{u1, u2} C _inst_1) AddCommGroupCat.{u1} AddCommGroupCat.largeCategory.{u1}) (CategoryTheory.preadditiveYoneda.{u1, u2} C _inst_1 _inst_2) G))
+but is expected to have type
+  forall {C : Type.{u2}} [_inst_1 : CategoryTheory.Category.{u1, u2} C] [_inst_2 : CategoryTheory.Preadditive.{u1, u2} C _inst_1] (G : C), Iff (CategoryTheory.IsCoseparator.{u1, u2} C _inst_1 G) (CategoryTheory.Faithful.{u1, u1, u2, succ u1} (Opposite.{succ u2} C) (CategoryTheory.Category.opposite.{u1, u2} C _inst_1) AddCommGroupCat.{u1} AddCommGroupCat.largeCategory.{u1} (Prefunctor.obj.{succ u1, max (succ u1) (succ u2), u2, max (succ u1) u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_1)) (CategoryTheory.Functor.{u1, u1, u2, succ u1} (Opposite.{succ u2} C) (CategoryTheory.Category.opposite.{u1, u2} C _inst_1) AddCommGroupCat.{u1} AddCommGroupCat.largeCategory.{u1}) (CategoryTheory.CategoryStruct.toQuiver.{max u2 u1, max u2 (succ u1)} (CategoryTheory.Functor.{u1, u1, u2, succ u1} (Opposite.{succ u2} C) (CategoryTheory.Category.opposite.{u1, u2} C _inst_1) AddCommGroupCat.{u1} AddCommGroupCat.largeCategory.{u1}) (CategoryTheory.Category.toCategoryStruct.{max u2 u1, max u2 (succ u1)} (CategoryTheory.Functor.{u1, u1, u2, succ u1} (Opposite.{succ u2} C) (CategoryTheory.Category.opposite.{u1, u2} C _inst_1) AddCommGroupCat.{u1} AddCommGroupCat.largeCategory.{u1}) (CategoryTheory.Functor.category.{u1, u1, u2, succ u1} (Opposite.{succ u2} C) (CategoryTheory.Category.opposite.{u1, u2} C _inst_1) AddCommGroupCat.{u1} AddCommGroupCat.largeCategory.{u1}))) (CategoryTheory.Functor.toPrefunctor.{u1, max u2 u1, u2, max u2 (succ u1)} C _inst_1 (CategoryTheory.Functor.{u1, u1, u2, succ u1} (Opposite.{succ u2} C) (CategoryTheory.Category.opposite.{u1, u2} C _inst_1) AddCommGroupCat.{u1} AddCommGroupCat.largeCategory.{u1}) (CategoryTheory.Functor.category.{u1, u1, u2, succ u1} (Opposite.{succ u2} C) (CategoryTheory.Category.opposite.{u1, u2} C _inst_1) AddCommGroupCat.{u1} AddCommGroupCat.largeCategory.{u1}) (CategoryTheory.preadditiveYoneda.{u1, u2} C _inst_1 _inst_2)) G))
+Case conversion may be inaccurate. Consider using '#align category_theory.is_coseparator_iff_faithful_preadditive_yoneda CategoryTheory.isCoseparator_iff_faithful_preadditiveYonedaₓ'. -/
 theorem isCoseparator_iff_faithful_preadditiveYoneda (G : C) :
     IsCoseparator G ↔ Faithful (preadditiveYoneda.obj G) :=
   by
@@ -77,6 +103,12 @@ theorem isCoseparator_iff_faithful_preadditiveYoneda (G : C) :
   exact ⟨fun h => faithful.of_comp _ (forget AddCommGroupCat), fun h => faithful.comp _ _⟩
 #align category_theory.is_coseparator_iff_faithful_preadditive_yoneda CategoryTheory.isCoseparator_iff_faithful_preadditiveYoneda
 
+/- warning: category_theory.is_coseparator_iff_faithful_preadditive_yoneda_obj -> CategoryTheory.isCoseparator_iff_faithful_preadditiveYonedaObj is a dubious translation:
+lean 3 declaration is
+  forall {C : Type.{u2}} [_inst_1 : CategoryTheory.Category.{u1, u2} C] [_inst_2 : CategoryTheory.Preadditive.{u1, u2} C _inst_1] (G : C), Iff (CategoryTheory.IsCoseparator.{u1, u2} C _inst_1 G) (CategoryTheory.Faithful.{u1, u1, u2, succ u1} (Opposite.{succ u2} C) (CategoryTheory.Category.opposite.{u1, u2} C _inst_1) (ModuleCat.{u1, u1} (CategoryTheory.End.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_1) G) (CategoryTheory.Preadditive.CategoryTheory.End.ring.{u1, u2} C _inst_1 _inst_2 G)) (ModuleCat.moduleCategory.{u1, u1} (CategoryTheory.End.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_1) G) (CategoryTheory.Preadditive.CategoryTheory.End.ring.{u1, u2} C _inst_1 _inst_2 G)) (CategoryTheory.preadditiveYonedaObj.{u1, u2} C _inst_1 _inst_2 G))
+but is expected to have type
+  forall {C : Type.{u2}} [_inst_1 : CategoryTheory.Category.{u1, u2} C] [_inst_2 : CategoryTheory.Preadditive.{u1, u2} C _inst_1] (G : C), Iff (CategoryTheory.IsCoseparator.{u1, u2} C _inst_1 G) (CategoryTheory.Faithful.{u1, u1, u2, succ u1} (Opposite.{succ u2} C) (CategoryTheory.Category.opposite.{u1, u2} C _inst_1) (ModuleCat.{u1, u1} (CategoryTheory.End.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_1) G) (CategoryTheory.Preadditive.instRingEndToCategoryStruct.{u1, u2} C _inst_1 _inst_2 G)) (ModuleCat.moduleCategory.{u1, u1} (CategoryTheory.End.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_1) G) (CategoryTheory.Preadditive.instRingEndToCategoryStruct.{u1, u2} C _inst_1 _inst_2 G)) (CategoryTheory.preadditiveYonedaObj.{u1, u2} C _inst_1 _inst_2 G))
+Case conversion may be inaccurate. Consider using '#align category_theory.is_coseparator_iff_faithful_preadditive_yoneda_obj CategoryTheory.isCoseparator_iff_faithful_preadditiveYonedaObjₓ'. -/
 theorem isCoseparator_iff_faithful_preadditiveYonedaObj (G : C) :
     IsCoseparator G ↔ Faithful (preadditiveYonedaObj G) :=
   by

lake-manifest.json

@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "1f9241f09dd2e5d82d6c21bcf643ad9c04fe7334",
+    "rev": "c66cdea27c43c4a581feb7626b81a5124a3631b4",
     "name": "lean3port",
-    "inputRev?": "1f9241f09dd2e5d82d6c21bcf643ad9c04fe7334"}},
+    "inputRev?": "c66cdea27c43c4a581feb7626b81a5124a3631b4"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "b237400a22f07afaf1f047b35bb179b16c1fb1c6",
+    "rev": "26e27864b672e8f2434880718ccaf2ed17f291b7",
     "name": "mathlib",
-    "inputRev?": "b237400a22f07afaf1f047b35bb179b16c1fb1c6"}},
+    "inputRev?": "26e27864b672e8f2434880718ccaf2ed17f291b7"}},
   {"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-25-10"
+def tag : String := "nightly-2023-04-25-12"
 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"@"1f9241f09dd2e5d82d6c21bcf643ad9c04fe7334"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"c66cdea27c43c4a581feb7626b81a5124a3631b4"
 
 @[default_target]
 lean_lib Mathbin where