feat: update mathlib mod-tac-stx 2022-11-01 (#536)

This adds all the changes to tactic syntax that have happened in the period [2022-02-22 thru 2022-11-01](https://github.com/leanprover-community/mathlib/pulls?q=is%3Apr+closed%3A2022-02-22..2022-11-01+label%3Amodifies-tactic-syntax).

Author: digama0

Mathlib/Algebra/Group/Defs.lean

@@ -245,7 +245,7 @@ attribute [to_additive AddZeroClass] MulOneClass
 
 @[ext, to_additive]
 theorem MulOneClass.ext {M : Type u} : ∀ ⦃m₁ m₂ : MulOneClass M⦄, m₁.mul = m₂.mul → m₁ = m₂ := by
-  rintro ⟨⟨one₁⟩, ⟨mul₁⟩, one_mul₁, mul_one₁⟩ ⟨⟨one₂⟩, ⟨mul₂⟩, one_mul₂, mul_one₂⟩ ⟨rfl⟩
+  rintro @⟨⟨one₁⟩, ⟨mul₁⟩, one_mul₁, mul_one₁⟩ @⟨⟨one₂⟩, ⟨mul₂⟩, one_mul₂, mul_one₂⟩ ⟨rfl⟩
   -- FIXME:
   -- congr
   suffices one₁ = one₂ by cases this; rfl

Mathlib/Mathport/Syntax.lean

@@ -231,6 +231,8 @@ namespace Tactic
 /- E -/ syntax (name := symm') "symm'" (ppSpace location)? : tactic
 /- E -/ syntax (name := trans') "trans'" (ppSpace term)? : tactic
 
+/- E -/ syntax (name := classical) "classical" : tactic
+
 /- M -/ syntax (name := injectionsAndClear) "injections_and_clear" : tactic
 
 /- E -/ syntax (name := tryFor) "try_for " term:max tacticSeq : tactic
@@ -268,12 +270,15 @@ namespace Tactic
 /- S -/ syntax (name := hint) "hint" : tactic
 
 /- N -/ syntax (name := congr') "congr" (ppSpace colGt num)?
-  (" with " (colGt rcasesPat)* (" : " num)?)? : tactic
-/- M -/ syntax (name := rcongr) "rcongr" (ppSpace colGt rcasesPat)* : tactic
+  (" with " (colGt rintroPat)* (" : " num)?)? : tactic
+/- M -/ syntax (name := rcongr) "rcongr" (ppSpace colGt rintroPat)* : tactic
+/- M -/ syntax (name := congrM) "congrm " term : tactic
 /- E -/ syntax (name := acChange) "ac_change " term (" using " num)? : tactic
 
 /- S -/ syntax (name := rcases?) "rcases?" casesTarget,* (" : " num)? : tactic
 /- S -/ syntax (name := rintro?) "rintro?" (" : " num)? : tactic
+/- E -/ syntax (name := rsuffices) "rsuffices"
+    (ppSpace Std.Tactic.RCases.rcasesPatMed)? (" : " term)? (" := " term,+)? : tactic
 
 /- M -/ syntax (name := decide!) "decide!" : tactic
 
@@ -334,19 +339,19 @@ syntax termList := " [" term,* "]"
 /- B -/ syntax (name := abel!) "abel!" (ppSpace (&"raw" <|> &"term"))? (ppSpace location)? : tactic
 
 syntax ringMode := &"SOP" <|> &"raw" <|> &"horner"
-/- E -/ syntax (name := ringNF) "ring_nf" (ppSpace ringMode)? (ppSpace location)? : tactic
-/- E -/ syntax (name := ringNF!) "ring_nf!" (ppSpace ringMode)? (ppSpace location)? : tactic
+/- E -/ syntax (name := ringNF) "ring_nf" (config)? (ppSpace ringMode)? (ppSpace location)? : tactic
+/- E -/ syntax (name := ringNF!) "ring_nf!" (config)? (ppSpace ringMode)? (ppSpace location)? :
+  tactic
 
 /- E -/ syntax (name := noncommRing) "noncomm_ring" : tactic
 
-syntax nameAndTerm := term:71 " * " term:66
-/- M -/ syntax (name := linearCombination) "linear_combination" (config)?
-  sepBy(atomic(nameAndTerm) <|> term:66, " + ") : tactic
+/- B -/ syntax (name := linearCombination) "linear_combination" (config)? (colGt term)? : tactic
 
 /- B -/ syntax (name := linarith) "linarith" (config)? (&" only")? (" [" term,* "]")? : tactic
 /- B -/ syntax (name := linarith!) "linarith!" (config)? (&" only")? (" [" term,* "]")? : tactic
 /- M -/ syntax (name := nlinarith) "nlinarith" (config)? (&" only")? (" [" term,* "]")? : tactic
 /- M -/ syntax (name := nlinarith!) "nlinarith!" (config)? (&" only")? (" [" term,* "]")? : tactic
+/- S -/ syntax (name := polyrith) "polyrith" (&" only")? (" [" term,* "]")? : tactic
 
 /- S -/ syntax (name := omega) "omega" (&" manual")? (&" nat" <|> &" int")? : tactic
 
@@ -410,6 +415,12 @@ syntax mono.side := &"left" <|> &"right" <|> &"both"
 /- M -/ syntax (name := elementwise!) "elementwise!" (ppSpace (colGt ident))* : tactic
 /- M -/ syntax (name := deriveElementwiseProof) "derive_elementwise_proof" : tactic
 
+/- M -/ syntax (name := computeDegree) "compute_degree" : tactic
+
+/- B -/ syntax (name := positivity) "positivity" : tactic
+
+/- E -/ syntax (name := qify) "qify" (simpArgs)? (ppSpace location)? : tactic
+
 /- S -/ syntax (name := mkDecorations) "mk_decorations" : tactic
 
 /- M -/ syntax (name := nontriviality) "nontriviality"
@@ -439,6 +450,8 @@ syntax mono.side := &"left" <|> &"right" <|> &"both"
 /- M -/ syntax (name := padicIndexSimp) "padic_index_simp" " [" term,* "]" (ppSpace location)? :
   tactic
 
+/- M -/ syntax (name := borelize) "borelize" (ppSpace colGt term:max)* : tactic
+
 /- E -/ syntax (name := uniqueDiffWithinAt_Ici_Iic_univ) "uniqueDiffWithinAt_Ici_Iic_univ" : tactic
 
 /- M -/ syntax (name := ghostFunTac) "ghost_fun_tac " term ", " term : tactic
@@ -447,8 +460,8 @@ syntax mono.side := &"left" <|> &"right" <|> &"both"
 /- E -/ syntax (name := ghostSimp) "ghost_simp" (simpArgs)? : tactic
 /- E -/ syntax (name := wittTruncateFunTac) "witt_truncate_fun_tac" : tactic
 
-/- M -/ @[nolint docBlame] syntax (name := pure_coherence) "pure_coherence" : tactic
-/- M -/ @[nolint docBlame] syntax (name := coherence) "coherence" : tactic
+/- M -/ syntax (name := pure_coherence) "pure_coherence" : tactic
+/- M -/ syntax (name := coherence) "coherence" : tactic
 
 namespace Conv
 
@@ -458,8 +471,8 @@ namespace Conv
 /- E -/ syntax (name := normNum1) "norm_num1" : conv
 /- E -/ syntax (name := normNum) "norm_num" (simpArgs)? : conv
 
-/- E -/ syntax (name := ringNF) "ring_nf" (ppSpace ringMode)? : conv
-/- E -/ syntax (name := ringNF!) "ring_nf!" (ppSpace ringMode)? : conv
+/- E -/ syntax (name := ringNF) "ring_nf" (config)? (ppSpace ringMode)? : conv
+/- E -/ syntax (name := ringNF!) "ring_nf!" (config)? (ppSpace ringMode)? : conv
 /- E -/ syntax (name := ring) "ring" : conv
 /- E -/ syntax (name := ring!) "ring!" : conv
 
@@ -483,6 +496,8 @@ namespace Attr
 
 /- M -/ syntax (name := mkIff) "mk_iff" (ppSpace ident)? : attr
 
+/- M -/ syntax (name := expandExists) "expand_exists" (ppSpace ident)+ : attr
+
 -- TODO: this should be handled in mathport
 /- S -/ syntax (name := protectProj) "protect_proj" (&" without" (ppSpace ident)+)? : attr
 
@@ -538,4 +553,9 @@ macro_rules
 
 /- S -/ syntax (name := sample) "#sample " term : command
 
+/- S -/ syntax (name := normNum) "#norm_num" (&" only")? (Tactic.simpArgs)? " :"? ppSpace term :
+  command
+
+/- S -/ syntax (name := pushNeg) "#push_neg " term : command
+
 end Command

Mathlib/Tactic/Basic.lean

@@ -7,6 +7,7 @@ import Lean
 import Std
 import Mathlib.Tactic.Cases
 
+namespace Mathlib.Tactic
 open Lean Parser.Tactic Elab Command Elab.Tactic Meta
 
 syntax (name := «variables») "variables" (bracketedBinder)* : command
@@ -32,7 +33,7 @@ resulting in two subgoals `h : p ⊢` and `h : ¬ p ⊢`.
 macro "by_cases " e:term : tactic =>
   `(tactic| by_cases $(mkIdent `h) : $e)
 
-macro (name := classical) "classical" : tactic =>
+macro (name := classical!) "classical!" : tactic =>
   `(tactic| have em := Classical.propDecidable)
 
 syntax "transitivity" (colGt term)? : tactic

lean_packages/manifest.json

@@ -1,7 +1,7 @@
 {"version": 2,
  "packages":
  [{"url": "https://github.com/leanprover/std4",
-   "rev": "52a6002d484643556cb1ce1b6e845c4db9452655",
+   "rev": "3251e4564c136993227bbb5224276e63f077cf8e",
    "name": "std",
    "inputRev": "main"},
   {"url": "https://github.com/gebner/quote4",

scripts/nolints.json

@@ -42,15 +42,9 @@
  ["docBlame", "Zero"],
  ["docBlame", "bit0"],
  ["docBlame", "bit1"],
- ["docBlame", "classical"],
- ["docBlame", "command_Lemma___"],
  ["docBlame", "decidable_eq_of_bool_pred"],
- ["docBlame", "elabVariables"],
- ["docBlame", "evalIntrov"],
  ["docBlame", "instHNeg"],
  ["docBlame", "setOf"],
- ["docBlame", "tacticMatch_target_"],
- ["docBlame", "tacticTransitivity__"],
  ["docBlame", "«term_+ᵥ_»"],
  ["docBlame", "«term_-ᵥ_»"],
  ["docBlame", "«term_ˣ»"],
@@ -63,7 +57,6 @@
  ["docBlame", "to_additive_ignore_args"],
  ["docBlame", "to_additive_relevant_arg"],
  ["docBlame", "to_additive_reorder"],
- ["docBlame", "variables"],
  ["docBlame", "AddCancelCommMonoid.toCancelMonoid"],
  ["docBlame", "AddCancelMonoid.add_right_cancel"],
  ["docBlame", "AddCommGroup.toCancelCommMonoid"],
@@ -341,8 +334,6 @@
  ["docBlame", "WriterT.run"],
  ["docBlame", "WriterT.runThe"],
  ["docBlame", "Zero.zero"],
- ["docBlame", "evalIntrov.intro1PStep"],
- ["docBlame", "evalIntrov.introsDep"],
  ["docBlame", "Array.heapSort.loop"],
  ["docBlame", "BinaryHeap.mkHeap.loop"],
  ["docBlame", "Lean.Attr.hintTacticAttr"],
@@ -374,16 +365,23 @@
  ["docBlame", "Lean.Meta.findCore"],
  ["docBlame", "Lean.PHashSet.toList"],
  ["docBlame", "Lean.Tactic.solveByElim"],
+ ["docBlame", "Mathlib.Tactic.classical!"],
+ ["docBlame", "Mathlib.Tactic.command_Lemma___"],
+ ["docBlame", "Mathlib.Tactic.elabVariables"],
+ ["docBlame", "Mathlib.Tactic.evalIntrov"],
  ["docBlame", "Mathlib.Tactic.haveLetCore"],
  ["docBlame", "Mathlib.Tactic.renameArg"],
  ["docBlame", "Mathlib.Tactic.set"],
  ["docBlame", "Mathlib.Tactic.setArgsRest"],
  ["docBlame", "Mathlib.Tactic.tacticHave_"],
  ["docBlame", "Mathlib.Tactic.tacticLeft"],
  ["docBlame", "Mathlib.Tactic.tacticLet_"],
+ ["docBlame", "Mathlib.Tactic.tacticMatch_target_"],
  ["docBlame", "Mathlib.Tactic.tacticRight"],
  ["docBlame", "Mathlib.Tactic.tacticSet!_"],
  ["docBlame", "Mathlib.Tactic.tacticSuffices_"],
+ ["docBlame", "Mathlib.Tactic.tacticTransitivity__"],
+ ["docBlame", "Mathlib.Tactic.variables"],
  ["docBlame", "Mathlib.WhatsNew.diffExtension"],
  ["docBlame", "Mathlib.WhatsNew.whatsNew"],
  ["docBlame", "Nat.AtLeastTwo.prop"],
@@ -455,6 +453,7 @@
  ["docBlame", "Lean.Meta.Simp.mkEqSymm"],
  ["docBlame", "Lean.Meta.findCore.check"],
  ["docBlame", "Lean.Parser.Attr.elementwise"],
+ ["docBlame", "Lean.Parser.Attr.expandExists"],
  ["docBlame", "Lean.Parser.Attr.ext"],
  ["docBlame", "Lean.Parser.Attr.higherOrder"],
  ["docBlame", "Lean.Parser.Attr.interactive"],
@@ -477,8 +476,10 @@
  ["docBlame", "Lean.Parser.Command.localized"],
  ["docBlame", "Lean.Parser.Command.mkIffOfInductiveProp"],
  ["docBlame", "Lean.Parser.Command.mkSimpAttribute"],
+ ["docBlame", "Lean.Parser.Command.normNum"],
  ["docBlame", "Lean.Parser.Command.omit"],
  ["docBlame", "Lean.Parser.Command.parameter"],
+ ["docBlame", "Lean.Parser.Command.pushNeg"],
  ["docBlame", "Lean.Parser.Command.reassoc_axiom"],
  ["docBlame", "Lean.Parser.Command.sample"],
  ["docBlame", "Lean.Parser.Command.setupTacticParser"],
@@ -499,15 +500,20 @@
  ["docBlame", "Lean.Parser.Tactic.applyWith'"],
  ["docBlame", "Lean.Parser.Tactic.assocRw"],
  ["docBlame", "Lean.Parser.Tactic.async"],
+ ["docBlame", "Lean.Parser.Tactic.borelize"],
  ["docBlame", "Lean.Parser.Tactic.cancelDenoms"],
  ["docBlame", "Lean.Parser.Tactic.cases'"],
  ["docBlame", "Lean.Parser.Tactic.cases''"],
  ["docBlame", "Lean.Parser.Tactic.cc"],
  ["docBlame", "Lean.Parser.Tactic.clarify"],
+ ["docBlame", "Lean.Parser.Tactic.classical"],
  ["docBlame", "Lean.Parser.Tactic.clean"],
  ["docBlame", "Lean.Parser.Tactic.clearValue"],
+ ["docBlame", "Lean.Parser.Tactic.coherence"],
  ["docBlame", "Lean.Parser.Tactic.compVal"],
+ ["docBlame", "Lean.Parser.Tactic.computeDegree"],
  ["docBlame", "Lean.Parser.Tactic.congr'"],
+ ["docBlame", "Lean.Parser.Tactic.congrM"],
  ["docBlame", "Lean.Parser.Tactic.continue"],
  ["docBlame", "Lean.Parser.Tactic.continuity"],
  ["docBlame", "Lean.Parser.Tactic.continuity!"],
@@ -573,7 +579,6 @@
  ["docBlame", "Lean.Parser.Tactic.mkDecorations"],
  ["docBlame", "Lean.Parser.Tactic.mono"],
  ["docBlame", "Lean.Parser.Tactic.mvBisim"],
- ["docBlame", "Lean.Parser.Tactic.nameAndTerm"],
  ["docBlame", "Lean.Parser.Tactic.nlinarith"],
  ["docBlame", "Lean.Parser.Tactic.nlinarith!"],
  ["docBlame", "Lean.Parser.Tactic.noncommRing"],
@@ -587,8 +592,12 @@
  ["docBlame", "Lean.Parser.Tactic.padicIndexSimp"],
  ["docBlame", "Lean.Parser.Tactic.piInstance"],
  ["docBlame", "Lean.Parser.Tactic.piInstanceDeriveField"],
+ ["docBlame", "Lean.Parser.Tactic.polyrith"],
+ ["docBlame", "Lean.Parser.Tactic.positivity"],
  ["docBlame", "Lean.Parser.Tactic.prettyCases"],
  ["docBlame", "Lean.Parser.Tactic.propagateTags"],
+ ["docBlame", "Lean.Parser.Tactic.pure_coherence"],
+ ["docBlame", "Lean.Parser.Tactic.qify"],
  ["docBlame", "Lean.Parser.Tactic.rcases?"],
  ["docBlame", "Lean.Parser.Tactic.rcongr"],
  ["docBlame", "Lean.Parser.Tactic.reassoc"],
@@ -603,6 +612,7 @@
  ["docBlame", "Lean.Parser.Tactic.ringNF!"],
  ["docBlame", "Lean.Parser.Tactic.rintro?"],
  ["docBlame", "Lean.Parser.Tactic.rsimp"],
+ ["docBlame", "Lean.Parser.Tactic.rsuffices"],
  ["docBlame", "Lean.Parser.Tactic.rwSearch"],
  ["docBlame", "Lean.Parser.Tactic.rwSearch?"],
  ["docBlame", "Lean.Parser.Tactic.safe"],
@@ -663,6 +673,8 @@
  ["docBlame", "Mathlib.Tactic.LibrarySearch.librarySearchLemmas"],
  ["docBlame", "Mathlib.Tactic.LibrarySearch.lines"],
  ["docBlame", "Mathlib.Tactic.LibrarySearch.«termLibrary_search%»"],
+ ["docBlame", "Mathlib.Tactic.evalIntrov.intro1PStep"],
+ ["docBlame", "Mathlib.Tactic.evalIntrov.introsDep"],
  ["docBlame", "Sat.Clause.reify.prop"],
  ["docBlame", "Sat.Fmla.reify.prop"],
  ["docBlame", "Sat.Fmla.subsumes.prop"],
@@ -683,6 +695,7 @@
  ["docBlame", "Lean.Parser.Tactic.Conv.slice"],
  ["docBlame", "Lean.Parser.Tactic.ElimApp.evalNames"],
  ["docBlame", "Lean.Parser.Tactic.mono.side"],
+ ["docBlame", "Lean.Parser.Tactic.rcasesPat.explicit"],
  ["docBlame", "Mathlib.Tactic.Sat.buildReify.mkPS"],
  ["unusedArguments", "Combinator.K"],
  ["unusedArguments", "Decidable.not_or_iff_and_not"]]