feat(push_neg): push_neg +distrib syntax (leanprover-community#31406)

JovanGerb · JovanGerb · commit 06bb38c58b39 · 2025-12-05T13:19:29.000Z
This PR adds the syntax `push_neg +distrib`, `by_cases! +distrib`, `contrapose! +distrib` and `by_contra! +distrib`. This is much more convenient to use than writing out `set_option push_neg.use_distrib true in`. All uses of the `set_option` version have been replaced with the new syntax.

I also add a missing `namespace` in the definition of `by_cases!` and `by_contra!`
diff --git a/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean b/Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@@ -854,10 +854,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 α`.
@@ -1007,10 +1006,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
@@ -662,10 +662,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
@@ -820,10 +819,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
@@ -260,7 +260,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⟩)
@@ -435,7 +435,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/Analysis/SpecialFunctions/BinaryEntropy.lean b/Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
@@ -183,7 +183,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
@@ -196,7 +195,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/Data/EReal/Operations.lean b/Mathlib/Data/EReal/Operations.lean
@@ -751,7 +751,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) :
@@ -763,7 +763,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/Finite/Prod.lean b/Mathlib/Data/Finite/Prod.lean
@@ -178,8 +178,7 @@ protected theorem infinite_prod :
     · exact h.1.prod_right h.2
 
 theorem finite_prod : (s ×ˢ t).Finite ↔ (s.Finite ∨ t = ∅) ∧ (t.Finite ∨ s = ∅) := by
-  set_option push_neg.use_distrib true in
-  contrapose!; exact Set.infinite_prod
+  contrapose! +distrib; exact Set.infinite_prod
 
 protected theorem Finite.offDiag {s : Set α} (hs : s.Finite) : s.offDiag.Finite :=
   (hs.prod hs).subset s.offDiag_subset_prod
@@ -236,7 +235,7 @@ theorem infinite_image2 (hfs : ∀ b ∈ t, InjOn (fun a => f a b) s) (hft : ∀
 
 lemma finite_image2 (hfs : ∀ b ∈ t, InjOn (f · b) s) (hft : ∀ a ∈ s, InjOn (f a) t) :
     (image2 f s t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅ := by
-  set_option push_neg.use_distrib true in contrapose!
+  contrapose! +distrib
   rw [Set.infinite_image2 hfs hft]
   grind only [Set.Infinite.nonempty]
 
diff --git a/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean b/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
@@ -410,8 +410,7 @@ theorem oangle_eq_zero_or_eq_pi_iff_right_eq_smul {x y : V} :
 are linearly independent. -/
 theorem oangle_ne_zero_and_ne_pi_iff_linearIndependent {x y : V} :
     o.oangle x y ≠ 0 ∧ o.oangle x y ≠ π ↔ LinearIndependent ℝ ![x, y] := by
-  set_option push_neg.use_distrib true in
-  contrapose!; exact oangle_eq_zero_or_eq_pi_iff_not_linearIndependent o
+  contrapose! +distrib; exact oangle_eq_zero_or_eq_pi_iff_not_linearIndependent o
 
 /-- Two vectors are equal if and only if they have equal norms and zero angle between them. -/
 theorem eq_iff_norm_eq_and_oangle_eq_zero (x y : V) : x = y ↔ ‖x‖ = ‖y‖ ∧ o.oangle x y = 0 := by
diff --git a/Mathlib/LinearAlgebra/LinearIndependent/Defs.lean b/Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
@@ -633,7 +633,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/NumberTheory/Padics/PadicVal/Basic.lean b/Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
@@ -98,7 +98,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
@@ -296,8 +296,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
@@ -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/Order/Quotient.lean b/Mathlib/Order/Quotient.lean
@@ -120,7 +120,7 @@ instance [DecidableRel (· ≈ · : α → α → Prop)] : LinearOrder (Quotient
 
 theorem mk_lt_mk {x y : α} : Quotient.mk s x < Quotient.mk s y ↔ x < y ∧ ¬ x ≈ y := by
   classical
-  set_option push_neg.use_distrib true in contrapose!
+  contrapose! +distrib
   rw [mk_le_mk, comm_of (· ≈ ·)]
 
 theorem lt_of_mk_lt_mk {x y : α} (h : Quotient.mk s x < Quotient.mk s y) : x < y :=
diff --git a/Mathlib/RingTheory/Ideal/Basic.lean b/Mathlib/RingTheory/Ideal/Basic.lean
@@ -277,7 +277,7 @@ theorem isField_iff_isSimpleOrder_ideal : IsField R ↔ IsSimpleOrder (Ideal R)
       ⟨fun h => (not_isField_of_subsingleton _ h).elim, fun h =>
         (false_of_nontrivial_of_subsingleton <| Ideal R).elim⟩
   rw [← not_iff_not, Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top]
-  set_option push_neg.use_distrib true in contrapose!
+  contrapose! +distrib
   simp_rw [not_lt_top_iff, not_bot_lt_iff]
   exact ⟨fun h => ⟨h⟩, fun h => h.2⟩
 
diff --git a/Mathlib/SetTheory/Cardinal/Arithmetic.lean b/Mathlib/SetTheory/Cardinal/Arithmetic.lean
@@ -575,7 +575,7 @@ theorem mk_arrow_eq_zero_iff : #(α → β') = 0 ↔ #α ≠ 0 ∧ #β' = 0 := b
 
 theorem mk_surjective_eq_zero_iff_lift :
     #{f : α → β' | Surjective f} = 0 ↔ lift.{v} #α < lift.{u} #β' ∨ (#α ≠ 0 ∧ #β' = 0) := by
-  set_option push_neg.use_distrib true in contrapose!
+  contrapose! +distrib
   rw [lift_mk_le', and_comm]
   simp_rw [mk_ne_zero_iff, mk_eq_zero_iff, nonempty_coe_sort,
     Set.Nonempty, mem_setOf, exists_surjective_iff, nonempty_fun]
diff --git a/Mathlib/Tactic/ByCases.lean b/Mathlib/Tactic/ByCases.lean
@@ -17,17 +17,26 @@ on the generated hypothesis that is a negation.
 
 public meta section
 
+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,
+`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
+
+local elab "try_push_neg_at" cfg:optConfig h:ident : tactic => do
+  Push.push (← Push.elabPushConfig cfg) none (.const ``Not) (.targets #[h] false)
+    (failIfUnchanged := false)
 
 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 => try_push_neg_at $cfg $h:ident)
+
+end Mathlib.Tactic.ByCases
diff --git a/Mathlib/Tactic/ByContra.lean b/Mathlib/Tactic/ByContra.lean
@@ -16,6 +16,7 @@ The `by_contra!` tactic is a variant of the `by_contra` tactic, for proofs of co
 
 public meta section
 
+namespace Mathlib.Tactic.ByContra
 open Lean Parser.Tactic
 
 /--
@@ -44,14 +45,29 @@ example : 1 < 2 := by
   -- h : ¬ 1 < 2 ⊢ False
 ```
 -/
-syntax (name := byContra!) "by_contra!" (ppSpace colGt rcasesPatMed)? (" : " term)? : tactic
+syntax (name := byContra!)
+  "by_contra!" optConfig (ppSpace colGt rcasesPatMed)? (" : " term)? : tactic
+
+local elab "try_push_neg_at" cfg:optConfig h:ident : tactic => do
+  Push.push (← Push.elabPushConfig cfg) none (.const ``Not) (.targets #[h] false)
+    (failIfUnchanged := false)
+
+local elab "try_push_neg" cfg:optConfig : tactic => do
+  Push.push (← Push.elabPushConfig cfg) none (.const ``Not) (.targets #[] true)
+    (failIfUnchanged := false)
 
 macro_rules
-| `(tactic| by_contra! $[$pat?]? $[: $ty?]?) => do
+| `(tactic| by_contra! $cfg $[$pat?]? $[: $ty?]?) => do
   let pat ← pat?.getDM `(rcasesPatMed| $(mkIdent `this):ident)
   let replaceTac ← match ty? with
-    | some ty => `(tactic| replace h : $ty := by (try push_neg); exact h) -- Let `h` have type `ty`.
+    | some ty => `(tactic|
+      replace h : $ty := by try_push_neg $cfg; exact h) -- Let `h` have type `ty`.
     | none => `(tactic| skip)
   -- We have to use `revert h; rintro $pat` instead of `obtain $pat := h`,
   -- because if `$pat` is a variable, `obtain $pat := h` doesn't do anything.
-  `(tactic| (by_contra h; (try push_neg at h); $replaceTac; revert h; rintro ($pat:rcasesPatMed)))
+  `(tactic| (
+    by_contra h;
+    try_push_neg_at $cfg h; $replaceTac;
+    revert h; rintro ($pat:rcasesPatMed)))
+
+end Mathlib.Tactic.ByContra
diff --git a/Mathlib/Tactic/Contrapose.lean b/Mathlib/Tactic/Contrapose.lean
@@ -21,7 +21,9 @@ implication or an iff. It also avoids creating a double negation if there alread
 -/
 
 public meta section
+
 namespace Mathlib.Tactic.Contrapose
+open Lean.Parser.Tactic
 
 /-- An option to turn off the feature that `contrapose` negates both sides of `↔` goals.
 This may be useful for teaching. -/
@@ -88,10 +90,18 @@ elab_rules : tactic
 Transforms the goal into its contrapositive and pushes negations in the result.
 Usage matches `contrapose`
 -/
-syntax (name := contrapose!) "contrapose!" (ppSpace colGt ident (" with " ident)?)? : tactic
+syntax (name := contrapose!)
+  "contrapose!" optConfig (ppSpace colGt ident (" with " ident)?)? : tactic
+
+local elab "try_push_neg" cfg:optConfig : tactic => do
+  Push.push (← Push.elabPushConfig cfg) none (.const ``Not) (.targets #[] true)
+    (failIfUnchanged := false)
+
 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; try_push_neg $cfg))
+  | `(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/Push.lean b/Mathlib/Tactic/Push.lean
diff --git a/MathlibTest/Contrapose.lean b/MathlibTest/Contrapose.lean
diff --git a/MathlibTest/byContra.lean b/MathlibTest/byContra.lean
diff --git a/MathlibTest/push_neg.lean b/MathlibTest/push_neg.lean
