From 738b1a97e85d528d395f215b4057bad4704e2ceb Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Sun, 3 Dec 2023 13:01:06 +0000 Subject: [PATCH] chore: rename `by_contra'` to `by_contra!` (#8797) To fit with the "please try harder" convention of `!` tactics. Co-authored-by: Scott Morrison --- Archive/Imo/Imo1972Q5.lean | 6 ++--- Archive/Imo/Imo1994Q1.lean | 2 +- Archive/Imo/Imo2008Q4.lean | 2 +- Archive/Imo/Imo2013Q5.lean | 6 ++--- .../AscendingDescendingSequences.lean | 2 +- Counterexamples/Phillips.lean | 2 +- Mathlib/Algebra/BigOperators/Finprod.lean | 2 +- Mathlib/Algebra/Order/CompleteField.lean | 2 +- Mathlib/Algebra/Order/Hom/Ring.lean | 2 +- Mathlib/Algebra/Order/ToIntervalMod.lean | 2 +- Mathlib/AlgebraicGeometry/Properties.lean | 2 +- Mathlib/Analysis/Complex/Polynomial.lean | 2 +- Mathlib/Analysis/ConstantSpeed.lean | 2 +- Mathlib/Analysis/Convex/Extreme.lean | 2 +- .../Convex/SimplicialComplex/Basic.lean | 2 +- Mathlib/Analysis/Convex/StoneSeparation.lean | 2 +- Mathlib/Analysis/LocallyConvex/Bounded.lean | 2 +- .../Analysis/LocallyConvex/WithSeminorms.lean | 2 +- Mathlib/Analysis/NormedSpace/Spectrum.lean | 2 +- .../Analysis/SpecialFunctions/Gaussian.lean | 2 +- Mathlib/Analysis/SpecificLimits/FloorPow.lean | 4 ++-- Mathlib/Analysis/SpecificLimits/Normed.lean | 2 +- .../Preadditive/Biproducts.lean | 2 +- Mathlib/Combinatorics/Colex.lean | 4 ++-- Mathlib/Combinatorics/Composition.lean | 2 +- .../Combinatorics/SetFamily/Intersecting.lean | 2 +- .../SimpleGraph/Connectivity.lean | 2 +- .../Combinatorics/SimpleGraph/Ends/Defs.lean | 2 +- Mathlib/Combinatorics/Young/YoungDiagram.lean | 2 +- Mathlib/Data/Fin/FlagRange.lean | 2 +- Mathlib/Data/Fin/Tuple/Sort.lean | 2 +- Mathlib/Data/Finset/Card.lean | 2 +- Mathlib/Data/Fintype/Card.lean | 2 +- Mathlib/Data/List/Chain.lean | 2 +- Mathlib/Data/MvPolynomial/CommRing.lean | 2 +- Mathlib/Data/Nat/Count.lean | 2 +- Mathlib/Data/Nat/Prime.lean | 2 +- .../Data/Polynomial/Degree/Definitions.lean | 2 +- Mathlib/Data/Polynomial/Derivative.lean | 2 +- Mathlib/Data/Real/ENNReal.lean | 2 +- Mathlib/Data/Set/Basic.lean | 2 +- Mathlib/Data/Set/Card.lean | 2 +- Mathlib/Data/Set/Finite.lean | 6 ++--- Mathlib/Data/Set/Intervals/Basic.lean | 2 +- Mathlib/Data/Set/Pointwise/SMul.lean | 4 ++-- .../RotationNumber/TranslationNumber.lean | 4 ++-- Mathlib/Dynamics/PeriodicPts.lean | 2 +- Mathlib/FieldTheory/Finite/Trace.lean | 2 +- Mathlib/FieldTheory/Minpoly/Basic.lean | 2 +- .../Geometry/Manifold/PartitionOfUnity.lean | 2 +- Mathlib/GroupTheory/Exponent.lean | 4 ++-- Mathlib/GroupTheory/Perm/Support.lean | 2 +- Mathlib/LinearAlgebra/Matrix/PosDef.lean | 2 +- .../MeasureTheory/Constructions/Polish.lean | 4 ++-- .../Covering/BesicovitchVectorSpace.lean | 2 +- .../Decomposition/SignedHahn.lean | 4 ++-- Mathlib/MeasureTheory/Function/LpSpace.lean | 2 +- .../Integral/FundThmCalculus.lean | 2 +- Mathlib/MeasureTheory/Measure/Hausdorff.lean | 2 +- .../MeasureTheory/Measure/Typeclasses.lean | 2 +- Mathlib/ModelTheory/Satisfiability.lean | 2 +- .../ClassNumber/AdmissibleCardPowDegree.lean | 2 +- Mathlib/NumberTheory/ClassNumber/Finite.lean | 2 +- .../Cyclotomic/PrimitiveRoots.lean | 2 +- Mathlib/NumberTheory/Divisors.lean | 2 +- Mathlib/NumberTheory/Padics/PadicNumbers.lean | 2 +- Mathlib/Order/Category/NonemptyFinLinOrd.lean | 2 +- Mathlib/Order/Extension/Linear.lean | 2 +- .../Order/SuccPred/LinearLocallyFinite.lean | 2 +- Mathlib/Order/SupIndep.lean | 2 +- Mathlib/Order/UpperLower/Basic.lean | 2 +- Mathlib/Order/WellFounded.lean | 2 +- Mathlib/Order/WellFoundedSet.lean | 2 +- Mathlib/RingTheory/DedekindDomain/PID.lean | 2 +- .../DiscreteValuationRing/Basic.lean | 2 +- .../DiscreteValuationRing/TFAE.lean | 8 +++---- Mathlib/RingTheory/GradedAlgebra/Radical.lean | 2 +- Mathlib/RingTheory/Ideal/Basic.lean | 2 +- Mathlib/RingTheory/IntegralClosure.lean | 2 +- Mathlib/RingTheory/Polynomial/Content.lean | 2 +- .../Polynomial/Cyclotomic/Eval.lean | 2 +- Mathlib/RingTheory/WittVector/Domain.lean | 2 +- Mathlib/SetTheory/Cardinal/Basic.lean | 2 +- Mathlib/SetTheory/Cardinal/Cofinality.lean | 6 ++--- Mathlib/SetTheory/Ordinal/Arithmetic.lean | 22 +++++++++---------- Mathlib/SetTheory/Ordinal/Exponential.lean | 2 +- Mathlib/SetTheory/Ordinal/NaturalOps.lean | 2 +- Mathlib/SetTheory/Ordinal/Principal.lean | 2 +- Mathlib/SetTheory/Ordinal/Topology.lean | 2 +- Mathlib/SetTheory/ZFC/Basic.lean | 2 +- Mathlib/Tactic/ByContra.lean | 22 +++++++++---------- Mathlib/Topology/Algebra/Module/Basic.lean | 2 +- .../Algebra/Module/FiniteDimension.lean | 2 +- .../Topology/Algebra/Order/LiminfLimsup.lean | 8 +++---- Mathlib/Topology/Category/Stonean/Basic.lean | 2 +- Mathlib/Topology/Compactness/Compact.lean | 6 ++--- Mathlib/Topology/Connected/Basic.lean | 2 +- .../Connected/TotallyDisconnected.lean | 2 +- .../Topology/EMetricSpace/Paracompact.lean | 4 ++-- Mathlib/Topology/Instances/RatLemmas.lean | 2 +- Mathlib/Topology/MetricSpace/PiNat.lean | 8 +++---- Mathlib/Topology/Order/Basic.lean | 4 ++-- Mathlib/Topology/Perfect.lean | 2 +- Mathlib/Topology/Separation/NotNormal.lean | 2 +- test/byContra.lean | 20 ++++++++--------- test/linarith.lean | 2 +- test/observe.lean | 2 +- 107 files changed, 164 insertions(+), 164 deletions(-) diff --git a/Archive/Imo/Imo1972Q5.lean b/Archive/Imo/Imo1972Q5.lean index 3fefb3563e990..9b016c1f1d2f7 100644 --- 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 index 05c0bdfec40bc..bc6aa2a85adca 100644 --- 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 index 0ea6215fb9966..4619f634d21ab 100644 --- 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 index 4b06d4fc31212..e88f9a448ef7b 100644 --- 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/Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean b/Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean index 96e556134a6be..3c88750dac1e8 100644 --- a/Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean +++ b/Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean @@ -136,7 +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 + 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/Counterexamples/Phillips.lean b/Counterexamples/Phillips.lean index 45437cd0ecd00..7470ff0135a33 100644 --- 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 index 617d15f8172ca..b0fd4dd8d3dcd 100644 --- 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 index a7570d25245e5..453f2cae49456 100644 --- 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 index b36301e0991c8..5ff8583808c1d 100644 --- 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 index ab267a52feae6..d568d1ebef8d4 100644 --- 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 index ddaaa15ca1518..cc8941ce209f7 100644 --- 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 index 1652ce99a70f5..637bf597f822f 100644 --- 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 index 46d6c05471fc5..9732aca5e18ba 100644 --- 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 index ba8b0bd56fb44..66b12335c033e 100644 --- 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 index fb1608f202286..8e9400a8bcbf4 100644 --- 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 index 0cd1081486832..7f238e873e683 100644 --- 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 index 03a794f0752c9..54236bc00f595 100644 --- 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 index bb842482e17cb..103535f3ba76b 100644 --- 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 index 149e59d47d98b..1ced47bd71136 100644 --- 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 index f6478f8a45995..0b2750511db20 100644 --- 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 index 82ea4049d0a68..9be939fc3a6d3 100644 --- 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 index 2f9983f5ee720..9a93c7c549190 100644 --- 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 index cbde774362322..ead97e98263d2 100644 --- 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 index ac900e8f6a081..6fb4153f4a31a 100644 --- 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 index 85346f059e7b7..644d7802b21b2 100644 --- 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 index b966a23ef1c40..7a854e03d9e32 100644 --- 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 index dae3cd0fa64e3..671f4ac3d2cd1 100644 --- 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 index a29d6f6d07630..b0bb6263e91f4 100644 --- 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 index 51675c03238bf..e226d162bdd15 100644 --- 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 index 343fc2fd9a12f..6d2f96ee9c456 100644 --- 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 index 406a4c059e083..8ddb303d1017a 100644 --- 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 index 1473f4dae7df4..64fddeb9862bb 100644 --- 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 index 8be249bcea7ff..dd578060bf36f 100644 --- 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 index 368b6cdf504f9..d70d94cd275ed 100644 --- 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 index e59bef54bdc09..fcb0b40bb546b 100644 --- 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 index d547c042e9ef5..5ae27b3fde4c8 100644 --- 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 index 0b6a42a989fe2..bc3d5c3f5537d 100644 --- 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 index 005f5ad729fa4..06eadf6592a09 100644 --- 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 index e3c921c66158a..6fb69830afa27 100644 --- 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 index 63b1462bbb86c..38e41bcb20ed5 100644 --- 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 ?_ diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean index 4c12ff20de92a..333aed946628a 100644 --- a/Mathlib/Data/Set/Basic.lean +++ b/Mathlib/Data/Set/Basic.lean @@ -2524,7 +2524,7 @@ theorem nontrivial_of_exists_ne {x} (hx : x ∈ s) (h : ∃ y ∈ s, y ≠ x) : #align set.nontrivial_of_exists_ne Set.nontrivial_of_exists_ne theorem Nontrivial.exists_ne (hs : s.Nontrivial) (z) : ∃ x ∈ s, x ≠ z := by - by_contra' H + by_contra! H rcases hs with ⟨x, hx, y, hy, hxy⟩ rw [H x hx, H y hy] at hxy exact hxy rfl diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean index 2e3db4ee4ffa8..d61cf4bc106c3 100644 --- a/Mathlib/Data/Set/Card.lean +++ b/Mathlib/Data/Set/Card.lean @@ -307,7 +307,7 @@ theorem one_lt_encard_iff : 1 < s.encard ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a rw [← not_iff_not, not_exists, not_lt, encard_le_one_iff]; aesop theorem exists_ne_of_one_lt_encard (h : 1 < s.encard) (a : α) : ∃ b ∈ s, b ≠ a := by - by_contra' h' + by_contra! h' obtain ⟨b, b', hb, hb', hne⟩ := one_lt_encard_iff.1 h apply hne rw [h' b hb, h' b' hb'] diff --git a/Mathlib/Data/Set/Finite.lean b/Mathlib/Data/Set/Finite.lean index ea186a579271d..f883762ff0cb6 100644 --- a/Mathlib/Data/Set/Finite.lean +++ b/Mathlib/Data/Set/Finite.lean @@ -964,7 +964,7 @@ protected theorem infinite_prod : (s ×ˢ t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty := by refine' ⟨fun h => _, _⟩ · simp_rw [Set.Infinite, @and_comm ¬_, ← not_imp] - by_contra' + by_contra! exact h ((this.1 h.nonempty.snd).prod $ this.2 h.nonempty.fst) · rintro (h | h) · exact h.1.prod_left h.2 @@ -1312,7 +1312,7 @@ alias ⟨_, Infinite.to_subtype⟩ := infinite_coe_iff #align set.infinite.to_subtype Set.Infinite.to_subtype lemma Infinite.exists_not_mem_finite (hs : s.Infinite) (ht : t.Finite) : ∃ a, a ∈ s ∧ a ∉ t := by - by_contra' h; exact hs $ ht.subset h + by_contra! h; exact hs $ ht.subset h lemma Infinite.exists_not_mem_finset (hs : s.Infinite) (t : Finset α) : ∃ a ∈ s, a ∉ t := hs.exists_not_mem_finite t.finite_toSet @@ -1322,7 +1322,7 @@ section Infinite variable [Infinite α] lemma Finite.exists_not_mem (hs : s.Finite) : ∃ a, a ∉ s := by - by_contra' h; exact infinite_univ (hs.subset fun a _ ↦ h _) + by_contra! h; exact infinite_univ (hs.subset fun a _ ↦ h _) lemma _root_.Finset.exists_not_mem (s : Finset α) : ∃ a, a ∉ s := s.finite_toSet.exists_not_mem diff --git a/Mathlib/Data/Set/Intervals/Basic.lean b/Mathlib/Data/Set/Intervals/Basic.lean index 8b5bf13b3acd4..75b44906da590 100644 --- a/Mathlib/Data/Set/Intervals/Basic.lean +++ b/Mathlib/Data/Set/Intervals/Basic.lean @@ -1180,7 +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 + 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/Data/Set/Pointwise/SMul.lean b/Mathlib/Data/Set/Pointwise/SMul.lean index fc7cd705c3915..4ec93b98e086f 100644 --- a/Mathlib/Data/Set/Pointwise/SMul.lean +++ b/Mathlib/Data/Set/Pointwise/SMul.lean @@ -563,7 +563,7 @@ scoped[Pointwise] attribute [instance] Set.distribMulActionSet Set.mulDistribMul instance [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] : NoZeroSMulDivisors (Set α) (Set β) := ⟨fun {s t} h ↦ by - by_contra' H + by_contra! H have hst : (s • t).Nonempty := h.symm.subst zero_nonempty rw [Ne.def, ← hst.of_smul_left.subset_zero_iff, Ne.def, ← hst.of_smul_right.subset_zero_iff] at H @@ -574,7 +574,7 @@ instance [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] : instance noZeroSMulDivisors_set [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] : NoZeroSMulDivisors α (Set β) := ⟨fun {a s} h ↦ by - by_contra' H + by_contra! H have hst : (a • s).Nonempty := h.symm.subst zero_nonempty rw [Ne.def, Ne.def, ← hst.of_image.subset_zero_iff, not_subset] at H obtain ⟨ha, b, ht, hb⟩ := H diff --git a/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean b/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean index 320e0c9ba1773..58a3f2ce6eb31 100644 --- a/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean +++ b/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean @@ -927,10 +927,10 @@ theorem lt_translationNumber_of_forall_add_lt (hf : Continuous f) {z : ℝ} (hz such that `f x = x + τ f`. -/ theorem exists_eq_add_translationNumber (hf : Continuous f) : ∃ x, f x = x + τ f := by obtain ⟨a, ha⟩ : ∃ x, f x ≤ x + τ f := by - by_contra' H + by_contra! H exact lt_irrefl _ (f.lt_translationNumber_of_forall_add_lt hf H) obtain ⟨b, hb⟩ : ∃ x, x + τ f ≤ f x := by - by_contra' H + by_contra! H exact lt_irrefl _ (f.translationNumber_lt_of_forall_lt_add hf H) exact intermediate_value_univ₂ hf (continuous_id.add continuous_const) ha hb #align circle_deg1_lift.exists_eq_add_translation_number CircleDeg1Lift.exists_eq_add_translationNumber diff --git a/Mathlib/Dynamics/PeriodicPts.lean b/Mathlib/Dynamics/PeriodicPts.lean index de8133e6a7144..b559b69559931 100644 --- a/Mathlib/Dynamics/PeriodicPts.lean +++ b/Mathlib/Dynamics/PeriodicPts.lean @@ -343,7 +343,7 @@ theorem minimalPeriod_apply (hx : x ∈ periodicPts f) : minimalPeriod f (f x) = theorem le_of_lt_minimalPeriod_of_iterate_eq {m n : ℕ} (hm : m < minimalPeriod f x) (hmn : f^[m] x = f^[n] x) : m ≤ n := by - by_contra' hmn' + by_contra! hmn' rw [← Nat.add_sub_of_le hmn'.le, add_comm, iterate_add_apply] at hmn exact ((IsPeriodicPt.minimalPeriod_le (tsub_pos_of_lt hmn') diff --git a/Mathlib/FieldTheory/Finite/Trace.lean b/Mathlib/FieldTheory/Finite/Trace.lean index 1706b02a38a44..6ee2bb18a4e2a 100644 --- a/Mathlib/FieldTheory/Finite/Trace.lean +++ b/Mathlib/FieldTheory/Finite/Trace.lean @@ -28,7 +28,7 @@ theorem trace_to_zmod_nondegenerate (F : Type*) [Field F] [Finite F] haveI : Fact (ringChar F).Prime := ⟨CharP.char_is_prime F _⟩ have htr := traceForm_nondegenerate (ZMod (ringChar F)) F a simp_rw [Algebra.traceForm_apply] at htr - by_contra' hf + by_contra! hf exact ha (htr hf) #align finite_field.trace_to_zmod_nondegenerate FiniteField.trace_to_zmod_nondegenerate diff --git a/Mathlib/FieldTheory/Minpoly/Basic.lean b/Mathlib/FieldTheory/Minpoly/Basic.lean index 01b36011e67c6..c66386a8854a3 100644 --- a/Mathlib/FieldTheory/Minpoly/Basic.lean +++ b/Mathlib/FieldTheory/Minpoly/Basic.lean @@ -244,7 +244,7 @@ variable [IsDomain A] [IsDomain B] theorem irreducible (hx : IsIntegral A x) : Irreducible (minpoly A x) := by refine' (irreducible_of_monic (monic hx) <| ne_one A x).2 fun f g hf hg he => _ rw [← hf.isUnit_iff, ← hg.isUnit_iff] - by_contra' h + by_contra! h have heval := congr_arg (Polynomial.aeval x) he rw [aeval A x, aeval_mul, mul_eq_zero] at heval cases' heval with heval heval diff --git a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean index 3bde26d14f86b..059b502b06fe5 100644 --- a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean +++ b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean @@ -159,7 +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 + 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/GroupTheory/Exponent.lean b/Mathlib/GroupTheory/Exponent.lean index e3ccd5d98e1e5..1479a4106e6b8 100644 --- a/Mathlib/GroupTheory/Exponent.lean +++ b/Mathlib/GroupTheory/Exponent.lean @@ -155,7 +155,7 @@ theorem exponent_min' (n : ℕ) (hpos : 0 < n) (hG : ∀ g : G, g ^ n = 1) : exp @[to_additive] theorem exponent_min (m : ℕ) (hpos : 0 < m) (hm : m < exponent G) : ∃ g : G, g ^ m ≠ 1 := by - by_contra' h + by_contra! h have hcon : exponent G ≤ m := exponent_min' m hpos h linarith #align monoid.exponent_min Monoid.exponent_min @@ -314,7 +314,7 @@ theorem exponent_eq_iSup_orderOf (h : ∀ g : G, 0 < orderOf g) : apply order_dvd_exponent refine' Nat.dvd_of_factors_subperm he _ rw [List.subperm_ext_iff] - by_contra' h + by_contra! h obtain ⟨p, hp, hpe⟩ := h replace hp := Nat.prime_of_mem_factors hp simp only [Nat.factors_count_eq] at hpe diff --git a/Mathlib/GroupTheory/Perm/Support.lean b/Mathlib/GroupTheory/Perm/Support.lean index 6a5437a5ab0af..d3e7fa25ec23c 100644 --- a/Mathlib/GroupTheory/Perm/Support.lean +++ b/Mathlib/GroupTheory/Perm/Support.lean @@ -438,7 +438,7 @@ theorem support_swap {x y : α} (h : x ≠ y) : support (swap x y) = {x, y} := b theorem support_swap_iff (x y : α) : support (swap x y) = {x, y} ↔ x ≠ y := by refine' ⟨fun h => _, fun h => support_swap h⟩ - by_contra' + by_contra! rw [← this] at h simp only [swap_self, support_refl, pair_eq_singleton] at h have : x ∈ ∅ := by diff --git a/Mathlib/LinearAlgebra/Matrix/PosDef.lean b/Mathlib/LinearAlgebra/Matrix/PosDef.lean index 356297c13900e..0f6fc99935760 100644 --- a/Mathlib/LinearAlgebra/Matrix/PosDef.lean +++ b/Mathlib/LinearAlgebra/Matrix/PosDef.lean @@ -197,7 +197,7 @@ noncomputable def NormedAddCommGroup.ofMatrix {M : Matrix n n 𝕜} (hM : M.PosD · simp [h] · exact le_of_lt (hM.re_dotProduct_pos h) definite := fun x (hx : dotProduct _ _ = 0) => by - by_contra' h + by_contra! h simpa [hx, lt_irrefl] using hM.re_dotProduct_pos h add_left := by simp only [star_add, add_dotProduct, eq_self_iff_true, forall_const] smul_left := fun x y r => by diff --git a/Mathlib/MeasureTheory/Constructions/Polish.lean b/Mathlib/MeasureTheory/Constructions/Polish.lean index 1f8bb4439a808..5e818e3b2203b 100644 --- a/Mathlib/MeasureTheory/Constructions/Polish.lean +++ b/Mathlib/MeasureTheory/Constructions/Polish.lean @@ -749,7 +749,7 @@ theorem measurableSet_range_of_continuous_injective {β : Type*} [TopologicalSpa have I : ∀ m n, ((s m).1 ∩ (s n).1).Nonempty := by intro m n rw [← not_disjoint_iff_nonempty_inter] - by_contra' h + by_contra! h have A : x ∈ q ⟨(s m, s n), h⟩ \ q ⟨(s n, s m), h.symm⟩ := haveI := mem_iInter.1 (hxs m).2 (s n) (mem_iInter.1 this h : _) @@ -777,7 +777,7 @@ theorem measurableSet_range_of_continuous_injective {β : Type*} [TopologicalSpa rw [← this] exact mem_range_self _ -- assume for a contradiction that `f z ≠ x`. - by_contra' hne + by_contra! hne -- introduce disjoint open sets `v` and `w` separating `f z` from `x`. obtain ⟨v, w, v_open, w_open, fzv, xw, hvw⟩ := t2_separation hne obtain ⟨δ, δpos, hδ⟩ : ∃ δ > (0 : ℝ), ball z δ ⊆ f ⁻¹' v := by diff --git a/Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean b/Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean index a319bcfcafd12..4941e0635489a 100644 --- a/Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean +++ b/Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean @@ -210,7 +210,7 @@ theorem exists_goodδ : subsequence, to obtain a `1`-separated set in the ball of radius `2` with cardinality `N = multiplicity E + 1`. To formalize this, we work with functions `Fin N → E`. -/ - by_contra' h + by_contra! h set N := multiplicity E + 1 with hN have : ∀ δ : ℝ, 0 < δ → ∃ f : Fin N → E, (∀ i : Fin N, ‖f i‖ ≤ 2) ∧ diff --git a/Mathlib/MeasureTheory/Decomposition/SignedHahn.lean b/Mathlib/MeasureTheory/Decomposition/SignedHahn.lean index 48cdbbafd0d46..2548a786a2ba2 100644 --- a/Mathlib/MeasureTheory/Decomposition/SignedHahn.lean +++ b/Mathlib/MeasureTheory/Decomposition/SignedHahn.lean @@ -342,7 +342,7 @@ theorem zero_mem_measureOfNegatives : (0 : ℝ) ∈ s.measureOfNegatives := theorem bddBelow_measureOfNegatives : BddBelow s.measureOfNegatives := by simp_rw [BddBelow, Set.Nonempty, mem_lowerBounds] - by_contra' h + by_contra! h have h' : ∀ n : ℕ, ∃ y : ℝ, y ∈ s.measureOfNegatives ∧ y < -n := fun n => h (-n) choose f hf using h' have hf' : ∀ n : ℕ, ∃ B, MeasurableSet B ∧ s ≤[B] 0 ∧ s B < -n := by @@ -395,7 +395,7 @@ theorem exists_compl_positive_negative (s : SignedMeasure α) : refine' ⟨Aᶜ, hA₁.compl, _, (compl_compl A).symm ▸ hA₂⟩ rw [restrict_le_restrict_iff _ _ hA₁.compl] intro C _ hC₁ - by_contra' hC₂ + by_contra! hC₂ rcases exists_subset_restrict_nonpos hC₂ with ⟨D, hD₁, hD, hD₂, hD₃⟩ have : s (A ∪ D) < sInf s.measureOfNegatives := by rw [← hA₃, diff --git a/Mathlib/MeasureTheory/Function/LpSpace.lean b/Mathlib/MeasureTheory/Function/LpSpace.lean index 8130d549ec91f..f268c7ffb6fdb 100644 --- a/Mathlib/MeasureTheory/Function/LpSpace.lean +++ b/Mathlib/MeasureTheory/Function/LpSpace.lean @@ -574,7 +574,7 @@ theorem snormEssSup_indicator_const_le (s : Set α) (c : G) : theorem snormEssSup_indicator_const_eq (s : Set α) (c : G) (hμs : μ s ≠ 0) : snormEssSup (s.indicator fun _ : α => c) μ = ‖c‖₊ := by refine' le_antisymm (snormEssSup_indicator_const_le s c) _ - by_contra' h + by_contra! h have h' := ae_iff.mp (ae_lt_of_essSup_lt h) push_neg at h' refine' hμs (measure_mono_null (fun x hx_mem => _) h') diff --git a/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean b/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean index 7b36a4391a5b5..87797dbeb4adb 100644 --- a/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean +++ b/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean @@ -1261,7 +1261,7 @@ theorem integrableOn_deriv_right_of_nonneg (hcont : ContinuousOn g (Icc a b)) exact (hderiv x hx).derivWithin (uniqueDiffWithinAt_Ioi _) suffices H : (∫⁻ x in Ioo a b, ‖g' x‖₊) ≤ ENNReal.ofReal (g b - g a) from ⟨meas_g'.aestronglyMeasurable, H.trans_lt ENNReal.ofReal_lt_top⟩ - by_contra' H + by_contra! H obtain ⟨f, fle, fint, hf⟩ : ∃ f : SimpleFunc ℝ ℝ≥0, (∀ x, f x ≤ ‖g' x‖₊) ∧ diff --git a/Mathlib/MeasureTheory/Measure/Hausdorff.lean b/Mathlib/MeasureTheory/Measure/Hausdorff.lean index 2faecad54a3ec..307dbe3b01522 100644 --- a/Mathlib/MeasureTheory/Measure/Hausdorff.lean +++ b/Mathlib/MeasureTheory/Measure/Hausdorff.lean @@ -617,7 +617,7 @@ theorem hausdorffMeasure_le_liminf_sum {β : Type*} {ι : β → Type*} [∀ n, /-- If `d₁ < d₂`, then for any set `s` we have either `μH[d₂] s = 0`, or `μH[d₁] s = ∞`. -/ theorem hausdorffMeasure_zero_or_top {d₁ d₂ : ℝ} (h : d₁ < d₂) (s : Set X) : μH[d₂] s = 0 ∨ μH[d₁] s = ∞ := by - by_contra' H + by_contra! H suffices ∀ c : ℝ≥0, c ≠ 0 → μH[d₂] s ≤ c * μH[d₁] s by rcases ENNReal.exists_nnreal_pos_mul_lt H.2 H.1 with ⟨c, hc0, hc⟩ exact hc.not_le (this c (pos_iff_ne_zero.1 hc0)) diff --git a/Mathlib/MeasureTheory/Measure/Typeclasses.lean b/Mathlib/MeasureTheory/Measure/Typeclasses.lean index 186159b884cf5..f957f76d25591 100644 --- a/Mathlib/MeasureTheory/Measure/Typeclasses.lean +++ b/Mathlib/MeasureTheory/Measure/Typeclasses.lean @@ -990,7 +990,7 @@ theorem sigmaFinite_bot_iff (μ : @Measure α ⊥) : SigmaFinite μ ↔ IsFinite · rw [h_univ_empty, @measure_empty α ⊥] exact ENNReal.zero_ne_top.lt_top obtain ⟨i, hsi⟩ : ∃ i, s i = Set.univ := by - by_contra' h_not_univ + by_contra! h_not_univ have h_empty : ∀ i, s i = ∅ := by simpa [h_not_univ] using hs_meas simp only [h_empty, iUnion_empty] at hs_univ exact h_univ_empty hs_univ.symm diff --git a/Mathlib/ModelTheory/Satisfiability.lean b/Mathlib/ModelTheory/Satisfiability.lean index e191b328a2afd..9a1e8b80f8dcb 100644 --- a/Mathlib/ModelTheory/Satisfiability.lean +++ b/Mathlib/ModelTheory/Satisfiability.lean @@ -683,7 +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 + 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 index d78b9be175ba1..814f1a5c0c94a 100644 --- a/Mathlib/NumberTheory/ClassNumber/AdmissibleCardPowDegree.lean +++ b/Mathlib/NumberTheory/ClassNumber/AdmissibleCardPowDegree.lean @@ -210,7 +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 + 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/NumberTheory/ClassNumber/Finite.lean b/Mathlib/NumberTheory/ClassNumber/Finite.lean index 3116973da911d..19f1281050748 100644 --- a/Mathlib/NumberTheory/ClassNumber/Finite.lean +++ b/Mathlib/NumberTheory/ClassNumber/Finite.lean @@ -69,7 +69,7 @@ noncomputable def normBound : ℤ := theorem normBound_pos : 0 < normBound abv bS := by obtain ⟨i, j, k, hijk⟩ : ∃ i j k, Algebra.leftMulMatrix bS (bS i) j k ≠ 0 := by - by_contra' h + by_contra! h obtain ⟨i⟩ := bS.index_nonempty apply bS.ne_zero i apply diff --git a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean index 31f2290895393..9ef15c8d2cbd4 100644 --- a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean +++ b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean @@ -218,7 +218,7 @@ theorem norm_eq_one [IsDomain L] [IsCyclotomicExtension {n} K L] (hn : n ≠ 2) · rw [h1, one_coe, one_right_iff] at hζ rw [hζ, show 1 = algebraMap K L 1 by simp, Algebra.norm_algebraMap, one_pow] · replace h1 : 2 ≤ n - · by_contra' h + · by_contra! h exact h1 (PNat.eq_one_of_lt_two h) -- Porting note: specyfing the type of `cyclotomic_coeff_zero K h1` was not needed. rw [← hζ.powerBasis_gen K, PowerBasis.norm_gen_eq_coeff_zero_minpoly, hζ.powerBasis_gen K, ← diff --git a/Mathlib/NumberTheory/Divisors.lean b/Mathlib/NumberTheory/Divisors.lean index ce4ab975a1d5e..55c241255ab9b 100644 --- a/Mathlib/NumberTheory/Divisors.lean +++ b/Mathlib/NumberTheory/Divisors.lean @@ -409,7 +409,7 @@ theorem properDivisors_eq_singleton_one_iff_prime : n.properDivisors = {1} ↔ n have := Nat.le_of_dvd ?_ hdvd · simp [hdvd, this] exact (le_iff_eq_or_lt.mp this).symm - · by_contra' + · by_contra! simp only [nonpos_iff_eq_zero.mp this, this] at h contradiction · exact fun h => Prime.properDivisors h diff --git a/Mathlib/NumberTheory/Padics/PadicNumbers.lean b/Mathlib/NumberTheory/Padics/PadicNumbers.lean index 3da605a32dcc0..bef5f88e80114 100644 --- a/Mathlib/NumberTheory/Padics/PadicNumbers.lean +++ b/Mathlib/NumberTheory/Padics/PadicNumbers.lean @@ -601,7 +601,7 @@ theorem defn (f : PadicSeq p) {ε : ℚ} (hε : 0 < ε) : ∃ N, ∀ i ≥ N, padicNormE (Padic.mk f - f i : ℚ_[p]) < ε := by dsimp [padicNormE] change ∃ N, ∀ i ≥ N, (f - const _ (f i)).norm < ε - by_contra' h + by_contra! h cases' cauchy₂ f hε with N hN rcases h N with ⟨i, hi, hge⟩ have hne : ¬f - const (padicNorm p) (f i) ≈ 0 := fun h ↦ by diff --git a/Mathlib/Order/Category/NonemptyFinLinOrd.lean b/Mathlib/Order/Category/NonemptyFinLinOrd.lean index 43a034041790e..56cfc23252b87 100644 --- a/Mathlib/Order/Category/NonemptyFinLinOrd.lean +++ b/Mathlib/Order/Category/NonemptyFinLinOrd.lean @@ -170,7 +170,7 @@ theorem epi_iff_surjective {A B : NonemptyFinLinOrd.{u}} (f : A ⟶ B) : constructor · intro dsimp only [Function.Surjective] - by_contra' hf' + by_contra! hf' rcases hf' with ⟨m, hm⟩ let Y := NonemptyFinLinOrd.of (ULift (Fin 2)) let p₁ : B ⟶ Y := diff --git a/Mathlib/Order/Extension/Linear.lean b/Mathlib/Order/Extension/Linear.lean index c9ef939ccc920..4fdb7b279deb9 100644 --- a/Mathlib/Order/Extension/Linear.lean +++ b/Mathlib/Order/Extension/Linear.lean @@ -53,7 +53,7 @@ theorem extend_partialOrder {α : Type u} (r : α → α → Prop) [IsPartialOrd haveI : IsPartialOrder α s := hs₁ refine ⟨s, { total := ?_, refl := hs₁.refl, trans := hs₁.trans, antisymm := hs₁.antisymm } , rs⟩ intro x y - by_contra' h + by_contra! h let s' x' y' := s x' y' ∨ s x' x ∧ s y y' rw [← hs₂ s' _ fun _ _ ↦ Or.inl] at h · apply h.1 (Or.inr ⟨refl _, refl _⟩) diff --git a/Mathlib/Order/SuccPred/LinearLocallyFinite.lean b/Mathlib/Order/SuccPred/LinearLocallyFinite.lean index 9c67025eed741..1a7f0ced832d4 100644 --- a/Mathlib/Order/SuccPred/LinearLocallyFinite.lean +++ b/Mathlib/Order/SuccPred/LinearLocallyFinite.lean @@ -134,7 +134,7 @@ instance (priority := 100) LinearLocallyFiniteOrder.isSuccArchimedean [LocallyFi swap · refine' ⟨0, _⟩ simpa only [Function.iterate_zero, id.def] using hij - by_contra' h + by_contra! h have h_lt : ∀ n, succ^[n] i < j := by intro n induction' n with n hn diff --git a/Mathlib/Order/SupIndep.lean b/Mathlib/Order/SupIndep.lean index d6f66d6b6396e..54c5af38d5118 100644 --- a/Mathlib/Order/SupIndep.lean +++ b/Mathlib/Order/SupIndep.lean @@ -422,7 +422,7 @@ theorem independent_ne_bot_iff_independent : theorem Independent.injOn (ht : Independent t) : InjOn t {i | t i ≠ ⊥} := by rintro i _ j (hj : t j ≠ ⊥) h - by_contra' contra + by_contra! contra apply hj suffices t j ≤ ⨆ (k) (_ : k ≠ i), t k by replace ht := (ht i).mono_right this diff --git a/Mathlib/Order/UpperLower/Basic.lean b/Mathlib/Order/UpperLower/Basic.lean index 37a308f8f2d7c..3fcd97344ebc5 100644 --- a/Mathlib/Order/UpperLower/Basic.lean +++ b/Mathlib/Order/UpperLower/Basic.lean @@ -416,7 +416,7 @@ section LinearOrder variable [LinearOrder α] {s t : Set α} theorem IsUpperSet.total (hs : IsUpperSet s) (ht : IsUpperSet t) : s ⊆ t ∨ t ⊆ s := by - by_contra' h + by_contra! h simp_rw [Set.not_subset] at h obtain ⟨⟨a, has, hat⟩, b, hbt, hbs⟩ := h obtain hab | hba := le_total a b diff --git a/Mathlib/Order/WellFounded.lean b/Mathlib/Order/WellFounded.lean index e07a25edd66f3..f92e43ee2cf9a 100644 --- a/Mathlib/Order/WellFounded.lean +++ b/Mathlib/Order/WellFounded.lean @@ -171,7 +171,7 @@ theorem eq_strictMono_iff_eq_range {f g : β → γ} (hf : StrictMono f) (hg : S #align well_founded.eq_strict_mono_iff_eq_range WellFounded.eq_strictMono_iff_eq_range theorem self_le_of_strictMono {f : β → β} (hf : StrictMono f) : ∀ n, n ≤ f n := by - by_contra' h₁ + by_contra! h₁ have h₂ := h.min_mem _ h₁ exact h.not_lt_min _ h₁ (hf h₂) h₂ #align well_founded.self_le_of_strict_mono WellFounded.self_le_of_strictMono diff --git a/Mathlib/Order/WellFoundedSet.lean b/Mathlib/Order/WellFoundedSet.lean index 2ddea5912cf55..a9d586c15bee9 100644 --- a/Mathlib/Order/WellFoundedSet.lean +++ b/Mathlib/Order/WellFoundedSet.lean @@ -356,7 +356,7 @@ theorem partiallyWellOrderedOn_iff_finite_antichains [IsSymm α r] : s.PartiallyWellOrderedOn r ↔ ∀ t, t ⊆ s → IsAntichain r t → t.Finite := by refine' ⟨fun h t ht hrt => hrt.finite_of_partiallyWellOrderedOn (h.mono ht), _⟩ rintro hs f hf - by_contra' H + by_contra! H refine' infinite_range_of_injective (fun m n hmn => _) (hs _ (range_subset_iff.2 hf) _) · obtain h | h | h := lt_trichotomy m n · refine' (H _ _ h _).elim diff --git a/Mathlib/RingTheory/DedekindDomain/PID.lean b/Mathlib/RingTheory/DedekindDomain/PID.lean index ca225eb4dc8a9..b38dbdc23d093 100644 --- a/Mathlib/RingTheory/DedekindDomain/PID.lean +++ b/Mathlib/RingTheory/DedekindDomain/PID.lean @@ -125,7 +125,7 @@ theorem FractionalIdeal.isPrincipal.of_finite_maximals_of_inv {A : Type*} [CommR left_lt_sup.1 ((hf.mem_toFinset.1 hM).ne_top.lt_top.trans_eq (Ideal.sup_iInf_eq_top <| coprime M hM).symm) have : ∀ M ∈ s, ∃ a ∈ I, ∃ b ∈ I', a * b ∉ IsLocalization.coeSubmodule A M := by - intro M hM; by_contra' h + intro M hM; by_contra! h obtain ⟨x, hx, hxM⟩ := SetLike.exists_of_lt ((IsLocalization.coeSubmodule_strictMono hS (hf.mem_toFinset.1 hM).ne_top.lt_top).trans_eq diff --git a/Mathlib/RingTheory/DiscreteValuationRing/Basic.lean b/Mathlib/RingTheory/DiscreteValuationRing/Basic.lean index 1c9365020c8f3..c093e5f223387 100644 --- a/Mathlib/RingTheory/DiscreteValuationRing/Basic.lean +++ b/Mathlib/RingTheory/DiscreteValuationRing/Basic.lean @@ -78,7 +78,7 @@ theorem irreducible_of_span_eq_maximalIdeal {R : Type*} [CommRing R] [LocalRing have h2 : ¬IsUnit ϖ := show ϖ ∈ maximalIdeal R from h.symm ▸ Submodule.mem_span_singleton_self ϖ refine' ⟨h2, _⟩ intro a b hab - by_contra' h + by_contra! h obtain ⟨ha : a ∈ maximalIdeal R, hb : b ∈ maximalIdeal R⟩ := h rw [h, mem_span_singleton'] at ha hb rcases ha with ⟨a, rfl⟩ diff --git a/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean b/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean index 716cca4c8b90f..c9ae1e0efb3de 100644 --- a/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean +++ b/Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean @@ -68,14 +68,14 @@ theorem exists_maximalIdeal_pow_eq_of_principal [IsNoetherianRing R] [LocalRing exact Associated.mul_mul (this _ (Multiset.mem_cons_self _ _)) hn have : ∃ n : ℕ, x ^ n ∈ I := by obtain ⟨r, hr₁, hr₂⟩ : ∃ r : R, r ∈ I ∧ r ≠ 0 := by - by_contra' h; apply hI; rw [eq_bot_iff]; exact h + by_contra! h; apply hI; rw [eq_bot_iff]; exact h obtain ⟨n, u, rfl⟩ := H' r hr₂ (le_maximalIdeal hI' hr₁) use n rwa [← I.unit_mul_mem_iff_mem u.isUnit, mul_comm] use Nat.find this apply le_antisymm · change ∀ s ∈ I, s ∈ _ - by_contra' hI'' + by_contra! hI'' obtain ⟨s, hs₁, hs₂⟩ := hI'' apply hs₂ by_cases hs₃ : s = 0; · rw [hs₃]; exact zero_mem _ @@ -94,7 +94,7 @@ theorem maximalIdeal_isPrincipal_of_isDedekindDomain [LocalRing R] [IsDomain R] by_cases ne_bot : maximalIdeal R = ⊥ · rw [ne_bot]; infer_instance obtain ⟨a, ha₁, ha₂⟩ : ∃ a ∈ maximalIdeal R, a ≠ (0 : R) := by - by_contra' h'; apply ne_bot; rwa [eq_bot_iff] + by_contra! h'; apply ne_bot; rwa [eq_bot_iff] have hle : Ideal.span {a} ≤ maximalIdeal R := by rwa [Ideal.span_le, Set.singleton_subset_iff] have : (Ideal.span {a}).radical = maximalIdeal R := by rw [Ideal.radical_eq_sInf] @@ -111,7 +111,7 @@ theorem maximalIdeal_isPrincipal_of_isDedekindDomain [LocalRing R] [IsDomain R] rw [hn, pow_zero, Ideal.one_eq_top] at this exact (Ideal.IsMaximal.ne_top inferInstance (eq_top_iff.mpr <| this.trans hle)).elim obtain ⟨b, hb₁, hb₂⟩ : ∃ b ∈ maximalIdeal R ^ n, ¬b ∈ Ideal.span {a} := by - by_contra' h'; rw [Nat.find_eq_iff] at hn; exact hn.2 n n.lt_succ_self fun x hx => h' x hx + by_contra! h'; rw [Nat.find_eq_iff] at hn; exact hn.2 n n.lt_succ_self fun x hx => h' x hx have hb₃ : ∀ m ∈ maximalIdeal R, ∃ k : R, k * a = b * m := by intro m hm; rw [← Ideal.mem_span_singleton']; apply Nat.find_spec this rw [hn, pow_succ']; exact Ideal.mul_mem_mul hb₁ hm diff --git a/Mathlib/RingTheory/GradedAlgebra/Radical.lean b/Mathlib/RingTheory/GradedAlgebra/Radical.lean index de41093e493f7..280da6b16972a 100644 --- a/Mathlib/RingTheory/GradedAlgebra/Radical.lean +++ b/Mathlib/RingTheory/GradedAlgebra/Radical.lean @@ -56,7 +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 + by_contra! rid obtain ⟨rid₁, rid₂⟩ := rid classical /- diff --git a/Mathlib/RingTheory/Ideal/Basic.lean b/Mathlib/RingTheory/Ideal/Basic.lean index ecefc41cac740..410e72ebb6203 100644 --- a/Mathlib/RingTheory/Ideal/Basic.lean +++ b/Mathlib/RingTheory/Ideal/Basic.lean @@ -650,7 +650,7 @@ lemma isPrime_of_maximally_disjoint (I : Ideal α) have : 1 ∈ (S : Set α) := S.one_mem aesop mem_or_mem' {x y} hxy := by - by_contra' rid + by_contra! rid have hx := maximally_disjoint (I ⊔ span {x}) (Submodule.lt_sup_iff_not_mem.mpr rid.1) have hy := maximally_disjoint (I ⊔ span {y}) (Submodule.lt_sup_iff_not_mem.mpr rid.2) simp only [Set.not_disjoint_iff, mem_inter_iff, SetLike.mem_coe, Submodule.mem_sup, diff --git a/Mathlib/RingTheory/IntegralClosure.lean b/Mathlib/RingTheory/IntegralClosure.lean index 59841c5e0543b..2cc38fdf8f000 100644 --- a/Mathlib/RingTheory/IntegralClosure.lean +++ b/Mathlib/RingTheory/IntegralClosure.lean @@ -267,7 +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' + by_contra! h' apply hN rwa [eq_bot_iff] have : Function.Injective f := by diff --git a/Mathlib/RingTheory/Polynomial/Content.lean b/Mathlib/RingTheory/Polynomial/Content.lean index fc7c5bf99595f..521b186c90a94 100644 --- a/Mathlib/RingTheory/Polynomial/Content.lean +++ b/Mathlib/RingTheory/Polynomial/Content.lean @@ -436,7 +436,7 @@ theorem exists_primitive_lcm_of_isPrimitive {p q : R[X]} (hp : p.IsPrimitive) (h suffices hs : ∀ (n : ℕ) (s : R[X]), s.natDegree = n → p ∣ s ∧ q ∣ s → r ∣ s · apply hs s.natDegree s rfl clear s - by_contra' con + by_contra! con rcases Nat.find_spec con with ⟨s, sdeg, ⟨ps, qs⟩, rs⟩ have s0 : s ≠ 0 := by contrapose! rs diff --git a/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean b/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean index c50c18f560f90..eeb0c4cc212ab 100644 --- a/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean +++ b/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean @@ -62,7 +62,7 @@ private theorem cyclotomic_neg_one_pos {n : ℕ} (hn : 2 < n) {R} [LinearOrdered simp only [Int.cast_one, Int.cast_neg] have h0 := cyclotomic_coeff_zero ℝ hn.le rw [coeff_zero_eq_eval_zero] at h0 - by_contra' hx + by_contra! hx have := intermediate_value_univ (-1) 0 (cyclotomic n ℝ).continuous obtain ⟨y, hy : IsRoot _ y⟩ := this (show (0 : ℝ) ∈ Set.Icc _ _ by simpa [h0] using hx) rw [@isRoot_cyclotomic_iff] at hy diff --git a/Mathlib/RingTheory/WittVector/Domain.lean b/Mathlib/RingTheory/WittVector/Domain.lean index 4593e1aa9118a..d17531348db65 100644 --- a/Mathlib/RingTheory/WittVector/Domain.lean +++ b/Mathlib/RingTheory/WittVector/Domain.lean @@ -88,7 +88,7 @@ theorem eq_iterate_verschiebung {x : 𝕎 R} {n : ℕ} (h : ∀ i < n, x.coeff i theorem verschiebung_nonzero {x : 𝕎 R} (hx : x ≠ 0) : ∃ n : ℕ, ∃ x' : 𝕎 R, x'.coeff 0 ≠ 0 ∧ x = verschiebung^[n] x' := by have hex : ∃ k : ℕ, x.coeff k ≠ 0 := by - by_contra' hall + by_contra! hall apply hx ext i simp only [hall, zero_coeff] diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean index e7cd746c9b9ae..b5756e8420852 100644 --- a/Mathlib/SetTheory/Cardinal/Basic.lean +++ b/Mathlib/SetTheory/Cardinal/Basic.lean @@ -1449,7 +1449,7 @@ theorem isLimit_aleph0 : IsLimit ℵ₀ := #align cardinal.is_limit_aleph_0 Cardinal.isLimit_aleph0 theorem IsLimit.aleph0_le {c : Cardinal} (h : IsLimit c) : ℵ₀ ≤ c := by - by_contra' h' + by_contra! h' rcases lt_aleph0.1 h' with ⟨_ | n, rfl⟩ · exact h.ne_zero.irrefl · rw [nat_succ] at h diff --git a/Mathlib/SetTheory/Cardinal/Cofinality.lean b/Mathlib/SetTheory/Cardinal/Cofinality.lean index 7104e6d954a95..5ad120c50dc9c 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality.lean @@ -640,7 +640,7 @@ theorem exists_fundamental_sequence (a : Ordinal.{u}) : · push_neg at h cases' wo.wf.min_mem _ h with hji hij refine' ⟨typein r' ⟨_, fun k hkj => lt_of_lt_of_le _ hij⟩, typein_lt_type _ _, _⟩ - · by_contra' H + · by_contra! H exact (wo.wf.not_lt_min _ h ⟨IsTrans.trans _ _ _ hkj hji, H⟩) hkj · rwa [bfamilyOfFamily'_typein] #align ordinal.exists_fundamental_sequence Ordinal.exists_fundamental_sequence @@ -781,7 +781,7 @@ theorem cof_univ : cof univ.{u, v} = Cardinal.univ.{u, v} := then s has an unbounded member -/ theorem unbounded_of_unbounded_sUnion (r : α → α → Prop) [wo : IsWellOrder α r] {s : Set (Set α)} (h₁ : Unbounded r <| ⋃₀ s) (h₂ : #s < StrictOrder.cof r) : ∃ x ∈ s, Unbounded r x := by - by_contra' h + by_contra! h simp_rw [not_unbounded_iff] at h let f : s → α := fun x : s => wo.wf.sup x (h x.1 x.2) refine' h₂.not_le (le_trans (csInf_le' ⟨range f, fun x => _, rfl⟩) mk_range_le) @@ -803,7 +803,7 @@ theorem unbounded_of_unbounded_iUnion {α β : Type u} (r : α → α → Prop) theorem infinite_pigeonhole {β α : Type u} (f : β → α) (h₁ : ℵ₀ ≤ #β) (h₂ : #α < (#β).ord.cof) : ∃ a : α, #(f ⁻¹' {a}) = #β := by have : ∃ a, #β ≤ #(f ⁻¹' {a}) := by - by_contra' h + by_contra! h apply mk_univ.not_lt rw [← preimage_univ, ← iUnion_of_singleton, preimage_iUnion] exact diff --git a/Mathlib/SetTheory/Ordinal/Arithmetic.lean b/Mathlib/SetTheory/Ordinal/Arithmetic.lean index f8708e3d7f39f..38b8fbaf35483 100644 --- a/Mathlib/SetTheory/Ordinal/Arithmetic.lean +++ b/Mathlib/SetTheory/Ordinal/Arithmetic.lean @@ -1282,7 +1282,7 @@ theorem ne_sup_iff_lt_sup {ι : Type u} {f : ι → Ordinal.{max u v}} : theorem sup_not_succ_of_ne_sup {ι : Type u} {f : ι → Ordinal.{max u v}} (hf : ∀ i, f i ≠ sup.{_, v} f) {a} (hao : a < sup.{_, v} f) : succ a < sup.{_, v} f := by - by_contra' hoa + by_contra! hoa exact hao.not_le (sup_le fun i => le_of_lt_succ <| (lt_of_le_of_ne (le_sup _ _) (hf i)).trans_le hoa) #align ordinal.sup_not_succ_of_ne_sup Ordinal.sup_not_succ_of_ne_sup @@ -1623,7 +1623,7 @@ theorem sup_eq_lsub_or_sup_succ_eq_lsub {ι : Type u} (f : ι → Ordinal.{max u theorem sup_succ_le_lsub {ι : Type u} (f : ι → Ordinal.{max u v}) : succ (sup.{_, v} f) ≤ lsub.{_, v} f ↔ ∃ i, f i = sup.{_, v} f := by refine' ⟨fun h => _, _⟩ - · by_contra' hf + · by_contra! hf exact (succ_le_iff.1 h).ne ((sup_le_lsub f).antisymm (lsub_le (ne_sup_iff_lt_sup.1 hf))) rintro ⟨_, hf⟩ rw [succ_le_iff, ← hf] @@ -1640,7 +1640,7 @@ theorem sup_eq_lsub_iff_succ {ι : Type u} (f : ι → Ordinal.{max u v}) : refine' ⟨fun h => _, fun hf => le_antisymm (sup_le_lsub f) (lsub_le fun i => _)⟩ · rw [← h] exact fun a => sup_not_succ_of_ne_sup fun i => (lsub_le_iff.1 (le_of_eq h.symm) i).ne - by_contra' hle + by_contra! hle have heq := (sup_succ_eq_lsub f).2 ⟨i, le_antisymm (le_sup _ _) hle⟩ have := hf _ @@ -1717,7 +1717,7 @@ theorem nonempty_compl_range {ι : Type u} (f : ι → Ordinal.{max u v}) : (Set theorem lsub_typein (o : Ordinal) : lsub.{u, u} (typein ((· < ·) : o.out.α → o.out.α → Prop)) = o := (lsub_le.{u, u} typein_lt_self).antisymm (by - by_contra' h + by_contra! h -- Porting note: `nth_rw` → `conv_rhs` & `rw` conv_rhs at h => rw [← type_lt o] simpa [typein_enum] using lt_lsub.{u, u} (typein (· < ·)) (enum (· < ·) _ h)) @@ -1839,7 +1839,7 @@ theorem bsup_eq_blsub_or_succ_bsup_eq_blsub {o : Ordinal.{u}} (f : ∀ a < o, Or theorem bsup_succ_le_blsub {o : Ordinal.{u}} (f : ∀ a < o, Ordinal.{max u v}) : succ (bsup.{_, v} o f) ≤ blsub.{_, v} o f ↔ ∃ i hi, f i hi = bsup.{_, v} o f := by refine' ⟨fun h => _, _⟩ - · by_contra' hf + · by_contra! hf exact ne_of_lt (succ_le_iff.1 h) (le_antisymm (bsup_le_blsub f) (blsub_le (lt_bsup_of_ne_bsup.1 hf))) @@ -2027,7 +2027,7 @@ theorem mex_not_mem_range {ι : Type u} (f : ι → Ordinal.{max u v}) : mex.{_, theorem le_mex_of_forall {ι : Type u} {f : ι → Ordinal.{max u v}} {a : Ordinal} (H : ∀ b < a, ∃ i, f i = b) : a ≤ mex.{_, v} f := by - by_contra' h + by_contra! h exact mex_not_mem_range f (H _ h) #align ordinal.le_mex_of_forall Ordinal.le_mex_of_forall @@ -2040,7 +2040,7 @@ theorem mex_le_of_ne {ι} {f : ι → Ordinal} {a} (ha : ∀ i, f i ≠ a) : mex #align ordinal.mex_le_of_ne Ordinal.mex_le_of_ne theorem exists_of_lt_mex {ι} {f : ι → Ordinal} {a} (ha : a < mex f) : ∃ i, f i = a := by - by_contra' ha' + by_contra! ha' exact ha.not_le (mex_le_of_ne ha') #align ordinal.exists_of_lt_mex Ordinal.exists_of_lt_mex @@ -2058,7 +2058,7 @@ theorem mex_monotone {α β : Type u} {f : α → Ordinal.{max u v}} {g : β → theorem mex_lt_ord_succ_mk {ι : Type u} (f : ι → Ordinal.{u}) : mex.{_, u} f < (succ #ι).ord := by - by_contra' h + by_contra! h apply (lt_succ #ι).not_le have H := fun a => exists_of_lt_mex ((typein_lt_self a).trans_le h) let g : (succ #ι).ord.out.α → ι := fun a => Classical.choose (H a) @@ -2088,7 +2088,7 @@ theorem bmex_not_mem_brange {o : Ordinal} (f : ∀ a < o, Ordinal) : bmex o f theorem le_bmex_of_forall {o : Ordinal} (f : ∀ a < o, Ordinal) {a : Ordinal} (H : ∀ b < a, ∃ i hi, f i hi = b) : a ≤ bmex o f := by - by_contra' h + by_contra! h exact bmex_not_mem_brange f (H _ h) #align ordinal.le_bmex_of_forall Ordinal.le_bmex_of_forall @@ -2268,7 +2268,7 @@ theorem enumOrd_surjective (hS : Unbounded (· < ·) S) : ∀ s ∈ S, ∃ a, en -- Porting note: `flip` is required to infer a metavariable. rcases flip exists_lt_of_lt_csSup ha ⟨0, this⟩ with ⟨b, hb, hab⟩ exact (enumOrd_strictMono hS hab).trans_le hb - · by_contra' h + · by_contra! h exact (le_csSup ⟨s, fun a => (lt_wf.self_le_of_strictMono (enumOrd_strictMono hS) a).trans⟩ (enumOrd_succ_le hS hs h)).not_lt @@ -2514,7 +2514,7 @@ theorem add_le_of_forall_add_lt {a b c : Ordinal} (hb : 0 < b) (h : ∀ d < b, a exact (h _ hb).le) rw [← H] apply add_le_add_left _ a - by_contra' hb + by_contra! hb exact (h _ hb).ne H #align ordinal.add_le_of_forall_add_lt Ordinal.add_le_of_forall_add_lt diff --git a/Mathlib/SetTheory/Ordinal/Exponential.lean b/Mathlib/SetTheory/Ordinal/Exponential.lean index 1001103c7694c..6d08cedf7a25c 100644 --- a/Mathlib/SetTheory/Ordinal/Exponential.lean +++ b/Mathlib/SetTheory/Ordinal/Exponential.lean @@ -413,7 +413,7 @@ theorem opow_mul_add_lt_opow_succ {b u v w : Ordinal} (hvb : v < b) (hw : w < b theorem log_opow_mul_add {b u v w : Ordinal} (hb : 1 < b) (hv : v ≠ 0) (hvb : v < b) (hw : w < b ^ u) : log b (b ^ u * v + w) = u := by have hne' := (opow_mul_add_pos (zero_lt_one.trans hb).ne' u hv w).ne' - by_contra' hne + by_contra! hne cases' lt_or_gt_of_ne hne with h h · rw [← lt_opow_iff_log_lt hb hne'] at h exact h.not_le ((le_mul_left _ (Ordinal.pos_iff_ne_zero.2 hv)).trans (le_add_right _ _)) diff --git a/Mathlib/SetTheory/Ordinal/NaturalOps.lean b/Mathlib/SetTheory/Ordinal/NaturalOps.lean index 26c85fcc48a33..9f4ac5173675b 100644 --- a/Mathlib/SetTheory/Ordinal/NaturalOps.lean +++ b/Mathlib/SetTheory/Ordinal/NaturalOps.lean @@ -373,7 +373,7 @@ instance add_covariantClass_le : CovariantClass NatOrdinal.{u} NatOrdinal.{u} ( instance add_contravariantClass_le : ContravariantClass NatOrdinal.{u} NatOrdinal.{u} (· + ·) (· ≤ ·) := ⟨fun a b c h => by - by_contra' h' + by_contra! h' exact h.not_lt (add_lt_add_left h' a)⟩ #align nat_ordinal.add_contravariant_class_le NatOrdinal.add_contravariantClass_le diff --git a/Mathlib/SetTheory/Ordinal/Principal.lean b/Mathlib/SetTheory/Ordinal/Principal.lean index 53af177bf8aa8..ef848f271cf68 100644 --- a/Mathlib/SetTheory/Ordinal/Principal.lean +++ b/Mathlib/SetTheory/Ordinal/Principal.lean @@ -162,7 +162,7 @@ theorem exists_lt_add_of_not_principal_add {a} (ha : ¬Principal (· + ·) a) : theorem principal_add_iff_add_lt_ne_self {a} : Principal (· + ·) a ↔ ∀ ⦃b c⦄, b < a → c < a → b + c ≠ a := ⟨fun ha b c 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, c, hb, hc, rfl⟩ exact (H hb hc).irrefl⟩ #align ordinal.principal_add_iff_add_lt_ne_self Ordinal.principal_add_iff_add_lt_ne_self diff --git a/Mathlib/SetTheory/Ordinal/Topology.lean b/Mathlib/SetTheory/Ordinal/Topology.lean index 54a456ab2d100..fb0415372b704 100644 --- a/Mathlib/SetTheory/Ordinal/Topology.lean +++ b/Mathlib/SetTheory/Ordinal/Topology.lean @@ -229,7 +229,7 @@ theorem enumOrd_isNormal_iff_isClosed (hs : s.Unbounded (· < ·)) : b hb rw [← hb] apply Hs.monotone - by_contra' hba + by_contra! hba apply (Hs (lt_succ b)).not_le rw [hb] exact le_bsup.{u, u} _ _ (ha.2 _ hba) diff --git a/Mathlib/SetTheory/ZFC/Basic.lean b/Mathlib/SetTheory/ZFC/Basic.lean index a4167046b4e37..8bfc3b9f71fad 100644 --- a/Mathlib/SetTheory/ZFC/Basic.lean +++ b/Mathlib/SetTheory/ZFC/Basic.lean @@ -1699,7 +1699,7 @@ theorem sInter_empty : ⋂₀ (∅ : Class.{u}) = univ := by theorem eq_univ_of_powerset_subset {A : Class} (hA : powerset A ⊆ A) : A = univ := eq_univ_of_forall (by - by_contra' hnA + by_contra! hnA exact WellFounded.min_mem ZFSet.mem_wf _ hnA (hA fun x hx => diff --git a/Mathlib/Tactic/ByContra.lean b/Mathlib/Tactic/ByContra.lean index f69d742c79423..ec7bc62e4cbd9 100644 --- a/Mathlib/Tactic/ByContra.lean +++ b/Mathlib/Tactic/ByContra.lean @@ -10,11 +10,11 @@ open Lean Lean.Parser Parser.Tactic Elab Command Elab.Tactic Meta /-- If the target of the main goal is a proposition `p`, -`by_contra'` reduces the goal to proving `False` using the additional hypothesis `this : ¬ p`. -`by_contra' h` can be used to name the hypothesis `h : ¬ p`. +`by_contra!` reduces the goal to proving `False` using the additional hypothesis `this : ¬ p`. +`by_contra! h` can be used to name the hypothesis `h : ¬ p`. The hypothesis `¬ p` will be negation normalized using `push_neg`. For instance, `¬ a < b` will be changed to `b ≤ a`. -`by_contra' h : q` will normalize negations in `¬ p`, normalize negations in `q`, +`by_contra! h : q` will normalize negations in `¬ p`, normalize negations in `q`, and then check that the two normalized forms are equal. The resulting hypothesis is the pre-normalized form, `q`. If the name `h` is not explicitly provided, then `this` will be used as name. @@ -23,22 +23,22 @@ It is a variant on the tactic `by_contra`. Examples: ```lean example : 1 < 2 := by - by_contra' h + by_contra! h -- h : 2 ≤ 1 ⊢ False example : 1 < 2 := by - by_contra' h : ¬ 1 < 2 + by_contra! h : ¬ 1 < 2 -- h : ¬ 1 < 2 ⊢ False ``` -/ -syntax (name := byContra') "by_contra'" (ppSpace colGt binderIdent)? Term.optType : tactic +syntax (name := byContra!) "by_contra!" (ppSpace colGt binderIdent)? Term.optType : tactic macro_rules - | `(tactic| by_contra'%$tk $[_%$under]? $[: $ty]?) => - `(tactic| by_contra' $(mkIdentFrom (under.getD tk) `this (canonical := true)):ident $[: $ty]?) - | `(tactic| by_contra' $e:ident) => `(tactic| (by_contra $e:ident; push_neg at $e:ident)) - | `(tactic| by_contra' $e:ident : $y) => `(tactic| - (by_contra' h; + | `(tactic| by_contra!%$tk $[_%$under]? $[: $ty]?) => + `(tactic| by_contra! $(mkIdentFrom (under.getD tk) `this (canonical := true)):ident $[: $ty]?) + | `(tactic| by_contra! $e:ident) => `(tactic| (by_contra $e:ident; push_neg at $e:ident)) + | `(tactic| by_contra! $e:ident : $y) => `(tactic| + (by_contra! h; -- if the below `exact` call fails then this tactic should fail with the message -- tactic failed: and are not definitionally equal have $e:ident : $y := by { push_neg; exact h }; diff --git a/Mathlib/Topology/Algebra/Module/Basic.lean b/Mathlib/Topology/Algebra/Module/Basic.lean index f87b4d89d3023..7abdc56957123 100644 --- a/Mathlib/Topology/Algebra/Module/Basic.lean +++ b/Mathlib/Topology/Algebra/Module/Basic.lean @@ -667,7 +667,7 @@ instance uniqueOfRight [Subsingleton M₂] : Unique (M₁ →SL[σ₁₂] M₂) #align continuous_linear_map.unique_of_right ContinuousLinearMap.uniqueOfRight theorem exists_ne_zero {f : M₁ →SL[σ₁₂] M₂} (hf : f ≠ 0) : ∃ x, f x ≠ 0 := by - by_contra' h + by_contra! h exact hf (ContinuousLinearMap.ext h) #align continuous_linear_map.exists_ne_zero ContinuousLinearMap.exists_ne_zero diff --git a/Mathlib/Topology/Algebra/Module/FiniteDimension.lean b/Mathlib/Topology/Algebra/Module/FiniteDimension.lean index 7680cd6ec9ffc..afb64a2a6e7f9 100644 --- a/Mathlib/Topology/Algebra/Module/FiniteDimension.lean +++ b/Mathlib/Topology/Algebra/Module/FiniteDimension.lean @@ -100,7 +100,7 @@ theorem unique_topology_of_t2 {t : TopologicalSpace 𝕜} (h₁ : @TopologicalAd · rw [mem_closedBall_zero_iff] -- Now suppose `ξ ≠ 0`. By contradiction, let's assume `ε < ‖ξ‖`, and show that -- `ξ₀ ∈ 𝓑 ⊆ {ξ₀}ᶜ`, which is a contradiction. - by_contra' h + by_contra! h suffices (ξ₀ * ξ⁻¹) • ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ by rw [smul_eq_mul 𝕜, mul_assoc, inv_mul_cancel hξ0, mul_one] at this exact not_mem_compl_iff.mpr (mem_singleton ξ₀) ((balancedCore_subset _) this) diff --git a/Mathlib/Topology/Algebra/Order/LiminfLimsup.lean b/Mathlib/Topology/Algebra/Order/LiminfLimsup.lean index 4c90b59cb76ef..79654909e4d9a 100644 --- a/Mathlib/Topology/Algebra/Order/LiminfLimsup.lean +++ b/Mathlib/Topology/Algebra/Order/LiminfLimsup.lean @@ -263,7 +263,7 @@ theorem tendsto_of_no_upcrossings [DenselyOrdered α] {f : Filter β} {u : β · exact ⟨sInf ∅, tendsto_bot⟩ refine' ⟨limsup u f, _⟩ apply tendsto_of_le_liminf_of_limsup_le _ le_rfl h h' - by_contra' hlt + by_contra! hlt obtain ⟨a, ⟨⟨la, au⟩, as⟩⟩ : ∃ a, (f.liminf u < a ∧ a < f.limsup u) ∧ a ∈ s := dense_iff_inter_open.1 hs (Set.Ioo (f.liminf u) (f.limsup u)) isOpen_Ioo (Set.nonempty_Ioo.2 hlt) @@ -357,13 +357,13 @@ theorem Antitone.map_limsSup_of_continuousAt {F : Filter R} [NeBot F] {f : R → have B : ∃ᶠ n in F, F.limsSup ≤ n := by apply (frequently_lt_of_lt_limsSup cobdd c_lt).mono intro x hx - by_contra' + by_contra! have : (Set.Ioo c F.limsSup).Nonempty := ⟨x, ⟨hx, this⟩⟩ simp only [hc, Set.not_nonempty_empty] at this apply liminf_le_of_frequently_le _ (bdd_above.isBoundedUnder f_decr) exact (B.mono fun x hx ↦ f_decr hx) push_neg at h' - by_contra' H + by_contra! H have not_bot : ¬ IsBot F.limsSup := fun maybe_bot ↦ lt_irrefl (F.liminf f) <| lt_of_le_of_lt (liminf_le_of_frequently_le (frequently_of_forall (fun r ↦ f_decr (maybe_bot r))) @@ -546,7 +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 + 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/Mathlib/Topology/Category/Stonean/Basic.lean b/Mathlib/Topology/Category/Stonean/Basic.lean index 8153eb46c2855..ce06f29a1c3bb 100644 --- a/Mathlib/Topology/Category/Stonean/Basic.lean +++ b/Mathlib/Topology/Category/Stonean/Basic.lean @@ -185,7 +185,7 @@ lemma epi_iff_surjective {X Y : Stonean} (f : X ⟶ Y) : refine ⟨?_, ConcreteCategory.epi_of_surjective _⟩ dsimp [Function.Surjective] intro h y - by_contra' hy + by_contra! hy let C := Set.range f have hC : IsClosed C := (isCompact_range f.continuous).isClosed let U := Cᶜ diff --git a/Mathlib/Topology/Compactness/Compact.lean b/Mathlib/Topology/Compactness/Compact.lean index da71c59517a1d..5bcdfe33ff9af 100644 --- a/Mathlib/Topology/Compactness/Compact.lean +++ b/Mathlib/Topology/Compactness/Compact.lean @@ -486,7 +486,7 @@ theorem exists_subset_nhds_of_isCompact' [Nonempty ι] {V : ι → Set X} obtain ⟨W, hsubW, W_op, hWU⟩ := exists_open_set_nhds hU suffices : ∃ i, V i ⊆ W · exact this.imp fun i hi => hi.trans hWU - by_contra' H + by_contra! H replace H : ∀ i, (V i ∩ Wᶜ).Nonempty := fun i => Set.inter_compl_nonempty_iff.mpr (H i) have : (⋂ i, V i ∩ Wᶜ).Nonempty := by refine' @@ -798,7 +798,7 @@ theorem finite_of_compact_of_discrete [CompactSpace X] [DiscreteTopology X] : Fi theorem exists_nhds_ne_neBot (X : Type*) [TopologicalSpace X] [CompactSpace X] [Infinite X] : ∃ x : X, (𝓝[≠] x).NeBot := by - by_contra' H + by_contra! H simp_rw [not_neBot] at H haveI := discreteTopology_iff_nhds_ne.2 H exact Infinite.not_finite (finite_of_compact_of_discrete : Finite X) @@ -938,7 +938,7 @@ theorem IsCompact.finite (hs : IsCompact s) (hs' : DiscreteTopology s) : s.Finit theorem exists_nhds_ne_inf_principal_neBot (hs : IsCompact s) (hs' : s.Infinite) : ∃ x ∈ s, (𝓝[≠] x ⊓ 𝓟 s).NeBot := by - by_contra' H + by_contra! H simp_rw [not_neBot] at H exact hs' (hs.finite <| discreteTopology_subtype_iff.mpr H) #align exists_nhds_ne_inf_principal_ne_bot exists_nhds_ne_inf_principal_neBot diff --git a/Mathlib/Topology/Connected/Basic.lean b/Mathlib/Topology/Connected/Basic.lean index 2d09d9df8a0f0..6369a5f29a852 100644 --- a/Mathlib/Topology/Connected/Basic.lean +++ b/Mathlib/Topology/Connected/Basic.lean @@ -1311,7 +1311,7 @@ continuous on a set `s`, is constant on s, then s is preconnected -/ theorem isPreconnected_of_forall_constant {s : Set α} (hs : ∀ f : α → Bool, ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y) : IsPreconnected s := by unfold IsPreconnected - by_contra' + by_contra! rcases this with ⟨u, v, u_op, v_op, hsuv, ⟨x, x_in_s, x_in_u⟩, ⟨y, y_in_s, y_in_v⟩, H⟩ have hy : y ∉ u := fun y_in_u => eq_empty_iff_forall_not_mem.mp H y ⟨y_in_s, ⟨y_in_u, y_in_v⟩⟩ have : ContinuousOn u.boolIndicator s := by diff --git a/Mathlib/Topology/Connected/TotallyDisconnected.lean b/Mathlib/Topology/Connected/TotallyDisconnected.lean index 252995bd769b3..850230f42c47c 100644 --- a/Mathlib/Topology/Connected/TotallyDisconnected.lean +++ b/Mathlib/Topology/Connected/TotallyDisconnected.lean @@ -95,7 +95,7 @@ theorem isTotallyDisconnected_of_isClopen_set {X : Type*} [TopologicalSpace X] IsTotallyDisconnected (Set.univ : Set X) := by rintro S - hS unfold Set.Subsingleton - by_contra' h_contra + by_contra! h_contra rcases h_contra with ⟨x, hx, y, hy, hxy⟩ obtain ⟨U, hU, hxU, hyU⟩ := hX hxy specialize diff --git a/Mathlib/Topology/EMetricSpace/Paracompact.lean b/Mathlib/Topology/EMetricSpace/Paracompact.lean index b4494c9f093de..ba1e0e2ac41ea 100644 --- a/Mathlib/Topology/EMetricSpace/Paracompact.lean +++ b/Mathlib/Topology/EMetricSpace/Paracompact.lean @@ -91,7 +91,7 @@ instance (priority := 100) instParacompactSpace [PseudoEMetricSpace α] : Paraco rcases ENNReal.exists_inv_two_pow_lt this.ne' with ⟨n, hn⟩ refine' ⟨n, Subset.trans (ball_subset_ball _) hε⟩ simpa only [div_eq_mul_inv, mul_comm] using (ENNReal.mul_lt_of_lt_div hn).le - by_contra' h + by_contra! h apply h n (ind x) exact memD.2 ⟨x, rfl, hn, fun _ _ _ => h _ _, mem_ball_self (pow_pos _)⟩ -- Each `D n i` is a union of open balls, hence it is an open set @@ -138,7 +138,7 @@ instance (priority := 100) instParacompactSpace [PseudoEMetricSpace α] : Paraco -- For each `m ≤ n + k` there is at most one `j` such that `D m j ∩ B` is nonempty. have Hle : ∀ m ≤ n + k, Set.Subsingleton { j | (D m j ∩ B).Nonempty } := by rintro m hm j₁ ⟨y, hyD, hyB⟩ j₂ ⟨z, hzD, hzB⟩ - by_contra' h' : j₁ ≠ j₂ + by_contra! h' : j₁ ≠ j₂ wlog h : j₁ < j₂ generalizing j₁ j₂ y z · exact this z hzD hzB y hyD hyB h'.symm (h'.lt_or_lt.resolve_left h) rcases memD.1 hyD with ⟨y', rfl, hsuby, -, hdisty⟩ diff --git a/Mathlib/Topology/Instances/RatLemmas.lean b/Mathlib/Topology/Instances/RatLemmas.lean index 8456bd0812040..139c858ac8be5 100644 --- a/Mathlib/Topology/Instances/RatLemmas.lean +++ b/Mathlib/Topology/Instances/RatLemmas.lean @@ -81,7 +81,7 @@ theorem not_secondCountableTopology_opc : ¬SecondCountableTopology ℚ∞ := by instance : TotallyDisconnectedSpace ℚ := by refine' ⟨fun s hsu hs x hx y hy => _⟩; clear hsu - by_contra' H : x ≠ y + by_contra! H : x ≠ y wlog hlt : x < y · refine' this s hs y hy x hx H.symm <| H.lt_or_lt.resolve_left hlt <;> assumption rcases exists_irrational_btwn (Rat.cast_lt.2 hlt) with ⟨z, hz, hxz, hzy⟩ diff --git a/Mathlib/Topology/MetricSpace/PiNat.lean b/Mathlib/Topology/MetricSpace/PiNat.lean index 9ba280a83c13a..88af496faa80c 100644 --- a/Mathlib/Topology/MetricSpace/PiNat.lean +++ b/Mathlib/Topology/MetricSpace/PiNat.lean @@ -90,7 +90,7 @@ theorem firstDiff_comm (x y : ∀ n, E n) : firstDiff x y = firstDiff y x := by theorem min_firstDiff_le (x y z : ∀ n, E n) (h : x ≠ z) : min (firstDiff x y) (firstDiff y z) ≤ firstDiff x z := by - by_contra' H + by_contra! H rw [lt_min_iff] at H refine apply_firstDiff_ne h ?_ calc @@ -154,7 +154,7 @@ theorem mem_cylinder_iff_le_firstDiff {x y : ∀ n, E n} (hne : x ≠ y) (i : x ∈ cylinder y i ↔ i ≤ firstDiff x y := by constructor · intro h - by_contra' + by_contra! exact apply_firstDiff_ne hne (h _ this) · intro hi j hj exact apply_eq_of_lt_firstDiff (hj.trans_le hi) @@ -317,7 +317,7 @@ theorem mem_cylinder_iff_dist_le {x y : ∀ n, E n} {n : ℕ} : suffices (∀ i : ℕ, i < n → y i = x i) ↔ n ≤ firstDiff y x by simpa [dist_eq_of_ne hne] constructor · intro hy - by_contra' H + by_contra! H exact apply_firstDiff_ne hne (hy _ H) · intro h i hi exact apply_eq_of_lt_firstDiff (hi.trans_le h) @@ -744,7 +744,7 @@ theorem exists_nat_nat_continuous_surjective_of_completeSpace (α : Type*) [Metr have dist' : dist x y = dist x.1 y.1 := rfl let n := firstDiff x.1 y.1 - 1 have diff_pos : 0 < firstDiff x.1 y.1 := by - by_contra' h + by_contra! h apply apply_firstDiff_ne hne' rw [le_zero_iff.1 h] apply apply_eq_of_dist_lt _ le_rfl diff --git a/Mathlib/Topology/Order/Basic.lean b/Mathlib/Topology/Order/Basic.lean index 4df33c7c2e5f3..1e1b84e6a24ad 100644 --- a/Mathlib/Topology/Order/Basic.lean +++ b/Mathlib/Topology/Order/Basic.lean @@ -1365,11 +1365,11 @@ theorem countable_setOf_covby_right [SecondCountableTopology α] : rcases hxx'.lt_or_lt with (h' | h') · refine' disjoint_left.2 fun u ux ux' => xt.2.2.1 _ refine' h'z x' x't ⟨ux'.1.trans_le (ux.2.trans (hy x xt.1).le), _⟩ - by_contra' H + by_contra! H exact lt_irrefl _ ((Hy _ _ xt.1 H).trans_lt h') · refine' disjoint_left.2 fun u ux ux' => x't.2.2.1 _ refine' h'z x xt ⟨ux.1.trans_le (ux'.2.trans (hy x' x't.1).le), _⟩ - by_contra' H + by_contra! H exact lt_irrefl _ ((Hy _ _ x't.1 H).trans_lt h') refine' this.countable_of_isOpen (fun x hx => _) fun x hx => ⟨x, hz x hx, le_rfl⟩ suffices H : Ioc (z x) x = Ioo (z x) (y x) diff --git a/Mathlib/Topology/Perfect.lean b/Mathlib/Topology/Perfect.lean index 5f7ee247574a9..a9b0a03418a19 100644 --- a/Mathlib/Topology/Perfect.lean +++ b/Mathlib/Topology/Perfect.lean @@ -191,7 +191,7 @@ theorem exists_countable_union_perfect_of_isClosed [SecondCountableTopology α] have : U ∈ v := ⟨hUb, hU_cnt⟩ apply xD.2 exact mem_biUnion this xU - by_contra' h + by_contra! h exact absurd (Countable.mono h (Set.countable_singleton _)) this · rw [inter_comm, inter_union_diff] #align exists_countable_union_perfect_of_is_closed exists_countable_union_perfect_of_isClosed diff --git a/Mathlib/Topology/Separation/NotNormal.lean b/Mathlib/Topology/Separation/NotNormal.lean index 0dc73955ff9bc..716dbf2c96da0 100644 --- a/Mathlib/Topology/Separation/NotNormal.lean +++ b/Mathlib/Topology/Separation/NotNormal.lean @@ -26,7 +26,7 @@ https://en.wikipedia.org/wiki/Moore_plane#Proof_that_the_Moore_plane_is_not_norm theorem IsClosed.mk_lt_continuum [NormalSpace X] {s : Set X} (hs : IsClosed s) [DiscreteTopology s] : #s < 𝔠 := by -- Proof by contradiction: assume `𝔠 ≤ #s` - by_contra' h + by_contra! h -- Choose a countable dense set `t : Set X` rcases exists_countable_dense X with ⟨t, htc, htd⟩ haveI := htc.to_subtype diff --git a/test/byContra.lean b/test/byContra.lean index 04e92a31db023..6cef8ec43c7b5 100644 --- a/test/byContra.lean +++ b/test/byContra.lean @@ -1,4 +1,4 @@ --- tests for byContra' tactic +-- tests for by_contra! tactic import Mathlib.Tactic.ByContra import Mathlib.Tactic.Rename import Mathlib.Tactic.Set @@ -6,32 +6,32 @@ import Mathlib.Data.Nat.Basic set_option autoImplicit true example (a b : ℕ) (foo : False) : a < b := by - by_contra' + by_contra! guard_hyp this : b ≤ a exact foo example (a b : ℕ) (h : False) : a < b := by - by_contra' foo + by_contra! foo revert foo; change b ≤ a → False; intro; exact h example (a b : ℕ) (h : False) : a < b := by - by_contra' foo : ¬ a < b -- can avoid push_neg + by_contra! foo : ¬ a < b -- can avoid push_neg guard_hyp foo : ¬ a < b exact h example : 1 < 2 := by - by_contra' + by_contra! guard_hyp this : 2 ≤ 1 contradiction example (p : Prop) (bar : False) : ¬ ¬ ¬ ¬ ¬ ¬ P := by - by_contra' foo : ¬ ¬ ¬ P -- normalises to ¬ P, as does ¬ (goal). + by_contra! foo : ¬ ¬ ¬ P -- normalises to ¬ P, as does ¬ (goal). guard_hyp foo : ¬ ¬ ¬ P exact bar example (p : Prop) (bar : False) : ¬ ¬ ¬ ¬ ¬ ¬ P := by - by_contra' : ¬ ¬ ¬ P + by_contra! : ¬ ¬ ¬ P guard_hyp this : ¬ ¬ ¬ P exact bar @@ -39,19 +39,19 @@ variable [LinearOrder α] [One α] [Mul α] example (x : α) (f : False) : x ≤ 1 := by set a := x * x - by_contra' h + by_contra! h guard_hyp h : 1 < x assumption example (x : α) (f : False) : x ≤ 1 := by let _a := x * x - by_contra' h + by_contra! h guard_hyp h : 1 < x assumption example (x : α) (f : False) : x ≤ 1 := by set a := x * x have : a ≤ a := le_rfl - by_contra' h + by_contra! h guard_hyp h : 1 < x assumption diff --git a/test/linarith.lean b/test/linarith.lean index a19a7e1ef7e5e..cb89b23fcd5f0 100644 --- a/test/linarith.lean +++ b/test/linarith.lean @@ -490,7 +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'' + by_contra! h'' linarith (config := {splitNe := true}) example (x y : ℚ) (h₁ : 0 ≤ y) (h₂ : y ≤ x) : y * x ≤ x * x := by nlinarith diff --git a/test/observe.lean b/test/observe.lean index 0cef4794d77c8..24d4b0d6252b9 100644 --- a/test/observe.lean +++ b/test/observe.lean @@ -13,7 +13,7 @@ theorem euclid (n : ℕ) : ∃ N, n < N ∧ N.Prime := by observe : n.factorial > 0 linarith constructor - · by_contra' + · by_contra! observe : p ∣ n.factorial observe : p ∣ N observe : p ∣ 1