Fix

Author: TwoFX

Mathlib/Algebra/Algebra/StrictPositivity.lean

@@ -60,7 +60,7 @@ lemma _root_.IsUnit.isStrictlyPositive [LE A] [Monoid A] [Zero A]
 lemma isSelfAdjoint [Semiring A] [PartialOrder A] [StarRing A] [StarOrderedRing A] {a : A}
     (ha : IsStrictlyPositive a) : IsSelfAdjoint a := ha.nonneg.isSelfAdjoint
 
-@[simp, grind]
+@[simp, grind .]
 lemma _root_.isStrictlyPositive_one [LE A] [Monoid A] [Zero A] [ZeroLEOneClass A] :
     IsStrictlyPositive (1 : A) := iff_of_unital.mpr ⟨zero_le_one, isUnit_one⟩
 

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean

@@ -115,12 +115,12 @@ variable {A : Type*} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A]
 matrices, operators on a Hilbert space, elements of a C⋆-algebra, etc. -/
 noncomputable def log (a : A) : A := cfc Real.log a
 
-@[simp, grind]
+@[simp, grind =>]
 protected lemma _root_.IsSelfAdjoint.log {a : A} : IsSelfAdjoint (log a) := cfc_predicate _ a
 
-@[simp, grind] lemma log_zero : log (0 : A) = 0 := by simp [log]
+@[simp, grind =] lemma log_zero : log (0 : A) = 0 := by simp [log]
 
-@[simp, grind] lemma log_one : log (1 : A) = 0 := by simp [log]
+@[simp, grind =] lemma log_one : log (1 : A) = 0 := by simp [log]
 
 @[simp, grind =]
 lemma log_algebraMap {r : ℝ} : log (algebraMap ℝ A r) = algebraMap ℝ A (Real.log r) := by

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean

@@ -93,7 +93,7 @@ noncomputable instance (priority := 100) : Pow A ℝ≥0 where
 @[simp]
 lemma nnrpow_eq_pow {a : A} {y : ℝ≥0} : nnrpow a y = a ^ y := rfl
 
-@[simp, grind]
+@[simp, grind =>]
 lemma nnrpow_nonneg {a : A} {x : ℝ≥0} : 0 ≤ a ^ x := cfcₙ_predicate _ a
 
 lemma nnrpow_def {a : A} {y : ℝ≥0} : a ^ y = cfcₙ (NNReal.nnrpow · y) a := rfl
@@ -226,7 +226,7 @@ section sqrt
 /-- Square roots of operators, based on the non-unital continuous functional calculus. -/
 noncomputable def sqrt (a : A) : A := cfcₙ NNReal.sqrt a
 
-@[simp, grind]
+@[simp, grind =>]
 lemma sqrt_nonneg (a : A) : 0 ≤ sqrt a := cfcₙ_predicate _ a
 
 lemma sqrt_eq_nnrpow (a : A) : sqrt a = a ^ (1 / 2 : ℝ≥0) := by
@@ -381,7 +381,7 @@ noncomputable instance (priority := 100) : Pow A ℝ where
 @[simp]
 lemma rpow_eq_pow {a : A} {y : ℝ} : rpow a y = a ^ y := rfl
 
-@[simp, grind]
+@[simp, grind =>]
 lemma rpow_nonneg {a : A} {y : ℝ} : 0 ≤ a ^ y := cfc_predicate _ a
 
 lemma rpow_def {a : A} {y : ℝ} : a ^ y = cfc (fun x : ℝ≥0 => x ^ y) a := rfl

MathlibTest/FindSyntax.lean

@@ -3,7 +3,7 @@ import Mathlib.Tactic.FindSyntax
 infix:65 " #find_syntax_add " => Nat.add
 
 /--
-info: Found 2 uses among over 700 syntax declarations
+info: Found 2 uses among over 800 syntax declarations
 In `MathlibTest.FindSyntax`:
   «term_#find_syntax_add_»: '#find_syntax_add'
 
@@ -14,23 +14,23 @@ In `Mathlib.Tactic.FindSyntax`:
 #find_syntax "#find_syntax" approx  -- an `infix` in two files, one being the current one
 
 /--
-info: Found 1 use among over 700 syntax declarations
+info: Found 1 use among over 800 syntax declarations
 In `Init.Notation`:
   «term_∘_»: '∘'
 -/
 #guard_msgs in
 #find_syntax "∘" approx  -- an `infixr`
 
 /--
-info: Found 1 use among over 700 syntax declarations
+info: Found 1 use among over 800 syntax declarations
 In `Init.Notation`:
   «term_∣_»: '∣'
 -/
 #guard_msgs in
 #find_syntax "∣" approx  -- an `infix`
 
 /--
-info: Found 2 uses among over 700 syntax declarations
+info: Found 2 uses among over 800 syntax declarations
 In `Init.Notation`:
   «stx_,*»: ',*'
   «stx_,*,?»: ',*,?'
@@ -39,15 +39,15 @@ In `Init.Notation`:
 #find_syntax ",*" approx  -- generated by a `macro`
 
 /--
-info: Found 1 use among over 700 syntax declarations
+info: Found 1 use among over 800 syntax declarations
 In `Init.Notation`:
   «term~~~_»: '~~~'
 -/
 #guard_msgs in
 #find_syntax "~~~" approx  -- a `prefix`
 
 /--
-info: Found 15 uses among over 700 syntax declarations
+info: Found 15 uses among over 800 syntax declarations
 In `Init.Tactics`:
   Lean.Parser.Tactic.mrefineMacro: 'mrefine'
   Lean.Parser.Tactic.refine: 'refine'

MathlibTest/Simps.lean

@@ -1269,7 +1269,7 @@ end UnderScoreDigit
 
 namespace Grind
 
-@[simps (attr := grind) -isSimp]
+@[simps (attr := grind =) -isSimp]
 def foo := (2, 3)
 
 example : foo.1 = 2 := by grind

MathlibTest/Util/PrintSorries.lean

@@ -193,26 +193,22 @@ warning: declaration uses 'sorry'
 Check that `admit` and `stop` are correctly handled
 -/
 
-/-- info: thm4 has sorry of type
+/--
+info: thm4 has sorry of type
   True
 ---
 warning: declaration uses 'sorry'
----
-warning: 'admit' tactic does nothing
-
-Note: This linter can be disabled with `set_option linter.unusedTactic false` -/
+-/
 #guard_msgs in
 #print sorries in
 theorem thm4 : True := by admit
 
-/-- info: thm5 has sorry of type
+/--
+info: thm5 has sorry of type
   True
 ---
 warning: declaration uses 'sorry'
----
-warning: 'stop admit' tactic does nothing
-
-Note: This linter can be disabled with `set_option linter.unusedTactic false` -/
+-/
 #guard_msgs in
 #print sorries in
 theorem thm5 : True := by stop admit