fix build

Mathlib.lean

@@ -26,11 +26,13 @@ import Mathlib.SetNotation
 import Mathlib.Tactic.Basic
 import Mathlib.Tactic.Block
 import Mathlib.Tactic.Coe
+import Mathlib.Tactic.Core
 import Mathlib.Tactic.NoMatch
 import Mathlib.Tactic.NormNum
 import Mathlib.Tactic.OpenPrivate
 import Mathlib.Tactic.PrintPrefix
 import Mathlib.Tactic.Ring
+import Mathlib.Tactic.RunTac
 import Mathlib.Tactic.Split
 import Mathlib.Tactic.Spread
 import Mathlib.Tactic.SudoSetOption

Mathlib/Tactic/Ring.lean

@@ -446,6 +446,8 @@ example {α} [CommSemiring α] (x y z : α) (n : ℕ) :
 --   (-(a * b) + c + d) * e = (c + (d + -a * b)) * e := by ring
 example (a n s: ℕ) : a * (n - s) = (n - s) * a := by ring
 
+example (A : ℕ) : (2 * A) ^ 2 = (2 * A) ^ 2 := by ring
+
 -- example (x y z : ℚ) (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) :
 --   x / (y / z) + y ⁻¹ + 1 / (y * -x) = -1/ (x * y) + (x * z + 1) / y :=
 -- begin