chore: use by_contra' instead of by_contra + push_neg (#8798)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Dec 3, 2023 · b1cd52a · b1cd52a
1 parent fa76ed8
commit b1cd52a
Show file tree

Hide file tree

Showing 11 changed files with 11 additions and 22 deletions.
diff --git a/Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean b/Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean
@@ -136,8 +136,7 @@ theorem erdos_szekeres {r s n : ℕ} {f : Fin n → α} (hn : r * s < n) (hf : I
   -- Finished both goals!
   -- Now that we have uniqueness of each label, it remains to do some counting to finish off.
   -- Suppose all the labels are small.
-  by_contra q
-  push_neg at q
+  by_contra' q
   -- Then the labels `(a_i, b_i)` all fit in the following set: `{ (x,y) | 1 ≤ x ≤ r, 1 ≤ y ≤ s }`
   let ran : Finset (ℕ × ℕ) := (range r).image Nat.succ ×ˢ (range s).image Nat.succ
   -- which we prove here.

diff --git a/Mathlib/Data/Set/Intervals/Basic.lean b/Mathlib/Data/Set/Intervals/Basic.lean
@@ -1180,8 +1180,7 @@ theorem Ico_eq_Ico_iff (h : a₁ < b₁ ∨ a₂ < b₂) : Ico a₁ b₁ = Ico a
 
 lemma Ici_eq_singleton_iff_isTop {x : α} : (Ici x = {x}) ↔ IsTop x := by
   refine ⟨fun h y ↦ ?_, fun h ↦ by ext y; simp [(h y).ge_iff_eq]⟩
-  by_contra H
-  push_neg at H
+  by_contra' H
   have : y ∈ Ici x := H.le
   rw [h, mem_singleton_iff] at this
   exact lt_irrefl y (this.le.trans_lt H)

diff --git a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean
@@ -159,8 +159,7 @@ theorem sum_eq_one {x} (hx : x ∈ s) : ∑ᶠ i, f i x = 1 :=
 #align smooth_partition_of_unity.sum_eq_one SmoothPartitionOfUnity.sum_eq_one
 
 theorem exists_pos_of_mem {x} (hx : x ∈ s) : ∃ i, 0 < f i x := by
-  by_contra h
-  push_neg at h
+  by_contra' h
   have H : ∀ i, f i x = 0 := fun i ↦ le_antisymm (h i) (f.nonneg i x)
   have := f.sum_eq_one hx
   simp_rw [H] at this

diff --git a/Mathlib/ModelTheory/Satisfiability.lean b/Mathlib/ModelTheory/Satisfiability.lean
@@ -683,8 +683,7 @@ theorem Categorical.isComplete (h : κ.Categorical T) (h1 : ℵ₀ ≤ κ)
   ⟨hS, fun φ => by
     obtain ⟨_, _⟩ := Theory.exists_model_card_eq ⟨hS.some, hT hS.some⟩ κ h1 h2
     rw [Theory.models_sentence_iff, Theory.models_sentence_iff]
-    by_contra con
-    push_neg at con
+    by_contra' con
     obtain ⟨⟨MF, hMF⟩, MT, hMT⟩ := con
     rw [Sentence.realize_not, Classical.not_not] at hMT
     refine' hMF _

diff --git a/Mathlib/NumberTheory/ClassNumber/AdmissibleCardPowDegree.lean b/Mathlib/NumberTheory/ClassNumber/AdmissibleCardPowDegree.lean
@@ -210,8 +210,7 @@ theorem exists_partition_polynomial_aux (n : ℕ) {ε : ℝ} (hε : 0 < ε) {b :
   -- but not that `j` is uniquely defined (which is needed to keep the induction going).
   obtain ⟨j, hj⟩ : ∃ j, ∀ i : Fin n,
       t' i = j → (cardPowDegree (A 0 % b - A i.succ % b) : ℝ) < cardPowDegree b • ε := by
-    by_contra hg
-    push_neg at hg
+    by_contra' hg
     obtain ⟨j₀, j₁, j_ne, approx⟩ := exists_approx_polynomial hb hε
       (Fin.cons (A 0) fun j => A (Fin.succ (Classical.choose (hg j))))
     revert j_ne approx

diff --git a/Mathlib/Order/SuccPred/LinearLocallyFinite.lean b/Mathlib/Order/SuccPred/LinearLocallyFinite.lean
@@ -134,8 +134,7 @@ instance (priority := 100) LinearLocallyFiniteOrder.isSuccArchimedean [LocallyFi
     swap
     · refine' ⟨0, _⟩
       simpa only [Function.iterate_zero, id.def] using hij
-    by_contra h
-    push_neg at h
+    by_contra' h
     have h_lt : ∀ n, succ^[n] i < j := by
       intro n
       induction' n with n hn

diff --git a/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean b/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean
@@ -75,8 +75,7 @@ theorem exists_maximalIdeal_pow_eq_of_principal [IsNoetherianRing R] [LocalRing
   use Nat.find this
   apply le_antisymm
   · change ∀ s ∈ I, s ∈ _
-    by_contra hI''
-    push_neg at hI''
+    by_contra' hI''
     obtain ⟨s, hs₁, hs₂⟩ := hI''
     apply hs₂
     by_cases hs₃ : s = 0; · rw [hs₃]; exact zero_mem _

diff --git a/Mathlib/RingTheory/GradedAlgebra/Radical.lean b/Mathlib/RingTheory/GradedAlgebra/Radical.lean
@@ -56,8 +56,7 @@ theorem Ideal.IsHomogeneous.isPrime_of_homogeneous_mem_or_mem {I : Ideal A} (hI
     Ideal.IsPrime I :=
   ⟨I_ne_top, by
     intro x y hxy
-    by_contra rid
-    push_neg at rid
+    by_contra' rid
     obtain ⟨rid₁, rid₂⟩ := rid
     classical
       /-

diff --git a/Mathlib/RingTheory/IntegralClosure.lean b/Mathlib/RingTheory/IntegralClosure.lean
@@ -267,8 +267,7 @@ theorem isIntegral_of_smul_mem_submodule {M : Type*} [AddCommGroup M] [Module R
       (by ext; apply one_smul)
       (by intros x y; ext; apply mul_smul)
   obtain ⟨a, ha₁, ha₂⟩ : ∃ a ∈ N, a ≠ (0 : M) := by
-    by_contra h'
-    push_neg at h'
+    by_contra' h'
     apply hN
     rwa [eq_bot_iff]
   have : Function.Injective f := by

diff --git a/Mathlib/Topology/Algebra/Order/LiminfLimsup.lean b/Mathlib/Topology/Algebra/Order/LiminfLimsup.lean
@@ -546,8 +546,7 @@ theorem limsup_eq_tendsto_sum_indicator_nat_atTop (s : ℕ → Set α) :
       exact zero_lt_one
   · rintro hω i
     rw [Set.mem_setOf_eq, tendsto_atTop_atTop] at hω
-    by_contra hcon
-    push_neg at hcon
+    by_contra' hcon
     obtain ⟨j, h⟩ := hω (i + 1)
     have : (∑ k in Finset.range j, (s (k + 1)).indicator 1 ω) ≤ i := by
       have hle : ∀ j ≤ i, (∑ k in Finset.range j, (s (k + 1)).indicator 1 ω) ≤ i := by

diff --git a/test/linarith.lean b/test/linarith.lean
@@ -490,8 +490,7 @@ end
 -- Checks that splitNe handles metavariables and also that conjunction splitting occurs
 -- before splitNe splitting
 example (r : ℚ) (h' : 1 = r * 2) : 1 = 0 ∨ r = 1 / 2 := by
-  by_contra h''
-  push_neg at h''
+  by_contra' h''
   linarith (config := {splitNe := true})
 
 example (x y : ℚ) (h₁ : 0 ≤ y) (h₂ : y ≤ x) : y * x ≤ x * x := by nlinarith