diff --git a/Mathlib/Algebra/Group/Fin/Basic.lean b/Mathlib/Algebra/Group/Fin/Basic.lean
index 852b1c37387130..600b1ed93b190c 100644
--- a/Mathlib/Algebra/Group/Fin/Basic.lean
+++ b/Mathlib/Algebra/Group/Fin/Basic.lean
@@ -111,7 +111,7 @@ lemma lt_sub_iff {n : ℕ} {a b : Fin n} : a < a - b ↔ a < b := by
   rcases n with - | n
   · exact a.elim0
   constructor
-  · contrapose!
+  · contrapose
     intro h
     obtain ⟨l, hl⟩ := Nat.exists_eq_add_of_le (Fin.not_lt.mp h)
     simpa only [Fin.not_lt, le_iff_val_le_val, sub_def, hl, ← Nat.add_assoc, Nat.add_mod_left,
diff --git a/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean b/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
index a3d2fd0aada20a..20bdc9b5e01ee1 100644
--- a/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
+++ b/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@@ -850,10 +850,9 @@ lemma Nonempty.pow (hs : s.Nonempty) : ∀ {n}, (s ^ n).Nonempty
   | 0 => by simp
   | n + 1 => by rw [pow_succ]; exact hs.pow.mul hs
 
-set_option push_neg.use_distrib true in
 @[to_additive (attr := simp)] lemma pow_eq_empty : s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0 := by
   constructor
-  · contrapose!
+  · contrapose! +distrib
     rintro (hs | rfl)
     -- TODO: The `nonempty_iff_ne_empty` would be unnecessary if `push_neg` knew how to simplify
     -- `s ≠ ∅` to `s.Nonempty` when `s : Finset α`.
@@ -1003,10 +1002,9 @@ lemma Nonempty.zpow (hs : s.Nonempty) : ∀ {n : ℤ}, (s ^ n).Nonempty
   | (n : ℕ) => hs.pow
   | .negSucc n => by simpa using hs.pow
 
-set_option push_neg.use_distrib true in
 @[to_additive (attr := simp)] lemma zpow_eq_empty : s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0 := by
   constructor
-  · contrapose!
+  · contrapose! +distrib
     rintro (hs | rfl)
     · exact nonempty_iff_ne_empty.1 (nonempty_iff_ne_empty.2 hs).zpow
     · rw [← nonempty_iff_ne_empty]
diff --git a/Mathlib/Algebra/Group/Pointwise/Set/Basic.lean b/Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
index f43c8fd6f8f71f..3a59f6636c4e24 100644
--- a/Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
+++ b/Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@@ -638,10 +638,9 @@ lemma Nonempty.pow (hs : s.Nonempty) : ∀ {n}, (s ^ n).Nonempty
   | 0 => by simp
   | n + 1 => by rw [pow_succ]; exact hs.pow.mul hs
 
-set_option push_neg.use_distrib true in
 @[to_additive (attr := simp)] lemma pow_eq_empty : s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0 := by
   constructor
-  · contrapose!
+  · contrapose! +distrib
     rintro (hs | rfl)
     · exact hs.pow
     · simp
@@ -796,10 +795,9 @@ lemma Nonempty.zpow (hs : s.Nonempty) : ∀ {n : ℤ}, (s ^ n).Nonempty
   | (n : ℕ) => hs.pow
   | .negSucc n => by simpa using hs.pow
 
-set_option push_neg.use_distrib true in
 @[to_additive (attr := simp)] lemma zpow_eq_empty : s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0 := by
   constructor
-  · contrapose!
+  · contrapose! +distrib
     rintro (hs | rfl)
     · exact hs.zpow
     · simp
diff --git a/Mathlib/Algebra/Group/UniqueProds/Basic.lean b/Mathlib/Algebra/Group/UniqueProds/Basic.lean
index 708ad92067c8df..88999c7827d611 100644
--- a/Mathlib/Algebra/Group/UniqueProds/Basic.lean
+++ b/Mathlib/Algebra/Group/UniqueProds/Basic.lean
@@ -256,7 +256,7 @@ attribute [to_additive] TwoUniqueProds
 lemma uniqueMul_of_twoUniqueMul {G} [Mul G] {A B : Finset G} (h : 1 < #A * #B →
     ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2)
     (hA : A.Nonempty) (hB : B.Nonempty) : ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b := by
-  set_option push_neg.use_distrib true in by_cases! hc : #A ≤ 1 ∧ #B ≤ 1
+  by_cases! +distrib hc : #A ≤ 1 ∧ #B ≤ 1
   · exact UniqueMul.of_card_le_one hA hB hc.1 hc.2
   rw [← Finset.card_pos] at hA hB
   obtain ⟨p, hp, _, _, _, hu, _⟩ := h (Nat.one_lt_mul_iff.mpr ⟨hA, hB, hc⟩)
@@ -431,7 +431,7 @@ open UniqueMul in
     let _ := isWellFounded_ssubset (α := ∀ i, G i) -- why need this?
     apply IsWellFounded.induction (· ⊂ ·) A; intro A ihA B hA
     apply IsWellFounded.induction (· ⊂ ·) B; intro B ihB hB
-    set_option push_neg.use_distrib true in by_cases! hc : #A ≤ 1 ∧ #B ≤ 1
+    by_cases! +distrib hc : #A ≤ 1 ∧ #B ≤ 1
     · exact of_card_le_one hA hB hc.1 hc.2
     obtain ⟨i, hc⟩ := exists_or.mpr (hc.imp exists_of_one_lt_card_pi exists_of_one_lt_card_pi)
     obtain ⟨ai, hA, bi, hB, hi⟩ := uniqueMul_of_nonempty (hA.image (· i)) (hB.image (· i))
diff --git a/Mathlib/Algebra/Homology/Embedding/Basic.lean b/Mathlib/Algebra/Homology/Embedding/Basic.lean
index 17e21792ba9dd7..8d98f49ddd7ebe 100644
--- a/Mathlib/Algebra/Homology/Embedding/Basic.lean
+++ b/Mathlib/Algebra/Homology/Embedding/Basic.lean
@@ -251,7 +251,7 @@ lemma notMem_range_embeddingUpIntLE_iff (n : ℤ) :
     (∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n) ↔ p < n := by
   constructor
   · intro h
-    by_contra!
+    by_contra
     exact h (p - n).natAbs (by simp; cutsat)
   · intros
     dsimp
@@ -264,7 +264,7 @@ lemma notMem_range_embeddingUpIntGE_iff (n : ℤ) :
     (∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n) ↔ n < p := by
   constructor
   · intro h
-    by_contra!
+    by_contra
     exact h (n - p).natAbs (by simp; cutsat)
   · intros
     dsimp
diff --git a/Mathlib/Algebra/Order/Archimedean/Class.lean b/Mathlib/Algebra/Order/Archimedean/Class.lean
index 91870b9194b86a..2e39be62a548f1 100644
--- a/Mathlib/Algebra/Order/Archimedean/Class.lean
+++ b/Mathlib/Algebra/Order/Archimedean/Class.lean
@@ -391,8 +391,8 @@ theorem mk_prod {ι : Type*} [LinearOrder ι] {s : Finset ι} (hnonempty : s.Non
     have hminmem : s.min' hs ∈ (Finset.cons i s hi) :=
       Finset.mem_cons_of_mem (Finset.min'_mem _ _)
     have hne : mk (a i) ≠ mk (a (s.min' hs)) := by
-      by_contra!
-      obtain eq := hmono.injOn (by simp) hminmem this
+      by_contra h
+      obtain eq := hmono.injOn (by simp) hminmem h
       rw [eq] at hi
       exact hi (Finset.min'_mem _ hs)
     rw [← ih] at hne
diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean b/Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean
index 6a2fdf7c4a8c75..e23bf5359c6efb 100644
--- a/Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean
+++ b/Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean
@@ -116,8 +116,8 @@ lemma isIso_of_nonDegenerate (x : X.nonDegenerate n)
   obtain ⟨x, hx⟩ := x
   induction m using SimplexCategory.rec with | _ m
   rw [mem_nonDegenerate_iff_notMem_degenerate] at hx
-  by_contra!
-  refine hx ⟨_, not_le.1 (fun h ↦ this ?_), f, y, hy⟩
+  by_contra hf
+  refine hx ⟨_, not_le.1 (fun h ↦ hf ?_), f, y, hy⟩
   rw [SimplexCategory.isIso_iff_of_epi]
   exact le_antisymm h (SimplexCategory.len_le_of_epi f)
 
diff --git a/Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean b/Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
index f91b953b5b54b9..5ac5a7f72e4434 100644
--- a/Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
+++ b/Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
@@ -179,7 +179,6 @@ lemma differentiableAt_binEntropy_iff_ne_zero_one :
     · simp [log_inv, mul_neg, ← neg_mul, ← negMulLog_def, differentiableAt_negMulLog_iff] at h
     · fun_prop (disch := simp)
 
-set_option push_neg.use_distrib true in
 /-- Binary entropy has derivative `log (1 - p) - log p`.
 It's not differentiable at `0` or `1` but the junk values of `deriv` and `log` coincide there. -/
 lemma deriv_binEntropy (p : ℝ) : deriv binEntropy p = log (1 - p) - log p := by
@@ -192,7 +191,7 @@ lemma deriv_binEntropy (p : ℝ) : deriv binEntropy p = log (1 - p) - log p := b
     all_goals fun_prop (disch := assumption)
   -- pathological case where `deriv = 0` since `binEntropy` is not differentiable there
   · rw [deriv_zero_of_not_differentiableAt (differentiableAt_binEntropy_iff_ne_zero_one.not.2 hp)]
-    push_neg at hp
+    push_neg +distrib at hp
     obtain rfl | rfl := hp <;> simp
 
 /-! ### `q`-ary entropy -/
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Preorder/WellOrderContinuous.lean b/Mathlib/CategoryTheory/Limits/Shapes/Preorder/WellOrderContinuous.lean
index ff7510b9ae3dcd..9818cc373e236e 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Preorder/WellOrderContinuous.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Preorder/WellOrderContinuous.lean
@@ -93,11 +93,11 @@ instance IsWellOrderContinuous.restriction_setIci
       dsimp only [f]
       by_cases! h : j' ≤ j
       · refine ⟨⟨⟨j, le_refl j⟩, ?_⟩, h⟩
-        by_contra!
-        simp only [Set.mem_Iio, not_lt] at this
+        by_contra h'
+        simp only [Set.mem_Iio, not_lt] at h'
         apply hm.1
         rintro ⟨k, hk⟩ hkm
-        exact this.trans hk
+        exact h'.trans hk
       · exact ⟨⟨⟨j', h.le⟩, hj'⟩, by rfl⟩
     exact (Functor.Final.isColimitWhiskerEquiv (F := hf.functor) _).2
       (F.isColimitOfIsWellOrderContinuous m.1 (Set.Ici.isSuccLimit_coe m hm))⟩
diff --git a/Mathlib/Combinatorics/Colex.lean b/Mathlib/Combinatorics/Colex.lean
index 6f58ec91d38f11..f3db8034c95eae 100644
--- a/Mathlib/Combinatorics/Colex.lean
+++ b/Mathlib/Combinatorics/Colex.lean
@@ -148,7 +148,7 @@ private lemma trans_aux (hst : toColex s ≤ toColex t) (htu : toColex t ≤ toC
 
 private lemma antisymm_aux (hst : toColex s ≤ toColex t) (hts : toColex t ≤ toColex s) : s ⊆ t := by
   intro a has
-  by_contra! hat
+  by_contra hat
   have ⟨_b, hb₁, hb₂, _⟩ := trans_aux hst hts has hat
   exact hb₂ hb₁
 
diff --git a/Mathlib/Combinatorics/SimpleGraph/Clique.lean b/Mathlib/Combinatorics/SimpleGraph/Clique.lean
index 5d3ed6bda97a61..2951c9fa685d81 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Clique.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Clique.lean
@@ -496,7 +496,7 @@ theorem cliqueFree_two : G.CliqueFree 2 ↔ G = ⊥ := by
 
 lemma CliqueFree.mem_of_sup_edge_isNClique {x y : α} {t : Finset α} {n : ℕ} (h : G.CliqueFree n)
     (hc : (G ⊔ edge x y).IsNClique n t) : x ∈ t := by
-  by_contra! hf
+  by_contra hf
   have ht : (t : Set α) \ {x} = t := sdiff_eq_left.mpr <| Set.disjoint_singleton_right.mpr hf
   exact h t ⟨ht ▸ hc.1.sdiff_of_sup_edge, hc.2⟩
 
diff --git a/Mathlib/Combinatorics/SimpleGraph/Metric.lean b/Mathlib/Combinatorics/SimpleGraph/Metric.lean
index 0ca20cac36849e..07d774f29e33d3 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Metric.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Metric.lean
@@ -195,7 +195,7 @@ protected theorem Reachable.pos_dist_of_ne (h : G.Reachable u v) (hne : u ≠ v)
 protected theorem Reachable.one_lt_dist_of_ne_of_not_adj (h : G.Reachable u v) (hne : u ≠ v)
     (hnadj : ¬G.Adj u v) : 1 < G.dist u v :=
   Nat.lt_of_le_of_ne (h.pos_dist_of_ne hne) (by
-    by_contra! hc
+    by_contra hc
     obtain ⟨p, hp⟩ := Reachable.exists_walk_length_eq_dist h
     exact hnadj (Walk.exists_length_eq_one_iff.mp ⟨p, hc ▸ hp⟩))
 
diff --git a/Mathlib/Data/EReal/Operations.lean b/Mathlib/Data/EReal/Operations.lean
index 61c8b7ad54af7c..f8f2b0a300414d 100644
--- a/Mathlib/Data/EReal/Operations.lean
+++ b/Mathlib/Data/EReal/Operations.lean
@@ -747,7 +747,7 @@ lemma mul_ne_top (a b : EReal) :
   rw [ne_eq, mul_eq_top]
   -- push the negation while keeping the disjunctions, that is converting `¬(p ∧ q)` into `¬p ∨ ¬q`
   -- rather than `p → ¬q`, since we already have disjunctions in the rhs
-  set_option push_neg.use_distrib true in push_neg
+  push_neg +distrib
   rfl
 
 lemma mul_eq_bot (a b : EReal) :
@@ -759,7 +759,7 @@ lemma mul_eq_bot (a b : EReal) :
 lemma mul_ne_bot (a b : EReal) :
     a * b ≠ ⊥ ↔ (a ≠ ⊥ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊤) := by
   rw [ne_eq, mul_eq_bot]
-  set_option push_neg.use_distrib true in push_neg
+  push_neg +distrib
   rfl
 
 /-- `EReal.toENNReal` is multiplicative. For the version with the nonnegativity
diff --git a/Mathlib/Data/Nat/Count.lean b/Mathlib/Data/Nat/Count.lean
index 50ae44d3e2ce0c..658c0ea26ce083 100644
--- a/Mathlib/Data/Nat/Count.lean
+++ b/Mathlib/Data/Nat/Count.lean
@@ -104,7 +104,7 @@ theorem count_strict_mono {m n : ℕ} (hm : p m) (hmn : m < n) : count p m < cou
   (count_lt_count_succ_iff.2 hm).trans_le <| count_monotone _ (Nat.succ_le_iff.2 hmn)
 
 theorem count_injective {m n : ℕ} (hm : p m) (hn : p n) (heq : count p m = count p n) : m = n := by
-  by_contra! h : m ≠ n
+  by_contra! h
   wlog hmn : m < n
   · exact this hn hm heq.symm h.symm (by grind)
   · simpa [heq] using count_strict_mono hm hmn
diff --git a/Mathlib/Data/Seq/Basic.lean b/Mathlib/Data/Seq/Basic.lean
index 4bdad1547925f1..b475543c3b4756 100644
--- a/Mathlib/Data/Seq/Basic.lean
+++ b/Mathlib/Data/Seq/Basic.lean
@@ -924,7 +924,7 @@ theorem at_least_as_long_as_coind {a : Seq α} {b : Seq β}
   by_cases ha : a.Terminates; swap
   · simp [length'_of_not_terminates ha]
   simp [length'_of_terminates ha, length'_le_iff]
-  by_contra! hb
+  by_contra hb
   have hb_cons : b.drop (a.length ha) ≠ .nil := by
     intro hb'
     simp only [← length'_eq_zero_iff_nil, drop_length', tsub_eq_zero_iff_le, length'_le_iff] at hb'
diff --git a/Mathlib/GroupTheory/Perm/ClosureSwap.lean b/Mathlib/GroupTheory/Perm/ClosureSwap.lean
index a8304b756211ed..a26cde5fe5abf1 100644
--- a/Mathlib/GroupTheory/Perm/ClosureSwap.lean
+++ b/Mathlib/GroupTheory/Perm/ClosureSwap.lean
@@ -114,7 +114,7 @@ theorem mem_closure_isSwap {S : Set (Perm α)} (hS : ∀ f ∈ S, f.IsSwap) {f :
     · rw [← orbit_eq_iff.mpr (hf b), h1, orbit_eq_iff.mpr (hf a)]; apply mem_orbit_self
     · rw [← orbit_eq_iff.mpr (hf b), h2]; apply hf
     · exact hf b
-  · contrapose! hb
+  · contrapose hb
     simp_rw [notMem_compl_iff, mem_fixedBy, Perm.smul_def, Perm.mul_apply, swap_apply_def,
       apply_eq_iff_eq]
     by_cases hb' : f b = b
diff --git a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean
index 9c39303aa00ce1..4b8e9316acfe0b 100644
--- a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean
+++ b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean
@@ -663,7 +663,7 @@ theorem IsCycle.isConj_iff (hσ : IsCycle σ) (hτ : IsCycle τ) :
     refine Finset.card_bij (fun a _ => π a) (fun _ ha => ?_) (fun _ _ _ _ ab => π.injective ab)
         fun b hb ↦ ⟨π⁻¹ b, ?_, π.apply_inv_self b⟩
     · simp [mem_support.1 ha]
-    contrapose! hb
+    contrapose hb
     rw [mem_support, Classical.not_not] at hb
     rw [mem_support, Classical.not_not, Perm.mul_apply, Perm.mul_apply, hb, Perm.apply_inv_self]
   mpr := hσ.isConj hτ
diff --git a/Mathlib/LinearAlgebra/LinearIndependent/Defs.lean b/Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
index 24abef8729e207..fa3deba7f25684 100644
--- a/Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
+++ b/Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
@@ -629,7 +629,7 @@ theorem not_linearIndependent_iffₒₛ :
       ∃ (s t : Finset ι) (f : ι → R),
         Disjoint s t ∧ ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i ∧ ∃ i ∈ s, 0 < f i := by
   simp only [linearIndependent_iffₒₛ, pos_iff_ne_zero]
-  set_option push_neg.use_distrib true in push_neg
+  push_neg +distrib
   refine ⟨fun ⟨s, t, f, hst, heq, h⟩ => ?_,
     fun ⟨s, t, f, hst, heq, hi⟩ => ⟨s, t, f, hst, heq, .inl hi⟩⟩
   rcases h with ⟨i, hi, hfi⟩ | ⟨i, hi, hgi⟩
diff --git a/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Semisimple.lean b/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Semisimple.lean
index 6746466db91a21..bbaeb8dd290183 100644
--- a/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Semisimple.lean
+++ b/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Semisimple.lean
@@ -180,6 +180,8 @@ open LieModule Matrix
 
 local notation "H" => cartanSubalgebra' b
 
+set_option maxHeartbeats 210000 in
+-- This declaration was already right at the heartbeats limit
 private lemma instIsIrreducible_aux₀ {U : LieSubmodule K H (b.support ⊕ ι → K)}
     (χ : H → K) (hχ : χ ≠ 0) (hχ' : genWeightSpace U χ ≠ ⊥) :
     ∃ i, v b i ∈ (genWeightSpace U χ).map U.incl := by
diff --git a/Mathlib/ModelTheory/Semantics.lean b/Mathlib/ModelTheory/Semantics.lean
index 6689dc1070bef2..0a4d00475e7db9 100644
--- a/Mathlib/ModelTheory/Semantics.lean
+++ b/Mathlib/ModelTheory/Semantics.lean
@@ -736,7 +736,7 @@ variable (M N)
 theorem realize_iff_of_model_completeTheory [N ⊨ L.completeTheory M] (φ : L.Sentence) :
     N ⊨ φ ↔ M ⊨ φ := by
   refine ⟨fun h => ?_, (L.completeTheory M).realize_sentence_of_mem⟩
-  contrapose! h
+  contrapose h
   rw [← Sentence.realize_not] at *
   exact (L.completeTheory M).realize_sentence_of_mem (mem_completeTheory.2 h)
 
diff --git a/Mathlib/NumberTheory/Padics/PadicVal/Basic.lean b/Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
index 2ce5ac863fede0..54bf408ea21cd7 100644
--- a/Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
+++ b/Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
@@ -94,7 +94,7 @@ theorem maxPowDiv_eq_multiplicity {p n : ℕ} (hp : 1 < p) (hn : n ≠ 0) (h : F
 @[csimp]
 theorem padicValNat_eq_maxPowDiv : @padicValNat = @maxPowDiv := by
   ext p n
-  set_option push_neg.use_distrib true in by_cases! h : 1 < p ∧ 0 < n
+  by_cases! +distrib h : 1 < p ∧ 0 < n
   · rw [padicValNat_def' h.1.ne' h.2.ne', maxPowDiv_eq_multiplicity h.1 h.2.ne']
     exact Nat.finiteMultiplicity_iff.2 ⟨h.1.ne', h.2⟩
   · rcases h with (h | h)
diff --git a/Mathlib/NumberTheory/WellApproximable.lean b/Mathlib/NumberTheory/WellApproximable.lean
index 37c6943e548636..3e0884759add40 100644
--- a/Mathlib/NumberTheory/WellApproximable.lean
+++ b/Mathlib/NumberTheory/WellApproximable.lean
@@ -292,8 +292,7 @@ theorem addWellApproximable_ae_empty_or_univ (δ : ℕ → ℝ) (hδ : Tendsto 
     rw [OrderIso.apply_blimsup e, ← hu₀ p]
     exact blimsup_congr (Eventually.of_forall fun n hn =>
       approxAddOrderOf.vadd_eq_of_mul_dvd (δ n) hn.1 hn.2)
-  set_option push_neg.use_distrib true in
-  by_cases! h : ∀ p : Nat.Primes, A p =ᵐ[μ] (∅ : Set 𝕊) ∧ B p =ᵐ[μ] (∅ : Set 𝕊)
+  by_cases! +distrib h : ∀ p : Nat.Primes, A p =ᵐ[μ] (∅ : Set 𝕊) ∧ B p =ᵐ[μ] (∅ : Set 𝕊)
   · replace h : ∀ p : Nat.Primes, (u p +ᵥ E : Set _) =ᵐ[μ] E := by
       intro p
       replace hE₂ : E =ᵐ[μ] C p := hE₂ p (h p)
diff --git a/Mathlib/Order/LiminfLimsup.lean b/Mathlib/Order/LiminfLimsup.lean
index b9922c123a722c..266ac3dd4f609f 100644
--- a/Mathlib/Order/LiminfLimsup.lean
+++ b/Mathlib/Order/LiminfLimsup.lean
@@ -703,7 +703,7 @@ theorem cofinite.blimsup_set_eq :
     blimsup s cofinite p = { x | { n | p n ∧ x ∈ s n }.Infinite } := by
   simp only [blimsup_eq, le_eq_subset, eventually_cofinite, not_forall, sInf_eq_sInter, exists_prop]
   ext x
-  refine ⟨fun h => ?_, fun hx t h => ?_⟩ <;> contrapose! h
+  refine ⟨fun h => ?_, fun hx t h => ?_⟩ <;> contrapose h
   · simp only [mem_sInter, mem_setOf_eq, not_forall, exists_prop]
     exact ⟨{x}ᶜ, by simpa using h, by simp⟩
   · exact hx.mono fun i hi => ⟨hi.1, fun hit => h (hit hi.2)⟩
@@ -850,7 +850,7 @@ theorem limsup_le_iff {x : β} (h₁ : f.IsCoboundedUnder (· ≤ ·) u := by is
     rcases h' y x_y with ⟨z, x_z, z_y⟩
     exact (limsup_le_of_le h₁ ((h z x_z).mono (fun _ ↦ le_of_lt))).trans_lt z_y
   · apply limsup_le_of_le h₁
-    set_option push_neg.use_distrib true in push_neg at h'
+    push_neg +distrib at h'
     rcases h' with ⟨z, x_z, hz⟩
     exact (h z x_z).mono  <| fun w hw ↦ (or_iff_left (not_le_of_gt hw)).1 (hz (u w))
 
@@ -878,7 +878,7 @@ theorem le_limsup_iff {x : β} (h₁ : f.IsCoboundedUnder (· ≤ ·) u := by is
     obtain ⟨z, y_z, z_x⟩ := h' y y_x
     exact y_z.trans_le (le_limsup_of_frequently_le ((h z z_x).mono (fun _ ↦ le_of_lt)) h₂)
   · apply le_limsup_of_frequently_le _ h₂
-    set_option push_neg.use_distrib true in push_neg at h'
+    push_neg +distrib at h'
     rcases h' with ⟨z, z_x, hz⟩
     exact (h z z_x).mono <| fun w hw ↦ (or_iff_right (not_le_of_gt hw)).1 (hz (u w))
 
diff --git a/Mathlib/RingTheory/HahnSeries/Basic.lean b/Mathlib/RingTheory/HahnSeries/Basic.lean
index be59722cf0fe5f..c942f71c69ae96 100644
--- a/Mathlib/RingTheory/HahnSeries/Basic.lean
+++ b/Mathlib/RingTheory/HahnSeries/Basic.lean
@@ -425,7 +425,7 @@ def embDomain (f : Γ ↪o Γ') : HahnSeries Γ R → HahnSeries Γ' R := fun x
   { coeff := fun b : Γ' => if h : b ∈ f '' x.support then x.coeff (Classical.choose h) else 0
     isPWO_support' :=
       (x.isPWO_support.image_of_monotone f.monotone).mono fun b hb => by
-        contrapose! hb
+        contrapose hb
         rw [Function.mem_support, dif_neg hb, Classical.not_not] }
 
 @[simp]
@@ -454,7 +454,7 @@ theorem embDomain_notin_image_support {f : Γ ↪o Γ'} {x : HahnSeries Γ R} {b
 theorem support_embDomain_subset {f : Γ ↪o Γ'} {x : HahnSeries Γ R} :
     support (embDomain f x) ⊆ f '' x.support := by
   intro g hg
-  contrapose! hg
+  contrapose hg
   rw [mem_support, embDomain_notin_image_support hg, Classical.not_not]
 
 theorem embDomain_notin_range {f : Γ ↪o Γ'} {x : HahnSeries Γ R} {b : Γ'} (hb : b ∉ Set.range f) :
diff --git a/Mathlib/RingTheory/HahnSeries/Multiplication.lean b/Mathlib/RingTheory/HahnSeries/Multiplication.lean
index 2a6d6f86c27de7..fd2927fb694307 100644
--- a/Mathlib/RingTheory/HahnSeries/Multiplication.lean
+++ b/Mathlib/RingTheory/HahnSeries/Multiplication.lean
@@ -180,7 +180,7 @@ instance instSMul : SMul (HahnSeries Γ R) (HahnModule Γ' R V) where
             { a : Γ' | (VAddAntidiagonal x.isPWO_support
               ((of R).symm y).isPWO_support a).Nonempty } := by
           intro a ha
-          contrapose! ha
+          contrapose ha
           simp [not_nonempty_iff_eq_empty.1 ha]
         isPWO_support_vaddAntidiagonal.mono h }
 
@@ -346,7 +346,7 @@ theorem support_smul_subset_vadd_support' [MulZeroClass R] [SMulWithZero R V] {x
   · exact x.isPWO_support
   · exact y.isPWO_support
   intro x hx
-  contrapose! hx
+  contrapose hx
   simp only [Set.mem_setOf_eq, not_nonempty_iff_eq_empty] at hx
   simp [hx, coeff_smul]
 
diff --git a/Mathlib/RingTheory/Ideal/AssociatedPrime/Basic.lean b/Mathlib/RingTheory/Ideal/AssociatedPrime/Basic.lean
index 8591bbc0f856e5..152a963b810653 100644
--- a/Mathlib/RingTheory/Ideal/AssociatedPrime/Basic.lean
+++ b/Mathlib/RingTheory/Ideal/AssociatedPrime/Basic.lean
@@ -131,7 +131,7 @@ theorem subset_union_of_exact (hf : Function.Injective f) (hfg : Function.Exact
       apply_fun f at hb
       rw [map_smul, map_zero, h, ← mul_smul, ← LinearMap.toSpanSingleton_apply,
         ← LinearMap.mem_ker, ← hx] at hb
-      contrapose! hb
+      contrapose hb
       exact p.primeCompl.mul_mem hb ha
   · right
     refine ⟨‹_›, g x, le_antisymm (fun b hb ↦ ?_) (fun b hb ↦ ?_)⟩
@@ -141,7 +141,7 @@ theorem subset_union_of_exact (hf : Function.Injective f) (hfg : Function.Exact
     · rw [LinearMap.mem_ker, LinearMap.toSpanSingleton_apply, ← map_smul, ← LinearMap.mem_ker,
         hfg.linearMap_ker_eq] at hb
       obtain ⟨y, hy⟩ := hb
-      by_contra! H
+      by_contra H
       exact h b H y hy
 
 variable (R M M') in
diff --git a/Mathlib/RingTheory/Ideal/Oka.lean b/Mathlib/RingTheory/Ideal/Oka.lean
index 5f64b5415c187b..78700aa5964a56 100644
--- a/Mathlib/RingTheory/Ideal/Oka.lean
+++ b/Mathlib/RingTheory/Ideal/Oka.lean
@@ -59,7 +59,7 @@ theorem isPrime_of_maximal_not {I : Ideal R} (hI : Maximal (¬P ·) I) : I.IsPri
 Then all the ideals of `R` satisfy `P`. -/
 theorem forall_of_forall_prime (hmax : ∀ I, ¬P I → ∃ I, Maximal (¬P ·) I)
     (hprime : ∀ I, I.IsPrime → P I) (I : Ideal R) : P I := by
-  by_contra! hI
+  by_contra hI
   obtain ⟨I, hI⟩ := hmax I hI
   exact hI.prop <| hprime I (hP.isPrime_of_maximal_not hI)
 
diff --git a/Mathlib/RingTheory/Localization/AtPrime/Basic.lean b/Mathlib/RingTheory/Localization/AtPrime/Basic.lean
index 6b31179527cbc3..99fffb1bfccc12 100644
--- a/Mathlib/RingTheory/Localization/AtPrime/Basic.lean
+++ b/Mathlib/RingTheory/Localization/AtPrime/Basic.lean
@@ -209,7 +209,7 @@ lemma AtPrime.eq_maximalIdeal_iff_comap_eq {J : Ideal (Localization.AtPrime I)}
 theorem le_comap_primeCompl_iff {J : Ideal P} [J.IsPrime] {f : R →+* P} :
     I.primeCompl ≤ J.primeCompl.comap f ↔ J.comap f ≤ I :=
   ⟨fun h x hx => by
-    contrapose! hx
+    contrapose hx
     exact h hx,
    fun h _ hx hfxJ => hx (h hfxJ)⟩
 
diff --git a/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean b/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean
index e93254d741b543..60dc45531aeb56 100644
--- a/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean
+++ b/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean
@@ -154,7 +154,7 @@ theorem rel_add_cases (x y : R) : x + y ≤ᵥ x ∨ x + y ≤ᵥ y :=
   (rel_total y x).imp (fun h => rel_add .rfl h) (fun h => rel_add h .rfl)
 
 lemma zero_srel_mul {x y : R} (hx : 0 <ᵥ x) (hy : 0 <ᵥ y) : 0 <ᵥ x * y := by
-  contrapose! hy
+  contrapose hy
   rw [not_srel_iff] at hy ⊢
   rw [show (0 : R) = x * 0 by simp, mul_comm x y, mul_comm x 0] at hy
   exact rel_mul_cancel hx hy
diff --git a/Mathlib/SetTheory/Ordinal/Principal.lean b/Mathlib/SetTheory/Ordinal/Principal.lean
index e2656043f8858c..34300661974ea4 100644
--- a/Mathlib/SetTheory/Ordinal/Principal.lean
+++ b/Mathlib/SetTheory/Ordinal/Principal.lean
@@ -181,7 +181,7 @@ theorem exists_lt_add_of_not_principal_add (ha : ¬ Principal (· + ·) a) :
 
 theorem principal_add_iff_add_lt_ne_self : Principal (· + ·) a ↔ ∀ b < a, ∀ c < a, b + c ≠ a :=
   ⟨fun ha _ hb _ hc => (ha hb hc).ne, fun H => by
-    by_contra! ha
+    by_contra ha
     rcases exists_lt_add_of_not_principal_add ha with ⟨b, hb, c, hc, rfl⟩
     exact (H b hb c hc).irrefl⟩
 
diff --git a/Mathlib/Tactic/ByCases.lean b/Mathlib/Tactic/ByCases.lean
index 6b2ebb51237671..9d242947a1d2d2 100644
--- a/Mathlib/Tactic/ByCases.lean
+++ b/Mathlib/Tactic/ByCases.lean
@@ -13,17 +13,21 @@ The `by_cases!` tactic is a variant of the `by_cases` tactic that also calls `pu
 on the generated hypothesis that is a negation.
 -/
 
+namespace Mathlib.Tactic.ByCases
+open Lean.Parser.Tactic
+
 /--
 `by_cases! h : p` runs the `by_cases h : p` tactic, followed by
-`try push_neg at h` in the second subgoal. For example,
-- `by_cases! h : a < b` creates one goal with hypothesis `h : a < b` and
-  another with `h : b ≤ a`.
-- `by_cases! h : a ≠ b` creates one goal with hypothesis `h : a ≠ b` and
-  another with `h : a = b`.
+`push_neg at h` in the second subgoal. For example,
+- `by_cases! h : a < b` creates one goal with hypothesis `h : a < b` and another with `h : b ≤ a`.
+- `by_cases! h : a ≠ b` creates one goal with hypothesis `h : a ≠ b` and another with `h : a = b`.
 -/
-syntax (name := byCases!) "by_cases! " (atomic(ident " : "))? term : tactic
+syntax (name := byCases!) "by_cases! " optConfig (atomic(ident " : "))? term : tactic
 
 macro_rules
-  | `(tactic| by_cases! $e) => `(tactic| by_cases! h : $e)
-  | `(tactic| by_cases! $h : $e) =>
-    `(tactic| by_cases $h : $e; try on_goal 2 => push_neg at $h:ident)
+  | `(tactic| by_cases! $cfg:optConfig $e) => `(tactic| by_cases! $cfg h : $e)
+  | `(tactic| by_cases! $cfg:optConfig $h : $e) =>
+    `(tactic| by_cases $h : $e;
+      on_goal 2 => push_neg $[$(getConfigItems cfg)]* +failIfUnchanged at $h:ident)
+
+end Mathlib.Tactic.ByCases
diff --git a/Mathlib/Tactic/ByContra.lean b/Mathlib/Tactic/ByContra.lean
index c04034caa40f4e..9e0979f72fed26 100644
--- a/Mathlib/Tactic/ByContra.lean
+++ b/Mathlib/Tactic/ByContra.lean
@@ -37,17 +37,18 @@ example : 1 < 2 := by
   -- h : ¬ 1 < 2 ⊢ False
 ```
 -/
-syntax (name := byContra!) "by_contra!" (ppSpace colGt binderIdent)? Term.optType : tactic
+syntax (name := byContra!) "by_contra!" optConfig (ppSpace colGt binderIdent)? Term.optType : tactic
 
 macro_rules
-  | `(tactic| by_contra! $[: $ty]?) =>
-    `(tactic| by_contra! $(mkIdent `this):ident $[: $ty]?)
-  | `(tactic| by_contra! _%$under $[: $ty]?) =>
-    `(tactic| by_contra! $(mkIdentFrom under `this):ident $[: $ty]?)
-  | `(tactic| by_contra! $e:ident) => `(tactic| (by_contra $e:ident; try push_neg at $e:ident))
-  | `(tactic| by_contra! $e:ident : $y) => `(tactic|
-       (by_contra! h
+  | `(tactic| by_contra! $cfg $[: $ty]?) =>
+    `(tactic| by_contra! $cfg $(mkIdent `this):ident $[: $ty]?)
+  | `(tactic| by_contra! $cfg _%$under $[: $ty]?) =>
+    `(tactic| by_contra! $cfg $(mkIdentFrom under `this):ident $[: $ty]?)
+  | `(tactic| by_contra! $cfg $e:ident) =>
+    `(tactic| by_contra $e:ident; push_neg $[$(getConfigItems cfg)]* +failIfUnchanged at $e:ident)
+  | `(tactic| by_contra! $cfg $e:ident : $y) => `(tactic|
+       (by_contra! $cfg h
         -- if the below `exact` call fails then this tactic should fail with the message
         -- tactic failed: <goal type> and <type of h> are not definitionally equal
-        have $e:ident : $y := by { (try push_neg); exact h }
+        have $e:ident : $y := by { push_neg $[$(getConfigItems cfg)]* -failIfUnchanged; exact h }
         clear h))
diff --git a/Mathlib/Tactic/Contrapose.lean b/Mathlib/Tactic/Contrapose.lean
index e52a9915dfc1a7..45688ceac6a6c6 100644
--- a/Mathlib/Tactic/Contrapose.lean
+++ b/Mathlib/Tactic/Contrapose.lean
@@ -20,6 +20,7 @@ implication.
 
 -/
 namespace Mathlib.Tactic.Contrapose
+open Lean.Parser.Tactic
 
 lemma mtr {p q : Prop} : (¬ q → ¬ p) → (p → q) := fun h hp ↦ by_contra (fun h' ↦ h h' hp)
 
@@ -39,10 +40,14 @@ macro_rules
 Transforms the goal into its contrapositive and uses pushes negations inside `P` and `Q`.
 Usage matches `contrapose`
 -/
-syntax (name := contrapose!) "contrapose!" (ppSpace colGt ident (" with " ident)?)? : tactic
+syntax (name := contrapose!)
+  "contrapose!" optConfig (ppSpace colGt ident (" with " ident)?)? : tactic
 macro_rules
-  | `(tactic| contrapose!) => `(tactic| (contrapose; try push_neg))
-  | `(tactic| contrapose! $e) => `(tactic| (revert $e:ident; contrapose!; intro $e:ident))
-  | `(tactic| contrapose! $e with $e') => `(tactic| (revert $e:ident; contrapose!; intro $e':ident))
+  | `(tactic| contrapose! $cfg) =>
+    `(tactic| (contrapose; push_neg $[$(getConfigItems cfg)]* +failIfUnchanged))
+  | `(tactic| contrapose! $cfg:optConfig $e) =>
+    `(tactic| (revert $e:ident; contrapose! $cfg; intro $e:ident))
+  | `(tactic| contrapose! $cfg:optConfig $e with $e') =>
+    `(tactic| (revert $e:ident; contrapose! $cfg; intro $e':ident))
 
 end Mathlib.Tactic.Contrapose
diff --git a/Mathlib/Tactic/NormNum/Core.lean b/Mathlib/Tactic/NormNum/Core.lean
index 087ce9a7a6d672..9ecceb69c9bf1e 100644
--- a/Mathlib/Tactic/NormNum/Core.lean
+++ b/Mathlib/Tactic/NormNum/Core.lean
@@ -243,7 +243,7 @@ def elabNormNum (cfg args loc : Syntax) (simpOnly := false) (useSimp := true) :
   let ctx ← getSimpContext cfg args (!useSimp || simpOnly)
   let loc := expandOptLocation loc
   transformAtNondepPropLocation (fun e ctx ↦ deriveSimp ctx useSimp e) "norm_num" loc
-    (failIfUnchanged := false) (mayCloseGoalFromHyp := true) ctx
+    (failIfUnchanged := .silent) (mayCloseGoalFromHyp := true) ctx
 
 end Meta.NormNum
 
diff --git a/Mathlib/Tactic/Push.lean b/Mathlib/Tactic/Push.lean
index 9eea6a116ad295..51bd3bc12d1d48 100644
--- a/Mathlib/Tactic/Push.lean
+++ b/Mathlib/Tactic/Push.lean
@@ -195,6 +195,17 @@ end ElabHead
 def elabDischarger (stx : TSyntax ``discharger) : TacticM Simp.Discharge :=
   (·.2) <$> tacticToDischarge stx.raw[3]
 
+/-- The configuration options for the `push` tactic. -/
+structure Config where
+  /-- If `true` (default `false`), rewrite `¬ (p ∧ q)` into `¬ p ∨ ¬ q` instead of `p → ¬ q`.
+  This is equivalent to using `set_option push_neg.use_distrib true`. -/
+  distrib : Bool := false
+  /-- If `true` (default: `true`), then calls to `push` will fail if they do not make progress. -/
+  failIfUnchanged : Bool := true
+
+/-- Function elaborating `Push.Config`. -/
+declare_config_elab elabPushConfig Config
+
 /--
 `push` pushes the given constant away from the head of the expression. For example
 - `push _ ∈ _` rewrites `x ∈ {y} ∪ zᶜ` into `x = y ∨ ¬ x ∈ z`.
@@ -212,12 +223,15 @@ To instead move a constant closer to the head of the expression, use the `pull`
 
 To push a constant at a hypothesis, use the `push ... at h` or `push ... at *` syntax.
 -/
-elab (name := push) "push" disch?:(discharger)? head:(ppSpace colGt term) loc:(location)? :
-    tactic => do
+elab (name := push) "push" cfg:optConfig disch?:(discharger)? head:(ppSpace colGt term)
+    loc:(location)? : tactic => do
+  let cfg ← elabPushConfig cfg
   let disch? ← disch?.mapM elabDischarger
   let head ← elabHead head
   let loc := (loc.map expandLocation).getD (.targets #[] true)
-  transformAtLocation (pushCore head · disch?) "push" loc (failIfUnchanged := true) false
+  let level : LogIfUnchanged := if cfg.failIfUnchanged then .error else .warning
+  (if cfg.distrib then withOptions (·.setBool `push_neg.use_distrib true) else id) <|
+    transformAtLocation (pushCore head · disch?) "push" loc level
 
 /--
 Push negations into the conclusion or a hypothesis.
@@ -228,7 +242,7 @@ For instance, a hypothesis `h : ¬ ∀ x, ∃ y, x ≤ y` will be transformed by
 The `push` tactic can be extended using the `@[push]` attribute. `push` has special-casing
 built in for `push Not`, so that it can preserve binder names, and so that `¬ (p ∧ q)` can be
 transformed to either `p → ¬ q` (the default) or `¬ p ∨ ¬ q`. To get `¬ p ∨ ¬ q`, use
-`set_option push_neg.use_distrib true`.
+`set_option push_neg.use_distrib true` or `push_neg +distrib`.
 
 Another example: given a hypothesis
 ```lean
@@ -243,7 +257,8 @@ using the relevant lemmas. One can use this tactic at the goal using `push_neg`,
 at every hypothesis and the goal using `push_neg at *` or at selected hypotheses and the goal
 using say `push_neg at h h' ⊢`, as usual.
 -/
-macro (name := push_neg) "push_neg" loc:(location)? : tactic => `(tactic| push Not $[$loc]?)
+macro (name := push_neg) "push_neg" cfg:optConfig loc:(location)? : tactic =>
+  `(tactic| push $cfg Not $[$loc]?)
 
 /--
 `pull` is the inverse tactic to `push`.
@@ -266,7 +281,7 @@ elab (name := pull) "pull" disch?:(discharger)? head:(ppSpace colGt term) loc:(l
   let disch? ← disch?.mapM elabDischarger
   let head ← elabHead head
   let loc := (loc.map expandLocation).getD (.targets #[] true)
-  transformAtLocation (pullCore head · disch?) "pull" loc (failIfUnchanged := true) false
+  transformAtLocation (pullCore head · disch?) "pull" loc (failIfUnchanged := .error) false
 
 /-- A simproc variant of `push fun _ ↦ _`, to be used as `simp [↓pushFun]`. -/
 simproc_decl _root_.pushFun (fun _ ↦ ?_) := pushStep .lambda
@@ -277,13 +292,18 @@ simproc_decl _root_.pullFun (_) := pullStep .lambda
 section Conv
 
 @[inherit_doc push]
-elab "push" disch?:(discharger)? head:(ppSpace colGt term) : conv => withMainContext do
+elab "push" cfg:optConfig disch?:(discharger)? head:(ppSpace colGt term) : conv =>
+  withMainContext do
+  let cfg ← elabPushConfig cfg
   let disch? ← disch?.mapM elabDischarger
   let head ← elabHead head
-  Conv.applySimpResult (← pushCore head (← instantiateMVars (← Conv.getLhs)) disch?)
+  (if cfg.distrib then withOptions (·.setBool `push_neg.use_distrib true) else id) <|
+    -- TODO: this doesn't throw an error when it does nothing.
+    -- Note that conv-mode `simp` has the same problem.
+    Conv.applySimpResult (← pushCore head (← instantiateMVars (← Conv.getLhs)) disch?)
 
 @[inherit_doc push_neg]
-macro "push_neg" : conv => `(conv| push Not)
+macro "push_neg" cfg:optConfig : conv => `(conv| push $cfg Not)
 
 /--
 The syntax is `#push head e`, where `head` is a constant and `e` is an expression,
@@ -291,8 +311,8 @@ which will print the `push head` form of `e`.
 
 `#push` understands local variables, so you can use them to introduce parameters.
 -/
-macro (name := pushCommand) tk:"#push " head:ident ppSpace e:term : command =>
-  `(command| #conv%$tk push $head:ident => $e)
+macro (name := pushCommand) tk:"#push " cfg:optConfig head:ident ppSpace e:term : command =>
+  `(command| #conv%$tk push $cfg $head:ident => $e)
 
 /--
 The syntax is `#push_neg e`, where `e` is an expression,
@@ -300,7 +320,8 @@ which will print the `push_neg` form of `e`.
 
 `#push_neg` understands local variables, so you can use them to introduce parameters.
 -/
-macro (name := pushNegCommand) tk:"#push_neg " e:term : command => `(command| #push%$tk Not $e)
+macro (name := pushNegCommand) tk:"#push_neg " cfg:optConfig e:term : command =>
+ `(command| #push%$tk $cfg Not $e)
 
 @[inherit_doc pull]
 elab "pull" disch?:(discharger)? head:(ppSpace colGt term) : conv => withMainContext do
diff --git a/Mathlib/Topology/LocallyFinsupp.lean b/Mathlib/Topology/LocallyFinsupp.lean
index 47a156797487d0..0cea1f75ed6461 100644
--- a/Mathlib/Topology/LocallyFinsupp.lean
+++ b/Mathlib/Topology/LocallyFinsupp.lean
@@ -183,7 +183,7 @@ protected def addSubgroup [AddCommGroup Y] : AddSubgroup (X → Y) where
   add_mem' {f g} hf hg := by
     constructor
     · intro x hx
-      contrapose! hx
+      contrapose hx
       simp [notMem_support.1 fun a ↦ hx (hf.1 a), notMem_support.1 fun a ↦ hx (hg.1 a)]
     · intro z hz
       obtain ⟨t₁, ht₁⟩ := hf.2 z hz
diff --git a/Mathlib/Topology/Maps/Basic.lean b/Mathlib/Topology/Maps/Basic.lean
index 5b3d82e70ed759..5008acbb0121f1 100644
--- a/Mathlib/Topology/Maps/Basic.lean
+++ b/Mathlib/Topology/Maps/Basic.lean
@@ -390,7 +390,7 @@ theorem isOpenMap_iff_clusterPt_comap :
   refine ⟨fun hf _ _ ↦ hf.clusterPt_comap, fun h ↦ ?_⟩
   simp only [isOpenMap_iff_nhds_le, le_map_iff]
   intro x s hs
-  contrapose! hs
+  contrapose hs
   rw [← mem_interior_iff_mem_nhds, mem_interior_iff_not_clusterPt_compl, not_not] at hs ⊢
   exact (h _ _ hs).mono <| by simp [subset_preimage_image]
 
diff --git a/Mathlib/Topology/Separation/Regular.lean b/Mathlib/Topology/Separation/Regular.lean
index 589d233beaa1ea..b624f39301846d 100644
--- a/Mathlib/Topology/Separation/Regular.lean
+++ b/Mathlib/Topology/Separation/Regular.lean
@@ -312,7 +312,7 @@ lemma IsCompact.closure_eq_nhdsKer [RegularSpace X] {s : Set X} (hs : IsCompact
   · rw [nhdsKer, ← hs.lift'_closure_nhdsSet]
     simp +contextual [Filter.lift', Filter.lift, closure_mono, subset_of_mem_nhdsSet]
   · intro y hy
-    by_contra! hy'
+    by_contra hy'
     rw [← _root_.disjoint_nhdsSet_nhds, Filter.disjoint_iff] at hy'
     obtain ⟨t, hts, t', ht'y, H⟩ := hy'
     exact Set.disjoint_iff.mp H ⟨hy t hts, mem_of_mem_nhds ht'y⟩
diff --git a/Mathlib/Util/AtLocation.lean b/Mathlib/Util/AtLocation.lean
index fde4cd6e93c590..9bc8a55859733e 100644
--- a/Mathlib/Util/AtLocation.lean
+++ b/Mathlib/Util/AtLocation.lean
@@ -42,16 +42,25 @@ def Lean.Elab.Tactic.withNondepPropLocation (loc : Location) (atLocal : FVarId 
 namespace Mathlib.Tactic
 open Lean Meta Elab.Tactic
 
+inductive LogIfUnchanged where
+  | silent
+  | warning
+  | error
+
 /-- Use the procedure `m` to rewrite the provided goal. -/
 def transformAtTarget (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (proc : String)
-    (failIfUnchanged : Bool) (goal : MVarId) :
+    (failIfUnchanged : LogIfUnchanged) (goal : MVarId) :
     ReaderT Simp.Context MetaM (Option MVarId) := do
   let tgt ← instantiateMVars (← goal.getType)
   let r ← m tgt
   -- we use expression equality here (rather than defeq) to be consistent with, e.g.,
   -- `applySimpResultToTarget`
   let unchanged := tgt.cleanupAnnotations == r.expr.cleanupAnnotations
-  if failIfUnchanged && unchanged then throwError "{proc} made no progress on goal"
+  if unchanged then
+    match failIfUnchanged with
+    | .warning => logWarning m!"{proc} made no progress on the goal"
+    | .error => throwError "{proc} made no progress on the goal"
+    | .silent => pure ()
   if r.expr.isTrue then
     goal.assign (← mkOfEqTrue (← r.getProof))
     pure none
@@ -67,7 +76,7 @@ The `simpTheorems` of the simp-context carried with `m` will be modified to remo
 this ensures that if the procedure `m` involves rewriting by this `SimpTheoremsArray`, then, e.g.,
 `h : x = y` is not transformed (by rewriting `h`) to `True`. -/
 def transformAtLocalDecl (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (proc : String)
-    (failIfUnchanged : Bool) (mayCloseGoal : Bool) (fvarId : FVarId) (goal : MVarId) :
+    (failIfUnchanged : LogIfUnchanged) (mayCloseGoal : Bool) (fvarId : FVarId) (goal : MVarId) :
     ReaderT Simp.Context MetaM (Option MVarId) := do
   let ldecl ← fvarId.getDecl
   if ldecl.isImplementationDetail then
@@ -78,13 +87,17 @@ def transformAtLocalDecl (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (
   let r ← withReader eraseFVarId <| m tgt
   -- we use expression equality here (rather than defeq) to be consistent with, e.g.,
   -- `applySimpResultToLocalDeclCore`
-  if failIfUnchanged && tgt.cleanupAnnotations == r.expr.cleanupAnnotations then
-    throwError "{proc} made no progress at {ldecl.userName}"
+  if tgt.cleanupAnnotations == r.expr.cleanupAnnotations then
+    match failIfUnchanged with
+    | .warning => logWarning m!"{proc} made no progress at {ldecl.userName}"
+    | .error => throwError "{proc} made no progress at {ldecl.userName}"
+    | .silent => pure ()
   return (← applySimpResultToLocalDecl goal fvarId r mayCloseGoal).map Prod.snd
 
 /-- Use the procedure `m` to transform at specified locations (hypotheses and/or goal). -/
 def transformAtLocation (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (proc : String)
-    (loc : Location) (failIfUnchanged : Bool := true) (mayCloseGoalFromHyp : Bool := false)
+    (loc : Location) (failIfUnchanged : LogIfUnchanged := .error)
+    (mayCloseGoalFromHyp : Bool := false)
     -- streamline the most common use case, in which the procedure `m`'s implementation is not
     -- simp-based and its `Simp.Context` is ignored
     (ctx : Simp.Context := default) :
@@ -98,7 +111,7 @@ def transformAtLocation (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (p
 
 In the wildcard case (`*`), filter out all dependent and/or non-Prop hypotheses. -/
 def transformAtNondepPropLocation (m : Expr → ReaderT Simp.Context MetaM Simp.Result)
-    (proc : String) (loc : Location) (failIfUnchanged : Bool := true)
+    (proc : String) (loc : Location) (failIfUnchanged : LogIfUnchanged := .error)
     (mayCloseGoalFromHyp : Bool := false)
     -- streamline the most common use case, in which the procedure `m`'s implementation is not
     -- simp-based and its `Simp.Context` is ignored
diff --git a/MathlibTest/Contrapose.lean b/MathlibTest/Contrapose.lean
index f016ae64237590..4e2eaafbb38690 100644
--- a/MathlibTest/Contrapose.lean
+++ b/MathlibTest/Contrapose.lean
@@ -44,3 +44,8 @@ example (p : Prop) (h : p) : p := by
 example (p q : Type) (h : p → q) : p → q := by
   fail_if_success { contrapose }
   exact h
+
+example (p q r : Prop) (h' : ¬p ∨ ¬q) (h : p ∧ q) : r := by
+  fail_if_success contrapose! +fdsewfjdsk h
+  contrapose! +distrib h
+  exact h'
diff --git a/MathlibTest/byContra.lean b/MathlibTest/byContra.lean
index 365c2ad9bc0130..f8102c04049a75 100644
--- a/MathlibTest/byContra.lean
+++ b/MathlibTest/byContra.lean
@@ -6,7 +6,6 @@ import Mathlib.Algebra.Notation.Defs
 import Mathlib.Data.Nat.Basic
 import Mathlib.Order.Basic
 
-set_option autoImplicit true
 example (a b : ℕ) (foo : False)  : a < b := by
   by_contra!
   guard_hyp this : b ≤ a
@@ -27,17 +26,23 @@ example : 1 < 2 := by
   guard_hyp this : 2 ≤ 1
   contradiction
 
-example (_p : Prop) (bar : False) : ¬ ¬ ¬ ¬ ¬ ¬ P := by
+example (P : Prop) (bar : False) : ¬ ¬ ¬ ¬ ¬ ¬ P := by
   by_contra! foo : ¬ ¬ ¬ P -- normalises to ¬ P, as does ¬ (goal).
   guard_hyp foo : ¬ ¬ ¬ P
   exact bar
 
-example (_p : Prop) (bar : False) : ¬ ¬ ¬ ¬ ¬ ¬ P := by
+example (P : Prop) (bar : False) : ¬ ¬ ¬ ¬ ¬ ¬ P := by
   by_contra! : ¬ ¬ ¬ P
   guard_hyp this : ¬ ¬ ¬ P
   exact bar
 
-variable [LinearOrder α] [One α] [Mul α]
+example (P Q : Prop) (h' : False) : P ∧ Q := by
+  fail_if_success by_contra! +fdsewfjdsk h
+  by_contra! +distrib h
+  guard_hyp h : ¬P ∨ ¬Q
+  exact h'
+
+variable {α} [LinearOrder α] [One α] [Mul α]
 
 example (x : α) (f : False) : x ≤ 1 := by
   set a := x * x
diff --git a/MathlibTest/push_neg.lean b/MathlibTest/push_neg.lean
index f71ca97a1fef97..10cdc4a6e64e6e 100644
--- a/MathlibTest/push_neg.lean
+++ b/MathlibTest/push_neg.lean
@@ -165,9 +165,15 @@ def inductive_proof : True := by
   trivial
 
 section use_distrib
+
+example (h : ¬ p ∨ ¬ q) : ¬ (p ∧ q) := by
+  push_neg +distrib
+  guard_target = ¬p ∨ ¬q
+  exact h
+
 set_option push_neg.use_distrib true
 
-example (h : ¬ p ∨ ¬ q): ¬ (p ∧ q) := by
+example (h : ¬ p ∨ ¬ q) : ¬ (p ∧ q) := by
   push_neg
   guard_target = ¬p ∨ ¬q
   exact h