chore: adaptations for batteries#1863

Mathlib/CategoryTheory/Category/Preorder.lean

@@ -81,7 +81,7 @@ theorem leOfHom {x y : X} (h : x ⟶ y) : x ≤ y :=
   h.down.down
 
 set_option linter.defProp false in
-@[nolint defLemma, inherit_doc leOfHom]
+@[inherit_doc leOfHom]
 abbrev _root_.Quiver.Hom.le := @leOfHom
 
 @[simp]

Mathlib/Combinatorics/Hindman.lean

@@ -107,17 +107,17 @@ variable {M} [Semigroup M] (a : Stream' M) (m : M) (h : FP a.tail m)
 
 set_option linter.defProp false in
 /-- Constructor for `FP`. This is the preferred spelling over `FP.head'`. -/
-@[to_additive (attr := match_pattern, nolint defLemma)
+@[to_additive (attr := match_pattern)
   /-- Constructor for `FS`. This is the preferred spelling over `FS.head'`. -/]
 abbrev FP.head : a.head ∈ FP a := FP.head' a
 set_option linter.defProp false in
 /-- Constructor for `FP`. This is the preferred spelling over `FP.tail'`. -/
-@[to_additive (attr := match_pattern, nolint defLemma)
+@[to_additive (attr := match_pattern)
   /-- Constructor for `FS`. This is the preferred spelling over `FS.tail'`. -/]
 abbrev FP.tail : m ∈ FP a := FP.tail' a m h
 set_option linter.defProp false in
 /-- Constructor for `FP`. This is the preferred spelling over `FP.cons'`. -/
-@[to_additive (attr := match_pattern, nolint defLemma)
+@[to_additive (attr := match_pattern)
   /-- Constructor for `FS`. This is the preferred spelling over `FS.cons'`. -/]
 abbrev FP.cons : a.head * m ∈ FP a := FP.cons' a m h
 

Mathlib/Data/Nat/Fib/Zeckendorf.lean

@@ -37,7 +37,7 @@ fibonacci, zeckendorf, digit
 open List Nat
 
 -- TODO: The `local` attribute makes this not considered as an instance by linters
-@[nolint defLemma docBlame]
+@[nolint docBlame]
 local instance : IsTrans ℕ fun a b ↦ b + 2 ≤ a where
   trans _a _b _c hba hcb := hcb.trans <| le_self_add.trans hba
 

Mathlib/Logic/Basic.lean

@@ -734,7 +734,7 @@ lemma eq_true_intro {a : Prop} (h : a) : a = True := propext (iff_true_intro h)
 lemma eq_false_intro {a : Prop} (h : ¬a) : a = False := propext (iff_false_intro h)
 
 -- FIXME: `alias` creates `def Iff.eq := propext` instead of `lemma Iff.eq := propext`
-@[nolint defLemma] alias Iff.eq := propext
+alias Iff.eq := propext
 
 lemma iff_eq_eq {a b : Prop} : (a ↔ b) = (a = b) := propext ⟨propext, Eq.to_iff⟩
 

Mathlib/Topology/Algebra/WithZeroTopology.lean

@@ -140,7 +140,6 @@ theorem isOpen_Iio {a : Γ₀} : IsOpen (Iio a) :=
 
 /-- The topology on a linearly ordered group with zero element adjoined is compatible with the order
 structure: the set `{p : Γ₀ × Γ₀ | p.1 ≤ p.2}` is closed. -/
-@[nolint defLemma]
 scoped instance (priority := 100) orderClosedTopology : OrderClosedTopology Γ₀ where
   isClosed_le' := by
     simp only [← isOpen_compl_iff, compl_setOf, not_le, isOpen_iff_mem_nhds]
@@ -149,7 +148,6 @@ scoped instance (priority := 100) orderClosedTopology : OrderClosedTopology Γ
     exact Iio_mem_nhds hab
 
 /-- The topology on a linearly ordered group with zero element adjoined is T₅. -/
-@[nolint defLemma]
 scoped instance (priority := 100) t5Space : T5Space Γ₀ where
   completely_normal := fun s t h₁ h₂ => by
     by_cases hs : 0 ∈ s
@@ -159,7 +157,6 @@ scoped instance (priority := 100) t5Space : T5Space Γ₀ where
 
 /-- The topology on a linearly ordered group with zero element adjoined makes it a topological
 monoid. -/
-@[nolint defLemma]
 scoped instance (priority := 100) : ContinuousMul Γ₀ where
   continuous_mul := by
     simp only [continuous_iff_continuousAt, ContinuousAt]
@@ -182,7 +179,6 @@ scoped instance (priority := 100) : ContinuousMul Γ₀ where
       rw [nhds_prod_eq, nhds_of_ne_zero hx, nhds_of_ne_zero hy, prod_pure_pure]
       exact pure_le_nhds (x * y)
 
-@[nolint defLemma]
 scoped instance (priority := 100) : ContinuousInv₀ Γ₀ :=
   ⟨fun γ h => by
     rw [ContinuousAt, nhds_of_ne_zero h]

lake-manifest.json

@@ -61,14 +61,14 @@
    "inputRev": "master",
    "inherited": false,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/batteries",
+  {"url": "https://github.com/grunweg/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "125807f43a86b5d58892b7ea6972eec0d6c164d2",
+   "rev": "b64b25708ba00b6f21fcee123be5e062bc12efba",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "remove-defLemma",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",

lakefile.lean

@@ -6,7 +6,7 @@ open Lake DSL
 ## Mathlib dependencies on upstream projects
 -/
 
-require "leanprover-community" / "batteries" @ git "main"
+require "leanprover-community" / "batteries" from git "https://github.com/grunweg/batteries" @ "remove-defLemma"
 require "leanprover-community" / "Qq" @ git "master"
 require "leanprover-community" / "aesop" @ git "master"
 require "leanprover-community" / "proofwidgets" @ git "main"