chore: update tests accordingly

Author: grunweg

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

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