fix: missing noWs in notations (#23822)

Also removed the `9000` priority, since this was probably chosen randomly, and there is no comment justifying it.

This somewhat follows on from #19900.

Author: eric-wieser

Mathlib/Algebra/Module/Torsion.lean

@@ -911,8 +911,16 @@ variable (A : Type*) [AddCommGroup A] (n : ℤ)
 def torsionBy : AddSubgroup A :=
   (Submodule.torsionBy ℤ A n).toAddSubgroup
 
-@[inherit_doc]
-scoped notation:max (priority := high) A"["n"]" => torsionBy A n
+@[inherit_doc torsionBy]
+scoped syntax:max (name := torsionByStx) (priority := high) term noWs "[" term "]" : term
+
+macro_rules | `($A[$n]) => `(torsionBy $A $n)
+
+/-- Unexpander for `torsionBy`. -/
+@[scoped app_unexpander torsionBy]
+def torsionByUnexpander : Lean.PrettyPrinter.Unexpander
+  | `($_ $A $n) => `($A[$n])
+  | _ => throw ()
 
 lemma torsionBy.neg : A[-n] = A[n] := by
   ext a

Mathlib/Algebra/MonoidAlgebra/Defs.lean

@@ -816,11 +816,19 @@ endowed with the convolution product.
 def AddMonoidAlgebra :=
   G →₀ k
 
-@[inherit_doc]
-scoped[AddMonoidAlgebra] notation:9000 R:max "[" A "]" => AddMonoidAlgebra R A
-
 namespace AddMonoidAlgebra
 
+@[inherit_doc AddMonoidAlgebra]
+scoped syntax:max (priority := high) term noWs "[" term "]" : term
+
+macro_rules | `($k[$g]) => `(AddMonoidAlgebra $k $g)
+
+/-- Unexpander for `AddMonoidAlgebra`. -/
+@[scoped app_unexpander AddMonoidAlgebra]
+def unexpander : Lean.PrettyPrinter.Unexpander
+  | `($_ $k $g) => `($k[$g])
+  | _ => throw ()
+
 instance inhabited : Inhabited k[G] :=
   inferInstanceAs (Inhabited (G →₀ k))