Merge branch 'bump/v4.22.0' of github.com:leanprover-community/mathlib4-nightly-testing into bump/v4.22.0

Author: kim-em

Mathlib/Algebra/CharP/Defs.lean

@@ -63,7 +63,7 @@ lemma cast_eq_mod (k : ℕ) : (k : R) = (k % p : ℕ) :=
     exact Nat.dvd_mul_right p a
   calc
     (k : R) = ↑(k % p + p * (k / p)) := by rw [Nat.mod_add_div]
-    _ = ↑(k % p) := by simp [cast_eq_zero, this]
+    _ = ↑(k % p) := by simp [this]
 
 lemma cast_eq_iff_mod_eq [IsLeftCancelAdd R] : (a:R) = (b:R) ↔ a % p = b % p := by
   wlog hle : a ≤ b

Mathlib/Data/Complex/Basic.lean

@@ -340,10 +340,10 @@ instance addGroupWithOne : AddGroupWithOne ℂ :=
     intCast_ofNat := fun _ => by ext <;> rfl
     intCast_negSucc := fun n => by
       ext
-      · simp [AddGroupWithOne.intCast_negSucc]
+      · simp only [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, neg_re]
         change -(1 : ℝ) + (-n) = -(↑(n + 1))
         simp [Nat.cast_add, add_comm]
-      · simp [AddGroupWithOne.intCast_negSucc]
+      · simp only [neg_im, zero_eq_neg]
         change im ⟨n, 0⟩ = 0
         rfl
     one := 1 }

Mathlib/Tactic/DeclarationNames.lean

@@ -51,5 +51,5 @@ def getAliasSyntax {m} [Monad m] [MonadResolveName m] (stx : Syntax) : m (Array
 /-- Used for linters which use `0` instead of `false` for disabling. -/
 def logLint0Disable {m} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
     (linterOption : Lean.Option Nat) (stx : Syntax) (msg : MessageData) : m Unit :=
-  let disable := m!"note: this linter can be disabled with `set_option {linterOption.name} 0`"
-  logWarningAt stx (.tagged linterOption.name m!"{msg}\n{disable}")
+  let disable := .note m!"This linter can be disabled with `set_option {linterOption.name} 0`"
+  logWarningAt stx (.tagged linterOption.name m!"{msg}{disable}")

Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean

@@ -169,7 +169,7 @@ def getDeprecatedSyntax : Syntax → Array (SyntaxNodeKind × Syntax × MessageD
         if trailing.toString.trimLeft.isEmpty then
           rargs.push (`MaxHeartbeats, stx,
             s!"Please, add a comment explaining the need for modifying the maxHeartbeat limit, \
-              as in\nset_option {opt} {n} in\n-- reason for change\n...\n")
+              as in\nset_option {opt} {n} in\n-- reason for change\n...")
         else
           rargs
     | _ => rargs

MathlibTest/CategoryTheory/MonoidalComp.lean

@@ -25,6 +25,6 @@ example {W X Y Z : C} (f : W ⟶ (X ⊗ Y) ⊗ Z) : W ⟶ X ⊗ (Y ⊗ Z) := f 
 
 example {U V W X Y : C} (f : U ⟶ V ⊗ (W ⊗ X)) (g : (V ⊗ W) ⊗ X ⟶ Y) :
     f ⊗≫ g = f ≫ (α_ _ _ _).inv ≫ g := by
-  simp [MonoidalCategory.tensorHom_def, monoidalComp]
+  simp [monoidalComp]
 
 end CategoryTheory

MathlibTest/CommandStart.lean

@@ -30,7 +30,8 @@ This part of the code
 should be written as
   'field1 : Nat'
 
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 -/
 #guard_msgs in
 structure A where
@@ -57,7 +58,8 @@ This part of the code
 should be written as
   'field1 : Nat'
 
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 -/
 #guard_msgs in
 structure D where
@@ -75,7 +77,8 @@ This part of the code
 should be written as
   'instance {R} :'
 
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 -/
 #guard_msgs in
 instance   {R} : Add R := sorry
@@ -89,7 +92,8 @@ This part of the code
 should be written as
   'instance {R} :'
 
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 -/
 #guard_msgs in
 instance   {R} : Add R := sorry
@@ -163,7 +167,8 @@ local infixl:50 " ≼ " => s
 
 /--
 warning: The `commandStart` linter had some parsing issues: feel free to silence it and report this error!
-note: this linter can be disabled with `set_option linter.style.commandStart.verbose false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart.verbose false`
 -/
 #guard_msgs in
 set_option linter.style.commandStart.verbose true in
@@ -186,7 +191,8 @@ This part of the code
 should be written as
   'variable [h :'
 
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 ---
 warning: extra space in the source
 
@@ -195,7 +201,8 @@ This part of the code
 should be written as
   '[h : Add'
 
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 ---
 warning: extra space in the source
 
@@ -204,7 +211,8 @@ This part of the code
 should be written as
   '[h : Add'
 
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 ---
 warning: extra space in the source
 
@@ -213,7 +221,8 @@ This part of the code
 should be written as
   'Nat] [Add'
 
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 ---
 warning: extra space in the source
 
@@ -222,7 +231,8 @@ This part of the code
 should be written as
   '[Add Nat]'
 
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 -/
 #guard_msgs in
 variable    [ h    : Add Nat   ] [ Add Nat]
@@ -235,7 +245,8 @@ This part of the code
 should be written as
   'omit [h :'
 
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 ---
 warning: extra space in the source
 
@@ -244,7 +255,8 @@ This part of the code
 should be written as
   ' [Add'
 
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 -/
 #guard_msgs in
 omit  [h : Add Nat]  [Add Nat]
@@ -260,7 +272,8 @@ This part of the code
 should be written as
   '@[aesop (rule_sets'
 
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 -/
 #guard_msgs in
 @[aesop  (rule_sets := [builtin]) safe apply] example : True := trivial
@@ -269,7 +282,8 @@ end misc
 
 /--
 warning: 'section' starts on column 1, but all commands should start at the beginning of the line.
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 -/
 #guard_msgs in
  section
@@ -282,7 +296,8 @@ This part of the code
 should be written as
   'example : True'
 
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 -/
 #guard_msgs in
 example    : True := trivial
@@ -299,7 +314,8 @@ This part of the code
 should be written as
   'example : True'
 
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 -/
 #guard_msgs in
 example  :  True :=trivial
@@ -312,7 +328,8 @@ This part of the code
 should be written as
   '(a : Nat)'
 
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 -/
 #guard_msgs in
 variable (a: Nat)
@@ -325,7 +342,8 @@ This part of the code
 should be written as
   '(_a : Nat)'
 
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 -/
 #guard_msgs in
 example (_a: Nat) : True := trivial
@@ -338,7 +356,8 @@ This part of the code
 should be written as
   '{a : Nat}'
 
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 -/
 #guard_msgs in
 example {a: Nat} : a = a := rfl
@@ -358,7 +377,8 @@ This part of the code
 should be written as
   ': Nat}'
 
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 -/
 #guard_msgs in
 example {a :Nat} : a = a := rfl
@@ -371,7 +391,8 @@ This part of the code
 should be written as
   'example {a :'
 
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 ---
 warning: missing space in the source
 
@@ -380,14 +401,16 @@ This part of the code
 should be written as
   ': Nat}'
 
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 -/
 #guard_msgs in
 example  {a :Nat} : a = a := rfl
 
 /--
 warning: unused variable `b`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 ---
 warning: missing space in the source
 
@@ -396,7 +419,8 @@ This part of the code
 should be written as
   'Nat} {b :'
 
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 -/
 #guard_msgs in
 example {a : Nat}{b : Nat} : a = a := rfl
@@ -409,7 +433,8 @@ This part of the code
 should be written as
   'Nat} : a ='
 
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 -/
 #guard_msgs in
 example {a : Nat}  : a = a := rfl
@@ -422,7 +447,8 @@ This part of the code
 should be written as
   'alpha] {a'
 
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 -/
 #guard_msgs in
 example {alpha} [Neg alpha   ] {a : Nat} : a = a := rfl
@@ -435,7 +461,8 @@ This part of the code
 should be written as
   'example : True'
 
-note: this linter can be disabled with `set_option linter.style.commandStart false`
+
+Note: This linter can be disabled with `set_option linter.style.commandStart false`
 -/
 #guard_msgs in
 /-- Check that doc/strings do not get removed as comments. -/

MathlibTest/DeprecatedModuleTest.lean

@@ -7,15 +7,17 @@ warning: We can also give more details about the deprecation
 import Mathlib.Tactic.Linter.DocPrime
 import Mathlib.Tactic.Linter.DocString
 
-note: this linter can be disabled with `set_option linter.deprecated.module false`
+
+Note: This linter can be disabled with `set_option linter.deprecated.module false`
 ---
 warning:
 'MathlibTest.DeprecatedModule' has been deprecated: please replace this import by
 
 import Mathlib.Tactic.Linter.DocPrime
 import Mathlib.Tactic.Linter.DocString
 
-note: this linter can be disabled with `set_option linter.deprecated.module false`
+
+Note: This linter can be disabled with `set_option linter.deprecated.module false`
 -/
 #guard_msgs in
 /-!