diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean
index d948baeee2b0ef..7a5e34cd9b6a84 100644
--- a/Mathlib/Algebra/Group/Defs.lean
+++ b/Mathlib/Algebra/Group/Defs.lean
@@ -800,6 +800,10 @@ attribute [to_additive existing] isMulTorsionFree_iff
 /-- An additive commutative monoid is an additive monoid with commutative `(+)`. -/
 class AddCommMonoid (M : Type u) extends AddMonoid M, AddCommSemigroup M
 
+-- addition is commutative 99.9% of the time in mathematics,
+-- the essentially unique counterexample being ordinals.
+attribute [instance 1100] AddCommMonoid.toAddMonoid
+
 /-- A commutative monoid is a monoid with commutative `(*)`. -/
 @[to_additive]
 class CommMonoid (M : Type u) extends Monoid M, CommSemigroup M
diff --git a/Mathlib/Data/ENNReal/Basic.lean b/Mathlib/Data/ENNReal/Basic.lean
index 218392836d7fad..1e0c9b4c375ac9 100644
--- a/Mathlib/Data/ENNReal/Basic.lean
+++ b/Mathlib/Data/ENNReal/Basic.lean
@@ -180,7 +180,7 @@ variable {a b c d : ℝ≥0∞} {r p q : ℝ≥0} {n : ℕ}
 instance : IsOrderedMonoid ℝ≥0∞ where
   mul_le_mul_left _ _ := mul_le_mul_left
 
-instance : Unique (AddUnits ℝ≥0∞) where
+noncomputable instance : Unique (AddUnits ℝ≥0∞) where
   default := 0
   uniq a := AddUnits.ext <| nonpos_iff_eq_zero.1 <| by rw [← a.add_neg]; exact le_self_add
 
diff --git a/Mathlib/Data/Matrix/Basic.lean b/Mathlib/Data/Matrix/Basic.lean
index 6511fb8b1a3a9d..f005f976601acb 100644
--- a/Mathlib/Data/Matrix/Basic.lean
+++ b/Mathlib/Data/Matrix/Basic.lean
@@ -431,7 +431,7 @@ theorem mapMatrix_neg [AddZeroClass α] [AddCommGroup β] (f : α →+ β) :
 @[simp]
 theorem mapMatrix_smul [Monoid A] [AddZeroClass α] [AddMonoid β] [DistribMulAction A β]
     (a : A) (f : α →+ β) :
-    (a • f).mapMatrix = (a • f.mapMatrix : Matrix m n α →+ _) := rfl
+    (a • f).mapMatrix = (a • (f.mapMatrix : Matrix m n α →+ _)) := rfl
 
 end AddMonoidHom
 
diff --git a/Mathlib/RingTheory/Polynomial/IsIntegral.lean b/Mathlib/RingTheory/Polynomial/IsIntegral.lean
index 1bda775fc4645b..d42c460c2c7ea9 100644
--- a/Mathlib/RingTheory/Polynomial/IsIntegral.lean
+++ b/Mathlib/RingTheory/Polynomial/IsIntegral.lean
@@ -217,7 +217,7 @@ theorem MvPolynomial.isIntegral_iff_isIntegral_coeff.{w} {σ : Type w} {f : MvPo
             ((rename Subtype.val).comp
                 (killCompl (f := ((↑) : f.vars → σ)) Subtype.val_injective)).toRingHom
         · exact RingHom.ext (by simp [MvPolynomial.killCompl_map])
-        · nth_rw 1 12 [← hg]; simp)) n (.of_fintype _)
+        · simp [← hg])) n (.of_fintype _)
     · rw [← hg, coeff_rename_eq_zero _ _ _ (by grind)]
       exact isIntegral_zero
   revert f n