chore(*): adaptations for batteries#1545 (#32581)

After [batteries#1545](leanprover-community/batteries#1545) is merged:

- [x] Edit the lakefile to point to leanprover-community/batteries:main
- [x] Run lake update batteries
- [x] Merge leanprover-community/mathlib4:master
- [ ] Wait for CI and merge

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: F. G. Dorais <fgdorais@gmail.com>

Author: 3 people

Mathlib.lean

@@ -6535,6 +6535,7 @@ public import Mathlib.Tactic.ExistsI
 public import Mathlib.Tactic.Explode
 public import Mathlib.Tactic.Explode.Datatypes
 public import Mathlib.Tactic.Explode.Pretty
+public import Mathlib.Tactic.Ext
 public import Mathlib.Tactic.ExtendDoc
 public import Mathlib.Tactic.ExtractGoal
 public import Mathlib.Tactic.ExtractLets

Mathlib/Data/Nat/Cast/Defs.lean

@@ -71,22 +71,6 @@ class AddMonoidWithOne (R : Type*) extends NatCast R, AddMonoid R, One R where
 /-- An `AddCommMonoidWithOne` is an `AddMonoidWithOne` satisfying `a + b = b + a`. -/
 class AddCommMonoidWithOne (R : Type*) extends AddMonoidWithOne R, AddCommMonoid R
 
-library_note2 «coercion into rings»
-/--
-Coercions such as `Nat.castCoe` that go from a concrete structure such as
-`ℕ` to an arbitrary ring `R` should be set up as follows:
-```lean
-instance : CoeTail ℕ R where coe := ...
-instance : CoeHTCT ℕ R where coe := ...
-```
-
-It needs to be `CoeTail` instead of `Coe` because otherwise type-class
-inference would loop when constructing the transitive coercion `ℕ → ℕ → ℕ → ...`.
-Sometimes we also need to declare the `CoeHTCT` instance
-if we need to shadow another coercion
-(e.g. `Nat.cast` should be used over `Int.ofNat`).
--/
-
 namespace Nat
 
 variable [AddMonoidWithOne R]

Mathlib/Tactic.lean

@@ -85,6 +85,7 @@ public import Mathlib.Tactic.ExistsI
 public import Mathlib.Tactic.Explode
 public import Mathlib.Tactic.Explode.Datatypes
 public import Mathlib.Tactic.Explode.Pretty
+public import Mathlib.Tactic.Ext
 public import Mathlib.Tactic.ExtendDoc
 public import Mathlib.Tactic.ExtractGoal
 public import Mathlib.Tactic.ExtractLets

Mathlib/Tactic/Basic.lean

@@ -12,6 +12,7 @@ public meta import Mathlib.Tactic.Lemma
 public meta import Mathlib.Tactic.TypeStar
 public meta import Mathlib.Tactic.Linter.OldObtain
 public meta import Mathlib.Tactic.Simproc.ExistsAndEq
+public import Batteries.Util.LibraryNote -- For `library_note` command.
 
 /-!
 # Basic tactics and utilities for tactic writing
@@ -157,39 +158,3 @@ def withResetServerInfo {α : Type} (t : TacticM α) :
     return { result?, msgs, trees }
 
 end Mathlib.Tactic
-
-/-- A mathlib library note: the note's content should be contained in its doc-string. -/
-@[expose] def LibraryNote := Unit
-
-open Lean in
-/-- `library_note2 «my note» /-- documentation -/` creates a library note named `my note`
-in the `Mathlib.LibraryNote` namespace, whose content is `/-- documentation -/`.
-You can access this note using, for example, `#print Mathlib.LibraryNote.«my note»`.
--/
-macro "library_note2 " name:ident ppSpace dc:docComment : command =>
-  `($dc:docComment def $(mkIdent (`_root_.Mathlib.LibraryNote ++ name.getId)) : LibraryNote := ())
-
-open Lean Elab Command in
-/-- Support the old `library_note "foo"` syntax, with a deprecation warning. -/
-elab "library_note2 " name:str ppSpace dc:docComment : command => do
-  logWarningAt name <|
-    "deprecation warning: library_note2 now takes an identifier instead of a string.\n" ++
-    "Hint: replace the double quotes with «french quotes»."
-  let name := Name.mkSimple name.getString
-  let stx ← `(library_note2 $(mkIdent name):ident $dc:docComment)
-  elabCommandTopLevel stx
-
-library_note2 «partially-applied ext lemmas»
-/--
-When possible, `ext` lemmas are stated without a full set of arguments. As an example, for bundled
-homs `f`, `g`, and `of`, `f.comp of = g.comp of → f = g` is a better `ext` lemma than
-`(∀ x, f (of x) = g (of x)) → f = g`, as the former allows a second type-specific extensionality
-lemmas to be applied to `f.comp of = g.comp of`.
-If the domain of `of` is `ℕ` or `ℤ` and `of` is a `RingHom`, such a lemma could then make the goal
-`f (of 1) = g (of 1)`.
-
-For bundled morphisms, there is a `ext` lemma that always applies of the form
-`(∀ x, ⇑f x = ⇑g x) → f = g`. When adding type-specific `ext` lemmas like the one above, we want
-these to be tried first. This happens automatically since the type-specific lemmas are inevitably
-defined later.
--/

Mathlib/Tactic/Ext.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2020 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+module
+
+public import Mathlib.Tactic.Basic
+
+/-!
+# Documentation for `ext` tactic
+
+This file contains a library note on the use of the `ext` tactic and `@[ext]` attribute.
+-/
+
+public section
+
+library_note «partially-applied ext lemmas»
+/--
+When possible, `ext` lemmas are stated without a full set of arguments. As an example, for bundled
+homs `f`, `g`, and `of`, `f.comp of = g.comp of → f = g` is a better `ext` lemma than
+`(∀ x, f (of x) = g (of x)) → f = g`, as the former allows a second type-specific extensionality
+lemmas to be applied to `f.comp of = g.comp of`.
+If the domain of `of` is `ℕ` or `ℤ` and `of` is a `RingHom`, such a lemma could then make the goal
+`f (of 1) = g (of 1)`.
+
+For bundled morphisms, there is a `ext` lemma that always applies of the form
+`(∀ x, ⇑f x = ⇑g x) → f = g`. When adding type-specific `ext` lemmas like the one above, we want
+these to be tried first. This happens automatically since the type-specific lemmas are inevitably
+defined later.
+-/