diff --git a/Mathlib/Algebra/Order/Field/Basic.lean b/Mathlib/Algebra/Order/Field/Basic.lean
index 25b0ac4f017443..b009de11667e74 100644
--- a/Mathlib/Algebra/Order/Field/Basic.lean
+++ b/Mathlib/Algebra/Order/Field/Basic.lean
@@ -661,11 +661,11 @@ theorem min_div_div_right_of_nonpos (hc : c ≤ 0) (a b : α) : min (a / c) (b /
 theorem max_div_div_right_of_nonpos (hc : c ≤ 0) (a b : α) : max (a / c) (b / c) = min a b / c :=
   Eq.symm <| Antitone.map_min fun _ _ => div_le_div_of_nonpos_of_le hc
 
-@[simp, grind =]
+@[simp, grind =, push]
 theorem abs_inv (a : α) : |a⁻¹| = |a|⁻¹ :=
   map_inv₀ (absHom : α →*₀ α) a
 
-@[grind =]
+@[grind =, push]
 theorem abs_div (a b : α) : |a / b| = |a| / |b| :=
   map_div₀ (absHom : α →*₀ α) a b
 
diff --git a/Mathlib/Algebra/Order/Field/Power.lean b/Mathlib/Algebra/Order/Field/Power.lean
index 8f888e8a9c5c2a..405c2c8df661bb 100644
--- a/Mathlib/Algebra/Order/Field/Power.lean
+++ b/Mathlib/Algebra/Order/Field/Power.lean
@@ -62,7 +62,7 @@ alias ⟨_, Odd.zpow_neg⟩ := Odd.zpow_neg_iff
 
 alias ⟨_, Odd.zpow_nonpos⟩ := Odd.zpow_nonpos_iff
 
-@[simp]
+@[simp, push]
 theorem abs_zpow (a : α) (p : ℤ) : |a ^ p| = |a| ^ p := map_zpow₀ absHom a p
 
 theorem abs_neg_one_zpow (p : ℤ) : |(-1 : α) ^ p| = 1 := by simp
diff --git a/Mathlib/Algebra/Order/Group/Unbundled/Abs.lean b/Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
index 307d844fe2d132..532d0b9f77ea09 100644
--- a/Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
+++ b/Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
@@ -73,7 +73,8 @@ meta def abs.unexpander : Lean.PrettyPrinter.Unexpander
 @[to_additive] lemma mabs_le_mabs (h₀ : a ≤ b) (h₁ : a⁻¹ ≤ b) : |a|ₘ ≤ |b|ₘ :=
   (mabs_le'.2 ⟨h₀, h₁⟩).trans (le_mabs_self b)
 
-@[to_additive (attr := simp)] lemma mabs_inv (a : α) : |a⁻¹|ₘ = |a|ₘ := by simp [mabs, sup_comm]
+@[to_additive (attr := simp, push)]
+lemma mabs_inv (a : α) : |a⁻¹|ₘ = |a|ₘ := by simp [mabs, sup_comm]
 
 @[to_additive] lemma mabs_div_comm (a b : α) : |a / b|ₘ = |b / a|ₘ := by rw [← mabs_inv, inv_div]
 
diff --git a/Mathlib/Algebra/Order/Ring/Abs.lean b/Mathlib/Algebra/Order/Ring/Abs.lean
index 55b6b50ea5fdc0..bca5539635768c 100644
--- a/Mathlib/Algebra/Order/Ring/Abs.lean
+++ b/Mathlib/Algebra/Order/Ring/Abs.lean
@@ -45,7 +45,7 @@ variable [Ring α] [LinearOrder α] [IsOrderedRing α] {n : ℕ} {a b : α}
 
 lemma abs_two : |(2 : α)| = 2 := abs_of_nonneg zero_le_two
 
-@[simp, grind =]
+@[simp, grind =, push]
 lemma abs_mul (a b : α) : |a * b| = |a| * |b| := by
   rw [abs_eq (mul_nonneg (abs_nonneg a) (abs_nonneg b))]
   rcases le_total a 0 with ha | ha <;> rcases le_total b 0 with hb | hb <;>
@@ -58,7 +58,7 @@ def absHom : α →*₀ α where
   map_one' := abs_one
   map_mul' := abs_mul
 
-@[simp, grind =]
+@[simp, grind =, push]
 lemma abs_pow (a : α) (n : ℕ) : |a ^ n| = |a| ^ n := (absHom.toMonoidHom : α →* α).map_pow _ _
 
 lemma pow_abs (a : α) (n : ℕ) : |a| ^ n = |a ^ n| := (abs_pow a n).symm
@@ -72,7 +72,7 @@ omit [IsOrderedRing α] in
 @[simp] lemma abs_mul_abs_self (a : α) : |a| * |a| = a * a :=
   abs_by_cases (fun x => x * x = a * a) rfl (neg_mul_neg a a)
 
-lemma abs_mul_self (a : α) : |a * a| = a * a := by simp
+@[push] lemma abs_mul_self (a : α) : |a * a| = a * a := by simp
 
 omit [IsOrderedRing α] in
 @[simp] lemma sq_abs (a : α) : |a| ^ 2 = a ^ 2 := by simpa only [sq] using abs_mul_abs_self a
diff --git a/MathlibTest/push.lean b/MathlibTest/push.lean
index 372b1d74fa0967..2c8c077500458a 100644
--- a/MathlibTest/push.lean
+++ b/MathlibTest/push.lean
@@ -148,3 +148,39 @@ example (a b c : α) (s : Set α) : a ∈ (∅ ∪ (Set.univ ∩ (({b, c} \ sᶜ
   exact test_sorry
 
 end membership
+
+section abs
+
+example (a b : ℝ) : |a * b| = |a| * |b| := by
+  push abs
+  rfl
+
+example (a : ℝ) (n : ℕ) : |a ^ n| = |a| ^ n := by
+  push abs
+  rfl
+
+example (a : ℝ) : |a⁻¹| = |a|⁻¹ := by
+  push abs
+  rfl
+
+example (a b : ℝ) : |a / b| = |a| / |b| := by
+  push abs
+  rfl
+
+example (a : ℝ) (p : ℤ) : |a ^ p| = |a| ^ p := by
+  push abs
+  rfl
+
+example (a : ℝ) : |-a| = |a| := by
+  push abs
+  rfl
+
+example (a : ℝ) : |a * a| = |a| * |a| := by
+  push abs
+  rfl
+
+example (a b : ℝ) (n : ℕ) : |a ^ n * b⁻¹ / (-a)| = |a| ^ n * |b|⁻¹ / |a| := by
+  push abs
+  rfl
+
+end abs