leanprover-community · semorrison · Dec 3, 2023 · Dec 3, 2023 · Dec 3, 2023 · Dec 3, 2023
diff --git a/Archive/Imo/Imo1972Q5.lean b/Archive/Imo/Imo1972Q5.lean
@@ -27,7 +27,7 @@ from `hneg` directly), finally raising a contradiction with `k' < k'`.
 theorem imo1972_q5 (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x - y) = 2 * f x * g y)
     (hf2 : ∀ y, ‖f y‖ ≤ 1) (hf3 : ∃ x, f x ≠ 0) (y : ℝ) : ‖g y‖ ≤ 1 := by
   -- Suppose the conclusion does not hold.
-  by_contra' hneg
+  by_contra! hneg
   set S := Set.range fun x => ‖f x‖
   -- Introduce `k`, the supremum of `f`.
   let k : ℝ := sSup S
@@ -82,8 +82,8 @@ This is a more concise version of the proof proposed by Ruben Van de Velde.
 -/
 theorem imo1972_q5' (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x - y) = 2 * f x * g y)
     (hf2 : BddAbove (Set.range fun x => ‖f x‖)) (hf3 : ∃ x, f x ≠ 0) (y : ℝ) : ‖g y‖ ≤ 1 := by
-  -- porting note: moved `by_contra'` up to avoid a bug
-  by_contra' H
+  -- porting note: moved `by_contra!` up to avoid a bug
+  by_contra! H
   obtain ⟨x, hx⟩ := hf3
   set k := ⨆ x, ‖f x‖
   have h : ∀ x, ‖f x‖ ≤ k := le_ciSup hf2

diff --git a/Archive/Imo/Imo1994Q1.lean b/Archive/Imo/Imo1994Q1.lean
@@ -75,7 +75,7 @@ theorem imo1994_q1 (n : ℕ) (m : ℕ) (A : Finset ℕ) (hm : A.card = m + 1)
     _ = (m + 1) * (n + 1) := by rw [sum_const, card_fin, Nat.nsmul_eq_mul]
   -- It remains to prove the key inequality, by contradiction
   rintro k -
-  by_contra' h : a k + a (rev k) < n + 1
+  by_contra! h : a k + a (rev k) < n + 1
   -- We exhibit `k+1` elements of `A` greater than `a (rev k)`
   set f : Fin (m + 1) ↪ ℕ :=
     ⟨fun i => a i + a (rev k), by

diff --git a/Archive/Imo/Imo2008Q4.lean b/Archive/Imo/Imo2008Q4.lean
@@ -68,7 +68,7 @@ theorem imo2008_q4 (f : ℝ → ℝ) (H₁ : ∀ x > 0, f x > 0) :
     field_simp at H₂ ⊢
     linear_combination 1 / 2 * H₂
   have h₃ : ∀ x > 0, f x = x ∨ f x = 1 / x := by simpa [sub_eq_zero] using h₂
-  by_contra' h
+  by_contra! h
   rcases h with ⟨⟨b, hb, hfb₁⟩, ⟨a, ha, hfa₁⟩⟩
   obtain hfa₂ := Or.resolve_right (h₃ a ha) hfa₁
   -- f(a) ≠ 1/a, f(a) = a

diff --git a/Archive/Imo/Imo2013Q5.lean b/Archive/Imo/Imo2013Q5.lean
@@ -35,7 +35,7 @@ namespace Imo2013Q5
 
 theorem le_of_all_pow_lt_succ {x y : ℝ} (hx : 1 < x) (hy : 1 < y)
     (h : ∀ n : ℕ, 0 < n → x ^ n - 1 < y ^ n) : x ≤ y := by
-  by_contra' hxy
+  by_contra! hxy
   have hxmy : 0 < x - y := sub_pos.mpr hxy
   have hn : ∀ n : ℕ, 0 < n → (x - y) * (n : ℝ) ≤ x ^ n - y ^ n := by
     intro n _
@@ -68,7 +68,7 @@ theorem le_of_all_pow_lt_succ {x y : ℝ} (hx : 1 < x) (hy : 1 < y)
 theorem le_of_all_pow_lt_succ' {x y : ℝ} (hx : 1 < x) (hy : 0 < y)
     (h : ∀ n : ℕ, 0 < n → x ^ n - 1 < y ^ n) : x ≤ y := by
   refine' le_of_all_pow_lt_succ hx _ h
-  by_contra' hy'' : y ≤ 1
+  by_contra! hy'' : y ≤ 1
   -- Then there exists y' such that 0 < y ≤ 1 < y' < x.
   let y' := (x + 1) / 2
   have h_y'_lt_x : y' < x :=
@@ -163,7 +163,7 @@ theorem fixed_point_of_gt_1 {f : ℚ → ℝ} {x : ℚ} (hx : 1 < x)
       (x : ℝ) + (a ^ N - x : ℚ) ≤ f x + (a ^ N - x : ℚ) := by gcongr; exact H5 x hx
       _ ≤ f x + f (a ^ N - x) := by gcongr; exact H5 _ h_big_enough
   have hxp : 0 < x := by positivity
-  have hNp : 0 < N := by by_contra' H; rw [le_zero_iff.mp H] at hN; linarith
+  have hNp : 0 < N := by by_contra! H; rw [le_zero_iff.mp H] at hN; linarith
   have h2 :=
     calc
       f x + f (a ^ N - x) ≤ f (x + (a ^ N - x)) := H2 x (a ^ N - x) hxp (by positivity)

diff --git a/Counterexamples/Phillips.lean b/Counterexamples/Phillips.lean
@@ -261,7 +261,7 @@ theorem exists_discrete_support_nonpos (f : BoundedAdditiveMeasure α) :
     In this proof, we use explicit coercions `↑s` for `s : A` as otherwise the system tries to find
     a `CoeFun` instance on `↥A`, which is too costly.
     -/
-  by_contra' h
+  by_contra! h
   -- We will formulate things in terms of the type of countable subsets of `α`, as this is more
   -- convenient to formalize the inductive construction.
   let A : Set (Set α) := {t | t.Countable}

diff --git a/Mathlib/Algebra/BigOperators/Finprod.lean b/Mathlib/Algebra/BigOperators/Finprod.lean
@@ -668,7 +668,7 @@ theorem finprod_mem_of_eqOn_one (hf : s.EqOn f 1) : ∏ᶠ i ∈ s, f i = 1 := b
       "If the product of `f i` over `i ∈ s` is not equal to `0`, then there is some `x ∈ s`
       such that `f x ≠ 0`."]
 theorem exists_ne_one_of_finprod_mem_ne_one (h : ∏ᶠ i ∈ s, f i ≠ 1) : ∃ x ∈ s, f x ≠ 1 := by
-  by_contra' h'
+  by_contra! h'
   exact h (finprod_mem_of_eqOn_one h')
 #align exists_ne_one_of_finprod_mem_ne_one exists_ne_one_of_finprod_mem_ne_one
 #align exists_ne_zero_of_finsum_mem_ne_zero exists_ne_zero_of_finsum_mem_ne_zero

diff --git a/Mathlib/Algebra/Order/CompleteField.lean b/Mathlib/Algebra/Order/CompleteField.lean
@@ -66,7 +66,7 @@ instance (priority := 100) ConditionallyCompleteLinearOrderedField.to_archimedea
     [ConditionallyCompleteLinearOrderedField α] : Archimedean α :=
   archimedean_iff_nat_lt.2
     (by
-      by_contra' h
+      by_contra! h
       obtain ⟨x, h⟩ := h
       have := csSup_le _ _ (range_nonempty Nat.cast)
         (forall_range_iff.2 fun m =>

diff --git a/Mathlib/Algebra/Order/Hom/Ring.lean b/Mathlib/Algebra/Order/Hom/Ring.lean
@@ -558,7 +558,7 @@ instance OrderRingHom.subsingleton [LinearOrderedField α] [LinearOrderedField
     Subsingleton (α →+*o β) :=
   ⟨fun f g => by
     ext x
-    by_contra' h' : f x ≠ g x
+    by_contra! h' : f x ≠ g x
     wlog h : f x < g x generalizing α β with h₂
     -- porting note: had to add the `generalizing` as there are random variables
     -- `F γ δ` flying around in context.

diff --git a/Mathlib/Algebra/Order/ToIntervalMod.lean b/Mathlib/Algebra/Order/ToIntervalMod.lean
@@ -877,7 +877,7 @@ private theorem toIxxMod_cyclic_left {x₁ x₂ x₃ : α} (h : toIcoMod hp x₁
 private theorem toIxxMod_antisymm (h₁₂₃ : toIcoMod hp a b ≤ toIocMod hp a c)
     (h₁₃₂ : toIcoMod hp a c ≤ toIocMod hp a b) :
     b ≡ a [PMOD p] ∨ c ≡ b [PMOD p] ∨ a ≡ c [PMOD p] := by
-  by_contra' h
+  by_contra! h
   rw [modEq_comm] at h
   rw [← (not_modEq_iff_toIcoMod_eq_toIocMod hp).mp h.2.2] at h₁₂₃
   rw [← (not_modEq_iff_toIcoMod_eq_toIocMod hp).mp h.1] at h₁₃₂

diff --git a/Mathlib/AlgebraicGeometry/Properties.lean b/Mathlib/AlgebraicGeometry/Properties.lean
@@ -261,7 +261,7 @@ theorem isIntegralOfIsIrreducibleIsReduced [IsReduced X] [H : IrreducibleSpace X
       (X.toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace.presheaf.obj (op U)) := by
     refine' ⟨fun {a b} e => _⟩
     simp_rw [← basicOpen_eq_bot_iff, ← Opens.not_nonempty_iff_eq_bot]
-    by_contra' h
+    by_contra! h
     obtain ⟨_, ⟨x, hx₁, rfl⟩, ⟨x, hx₂, e'⟩⟩ :=
       nonempty_preirreducible_inter (X.basicOpen a).2 (X.basicOpen b).2 h.1 h.2
     replace e' := Subtype.eq e'

diff --git a/Mathlib/Analysis/Complex/Polynomial.lean b/Mathlib/Analysis/Complex/Polynomial.lean
@@ -27,7 +27,7 @@ namespace Complex
 /-- **Fundamental theorem of algebra**: every non constant complex polynomial
   has a root -/
 theorem exists_root {f : ℂ[X]} (hf : 0 < degree f) : ∃ z : ℂ, IsRoot f z := by
-  by_contra' hf'
+  by_contra! hf'
   /- Since `f` has no roots, `f⁻¹` is differentiable. And since `f` is a polynomial, it tends to
   infinity at infinity, thus `f⁻¹` tends to zero at infinity. By Liouville's theorem, `f⁻¹ = 0`. -/
   have (z : ℂ) : (f.eval z)⁻¹ = 0 :=

diff --git a/Mathlib/Analysis/ConstantSpeed.lean b/Mathlib/Analysis/ConstantSpeed.lean
@@ -159,7 +159,7 @@ theorem hasConstantSpeedOnWith_zero_iff :
   dsimp [HasConstantSpeedOnWith]
   simp only [zero_mul, ENNReal.ofReal_zero, ← eVariationOn.eq_zero_iff]
   constructor
-  · by_contra'
+  · by_contra!
     obtain ⟨h, hfs⟩ := this
     simp_rw [ne_eq, eVariationOn.eq_zero_iff] at hfs h
     push_neg at hfs

diff --git a/Mathlib/Analysis/Convex/Extreme.lean b/Mathlib/Analysis/Convex/Extreme.lean
@@ -273,7 +273,7 @@ theorem Convex.mem_extremePoints_iff_convex_diff (hA : Convex 𝕜 A) :
   rintro ⟨hxA, hAx⟩
   refine' mem_extremePoints_iff_forall_segment.2 ⟨hxA, fun x₁ hx₁ x₂ hx₂ hx ↦ _⟩
   rw [convex_iff_segment_subset] at hAx
-  by_contra' h
+  by_contra! h
   exact (hAx ⟨hx₁, fun hx₁ ↦ h.1 (mem_singleton_iff.2 hx₁)⟩
       ⟨hx₂, fun hx₂ ↦ h.2 (mem_singleton_iff.2 hx₂)⟩ hx).2 rfl
 #align convex.mem_extreme_points_iff_convex_diff Convex.mem_extremePoints_iff_convex_diff

diff --git a/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean b/Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
@@ -107,7 +107,7 @@ theorem disjoint_or_exists_inter_eq_convexHull (hs : s ∈ K.faces) (ht : t ∈
     Disjoint (convexHull 𝕜 (s : Set E)) (convexHull 𝕜 ↑t) ∨
       ∃ u ∈ K.faces, convexHull 𝕜 (s : Set E) ∩ convexHull 𝕜 ↑t = convexHull 𝕜 ↑u := by
   classical
-  by_contra' h
+  by_contra! h
   refine' h.2 (s ∩ t) (K.down_closed hs (inter_subset_left _ _) fun hst => h.1 <|
     disjoint_iff_inf_le.mpr <| (K.inter_subset_convexHull hs ht).trans _) _
   · rw [← coe_inter, hst, coe_empty, convexHull_empty]

diff --git a/Mathlib/Analysis/Convex/StoneSeparation.lean b/Mathlib/Analysis/Convex/StoneSeparation.lean
@@ -101,7 +101,7 @@ theorem exists_convex_convex_compl_subset (hs : Convex 𝕜 s) (ht : Convex 𝕜
         (hC.2.symm.mono (ht.segment_subset hut hvt) <| convexHull_min _ hC.1)
     simpa [insert_subset_iff, hp, hq, singleton_subset_iff.2 hzC]
   rintro c hc
-  by_contra' h
+  by_contra! h
   suffices h : Disjoint (convexHull 𝕜 (insert c C)) t
   · rw [←
       hCmax _ ⟨convex_convexHull _ _, h⟩ ((subset_insert _ _).trans <| subset_convexHull _ _)] at hc

diff --git a/Mathlib/Analysis/LocallyConvex/Bounded.lean b/Mathlib/Analysis/LocallyConvex/Bounded.lean
@@ -162,7 +162,7 @@ theorem isVonNBounded_of_smul_tendsto_zero {ε : ι → 𝕝} {l : Filter ι} [l
     (hε : ∀ᶠ n in l, ε n ≠ 0) {S : Set E}
     (H : ∀ x : ι → E, (∀ n, x n ∈ S) → Tendsto (ε • x) l (𝓝 0)) : IsVonNBounded 𝕝 S := by
   rw [(nhds_basis_balanced 𝕝 E).isVonNBounded_basis_iff]
-  by_contra' H'
+  by_contra! H'
   rcases H' with ⟨V, ⟨hV, hVb⟩, hVS⟩
   have : ∀ᶠ n in l, ∃ x : S, ε n • (x : E) ∉ V := by
     filter_upwards [hε] with n hn

diff --git a/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean b/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
@@ -354,7 +354,7 @@ theorem WithSeminorms.T1_of_separating (hp : WithSeminorms p)
 theorem WithSeminorms.separating_of_T1 [T1Space E] (hp : WithSeminorms p) (x : E) (hx : x ≠ 0) :
     ∃ i, p i x ≠ 0 := by
   have := ((t1Space_TFAE E).out 0 9).mp (inferInstanceAs <| T1Space E)
-  by_contra' h
+  by_contra! h
   refine' hx (this _)
   rw [hp.hasBasis_zero_ball.specializes_iff]
   rintro ⟨s, r⟩ (hr : 0 < r)

diff --git a/Mathlib/Analysis/NormedSpace/Spectrum.lean b/Mathlib/Analysis/NormedSpace/Spectrum.lean
@@ -380,7 +380,7 @@ variable [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [Nontrivial A] (
 protected theorem nonempty : (spectrum ℂ a).Nonempty := by
   /- Suppose `σ a = ∅`, then resolvent set is `ℂ`, any `(z • 1 - a)` is a unit, and `resolvent a`
     is differentiable on `ℂ`. -/
-  by_contra' h
+  by_contra! h
   have H₀ : resolventSet ℂ a = Set.univ := by rwa [spectrum, Set.compl_empty_iff] at h
   have H₁ : Differentiable ℂ fun z : ℂ => resolvent a z := fun z =>
     (hasDerivAt_resolvent (H₀.symm ▸ Set.mem_univ z : z ∈ resolventSet ℂ a)).differentiableAt

diff --git a/Mathlib/Analysis/SpecialFunctions/Gaussian.lean b/Mathlib/Analysis/SpecialFunctions/Gaussian.lean
@@ -151,7 +151,7 @@ theorem integrable_exp_neg_mul_sq {b : ℝ} (hb : 0 < b) : Integrable fun x :
 theorem integrableOn_Ioi_exp_neg_mul_sq_iff {b : ℝ} :
     IntegrableOn (fun x : ℝ => exp (-b * x ^ 2)) (Ioi 0) ↔ 0 < b := by
   refine' ⟨fun h => _, fun h => (integrable_exp_neg_mul_sq h).integrableOn⟩
-  by_contra' hb
+  by_contra! hb
   have : ∫⁻ _ : ℝ in Ioi 0, 1 ≤ ∫⁻ x : ℝ in Ioi 0, ‖exp (-b * x ^ 2)‖₊ := by
     apply lintegral_mono (fun x ↦ _)
     simp only [neg_mul, ENNReal.one_le_coe_iff, ← toNNReal_one, toNNReal_le_iff_le_coe,

diff --git a/Mathlib/Analysis/SpecificLimits/FloorPow.lean b/Mathlib/Analysis/SpecificLimits/FloorPow.lean
@@ -70,7 +70,7 @@ theorem tendsto_div_of_monotone_of_exists_subseq_tendsto_div (u : ℕ → ℝ) (
     let N := Nat.find exN
     have ncN : n < c N := Nat.find_spec exN
     have aN : a + 1 ≤ N := by
-      by_contra' h
+      by_contra! h
       have cNM : c N ≤ M := by
         apply le_max'
         apply mem_image_of_mem
@@ -133,7 +133,7 @@ theorem tendsto_div_of_monotone_of_exists_subseq_tendsto_div (u : ℕ → ℝ) (
     let N := Nat.find exN
     have ncN : n < c N := Nat.find_spec exN
     have aN : a + 1 ≤ N := by
-      by_contra' h
+      by_contra! h
       have cNM : c N ≤ M := by
         apply le_max'
         apply mem_image_of_mem

diff --git a/Mathlib/Analysis/SpecificLimits/Normed.lean b/Mathlib/Analysis/SpecificLimits/Normed.lean
@@ -513,7 +513,7 @@ theorem summable_of_ratio_norm_eventually_le {α : Type*} [SeminormedAddCommGrou
   · push_neg at hr₀
     refine' .of_norm_bounded_eventually_nat 0 summable_zero _
     filter_upwards [h] with _ hn
-    by_contra' h
+    by_contra! h
     exact not_lt.mpr (norm_nonneg _) (lt_of_le_of_lt hn <| mul_neg_of_neg_of_pos hr₀ h)
 #align summable_of_ratio_norm_eventually_le summable_of_ratio_norm_eventually_le
 

diff --git a/Mathlib/CategoryTheory/Preadditive/Biproducts.lean b/Mathlib/CategoryTheory/Preadditive/Biproducts.lean
@@ -811,7 +811,7 @@ def Biprod.isoElim (f : X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂) [IsIso (biprod.inl ≫
 
 theorem Biprod.column_nonzero_of_iso {W X Y Z : C} (f : W ⊞ X ⟶ Y ⊞ Z) [IsIso f] :
     𝟙 W = 0 ∨ biprod.inl ≫ f ≫ biprod.fst ≠ 0 ∨ biprod.inl ≫ f ≫ biprod.snd ≠ 0 := by
-  by_contra' h
+  by_contra! h
   rcases h with ⟨nz, a₁, a₂⟩
   set x := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
   have h₁ : x = 𝟙 W := by simp

diff --git a/Mathlib/Combinatorics/Colex.lean b/Mathlib/Combinatorics/Colex.lean
@@ -119,7 +119,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₁
 
@@ -334,7 +334,7 @@ def IsInitSeg (𝒜 : Finset (Finset α)) (r : ℕ) : Prop :=
 lemma IsInitSeg.total (h₁ : IsInitSeg 𝒜₁ r) (h₂ : IsInitSeg 𝒜₂ r) : 𝒜₁ ⊆ 𝒜₂ ∨ 𝒜₂ ⊆ 𝒜₁ := by
   classical
   simp_rw [← sdiff_eq_empty_iff_subset, ← not_nonempty_iff_eq_empty]
-  by_contra' h
+  by_contra! h
   have ⟨⟨s, hs⟩, t, ht⟩ := h
   rw [mem_sdiff] at hs ht
   obtain hst | hst | hts := trichotomous_of (α := Colex α) (· < ·) (toColex s) (toColex t)

diff --git a/Mathlib/Combinatorics/Composition.lean b/Mathlib/Combinatorics/Composition.lean
@@ -332,7 +332,7 @@ theorem sizeUpTo_index_le (j : Fin n) : c.sizeUpTo (c.index j) ≤ j := by
   set i := c.index j
   push_neg at H
   have i_pos : (0 : ℕ) < i := by
-    by_contra' i_pos
+    by_contra! i_pos
     revert H
     simp [nonpos_iff_eq_zero.1 i_pos, c.sizeUpTo_zero]
   let i₁ := (i : ℕ).pred

diff --git a/Mathlib/Combinatorics/SetFamily/Intersecting.lean b/Mathlib/Combinatorics/SetFamily/Intersecting.lean
@@ -183,7 +183,7 @@ theorem Intersecting.is_max_iff_card_eq (hs : (s : Set α).Intersecting) :
       image_eq_preimage_of_inverse compl_compl compl_compl]
     refine' eq_univ_of_forall fun a => _
     simp_rw [mem_union, mem_preimage]
-    by_contra' ha
+    by_contra! ha
     refine' s.ne_insert_of_not_mem _ ha.1 (h _ _ <| s.subset_insert _)
     rw [coe_insert]
     refine' hs.insert _ fun b hb hab => ha.2 <| (hs.isUpperSet' h) hab.le_compl_left hb

diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity.lean
@@ -2623,7 +2623,7 @@ theorem adj_and_reachable_delete_edges_iff_exists_cycle {v w : V} :
     · simp only [Sym2.eq_swap, Walk.edges_cons, List.mem_cons, eq_self_iff_true, true_or_iff]
   · rintro ⟨u, c, hc, he⟩
     refine ⟨c.adj_of_mem_edges he, ?_⟩
-    by_contra' hb
+    by_contra! hb
     have hb' : ∀ p : G.Walk w v, ⟦(w, v)⟧ ∈ p.edges := by
       intro p
       simpa [Sym2.eq_swap] using hb p.reverse

diff --git a/Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean b/Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean
@@ -159,7 +159,7 @@ theorem exists_adj_boundary_pair (Gc : G.Preconnected) (hK : K.Nonempty) :
   refine' ComponentCompl.ind fun v vnK => _
   let C : G.ComponentCompl K := G.componentComplMk vnK
   let dis := Set.disjoint_iff.mp C.disjoint_right
-  by_contra' h
+  by_contra! h
   suffices Set.univ = (C : Set V) by exact dis ⟨hK.choose_spec, this ▸ Set.mem_univ hK.some⟩
   symm
   rw [Set.eq_univ_iff_forall]

diff --git a/Mathlib/Combinatorics/Young/YoungDiagram.lean b/Mathlib/Combinatorics/Young/YoungDiagram.lean
@@ -325,7 +325,7 @@ theorem rowLen_eq_card (μ : YoungDiagram) {i : ℕ} : μ.rowLen i = (μ.row i).
 
 @[mono]
 theorem rowLen_anti (μ : YoungDiagram) (i1 i2 : ℕ) (hi : i1 ≤ i2) : μ.rowLen i2 ≤ μ.rowLen i1 := by
-  by_contra' h_lt
+  by_contra! h_lt
   rw [← lt_self_iff_false (μ.rowLen i1)]
   rw [← mem_iff_lt_rowLen] at h_lt ⊢
   exact μ.up_left_mem hi (by rfl) h_lt

diff --git a/Mathlib/Data/Fin/FlagRange.lean b/Mathlib/Data/Fin/FlagRange.lean
@@ -33,7 +33,7 @@ theorem IsMaxChain.range_fin_of_covby (h0 : f 0 = ⊥) (hlast : f (.last n) =
     IsMaxChain (· ≤ ·) (range f) := by
   have hmono : Monotone f := Fin.monotone_iff_le_succ.2 fun k ↦ (hcovby k).1
   refine ⟨hmono.isChain_range, fun t htc hbt ↦ hbt.antisymm fun x hx ↦ ?_⟩
-  rw [mem_range]; by_contra' h
+  rw [mem_range]; by_contra! h
   suffices ∀ k, f k < x by simpa [hlast] using this (.last _)
   intro k
   induction k using Fin.induction with

diff --git a/Mathlib/Data/Fin/Tuple/Sort.lean b/Mathlib/Data/Fin/Tuple/Sort.lean
@@ -123,7 +123,7 @@ theorem lt_card_le_iff_apply_le_of_monotone [PartialOrder α] [DecidableRel (α
     j < Fintype.card {i // f i ≤ a} ↔ f j ≤ a := by
   suffices h1 : ∀ k : Fin m, (k < Fintype.card {i // f i ≤ a}) → f k ≤ a
   · refine ⟨h1 j, fun h ↦ ?_⟩
-    by_contra' hc
+    by_contra! hc
     let p : Fin m → Prop := fun x ↦ f x ≤ a
     let q : Fin m → Prop := fun x ↦ x < Fintype.card {i // f i ≤ a}
     let q' : {i // f i ≤ a} → Prop := fun x ↦ q x

diff --git a/Mathlib/Data/Finset/Card.lean b/Mathlib/Data/Finset/Card.lean
@@ -358,7 +358,7 @@ theorem card_le_card_of_inj_on {t : Finset β} (f : α → β) (hf : ∀ a ∈ s
 theorem exists_ne_map_eq_of_card_lt_of_maps_to {t : Finset β} (hc : t.card < s.card) {f : α → β}
     (hf : ∀ a ∈ s, f a ∈ t) : ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y := by
   classical
-    by_contra' hz
+    by_contra! hz
     refine' hc.not_le (card_le_card_of_inj_on f hf _)
     intro x hx y hy
     contrapose

diff --git a/Mathlib/Data/Fintype/Card.lean b/Mathlib/Data/Fintype/Card.lean
@@ -1199,7 +1199,7 @@ See also: `Finite.exists_ne_map_eq_of_infinite`
 theorem Finite.exists_infinite_fiber [Infinite α] [Finite β] (f : α → β) :
     ∃ y : β, Infinite (f ⁻¹' {y}) := by
   classical
-    by_contra' hf
+    by_contra! hf
     cases nonempty_fintype β
     haveI := fun y => fintypeOfNotInfinite <| hf y
     let key : Fintype α :=

diff --git a/Mathlib/Data/List/Chain.lean b/Mathlib/Data/List/Chain.lean
@@ -457,7 +457,7 @@ theorem Chain'.cons_of_le [LinearOrder α] {a : α} {as m : List α}
       refine gt_of_gt_of_ge ha.1 ?_
       rw [le_iff_lt_or_eq] at hmas
       cases' hmas with hmas hmas
-      · by_contra' hh
+      · by_contra! hh
         rw [← not_le] at hmas
         apply hmas
         apply le_of_lt

diff --git a/Mathlib/Data/MvPolynomial/CommRing.lean b/Mathlib/Data/MvPolynomial/CommRing.lean
@@ -189,7 +189,7 @@ theorem degreeOf_sub_lt {x : σ} {f g : MvPolynomial σ R} {k : ℕ} (h : 0 < k)
   classical
   rw [degreeOf_lt_iff h]
   intro m hm
-  by_contra' hc
+  by_contra! hc
   have h := support_sub σ f g hm
   simp only [mem_support_iff, Ne.def, coeff_sub, sub_eq_zero] at hm
   cases' Finset.mem_union.1 h with cf cg

diff --git a/Mathlib/Data/Nat/Count.lean b/Mathlib/Data/Nat/Count.lean
@@ -131,7 +131,7 @@ theorem count_strict_mono {m n : ℕ} (hm : p m) (hmn : m < n) : count p m < cou
 #align nat.count_strict_mono Nat.count_strict_mono
 
 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 : m ≠ n
   wlog hmn : m < n
   · exact this hn hm heq.symm h.symm (h.lt_or_lt.resolve_left hmn)
   · simpa [heq] using count_strict_mono hm hmn

diff --git a/Mathlib/Data/Nat/Prime.lean b/Mathlib/Data/Nat/Prime.lean
@@ -174,7 +174,7 @@ theorem prime_three : Prime 3 := by decide
 
 theorem Prime.five_le_of_ne_two_of_ne_three {p : ℕ} (hp : p.Prime) (h_two : p ≠ 2)
     (h_three : p ≠ 3) : 5 ≤ p := by
-  by_contra' h
+  by_contra! h
   revert h_two h_three hp
   -- Porting note: was `decide!`
   match p with

diff --git a/Mathlib/Data/Polynomial/Degree/Definitions.lean b/Mathlib/Data/Polynomial/Degree/Definitions.lean
@@ -957,7 +957,7 @@ theorem coeff_mul_degree_add_degree (p q : R[X]) :
               rw [coeff_eq_zero_of_degree_lt
                   (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 this)),
                 mul_zero]
-            · by_contra' H'
+            · by_contra! H'
               exact
                 ne_of_lt (Nat.lt_of_lt_of_le (Nat.add_lt_add_right H j) (Nat.add_le_add_left H' _))
                   h₁

diff --git a/Mathlib/Data/Polynomial/Derivative.lean b/Mathlib/Data/Polynomial/Derivative.lean
@@ -273,7 +273,7 @@ theorem natDegree_eq_zero_of_derivative_eq_zero [NoZeroSMulDivisors ℕ R] {f :
   rcases eq_or_ne f 0 with (rfl | hf)
   · exact natDegree_zero
   rw [natDegree_eq_zero_iff_degree_le_zero]
-  by_contra' f_nat_degree_pos
+  by_contra! f_nat_degree_pos
   rw [← natDegree_pos_iff_degree_pos] at f_nat_degree_pos
   let m := f.natDegree - 1
   have hm : m + 1 = f.natDegree := tsub_add_cancel_of_le f_nat_degree_pos

diff --git a/Mathlib/Data/Real/ENNReal.lean b/Mathlib/Data/Real/ENNReal.lean
@@ -954,7 +954,7 @@ theorem coe_max (r p : ℝ≥0) : ((max r p : ℝ≥0) : ℝ≥0∞) = max (r :
 
 theorem le_of_top_imp_top_of_toNNReal_le {a b : ℝ≥0∞} (h : a = ⊤ → b = ⊤)
     (h_nnreal : a ≠ ⊤ → b ≠ ⊤ → a.toNNReal ≤ b.toNNReal) : a ≤ b := by
-  by_contra' hlt
+  by_contra! hlt
   lift b to ℝ≥0 using hlt.ne_top
   lift a to ℝ≥0 using mt h coe_ne_top
   refine hlt.not_le ?_