diff --git a/Mathlib/Tactic/ByContra.lean b/Mathlib/Tactic/ByContra.lean
index e47cd3d1b821e0..a7f49768a74ea9 100644
--- a/Mathlib/Tactic/ByContra.lean
+++ b/Mathlib/Tactic/ByContra.lean
@@ -54,7 +54,7 @@ local elab "try_push_neg_at" cfg:optConfig h:ident : tactic => do
 
 local elab "try_push_neg" cfg:optConfig : tactic => do
   Push.push (← Push.elabPushConfig cfg) none (.const ``Not) (.targets #[] true)
-    (ifUnchanged := .silent)
+    (ifUnchanged := .warning)
 
 macro_rules
 | `(tactic| by_contra! $cfg $[$pat?]? $[: $ty?]?) => do
diff --git a/Mathlib/Tactic/Contrapose.lean b/Mathlib/Tactic/Contrapose.lean
index 76306f4b2e3341..66298dbfdda262 100644
--- a/Mathlib/Tactic/Contrapose.lean
+++ b/Mathlib/Tactic/Contrapose.lean
@@ -127,7 +127,7 @@ syntax (name := contrapose!)
 
 local elab "try_push_neg" cfg:optConfig : tactic => do
   Push.push (← Push.elabPushConfig cfg) none (.const ``Not) (.targets #[] true)
-    (ifUnchanged := .silent)
+    (ifUnchanged := .warning)
 
 macro_rules
   | `(tactic| contrapose! $cfg) => `(tactic| (contrapose; try_push_neg $cfg))
diff --git a/MathlibTest/Contrapose.lean b/MathlibTest/Contrapose.lean
index 78198d0ada629f..336ccc5ddae208 100644
--- a/MathlibTest/Contrapose.lean
+++ b/MathlibTest/Contrapose.lean
@@ -38,20 +38,43 @@ example (p q : Prop) (h : ¬q → p) : ¬p → q := by
   exact h
 
 example (p q : Prop) (h : q → p) : ¬p → ¬q := by
-  contrapose!
+  contrapose
   guard_target = q → p
   exact h
 
+example (p q : Prop) (h : ¬p) (hpq : q → p) : ¬q := by
+  contrapose h
+  guard_target = p
+  exact hpq h
+
+example (p q : Prop) (h : ¬p) (hpq : q → p) : ¬q := by
+  contrapose h with h'
+  guard_target = p
+  exact hpq h'
+
+example (p q : Prop) (h : q → p) : ¬p → ¬q := by
+  contrapose
+  guard_target = q → p
+  exact h
+
+section -- Using contrapose in a superfluous way warns.
+
+/-- warning: `push` made no progress on the goal -/
+#guard_msgs in
 example (p q : Prop) (h : ¬p) (hpq : q → p) : ¬q := by
   contrapose! h
   guard_target = p
   exact hpq h
 
+/-- warning: `push` made no progress on the goal -/
+#guard_msgs in
 example (p q : Prop) (h : ¬p) (hpq : q → p) : ¬q := by
   contrapose! h with h'
   guard_target = p
   exact hpq h'
 
+end
+
 example (p q r : Prop) (h : ¬ q ∧ ¬ r → ¬ p) : p → q ∨ r := by
   fail_if_success (contrapose; exact h)
   contrapose!; exact h
diff --git a/MathlibTest/byContra.lean b/MathlibTest/byContra.lean
index b25d24fb77beed..bc46b80fbc5982 100644
--- a/MathlibTest/byContra.lean
+++ b/MathlibTest/byContra.lean
@@ -85,6 +85,12 @@ example (x : α) (f : False) : x ≤ 1 := by
 
 end order
 
+example (n : ℕ) (h : n ≠ 0) : n ≠ 0 := by
+  by_contra rfl
+  simp only [Ne, not_true_eq_false] at h
+
+/-- warning: `push` made no progress at h._@.MathlibTest.byContra.2021293407._hygCtx._hyg.18 -/
+#guard_msgs in
 example (n : ℕ) (h : n ≠ 0) : n ≠ 0 := by
   by_contra! rfl
   simp only [Ne, not_true_eq_false] at h
@@ -93,6 +99,13 @@ example (p q : Prop) (hnp : ¬ p) : ¬ p ∨ ¬ q := by
   by_contra! ⟨hp, _⟩
   exact hnp hp
 
+example (p q : Prop) (hnp : ¬ p) (hnq : ¬ q) : ¬ (p ∨ q) := by
+  by_contra hp | hq
+  · exact hnp hp
+  · exact hnq hq
+
+/-- warning: `push` made no progress at h._@.MathlibTest.byContra.2021293410._hygCtx._hyg.25 -/
+#guard_msgs in
 example (p q : Prop) (hnp : ¬ p) (hnq : ¬ q) : ¬ (p ∨ q) := by
   by_contra! hp | hq
   · exact hnp hp