Trigger CI for leanprover-community/batteries#811

leanprover-community · Nov 2, 2024 · 0d82e3e · 0d82e3e
2 parents b62ef15 + 12bee1a
commit 0d82e3e
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 8 deletions.
diff --git a/Mathlib/Logic/Small/Basic.lean b/Mathlib/Logic/Small/Basic.lean
@@ -12,10 +12,9 @@ import Mathlib.Logic.Equiv.Set
 In particular we prove `small_of_injective` and `small_of_surjective`.
 -/
 
-universe u w v v'
-
-section
+assert_not_exists Countable
 
+universe u w v v'
 
 -- TODO(timotree3): lower the priority on this instance?
 -- This instance applies to every synthesis problem of the form `Small ↥s` for some set `s`,
@@ -66,5 +65,3 @@ instance small_sum {α β} [Small.{w} α] [Small.{w} β] : Small.{w} (α ⊕ β)
 
 instance small_set {α} [Small.{w} α] : Small.{w} (Set α) :=
   ⟨⟨Set (Shrink α), ⟨Equiv.Set.congr (equivShrink α)⟩⟩⟩
-
-end
diff --git a/Mathlib/RingTheory/Flat/Basic.lean b/Mathlib/RingTheory/Flat/Basic.lean
@@ -151,14 +151,14 @@ lemma equiv_iff (e : M ≃ₗ[R] N) : Flat R M ↔ Flat R N :=
 instance ulift [Module.Flat R M] : Module.Flat R (ULift.{v'} M) :=
   of_linearEquiv R M (ULift.{v'} M) ULift.moduleEquiv
 
--- Making this an instance cases an infinite sequence `M → ULift M → ULift (ULift M) → ...`.
+-- Making this an instance causes an infinite sequence `M → ULift M → ULift (ULift M) → ...`.
 lemma of_ulift [Module.Flat R (ULift.{v'} M)] : Module.Flat R M :=
   of_linearEquiv R (ULift.{v'} M) M ULift.moduleEquiv.symm
 
 instance shrink [Small.{v'} M] [Module.Flat R M] : Module.Flat R (Shrink.{v'} M) :=
   of_linearEquiv R M (Shrink.{v'} M) (Shrink.linearEquiv M R)
 
--- Making this an instance cases an infinite sequence `M → Shrink M → Shrink (Shrink M) → ...`.
+-- Making this an instance causes an infinite sequence `M → Shrink M → Shrink (Shrink M) → ...`.
 lemma of_shrink [Small.{v'} M] [Module.Flat R (Shrink.{v'} M)] :
     Module.Flat R M :=
   of_linearEquiv R (Shrink.{v'} M) M (Shrink.linearEquiv M R).symm

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "273182e922bc3f76b06d402015d54ab7dbee6537",
+   "rev": "8f33cf604130d860d235997aecaf3ccdcddd30cb",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "runLinter-default-module-detection",