diff --git a/Archive/Imo/Imo1988Q6.lean b/Archive/Imo/Imo1988Q6.lean index 82b00ffa484810..0fcd35a8212242 100644 --- a/Archive/Imo/Imo1988Q6.lean +++ b/Archive/Imo/Imo1988Q6.lean @@ -179,7 +179,7 @@ theorem constant_descent_vieta_jumping (x y : ℕ) {claim : Prop} {H : ℕ → suffices hc : c ≠ mx from lt_of_le_of_ne (mod_cast c_lt) hc -- However, recall that B(m_x) ≠ m_x + m_y. -- If c = m_x, we can prove B(m_x) = m_x + m_y. - contrapose! hm_B₂ + contrapose hm_B₂ subst c simp [hV₁] -- Hence p' = (c, m_x) lies on the upper branch, and we are done. diff --git a/Archive/Imo/Imo2008Q2.lean b/Archive/Imo/Imo2008Q2.lean index ff496520689f73..4b42c50b06d645 100644 --- a/Archive/Imo/Imo2008Q2.lean +++ b/Archive/Imo/Imo2008Q2.lean @@ -46,9 +46,9 @@ theorem imo2008_q2a (x y z : ℝ) (h : x * y * z = 1) (hx : x ≠ 1) (hy : y ≠ x ^ 2 / (x - 1) ^ 2 + y ^ 2 / (y - 1) ^ 2 + z ^ 2 / (z - 1) ^ 2 ≥ 1 := by obtain ⟨a, b, c, ha, hb, hc, rfl, rfl, rfl⟩ := subst_abc h obtain ⟨m, n, rfl, rfl⟩ : ∃ m n, b = c - m ∧ a = c - m - n := by use c - b, b - a; simp - have hm_ne_zero : m ≠ 0 := by contrapose! hy; simpa [field] - have hn_ne_zero : n ≠ 0 := by contrapose! hx; simpa [field] - have hmn_ne_zero : m + n ≠ 0 := by contrapose! hz; field_simp; linarith + have hm_ne_zero : m ≠ 0 := by contrapose hy; simpa [field] + have hn_ne_zero : n ≠ 0 := by contrapose hx; simpa [field] + have hmn_ne_zero : m + n ≠ 0 := by contrapose hz; field_simp; linarith have hc_sub_sub : c - (c - m - n) = m + n := by abel rw [ge_iff_le, ← sub_nonneg] convert sq_nonneg ((c * (m ^ 2 + n ^ 2 + m * n) - m * (m + n) ^ 2) / (m * n * (m + n))) diff --git a/Archive/MiuLanguage/DecisionNec.lean b/Archive/MiuLanguage/DecisionNec.lean index 2323668fd6f718..88049d53350662 100644 --- a/Archive/MiuLanguage/DecisionNec.lean +++ b/Archive/MiuLanguage/DecisionNec.lean @@ -133,7 +133,7 @@ theorem goodm_of_rule2 (xs : Miustr) (_ : Derivable (M :: xs)) (h₂ : Goodm (M constructor · rfl · obtain ⟨mhead, mtail⟩ := h₂ - contrapose! mtail + contrapose mtail rw [cons_append] at mtail exact or_self_iff.mp (mem_append.mp mtail) @@ -145,7 +145,7 @@ theorem goodm_of_rule3 (as bs : Miustr) (h₁ : Derivable (as ++ [I, I, I] ++ bs · cases as · contradiction exact mhead - · contrapose! nmtail + · contrapose nmtail rcases exists_cons_of_ne_nil k with ⟨x, xs, rfl⟩ simp_rw [cons_append] at nmtail ⊢ simpa using nmtail @@ -163,7 +163,7 @@ theorem goodm_of_rule4 (as bs : Miustr) (h₁ : Derivable (as ++ [U, U] ++ bs)) · cases as · contradiction exact mhead - · contrapose! nmtail + · contrapose nmtail rcases exists_cons_of_ne_nil k with ⟨x, xs, rfl⟩ simp_rw [cons_append] at nmtail ⊢ simpa using nmtail diff --git a/Archive/Sensitivity.lean b/Archive/Sensitivity.lean index bf4694a36479d1..a7fddf3e39c46c 100644 --- a/Archive/Sensitivity.lean +++ b/Archive/Sensitivity.lean @@ -131,7 +131,7 @@ theorem adj_iff_proj_adj {p q : Q n.succ} (h₀ : p 0 = q 0) : rw [← Fin.pred_inj (ha := (?ha : y ≠ 0)) (hb := (?hb : i.succ ≠ 0)), Fin.pred_succ] case ha => - contrapose! hy + contrapose hy rw [hy, h₀] case hb => apply Fin.succ_ne_zero diff --git a/Archive/Wiedijk100Theorems/PerfectNumbers.lean b/Archive/Wiedijk100Theorems/PerfectNumbers.lean index 3fbb21263e23a2..6a2e85fa4df2dc 100644 --- a/Archive/Wiedijk100Theorems/PerfectNumbers.lean +++ b/Archive/Wiedijk100Theorems/PerfectNumbers.lean @@ -62,7 +62,7 @@ theorem eq_two_pow_mul_odd {n : ℕ} (hpos : 0 < n) : ∃ k m : ℕ, n = 2 ^ k * refine ⟨hm, ?_⟩ rw [even_iff_two_dvd] have hg := h.not_pow_dvd_of_multiplicity_lt (Nat.lt_succ_self _) - contrapose! hg + contrapose hg rcases hg with ⟨k, rfl⟩ apply Dvd.intro k rw [pow_succ, mul_assoc, ← hm] @@ -105,7 +105,7 @@ theorem eq_two_pow_mul_prime_mersenne_of_even_perfect {n : ℕ} (ev : Even n) (p apply ne_of_lt _ jcon2 rw [mersenne, ← Nat.pred_eq_sub_one, Nat.lt_pred_iff, ← pow_one (Nat.succ 1)] apply pow_lt_pow_right₀ (Nat.lt_succ_self 1) (Nat.succ_lt_succ k.succ_pos) - contrapose! hm + contrapose hm simp [hm] /-- The Euclid-Euler theorem characterizing even perfect numbers -/ diff --git a/Archive/Wiedijk100Theorems/SolutionOfCubicQuartic.lean b/Archive/Wiedijk100Theorems/SolutionOfCubicQuartic.lean index cee897a3533003..4e3508a10013dd 100644 --- a/Archive/Wiedijk100Theorems/SolutionOfCubicQuartic.lean +++ b/Archive/Wiedijk100Theorems/SolutionOfCubicQuartic.lean @@ -91,7 +91,7 @@ theorem cubic_depressed_eq_zero_iff (hω : IsPrimitiveRoot ω 3) (hp_nonzero : p rw [h₁] apply Eq.congr_left have hs_nonzero : s ≠ 0 := by - contrapose! hp_nonzero with hs_nonzero + contrapose hp_nonzero with hs_nonzero linear_combination -1 * ht + t * hs_nonzero rw [← mul_left_inj' (pow_ne_zero 3 hs_nonzero)] have H := cube_root_of_unity_sum hω @@ -172,7 +172,7 @@ theorem quartic_depressed_eq_zero_iff have hi2 : (2 : K) ≠ 0 := Invertible.ne_zero _ have h4 : (4 : K) = 2 ^ 2 := by norm_num have hs_nonzero : s ≠ 0 := by - contrapose! hq_nonzero with hs0 + contrapose hq_nonzero with hs0 linear_combination (exp := 2) -hu + (4 * r - u ^ 2) * hs + (u ^ 2 * s - 4 * r * s) * hs0 calc _ ↔ 4 * (x ^ 4 + p * x ^ 2 + q * x + r) = 0 := by simp [h4, hi2] diff --git a/Mathlib/Algebra/Algebra/Spectrum/Basic.lean b/Mathlib/Algebra/Algebra/Spectrum/Basic.lean index 327ea670243101..2d3b1f95f0b8bb 100644 --- a/Mathlib/Algebra/Algebra/Spectrum/Basic.lean +++ b/Mathlib/Algebra/Algebra/Spectrum/Basic.lean @@ -440,7 +440,7 @@ lemma spectrum.units_conjugate {a : A} {u : Aˣ} : simp [mul_assoc] intro a u μ hμ rw [spectrum.mem_iff] at hμ ⊢ - contrapose! hμ + contrapose hμ simpa [mul_sub, sub_mul, Algebra.right_comm] using u.isUnit.mul hμ |>.mul u⁻¹.isUnit /-- Conjugation by a unit preserves the spectrum, inverse on left. -/ diff --git a/Mathlib/Algebra/GCDMonoid/Basic.lean b/Mathlib/Algebra/GCDMonoid/Basic.lean index 072f2874678fa6..b269f4d38a43e6 100644 --- a/Mathlib/Algebra/GCDMonoid/Basic.lean +++ b/Mathlib/Algebra/GCDMonoid/Basic.lean @@ -1013,7 +1013,7 @@ noncomputable def gcdMonoidOfGCD [DecidableEq α] (gcd : α → α → α) · rfl have h := (Classical.choose_spec ((gcd_dvd_left a 0).trans (Dvd.intro 0 rfl))).symm have a0' : gcd a 0 ≠ 0 := by - contrapose! a0 + contrapose a0 rw [← associated_zero_iff_eq_zero, ← a0] exact associated_of_dvd_dvd (dvd_gcd (dvd_refl a) (dvd_zero a)) (gcd_dvd_left _ _) apply Or.resolve_left (mul_eq_zero.1 _) a0' @@ -1051,7 +1051,7 @@ noncomputable def normalizedGCDMonoidOfGCD [NormalizationMonoid α] [DecidableEq · rw [hl, zero_mul] have h1 : gcd a b ≠ 0 := by have hab : a * b ≠ 0 := mul_ne_zero a0 hb - contrapose! hab + contrapose hab rw [← normalize_eq_zero, ← this, hab, zero_mul] have h2 : normalize (gcd a b * l) = gcd a b * l := by rw [this, normalize_idem] rw [← normalize_gcd] at this diff --git a/Mathlib/Algebra/Group/Irreducible/Indecomposable.lean b/Mathlib/Algebra/Group/Irreducible/Indecomposable.lean index ef97f0b2b4d67a..84d433be7f56d1 100644 --- a/Mathlib/Algebra/Group/Irreducible/Indecomposable.lean +++ b/Mathlib/Algebra/Group/Irreducible/Indecomposable.lean @@ -102,7 +102,7 @@ lemma Submonoid.closure_image_isMulIndecomposable_baseOf [Finite ι] have ⟨(hi₀ : 1 < f (v i)), (hi₁ : v i ∉ _)⟩ : i ∈ s := hi.prop have hi₂ (k : ι) (hk₀ : 1 < f (v k)) (hk₁ : f (v k) < f (v i)) : v k ∈ closure (v '' t) := by by_contra hk₂; exact not_le.mpr hk₁ <| hi.le_of_le ⟨hk₀, hk₂⟩ hk₁.le - have hi₃ : i ∉ t := by contrapose! hi₁; exact subset_closure <| mem_image_of_mem v hi₁ + have hi₃ : i ∉ t := by contrapose hi₁; exact subset_closure <| mem_image_of_mem v hi₁ obtain ⟨j, k, hj, hk, hjk⟩ : ∃ (j k : ι) (hj : 1 < f (v j)) (hk : 1 < f (v k)), v i = v j * v k := by grind [IsMulIndecomposable] diff --git a/Mathlib/Algebra/Group/UniqueProds/Basic.lean b/Mathlib/Algebra/Group/UniqueProds/Basic.lean index 1957418e2b831f..7ca8f897c7837f 100644 --- a/Mathlib/Algebra/Group/UniqueProds/Basic.lean +++ b/Mathlib/Algebra/Group/UniqueProds/Basic.lean @@ -560,7 +560,7 @@ theorem of_mulOpposite (h : TwoUniqueProds Gᵐᵒᵖ) : TwoUniqueProds G where simp_rw [mem_product] at h1 h2 ⊢ refine ⟨(_, _), ⟨?_, ?_⟩, (_, _), ⟨?_, ?_⟩, ?_, hu1.of_mulOpposite, hu2.of_mulOpposite⟩ pick_goal 5 - · contrapose! hne; rw [Prod.ext_iff] at hne ⊢ + · contrapose hne; rw [Prod.ext_iff] at hne ⊢ exact ⟨unop_injective hne.2, unop_injective hne.1⟩ all_goals apply (mem_map' f).mp exacts [h1.2, h1.1, h2.2, h2.1] diff --git a/Mathlib/Algebra/GroupWithZero/Associated.lean b/Mathlib/Algebra/GroupWithZero/Associated.lean index 3a3cf67f419dca..f954c4071a8ea3 100644 --- a/Mathlib/Algebra/GroupWithZero/Associated.lean +++ b/Mathlib/Algebra/GroupWithZero/Associated.lean @@ -338,7 +338,7 @@ theorem Associated.of_pow_associated_of_prime' [CommMonoidWithZero M] [IsCancelM lemma Irreducible.isRelPrime_iff_not_dvd [Monoid M] {p n : M} (hp : Irreducible p) : IsRelPrime p n ↔ ¬ p ∣ n := by refine ⟨fun h contra ↦ hp.not_isUnit (h dvd_rfl contra), fun hpn d hdp hdn ↦ ?_⟩ - contrapose! hpn + contrapose hpn suffices Associated p d from this.dvd.trans hdn exact (hp.dvd_iff.mp hdp).resolve_left hpn @@ -669,7 +669,7 @@ theorem dvdNotUnit_of_lt {a b : Associates M} (hlt : a < b) : DvdNotUnit a b := apply dvd_zero rcases hlt with ⟨⟨x, rfl⟩, ndvd⟩ refine ⟨x, ?_, rfl⟩ - contrapose! ndvd + contrapose ndvd rcases ndvd with ⟨u, rfl⟩ simp diff --git a/Mathlib/Algebra/Lie/Semisimple/Basic.lean b/Mathlib/Algebra/Lie/Semisimple/Basic.lean index ca03a9c20385d5..9cf49fa76d1e1c 100644 --- a/Mathlib/Algebra/Lie/Semisimple/Basic.lean +++ b/Mathlib/Algebra/Lie/Semisimple/Basic.lean @@ -86,7 +86,7 @@ instance : LieModule.IsIrreducible R L L := by suffices Nontrivial (LieIdeal R L) from ⟨IsSimple.eq_bot_or_eq_top⟩ rw [LieSubmodule.nontrivial_iff, ← not_subsingleton_iff_nontrivial] have _i : ¬ IsLieAbelian L := IsSimple.non_abelian R - contrapose! _i + contrapose _i infer_instance protected lemma isAtom_top : IsAtom (⊤ : LieIdeal R L) := isAtom_top @@ -185,7 +185,7 @@ lemma isSimple_of_isAtom (I : LieIdeal R L) (hI : IsAtom I) : IsSimple R I where exact x.2 -- So we need to show `J ≠ I` as ideals of `L`. -- This follows from our assumption that `J ≠ ⊤` as ideals of `I`. - contrapose! hJ + contrapose hJ rw [eq_top_iff] rintro ⟨x, hx⟩ - rw [← hJ] at hx @@ -260,7 +260,7 @@ lemma finitelyAtomistic : ∀ s : Finset (LieIdeal R L), ↑s ⊆ {I : LieIdeal exact LieSubmodule.lie_mem_lie j.2 hx -- Indeed `J ⊓ I = ⊥`, since `J` is an atom that is not contained in `I`. apply ((hs hJs).le_iff.mp _).resolve_right - · contrapose! hJI + · contrapose hJI rw [← hJI] exact inf_le_right exact inf_le_left diff --git a/Mathlib/Algebra/Lie/Sl2.lean b/Mathlib/Algebra/Lie/Sl2.lean index 29b8862c0f8009..6417564571f741 100644 --- a/Mathlib/Algebra/Lie/Sl2.lean +++ b/Mathlib/Algebra/Lie/Sl2.lean @@ -65,12 +65,12 @@ lemma lie_lie_smul_f (t : IsSl2Triple h e f) : ⁅h, f⁆ = -((2 : R) • f) := lemma e_ne_zero (t : IsSl2Triple h e f) : e ≠ 0 := by have := t.h_ne_zero - contrapose! this + contrapose this simpa [this] using t.lie_e_f.symm lemma f_ne_zero (t : IsSl2Triple h e f) : f ≠ 0 := by have := t.h_ne_zero - contrapose! this + contrapose this simpa [this] using t.lie_e_f.symm variable {R} diff --git a/Mathlib/Algebra/Lie/Weights/Basic.lean b/Mathlib/Algebra/Lie/Weights/Basic.lean index f0179d1949eca9..890735c20ec770 100644 --- a/Mathlib/Algebra/Lie/Weights/Basic.lean +++ b/Mathlib/Algebra/Lie/Weights/Basic.lean @@ -278,7 +278,7 @@ def equivSetOf : Weight R L M ≃ {χ : L → R | genWeightSpace M χ ≠ ⊥} w lemma genWeightSpaceOf_ne_bot (χ : Weight R L M) (x : L) : genWeightSpaceOf M (χ x) x ≠ ⊥ := by have : ⨅ x, genWeightSpaceOf M (χ x) x ≠ ⊥ := χ.genWeightSpace_ne_bot - contrapose! this + contrapose this rw [eq_bot_iff] exact le_of_le_of_eq (iInf_le _ _) this diff --git a/Mathlib/Algebra/Lie/Weights/Killing.lean b/Mathlib/Algebra/Lie/Weights/Killing.lean index e9b52edadfb495..906303c848f8c0 100644 --- a/Mathlib/Algebra/Lie/Weights/Killing.lean +++ b/Mathlib/Algebra/Lie/Weights/Killing.lean @@ -440,7 +440,7 @@ lemma disjoint_ker_weight_corootSpace (α : Weight K H L) : lemma root_apply_cartanEquivDual_symm_ne_zero {α : Weight K H L} (hα : α.IsNonZero) : α ((cartanEquivDual H).symm α) ≠ 0 := by - contrapose! hα + contrapose hα suffices (cartanEquivDual H).symm α ∈ α.ker ⊓ corootSpace α by rw [(disjoint_ker_weight_corootSpace α).eq_bot] at this simpa using this @@ -540,7 +540,7 @@ lemma traceForm_eq_zero_of_mem_ker_of_mem_span_coroot {α : Weight K H L} {x y : simp [hα.eq, hβ.eq] else have hβ : β.IsNonZero := by - contrapose! hα + contrapose hα simp only [← coroot_eq_zero_iff] at hα ⊢ rwa [hyp] have : α.ker = β.ker := by @@ -600,7 +600,7 @@ lemma _root_.IsSl2Triple.h_eq_coroot {α : Weight K H L} (hα : α.IsNonZero) use (2 • (α α')⁻¹) * (killingForm K L e f)⁻¹ have hef₀ : killingForm K L e f ≠ 0 := by have := ht.h_ne_zero - contrapose! this + contrapose this simpa [this] using h_eq rw [h_eq, smul_smul, mul_assoc, inv_mul_cancel₀ hef₀, mul_one, smul_assoc, coroot] diff --git a/Mathlib/Algebra/Module/Submodule/Union.lean b/Mathlib/Algebra/Module/Submodule/Union.lean index 8ee06a4640cccb..29dbb5e9fdb41e 100644 --- a/Mathlib/Algebra/Module/Submodule/Union.lean +++ b/Mathlib/Algebra/Module/Submodule/Union.lean @@ -43,7 +43,7 @@ lemma Submodule.iUnion_ssubset_of_forall_ne_top_of_card_lt (s : Finset ι) (p : · simpa using h₁ j replace h₂ : s.card + 1 < ENat.card K := by simpa [Finset.card_insert_of_notMem hj] using h₂ specialize hj' (lt_trans ENat.natCast_lt_succ h₂) - contrapose! hj' + contrapose hj' replace hj' : (p j : Set M) ∪ (⋃ i ∈ s, p i) = univ := by simpa only [Finset.mem_insert, iUnion_iUnion_eq_or_left] using hj' suffices (p j : Set M) ⊆ ⋃ i ∈ s, p i by rwa [union_eq_right.mpr this] at hj' diff --git a/Mathlib/Algebra/Module/ZLattice/Basic.lean b/Mathlib/Algebra/Module/ZLattice/Basic.lean index 4f01cca3921ae1..670b8bd0d92290 100644 --- a/Mathlib/Algebra/Module/ZLattice/Basic.lean +++ b/Mathlib/Algebra/Module/ZLattice/Basic.lean @@ -568,7 +568,7 @@ theorem ZLattice.rank [hs : IsZLattice K L] : finrank ℤ L = finrank K E := by rwa [h_card, ← topEquiv.finrank_eq, ← h_spanE, ← ht_span, finrank_span_set_eq_card ht_lin] -- Assume that `e ∪ {v}` is not `ℤ`-linear independent then we get the contradiction suffices ¬ LinearIndepOn ℤ id (insert v (Set.range e)) by - contrapose! this + contrapose this refine this.mono ?_ exact Set.insert_subset (Set.mem_of_mem_diff hv) (by simp [e, ht_inc]) -- We prove finally that `e ∪ {v}` is not ℤ-linear independent or, equivalently, diff --git a/Mathlib/Algebra/MvPolynomial/Eval.lean b/Mathlib/Algebra/MvPolynomial/Eval.lean index f26569ae329f9d..574e7e2fc76f42 100644 --- a/Mathlib/Algebra/MvPolynomial/Eval.lean +++ b/Mathlib/Algebra/MvPolynomial/Eval.lean @@ -455,7 +455,7 @@ theorem constantCoeff_comp_map (f : R →+* S₁) : theorem support_map_subset (p : MvPolynomial σ R) : (map f p).support ⊆ p.support := by simp only [Finset.subset_iff, mem_support_iff] intro x hx - contrapose! hx + contrapose hx rw [coeff_map, hx, map_zero] theorem support_map_of_injective (p : MvPolynomial σ R) {f : R →+* S₁} (hf : Injective f) : @@ -464,7 +464,7 @@ theorem support_map_of_injective (p : MvPolynomial σ R) {f : R →+* S₁} (hf · exact MvPolynomial.support_map_subset _ _ simp only [Finset.subset_iff, mem_support_iff] intro x hx - contrapose! hx + contrapose hx rw [coeff_map, ← f.map_zero] at hx exact hf hx diff --git a/Mathlib/Algebra/MvPolynomial/NoZeroDivisors.lean b/Mathlib/Algebra/MvPolynomial/NoZeroDivisors.lean index 5949040d22d7ec..df972cdcceac7a 100644 --- a/Mathlib/Algebra/MvPolynomial/NoZeroDivisors.lean +++ b/Mathlib/Algebra/MvPolynomial/NoZeroDivisors.lean @@ -123,7 +123,7 @@ theorem degreeOf_C_mul (j : σ) (c : R) (hc : c ∈ R⁰) : degreeOf j (C c * p) exact hp (rename_injective _ (Equiv.injective _) (by simpa using h)) simp_rw [ne_eq, renameEquiv_apply, algHom_C, algebraMap_eq, optionEquivLeft_C, Polynomial.leadingCoeff_C] - contrapose! hp' + contrapose hp' ext m apply hc.1 simpa using congr_arg (coeff m) hp' diff --git a/Mathlib/Algebra/Order/Archimedean/Hom.lean b/Mathlib/Algebra/Order/Archimedean/Hom.lean index 2be4c7abbed53b..6a7bb3d7eaac75 100644 --- a/Mathlib/Algebra/Order/Archimedean/Hom.lean +++ b/Mathlib/Algebra/Order/Archimedean/Hom.lean @@ -28,7 +28,7 @@ instance OrderRingHom.subsingleton [IsStrictOrderedRing β] [Archimedean β] : 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 with h₂ · exact h₂ g f x (Ne.symm h') (h'.lt_or_gt.resolve_left h) obtain ⟨q, hf, hg⟩ := exists_rat_btwn h diff --git a/Mathlib/Algebra/Order/Module/HahnEmbedding.lean b/Mathlib/Algebra/Order/Module/HahnEmbedding.lean index 860b791824d6bf..f62941aabb2aa1 100644 --- a/Mathlib/Algebra/Order/Module/HahnEmbedding.lean +++ b/Mathlib/Algebra/Order/Module/HahnEmbedding.lean @@ -609,7 +609,7 @@ theorem eval_smul [IsOrderedAddMonoid R] [Archimedean R] (k : K) (x : M) : exact Submodule.smul_mem _ _ hy simp [f.evalCoeff_eq hy, f.evalCoeff_eq hy', LinearPMap.map_smul] have h' : ¬∃ y : f.val.domain, y.val - k • x ∈ ball K c := by - contrapose! h + contrapose h obtain ⟨y, hy⟩ := h use k⁻¹ • y have heq : (k⁻¹ • y).val - x = k⁻¹ • (y.val - k • x) := by @@ -644,7 +644,7 @@ theorem archimedeanClassMk_le_of_eval_eq [IsOrderedAddMonoid R] [Archimedean R] set_option backward.isDefEq.respectTransparency false in theorem val_sub_ne_zero {x : M} (hx : x ∉ f.val.domain) (y : f.val.domain) : y.val - x ≠ 0 := by - contrapose! hx + contrapose hx obtain rfl : x = y.val := (sub_eq_zero.mp hx).symm simp @@ -781,7 +781,7 @@ set_option backward.isDefEq.respectTransparency false in theorem extendFun_strictMono [IsOrderedAddMonoid R] [Archimedean R] {x : M} (hx : x ∉ f.val.domain) : StrictMono (f.extendFun hx) := by have hx' {c : K} (hc : c ≠ 0) : -c • x ∉ f.val.domain := by - contrapose! hx + contrapose hx rwa [neg_smul, neg_mem_iff, Submodule.smul_mem_iff _ hc] at hx -- only need to prove `0 < f v` for `0 < v = z - y` intro y z hyz @@ -848,7 +848,7 @@ theorem truncLT_eval_mem_range_extendFun [IsOrderedAddMonoid R] [Archimedean R] · rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_lt hdc] rw [HahnSeries.coe_truncLTLinearMap, HahnSeries.coeff_truncLT_of_le hdc, eval, ofLex_toLex] apply f.evalCoeff_eq_zero - contrapose! h + contrapose h obtain ⟨y, hy⟩ := h exact ⟨y, Set.mem_of_mem_of_subset hy (by simpa using (ball_strictAnti K).antitone hdc)⟩ diff --git a/Mathlib/Algebra/Polynomial/CancelLeads.lean b/Mathlib/Algebra/Polynomial/CancelLeads.lean index ca71cbddbbdd97..963350a3567d4e 100644 --- a/Mathlib/Algebra/Polynomial/CancelLeads.lean +++ b/Mathlib/Algebra/Polynomial/CancelLeads.lean @@ -62,7 +62,7 @@ theorem natDegree_cancelLeads_lt_of_natDegree_le_natDegree_of_comm apply lt_of_le_of_ne · compute_degree! rwa [Nat.sub_add_cancel] - · contrapose! h0 + · contrapose h0 rw [← leadingCoeff_eq_zero, leadingCoeff, h0, mul_assoc, X_pow_mul, ← tsub_add_cancel_of_le h, add_comm _ p.natDegree] simp only [coeff_mul_X_pow, coeff_neg, coeff_C_mul, add_tsub_cancel_left, coeff_add] diff --git a/Mathlib/Algebra/Polynomial/Coeff.lean b/Mathlib/Algebra/Polynomial/Coeff.lean index 04e40e979c3f85..fd093df8b3d395 100644 --- a/Mathlib/Algebra/Polynomial/Coeff.lean +++ b/Mathlib/Algebra/Polynomial/Coeff.lean @@ -53,7 +53,7 @@ theorem support_smul [SMulZeroClass S R] (r : S) (p : R[X]) : support (r • p) ⊆ support p := by intro i hi rw [mem_support_iff] at hi ⊢ - contrapose! hi + contrapose hi simp [hi] open scoped Pointwise in diff --git a/Mathlib/Algebra/Polynomial/Derivative.lean b/Mathlib/Algebra/Polynomial/Derivative.lean index f03eb011b5d7e6..8e5b18bf65ce4b 100644 --- a/Mathlib/Algebra/Polynomial/Derivative.lean +++ b/Mathlib/Algebra/Polynomial/Derivative.lean @@ -689,7 +689,7 @@ theorem iterate_derivative_eq_zero_of_degree_lt {k : ℕ} {P : R[X]} (h : P.degr case pos hP' => simp [hP'] case neg hP' => have hP'' : P.natDegree ≠ 0 := by - contrapose! hP' + contrapose hP' exact derivative_of_natDegree_zero hP' refine ind <| (natDegree_lt_iff_degree_lt hP').mp ?_ linarith [(natDegree_lt_iff_degree_lt hP).mpr h, natDegree_derivative_lt hP''] diff --git a/Mathlib/Algebra/Polynomial/Div.lean b/Mathlib/Algebra/Polynomial/Div.lean index 0a7c01b4607fed..29a02efd5c24d1 100644 --- a/Mathlib/Algebra/Polynomial/Div.lean +++ b/Mathlib/Algebra/Polynomial/Div.lean @@ -172,7 +172,7 @@ theorem natDegree_modByMonic_lt (p : R[X]) {q : R[X]} (hmq : Monic q) (hq : q natDegree (p %ₘ q) < q.natDegree := by by_cases hpq : p %ₘ q = 0 · rw [hpq, natDegree_zero, Nat.pos_iff_ne_zero] - contrapose! hq + contrapose hq exact eq_one_of_monic_natDegree_zero hmq hq · haveI := Nontrivial.of_polynomial_ne hpq exact natDegree_lt_natDegree hpq (degree_modByMonic_lt p hmq) diff --git a/Mathlib/Algebra/Polynomial/Eval/Coeff.lean b/Mathlib/Algebra/Polynomial/Eval/Coeff.lean index c61f3852b9ea8d..d1398c79267c17 100644 --- a/Mathlib/Algebra/Polynomial/Eval/Coeff.lean +++ b/Mathlib/Algebra/Polynomial/Eval/Coeff.lean @@ -205,7 +205,7 @@ section Map theorem support_map_subset [Semiring R] [Semiring S] (f : R →+* S) (p : R[X]) : (map f p).support ⊆ p.support := by intro x - contrapose! + contrapose simp +contextual theorem support_map_of_injective [Semiring R] [Semiring S] (p : R[X]) {f : R →+* S} diff --git a/Mathlib/Algebra/Polynomial/FieldDivision.lean b/Mathlib/Algebra/Polynomial/FieldDivision.lean index 0c8fb88ceec119..c2045fbe577126 100644 --- a/Mathlib/Algebra/Polynomial/FieldDivision.lean +++ b/Mathlib/Algebra/Polynomial/FieldDivision.lean @@ -186,7 +186,7 @@ theorem isRoot_of_isRoot_of_dvd_derivative_mul [CharZero R] {f g : R[X]} (hf0 : (hfd : f ∣ f.derivative * g) {a : R} (haf : f.IsRoot a) : g.IsRoot a := by rcases hfd with ⟨r, hr⟩ have hdf0 : derivative f ≠ 0 := by - contrapose! haf + contrapose haf rw [eq_C_of_derivative_eq_zero haf] at hf0 ⊢ exact not_isRoot_C _ _ <| C_ne_zero.mp hf0 by_contra hg @@ -423,13 +423,13 @@ lemma natDegree_mod_lt [Field k] (p : k[X]) {q : k[X]} (hq : q.natDegree ≠ 0) (p % q).natDegree < q.natDegree := by have hq' : q.leadingCoeff ≠ 0 := by rw [leadingCoeff_ne_zero] - contrapose! hq + contrapose hq simp [hq] rw [mod_def] refine (natDegree_modByMonic_lt p ?_ ?_).trans_le ?_ · refine monic_mul_C_of_leadingCoeff_mul_eq_one ?_ rw [mul_inv_eq_one₀ hq'] - · contrapose! hq + · contrapose hq rw [← natDegree_mul_C_eq_of_mul_eq_one ((inv_mul_eq_one₀ hq').mpr rfl)] simp [hq] · exact natDegree_mul_C_le q q.leadingCoeff⁻¹ @@ -654,7 +654,7 @@ theorem isCoprime_of_is_root_of_eval_derivative_ne_zero {K : Type*} [Field K] (f refine Or.resolve_left (EuclideanDomain.dvd_or_coprime (X - C a) (f /ₘ (X - C a)) (irreducible_of_degree_eq_one (Polynomial.degree_X_sub_C a))) ?_ - contrapose! hf' with h + contrapose hf' with h have : X - C a ∣ derivative f := X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic f h rw [← modByMonic_eq_zero_iff_dvd (monic_X_sub_C _), modByMonic_X_sub_C_eq_C_eval] at this rwa [← C_inj, C_0] @@ -669,7 +669,7 @@ theorem irreducible_iff_degree_lt (p : R[X]) (hp0 : p ≠ 0) (hpu : ¬ IsUnit p) rw [← irreducible_mul_leadingCoeff_inv, (monic_mul_leadingCoeff_inv hp0).irreducible_iff_degree_lt] · simp [hp0, natDegree_mul_leadingCoeff_inv] - · contrapose! hpu + · contrapose hpu exact .of_mul_eq_one _ hpu /-- To check a polynomial `p` over a field is irreducible, it suffices to check there are no @@ -680,7 +680,7 @@ See also: `Polynomial.Monic.irreducible_iff_natDegree'`. theorem irreducible_iff_lt_natDegree_lt {p : R[X]} (hp0 : p ≠ 0) (hpu : ¬ IsUnit p) : Irreducible p ↔ ∀ q, Monic q → natDegree q ∈ Finset.Ioc 0 (natDegree p / 2) → ¬ q ∣ p := by have : p * C (leadingCoeff p)⁻¹ ≠ 1 := by - contrapose! hpu + contrapose hpu exact .of_mul_eq_one _ hpu rw [← irreducible_mul_leadingCoeff_inv, (monic_mul_leadingCoeff_inv hp0).irreducible_iff_lt_natDegree_lt this, diff --git a/Mathlib/Algebra/Polynomial/Monic.lean b/Mathlib/Algebra/Polynomial/Monic.lean index 5dd82b6a472e0e..82a16f5742970a 100644 --- a/Mathlib/Algebra/Polynomial/Monic.lean +++ b/Mathlib/Algebra/Polynomial/Monic.lean @@ -105,12 +105,12 @@ theorem Monic.add_of_right (hq : Monic q) (hpq : degree p < degree q) : Monic (p rwa [Monic, leadingCoeff_add_of_degree_lt hpq] theorem Monic.of_mul_monic_left (hp : p.Monic) (hpq : (p * q).Monic) : q.Monic := by - contrapose! hpq + contrapose hpq rw [Monic.def] at hpq ⊢ rwa [leadingCoeff_monic_mul hp] theorem Monic.of_mul_monic_right (hq : q.Monic) (hpq : (p * q).Monic) : p.Monic := by - contrapose! hpq + contrapose hpq rw [Monic.def] at hpq ⊢ rwa [leadingCoeff_mul_monic hq] @@ -541,7 +541,7 @@ theorem natDegree_smul_of_smul_regular {S : Type*} [SMulZeroClass S R] {k : S} · simp [hp] rw [← Nat.cast_inj (R := WithBot ℕ), ← degree_eq_natDegree hp, ← degree_eq_natDegree, degree_smul_of_smul_regular p h] - contrapose! hp + contrapose hp rw [← smul_zero k] at hp exact h.polynomial hp diff --git a/Mathlib/Algebra/Polynomial/OfFn.lean b/Mathlib/Algebra/Polynomial/OfFn.lean index 8e5b652cb13b01..db8f8fbcbea18f 100644 --- a/Mathlib/Algebra/Polynomial/OfFn.lean +++ b/Mathlib/Algebra/Polynomial/OfFn.lean @@ -60,7 +60,7 @@ theorem ofFn_zero (n : ℕ) : ofFn n (0 : Fin n → R) = 0 := by simp theorem ofFn_zero' (v : Fin 0 → R) : ofFn 0 v = 0 := rfl lemma ne_zero_of_ofFn_ne_zero {n : ℕ} {v : Fin n → R} (h : ofFn n v ≠ 0) : n ≠ 0 := by - contrapose! h + contrapose h subst h simp diff --git a/Mathlib/Algebra/Tropical/Lattice.lean b/Mathlib/Algebra/Tropical/Lattice.lean index 43ad814ce39d32..9ad8fd20da51b0 100644 --- a/Mathlib/Algebra/Tropical/Lattice.lean +++ b/Mathlib/Algebra/Tropical/Lattice.lean @@ -68,7 +68,7 @@ instance [ConditionallyCompleteLinearOrder R] : ConditionallyCompleteLinearOrder have : Set.range untrop = (Set.univ : Set R) := Equiv.range_eq_univ tropEquiv.symm simp only [sSup, Set.image_empty, trop_inj_iff] apply csSup_of_not_bddAbove - contrapose! hs + contrapose hs change BddAbove (tropOrderIso.symm '' s) at hs exact tropOrderIso.symm.bddAbove_image.1 hs csInf_of_not_bddBelow := by @@ -76,6 +76,6 @@ instance [ConditionallyCompleteLinearOrder R] : ConditionallyCompleteLinearOrder have : Set.range untrop = (Set.univ : Set R) := Equiv.range_eq_univ tropEquiv.symm simp only [sInf, Set.image_empty, trop_inj_iff] apply csInf_of_not_bddBelow - contrapose! hs + contrapose hs change BddBelow (tropOrderIso.symm '' s) at hs exact tropOrderIso.symm.bddBelow_image.1 hs } diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Formula.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Formula.lean index 2e73e148e2c07b..91e1adfba4b9fe 100644 --- a/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Formula.lean +++ b/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Formula.lean @@ -139,7 +139,7 @@ lemma Y_ne_negY_of_Y_ne [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P y ≠ W'.negY P := by have hy' : P y * Q z ^ 3 - W'.negY Q * P z ^ 3 = 0 := (mul_eq_zero.mp <| Y_sub_Y_mul_Y_sub_negY hP hQ hx).resolve_left <| sub_ne_zero_of_ne hy - contrapose! hy + contrapose hy linear_combination (norm := ring1) Y_sub_Y_add_Y_sub_negY hx + Q z ^ 3 * hy - hy' lemma Y_ne_negY_of_Y_ne' [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) @@ -147,7 +147,7 @@ lemma Y_ne_negY_of_Y_ne' [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equatio (hy : P y * Q z ^ 3 ≠ W'.negY Q * P z ^ 3) : P y ≠ W'.negY P := by have hy' : P y * Q z ^ 3 - Q y * P z ^ 3 = 0 := (mul_eq_zero.mp <| Y_sub_Y_mul_Y_sub_negY hP hQ hx).resolve_right <| sub_ne_zero_of_ne hy - contrapose! hy + contrapose hy linear_combination (norm := ring1) Y_sub_Y_add_Y_sub_negY hx + Q z ^ 3 * hy - hy' lemma Y_eq_negY_of_Y_eq [NoZeroDivisors R] {P Q : Fin 3 → R} (hQz : Q z ≠ 0) diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Formula.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Formula.lean index 8b223c119d798f..d9b7d05385c95f 100644 --- a/Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Formula.lean +++ b/Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Formula.lean @@ -137,14 +137,14 @@ lemma Y_ne_negY_of_Y_ne [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation (hQ : W'.Equation Q) (hPz : P z ≠ 0) (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z) (hy : P y * Q z ≠ Q y * P z) : P y ≠ W'.negY P := by have hy' : P y * Q z - W'.negY Q * P z = 0 := sub_eq_zero.mpr <| Y_eq_of_Y_ne hP hQ hPz hQz hx hy - contrapose! hy + contrapose hy linear_combination (norm := ring1) Y_sub_Y_add_Y_sub_negY hx + Q z * hy - hy' lemma Y_ne_negY_of_Y_ne' [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hPz : P z ≠ 0) (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z) (hy : P y * Q z ≠ W'.negY Q * P z) : P y ≠ W'.negY P := by have hy' : P y * Q z - Q y * P z = 0 := sub_eq_zero.mpr <| Y_eq_of_Y_ne' hP hQ hPz hQz hx hy - contrapose! hy + contrapose hy linear_combination (norm := ring1) Y_sub_Y_add_Y_sub_negY hx + Q z * hy - hy' lemma Y_eq_negY_of_Y_eq [NoZeroDivisors R] {P Q : Fin 3 → R} (hQz : Q z ≠ 0) diff --git a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean index fa425bf50243af..4e86867a65921d 100644 --- a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean +++ b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean @@ -429,7 +429,7 @@ def openCoverOfMapIrrelevantEqTop : X.OpenCover := · intro x hx rw [← DirectSum.sum_support_decompose 𝒜 x] refine Ideal.sum_mem _ fun c hc ↦ ?_ - have : c ≠ 0 := by contrapose! hc; simpa [hc] using hx + have : c ≠ 0 := by contrapose hc; simpa [hc] using hx exact Ideal.subset_span ⟨⟨c, _, this.bot_lt, by simp⟩, rfl⟩ ext1 apply compl_injective diff --git a/Mathlib/Analysis/Analytic/IsolatedZeros.lean b/Mathlib/Analysis/Analytic/IsolatedZeros.lean index 47acf6695e6992..5815500f7fd8d7 100644 --- a/Mathlib/Analysis/Analytic/IsolatedZeros.lean +++ b/Mathlib/Analysis/Analytic/IsolatedZeros.lean @@ -192,7 +192,7 @@ theorem exists_eventuallyEq_pow_smul_nonzero_iff (hf : AnalyticAt 𝕜 f z₀) : ∀ᶠ z in 𝓝 z₀, f z = (z - z₀) ^ n • g z) ↔ (¬∀ᶠ z in 𝓝 z₀, f z = 0) := by constructor · rintro ⟨n, g, hg_an, hg_ne, hg_eq⟩ - contrapose! hg_ne + contrapose hg_ne apply EventuallyEq.eq_of_nhds rw [EventuallyEq, ← AnalyticAt.frequently_eq_iff_eventually_eq hg_an analyticAt_const] refine (eventually_nhdsWithin_iff.mpr ?_).frequently @@ -324,7 +324,7 @@ theorem AnalyticAt.preimage_of_nhdsNE {x : 𝕜} {f : 𝕜 → E} {s : Set E} (h have : ∀ᶠ (z : 𝕜) in 𝓝 x, f z ∈ insert (f x) s := by filter_upwards [hfx.continuousAt.preimage_mem_nhds (insert_mem_nhds_iff.2 hs)] tauto - contrapose! h₂f with h + contrapose h₂f with h rw [eventuallyConst_iff_exists_eventuallyEq] use f x rw [EventuallyEq, ← hfx.frequently_eq_iff_eventually_eq analyticAt_const] diff --git a/Mathlib/Analysis/Analytic/Order.lean b/Mathlib/Analysis/Analytic/Order.lean index 33476c7512d42b..a740430c245744 100644 --- a/Mathlib/Analysis/Analytic/Order.lean +++ b/Mathlib/Analysis/Analytic/Order.lean @@ -415,7 +415,7 @@ lemma AnalyticAt.exists_eq_sum_add_pow_mul [CharZero 𝕜] [CompleteSpace E] · simp only [if_neg hz] rw [smul_inv_smul₀] · module - · contrapose! hz + · contrapose hz exact (pow_eq_zero_iff'.mp hz).1 ▸ mem_of_mem_nhds hU0 end NormedSpace diff --git a/Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean b/Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean index 752f11b6f45519..c028e1390ef8b5 100644 --- a/Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean +++ b/Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean @@ -169,7 +169,7 @@ theorem IsOpen.exists_contDiff_support_eq {n : ℕ∞} {s : Set E} (hs : IsOpen · apply Subset.antisymm · intro x hx simp only [Pi.smul_apply, smul_eq_mul, mem_support, Ne] at hx - contrapose! hx + contrapose hx have : ∀ n, g n x = 0 := by intro n contrapose! hx diff --git a/Mathlib/Analysis/Calculus/FDeriv/Add.lean b/Mathlib/Analysis/Calculus/FDeriv/Add.lean index 5b2b4b747cdf39..986b9b3b7080b0 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Add.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Add.lean @@ -111,7 +111,7 @@ theorem fderivWithin_const_smul_of_invertible (c : R) [Invertible c] by_cases h : DifferentiableWithinAt 𝕜 f s x · exact (h.hasFDerivWithinAt.const_smul c).fderivWithin hs · have : ¬DifferentiableWithinAt 𝕜 (c • f) s x := by - contrapose! h + contrapose h exact (differentiableWithinAt_smul_iff c).mp h simp [fderivWithin_zero_of_not_differentiableWithinAt h, fderivWithin_zero_of_not_differentiableWithinAt this] diff --git a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean index 19e317f6ca63ad..5c81f494a2fa29 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Analytic.lean @@ -758,13 +758,13 @@ theorem hasFTaylorSeriesUpTo_iteratedFDeriv : apply h simp_rw [← Equiv.embeddingFinSucc_snd e] · have hkf : k ∉ Set.range (Equiv.embeddingFinSucc n ι e).1 := by - contrapose! hke + contrapose hke rw [Equiv.embeddingFinSucc_fst] at hke exact Set.range_comp_subset_range _ _ hke simp only [hke, hkf, ↓reduceDIte, Pi.compRightL, ContinuousLinearMap.coe_mk', LinearMap.coe_mk, AddHom.coe_mk] rw [Function.update_of_ne] - contrapose! hke + contrapose hke rw [show k = _ from Subtype.ext_iff.1 hke, Equiv.embeddingFinSucc_snd e] exact Set.mem_range_self _ · rintro n - diff --git a/Mathlib/Analysis/Calculus/FDeriv/Const.lean b/Mathlib/Analysis/Calculus/FDeriv/Const.lean index 05a80e44a13b74..a35d81e96fb6e0 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Const.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Const.lean @@ -335,7 +335,7 @@ it is differentiable within `s` at `x`. -/ lemma differentiableWithinAt_of_fderivWithin_injective (hf : Injective (fderivWithin 𝕜 f s x)) : DifferentiableWithinAt 𝕜 f s x := by nontriviality E - contrapose! hf + contrapose hf rw [fderivWithin_zero_of_not_differentiableWithinAt hf] exact not_injective_const diff --git a/Mathlib/Analysis/Calculus/LagrangeMultipliers.lean b/Mathlib/Analysis/Calculus/LagrangeMultipliers.lean index 0b21c2093b7304..1a2d30db0a7667 100644 --- a/Mathlib/Analysis/Calculus/LagrangeMultipliers.lean +++ b/Mathlib/Analysis/Calculus/LagrangeMultipliers.lean @@ -87,7 +87,7 @@ theorem IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d {f : E → ℝ} (hφ' : HasStrictFDerivAt φ φ' x₀) : ∃ a b : ℝ, (a, b) ≠ 0 ∧ a • f' + b • φ' = 0 := by obtain ⟨Λ, Λ₀, hΛ, hfΛ⟩ := hextr.exists_linear_map_of_hasStrictFDerivAt hf' hφ' refine ⟨Λ 1, Λ₀, ?_, ?_⟩ - · contrapose! hΛ + · contrapose hΛ simp only [Prod.mk_eq_zero] at hΛ ⊢ refine ⟨LinearMap.ext fun x => ?_, hΛ.2⟩ simpa [hΛ.1] using Λ.map_smul x 1 diff --git a/Mathlib/Analysis/Calculus/Rademacher.lean b/Mathlib/Analysis/Calculus/Rademacher.lean index 15119acd30987d..8f768fe10fdca6 100644 --- a/Mathlib/Analysis/Calculus/Rademacher.lean +++ b/Mathlib/Analysis/Calculus/Rademacher.lean @@ -150,11 +150,11 @@ theorem integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul' _ = K.indicator (fun x ↦ (C * ‖v‖) * ‖g x‖) x := by rw [indicator_of_mem hx] · have A : f x = 0 := by rw [← Function.notMem_support] - contrapose! hx + contrapose hx exact self_subset_cthickening _ (subset_tsupport _ hx) have B : f (x + t • v) = 0 := by rw [← Function.notMem_support] - contrapose! hx + contrapose hx apply mem_cthickening_of_dist_le _ _ (‖v‖) (tsupport f) (subset_tsupport _ hx) simp only [dist_eq_norm, sub_add_cancel_left, norm_neg, norm_smul, Real.norm_eq_abs, abs_of_nonneg t_pos.le] diff --git a/Mathlib/Analysis/Calculus/TangentCone/Basic.lean b/Mathlib/Analysis/Calculus/TangentCone/Basic.lean index 9629bc78ec8bc0..6b15b633c211e8 100644 --- a/Mathlib/Analysis/Calculus/TangentCone/Basic.lean +++ b/Mathlib/Analysis/Calculus/TangentCone/Basic.lean @@ -175,7 +175,7 @@ theorem tangentConeAt_subset_zero [T2Space E] (hx : ¬AccPt x (𝓟 s)) : tangen theorem AccPt.of_mem_tangentConeAt_ne_zero [T2Space E] {y : E} (hy : y ∈ tangentConeAt 𝕜 s x) (hy₀ : y ≠ 0) : AccPt x (𝓟 s) := by - contrapose! hy₀ + contrapose hy₀ exact tangentConeAt_subset_zero hy₀ hy theorem UniqueDiffWithinAt.accPt [T2Space E] [Nontrivial E] (h : UniqueDiffWithinAt 𝕜 s x) : diff --git a/Mathlib/Analysis/Calculus/TangentCone/ProperSpace.lean b/Mathlib/Analysis/Calculus/TangentCone/ProperSpace.lean index e96a195ec05530..d19c71fbd30466 100644 --- a/Mathlib/Analysis/Calculus/TangentCone/ProperSpace.lean +++ b/Mathlib/Analysis/Calculus/TangentCone/ProperSpace.lean @@ -52,7 +52,7 @@ theorem tangentConeAt_nonempty_of_properSpace [ProperSpace E] Metric.mem_ball, not_lt, true_and, le_c n] refine ⟨l, ?_, ?_⟩; swap · push _ ∈ _ - contrapose! l_mem + contrapose l_mem simp only [one_div, l_mem, mem_diff, Metric.mem_closedBall, dist_self, zero_le_one, Metric.mem_ball, inv_pos, norm_pos_iff, ne_eq, not_not, true_and] contrapose! hr diff --git a/Mathlib/Analysis/Complex/Conformal.lean b/Mathlib/Analysis/Complex/Conformal.lean index 613972d5118af4..44c1102980715d 100644 --- a/Mathlib/Analysis/Complex/Conformal.lean +++ b/Mathlib/Analysis/Complex/Conformal.lean @@ -124,7 +124,7 @@ theorem isConformalMap_iff_is_complex_or_conj_linear : · exact fun h => ⟨h.is_complex_or_conj_linear, h.ne_zero⟩ · rintro ⟨⟨map, rfl⟩ | ⟨map, hmap⟩, h₂⟩ · refine isConformalMap_complex_linear ?_ - contrapose! h₂ with w + contrapose h₂ with w simp only [w, restrictScalars_zero] · have minor₁ : g = map.restrictScalars ℝ ∘L ↑conjCLE := by ext1 @@ -132,7 +132,7 @@ theorem isConformalMap_iff_is_complex_or_conj_linear : conjCLE_apply, starRingEnd_self_apply] rw [minor₁] at h₂ ⊢ refine isConformalMap_complex_linear_conj ?_ - contrapose! h₂ with w + contrapose h₂ with w simp only [w, restrictScalars_zero, zero_comp] end ConformalIntoComplexPlane diff --git a/Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean b/Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean index 25299bc563ea3f..3b2730d8745fc2 100644 --- a/Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean +++ b/Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean @@ -41,7 +41,7 @@ lemma denom_neg (g : GL (Fin 2) ℝ) (z : ℂ) : denom (-g) z = -(denom g z) := theorem linear_ne_zero_of_im {cd : Fin 2 → ℝ} {z : ℂ} (hz : z.im ≠ 0) (h : cd ≠ 0) : (cd 0 : ℂ) * z + cd 1 ≠ 0 := by - contrapose! h + contrapose h have : cd 0 = 0 := by -- we will need this twice apply_fun Complex.im at h diff --git a/Mathlib/Analysis/Convex/Between.lean b/Mathlib/Analysis/Convex/Between.lean index 957e9d0ca4125b..fa7552f8864491 100644 --- a/Mathlib/Analysis/Convex/Between.lean +++ b/Mathlib/Analysis/Convex/Between.lean @@ -1118,7 +1118,7 @@ theorem AffineIndependent.not_wbtw_of_injective {ι} (i j k : ι) ¬ Wbtw R (T i) (T j) (T k) := by replace hT := hT.comp_embedding ⟨_, h⟩ rw [affineIndependent_iff_not_collinear] at hT - contrapose! hT + contrapose hT simp [Set.range_comp, Set.image_insert_eq, hT.symm.collinear] variable (R) diff --git a/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean b/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean index 6641f662a2067f..94dfe931b0ba52 100644 --- a/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean +++ b/Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean @@ -105,7 +105,7 @@ theorem one_add_mul_self_lt_rpow_one_add {s : ℝ} (hs : -1 ≤ s) (hs' : s ≠ · exact hs2.trans_lt (rpow_pos_of_pos hs1 _) have hs3 : 1 + s ≠ 1 := hs' ∘ add_eq_left.mp have hs4 : 1 + p * s ≠ 1 := by - contrapose! hs'; rwa [add_eq_left, mul_eq_zero, eq_false_intro hp'.ne', false_or] at hs' + contrapose hs'; rwa [add_eq_left, mul_eq_zero, eq_false_intro hp'.ne', false_or] at hs' rw [rpow_def_of_pos hs1, ← exp_log hs2] apply exp_strictMono rcases lt_or_gt_of_ne hs' with hs' | hs' @@ -146,7 +146,7 @@ theorem rpow_one_add_lt_one_add_mul_self {s : ℝ} (hs : -1 ≤ s) (hs' : s ≠ · exact neg_one_lt_zero.trans (mul_pos hp1 h) have hs3 : 1 + s ≠ 1 := hs' ∘ add_eq_left.mp have hs4 : 1 + p * s ≠ 1 := by - contrapose! hs'; rwa [add_eq_left, mul_eq_zero, eq_false_intro hp1.ne', false_or] at hs' + contrapose hs'; rwa [add_eq_left, mul_eq_zero, eq_false_intro hp1.ne', false_or] at hs' rw [rpow_def_of_pos hs1, ← exp_log hs2] apply exp_strictMono rcases lt_or_gt_of_ne hs' with hs' | hs' @@ -219,7 +219,7 @@ theorem strictConcaveOn_log_Iio : StrictConcaveOn ℝ (Iio 0) log := by intro x (hx : x < 0) y (hy : y < 0) hxy a b ha hb hab have hx' : 0 < -x := by linarith have hy' : 0 < -y := by linarith - have hxy' : -x ≠ -y := by contrapose! hxy; linarith + have hxy' : -x ≠ -y := by contrapose hxy; linarith calc a • log x + b • log y = a • log (-x) + b • log (-y) := by simp_rw [log_neg_eq_log] _ < log (a • -x + b • -y) := strictConcaveOn_log_Ioi.2 hx' hy' hxy' ha hb hab diff --git a/Mathlib/Analysis/Convex/Star.lean b/Mathlib/Analysis/Convex/Star.lean index 217bd3c0f25245..a375ccd0faeee6 100644 --- a/Mathlib/Analysis/Convex/Star.lean +++ b/Mathlib/Analysis/Convex/Star.lean @@ -369,7 +369,7 @@ variable [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E] [Module 𝕜 E lemma starConvex_compl_Iic (h : x < y) : StarConvex 𝕜 y (Iic x)ᶜ := by refine (starConvex_iff_forall_pos <| by simp [h.not_ge]).mpr fun z hz a b ha hb hab ↦ ?_ rw [mem_compl_iff, mem_Iic] at hz ⊢ - contrapose! hz + contrapose hz refine (lt_of_smul_lt_smul_of_nonneg_left ?_ hb.le).le calc b • z ≤ (a + b) • x - a • y := by rwa [le_sub_iff_add_le', hab, one_smul] diff --git a/Mathlib/Analysis/Convolution.lean b/Mathlib/Analysis/Convolution.lean index e9efff5c11e28d..bea024fb3e1b1d 100644 --- a/Mathlib/Analysis/Convolution.lean +++ b/Mathlib/Analysis/Convolution.lean @@ -574,7 +574,7 @@ theorem continuousOn_convolution_right_with_param {g : P → G → E'} {s : Set (hf.integrableOn_isCompact k'_comp) rintro ⟨p, x⟩ y ⟨hp, hx⟩ hy apply hgs p _ hp - contrapose! hy + contrapose hy exact ⟨y - x, by simpa using hy, x, hx, by simp⟩ apply ContinuousWithinAt.mono_of_mem_nhdsWithin (B (q₀, x₀) ⟨hq₀, mem_of_mem_nhds ht⟩) exact mem_nhdsWithin_prod_iff.2 ⟨s, self_mem_nhdsWithin, t, nhdsWithin_le_nhds ht, Subset.rfl⟩ diff --git a/Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean b/Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean index d4552cafa15830..ba3dbc82cd3dba 100644 --- a/Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean +++ b/Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean @@ -88,7 +88,7 @@ theorem ae_eq_zero_of_integral_contMDiff_smul_eq_zero [SigmaCompactSpace M] rw [Real.norm_of_nonneg this.1] exact this.2 exact mul_le_of_le_one_left (norm_nonneg _) this - · have : g n x = 0 := by rw [← notMem_support, g_supp]; contrapose! hxK; exact vK n hxK + · have : g n x = 0 := by rw [← notMem_support, g_supp]; contrapose hxK; exact vK n hxK simp [this] have D : ∀ᵐ x ∂μ, Tendsto (fun n => g n x • f x) atTop (𝓝 (s.indicator f x)) := by filter_upwards with x @@ -104,7 +104,7 @@ theorem ae_eq_zero_of_integral_contMDiff_smul_eq_zero [SigmaCompactSpace M] simpa using hxs filter_upwards [(tendsto_order.1 u_lim).2 _ εpos] with n hn rw [← notMem_support, g_supp] - contrapose! hε + contrapose hε exact thickening_mono hn.le s hε exact tendsto_integral_of_dominated_convergence bound A B C D -- deduce that `∫ x in s, f = 0` as each integral `∫ gₙ f` vanishes by assumption diff --git a/Mathlib/Analysis/Fourier/AddCircle.lean b/Mathlib/Analysis/Fourier/AddCircle.lean index adeceb59e11905..f5f4b7a7b42bc7 100644 --- a/Mathlib/Analysis/Fourier/AddCircle.lean +++ b/Mathlib/Analysis/Fourier/AddCircle.lean @@ -231,7 +231,7 @@ theorem fourierSubalgebra_separatesPoints : (@fourierSubalgebra T).SeparatesPoin intro x y hxy refine ⟨_, ⟨fourier 1, subset_adjoin ⟨1, rfl⟩, rfl⟩, ?_⟩ dsimp only; rw [fourier_one, fourier_one] - contrapose! hxy + contrapose hxy rw [Subtype.coe_inj] at hxy exact injective_toCircle hT.elim.ne' hxy diff --git a/Mathlib/Analysis/Fourier/AddCircleMulti.lean b/Mathlib/Analysis/Fourier/AddCircleMulti.lean index 202ee01c093996..0f25daf87c5c09 100644 --- a/Mathlib/Analysis/Fourier/AddCircleMulti.lean +++ b/Mathlib/Analysis/Fourier/AddCircleMulti.lean @@ -124,7 +124,7 @@ theorem mFourierSubalgebra_separatesPoints : (mFourierSubalgebra d).SeparatesPoi refine ⟨_, ⟨mFourier (Pi.single i 1), subset_adjoin ⟨Pi.single i 1, rfl⟩, rfl⟩, ?_⟩ dsimp only rw [mFourier_single, mFourier_single, fourier_one, fourier_one, Ne, Subtype.coe_inj] - contrapose! hi + contrapose hi exact AddCircle.injective_toCircle one_ne_zero hi /-- The subalgebra of `C(UnitAddTorus d, ℂ)` generated by `mFourier n` for `n : d → ℤ` is dense. -/ diff --git a/Mathlib/Analysis/Matrix/Order.lean b/Mathlib/Analysis/Matrix/Order.lean index e4d39032020875..b37b82568b372f 100644 --- a/Mathlib/Analysis/Matrix/Order.lean +++ b/Mathlib/Analysis/Matrix/Order.lean @@ -183,7 +183,7 @@ theorem PosSemidef.posDef_iff_isUnit [DecidableEq n] {x : Matrix n n 𝕜} obtain ⟨y, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hx.nonneg simp_rw [dotProduct_mulVec, ← vecMul_vecMul, star_eq_conjTranspose, ← star_mulVec, ← dotProduct_mulVec, dotProduct_star_self_pos_iff] - contrapose! hv + contrapose hv rw [← map_eq_zero_iff (f := (yᴴ * y).mulVecLin) (mulVec_injective_iff_isUnit.mpr h), mulVecLin_apply, ← mulVec_mulVec, hv, mulVec_zero] diff --git a/Mathlib/Analysis/Matrix/Spectrum.lean b/Mathlib/Analysis/Matrix/Spectrum.lean index a9b64713c1e593..30840fd778cc2d 100644 --- a/Mathlib/Analysis/Matrix/Spectrum.lean +++ b/Mathlib/Analysis/Matrix/Spectrum.lean @@ -229,7 +229,7 @@ lemma exists_eigenvector_of_ne_zero (hA : IsHermitian A) (h_ne : A ≠ 0) : ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v := by classical have : hA.eigenvalues ≠ 0 := by - contrapose! h_ne + contrapose h_ne have := hA.spectral_theorem rwa [h_ne, Pi.comp_zero, RCLike.ofReal_zero, (by rfl : Function.const n (0 : 𝕜) = fun _ ↦ 0), diagonal_zero, map_zero] at this diff --git a/Mathlib/Analysis/Meromorphic/Order.lean b/Mathlib/Analysis/Meromorphic/Order.lean index 65486cc55ea251..274e3b9f5e6414 100644 --- a/Mathlib/Analysis/Meromorphic/Order.lean +++ b/Mathlib/Analysis/Meromorphic/Order.lean @@ -56,7 +56,7 @@ lemma meromorphicOrderAt_of_not_meromorphicAt (hf : ¬ MeromorphicAt f x) : lemma meromorphicAt_of_meromorphicOrderAt_ne_zero (hf : meromorphicOrderAt f x ≠ 0) : MeromorphicAt f x := by - contrapose! hf + contrapose hf simp [hf] /-- The order of a meromorphic function `f` at a `z₀` is infinity iff `f` vanishes locally around @@ -66,7 +66,7 @@ lemma meromorphicOrderAt_eq_top_iff : by_cases hf : MeromorphicAt f x; swap · simp only [hf, not_false_eq_true, meromorphicOrderAt_of_not_meromorphicAt, WithTop.zero_ne_top, false_iff] - contrapose! hf + contrapose hf exact (MeromorphicAt.const 0 x).congr (EventuallyEq.symm hf) simp only [meromorphicOrderAt, hf, ↓reduceDIte, sub_eq_top_iff, ENat.map_eq_top_iff, WithTop.natCast_ne_top, or_false] @@ -77,7 +77,7 @@ lemma meromorphicOrderAt_eq_top_iff : rwa [smul_eq_zero_iff_right <| pow_ne_zero _ (sub_ne_zero.mpr hz)] at hf · obtain ⟨m, hm⟩ := ENat.ne_top_iff_exists.mp h simp only [← hm, ENat.coe_ne_top, false_iff] - contrapose! h + contrapose h rw [analyticOrderAt_eq_top] rw [← hf.choose_spec.frequently_eq_iff_eventually_eq analyticAt_const] apply Eventually.frequently @@ -262,7 +262,7 @@ theorem meromorphicOrderAt_congr (hf₁₂ : f₁ =ᶠ[𝓝[≠] x] f₂) : meromorphicOrderAt f₁ x = meromorphicOrderAt f₂ x := by by_cases hf₁ : MeromorphicAt f₁ x; swap · have : ¬ MeromorphicAt f₂ x := by - contrapose! hf₁ + contrapose hf₁ exact hf₁.congr hf₁₂.symm simp [hf₁, this] by_cases h₁f₁ : meromorphicOrderAt f₁ x = ⊤ @@ -492,7 +492,7 @@ theorem meromorphicOrderAt_fun_prod {x : 𝕜} {ι : Type*} {s : Finset ι} {f : meromorphicOrderAt (f⁻¹) x = -meromorphicOrderAt f x := by by_cases hf : MeromorphicAt f x; swap · have : ¬ MeromorphicAt (f⁻¹) x := by - contrapose! hf + contrapose hf simpa using hf.inv simp [hf, this] by_cases h₂f : meromorphicOrderAt f x = ⊤ @@ -581,7 +581,7 @@ lemma meromorphicOrderAt_add_eq_left_of_lt (hf₂ : MeromorphicAt f₂ x) meromorphicOrderAt (f₁ + f₂) x = meromorphicOrderAt f₁ x := by by_cases hf₁ : MeromorphicAt f₁ x; swap · have : ¬ (MeromorphicAt (f₁ + f₂) x) := by - contrapose! hf₁ + contrapose hf₁ simpa using hf₁.sub hf₂ simp [this, hf₁] -- Trivial case: f₂ vanishes identically around z₀ diff --git a/Mathlib/Analysis/Normed/Group/AddCircle.lean b/Mathlib/Analysis/Normed/Group/AddCircle.lean index 3cacb0ddd53a80..32225d46146d32 100644 --- a/Mathlib/Analysis/Normed/Group/AddCircle.lean +++ b/Mathlib/Analysis/Normed/Group/AddCircle.lean @@ -211,7 +211,7 @@ theorem le_add_order_smul_norm_of_isOfFinAddOrder {u : AddCircle p} (hu : IsOfFi conv_lhs => rw [← mul_one p] rw [hn, nsmul_eq_mul, ← mul_assoc, mul_comm _ p, mul_assoc, mul_div_cancel₀ _ hu, mul_le_mul_iff_right₀ hp.out, Nat.one_le_cast, Nat.one_le_iff_ne_zero] - contrapose! hu' + contrapose hu' simpa only [hu', Nat.cast_zero, zero_div, mul_zero, norm_eq_zero] using hn end FiniteOrderPoints diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean index cfe072fa878d43..8087dc3e00f567 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean @@ -35,11 +35,11 @@ theorem tan_arctan {z : ℂ} (h₁ : z ≠ I) (h₂ : z ≠ -I) : tan (arctan z) ← mul_div_mul_right _ _ (exp_ne_zero (arctan z * I)), sub_mul, add_mul, ← exp_add, neg_mul, neg_add_cancel, exp_zero, ← exp_add, ← two_mul] have z₁ : 1 + z * I ≠ 0 := by - contrapose! h₁ + contrapose h₁ rw [add_eq_zero_iff_neg_eq, ← div_eq_iff I_ne_zero, div_I, neg_one_mul, neg_neg] at h₁ exact h₁.symm have z₂ : 1 - z * I ≠ 0 := by - contrapose! h₂ + contrapose h₂ rw [sub_eq_zero, ← div_eq_iff I_ne_zero, div_I, one_mul] at h₂ exact h₂.symm have key : exp (2 * (arctan z * I)) = (1 + z * I) / (1 - z * I) := by @@ -58,7 +58,7 @@ lemma cos_ne_zero_of_arctan_bounds {z : ℂ} (h₀ : z ≠ π / 2) (h₁ : -(π rw [ne_eq, Complex.ext_iff, not_and_or] at h₀ ⊢ norm_cast at h₀ ⊢ rcases h₀ with nr | ni - · left; contrapose! nr + · left; contrapose nr rw [nr, mul_div_assoc, neg_eq_neg_one_mul, mul_lt_mul_iff_of_pos_right (by positivity)] at h₁ rw [nr, ← one_mul (π / 2), mul_div_assoc, mul_le_mul_iff_of_pos_right (by positivity)] at h₂ norm_cast at h₁ h₂ diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean index 7652303237efff..14d25fb22eb80f 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean @@ -521,7 +521,7 @@ theorem Gamma_ne_zero {s : ℝ} (hs : ∀ m : ℕ, s ≠ -m) : Gamma s ≠ 0 := apply n_ih · intro m specialize hs (1 + m) - contrapose! hs + contrapose hs rw [← eq_sub_iff_add_eq] at hs rw [hs] push_cast diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean index d52445dc759541..ab9def634171e1 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean @@ -434,7 +434,7 @@ theorem Gamma_ne_zero {s : ℂ} (hs : ∀ m : ℕ, s ≠ -m) : Gamma s ≠ 0 := rw [this, Gamma_ofReal, ofReal_ne_zero] refine Real.Gamma_ne_zero fun n => ?_ specialize hs n - contrapose! hs + contrapose hs rwa [this, ← ofReal_natCast, ← ofReal_neg, ofReal_inj] · have : sin (↑π * s) ≠ 0 := by rw [Complex.sin_ne_zero_iff] diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean index 307ce2e1cc25c5..622be5ed056d62 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean @@ -74,7 +74,7 @@ theorem differentiableAt_GammaAux (s : ℂ) (n : ℕ) (h1 : 1 - s.re < n) (h2 : rw [Nat.cast_succ] at h1; rw [Complex.add_re, Complex.one_re]; linarith have b : ∀ m : ℕ, s + 1 ≠ -m := by intro m; have := h2 (1 + m) - contrapose! this + contrapose this rw [← eq_sub_iff_add_eq] at this simpa using this refine DifferentiableAt.div (DifferentiableAt.comp _ (hn a b) ?_) ?_ ?_ @@ -127,7 +127,7 @@ theorem not_continuousAt_Gamma_neg_nat (n : ℕ) : ¬ ContinuousAt Gamma (-n) := rw [Nat.cast_zero, neg_zero] exact not_continuousAt_Gamma_zero case succ n ih => - contrapose! ih + contrapose ih rw [Nat.cast_add, Nat.cast_one] at ih suffices ContinuousAt (fun s ↦ Gamma (s - 1 + 1)) (-n) by simpa using this suffices ContinuousAt (fun s ↦ Gamma (s + 1)) (-n - 1) from diff --git a/Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean index 30e04adcabb923..394fbeedb00916 100644 --- a/Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean @@ -125,7 +125,7 @@ theorem integral_cpow {r : ℂ} (h : -1 < r.re ∨ r ≠ -1 ∧ (0 : ℝ) ∉ [[ · apply integral_eq_sub_of_hasDerivAt (fun x hx => ?_) (intervalIntegrable_cpow (r := r) <| Or.inr hab) refine hasDerivAt_ofReal_cpow_const' (ne_of_mem_of_not_mem hx hab) ?_ - contrapose! hr; rwa [add_eq_zero_iff_eq_neg] + contrapose hr; rwa [add_eq_zero_iff_eq_neg] replace h : -1 < r.re := by tauto suffices ∀ c : ℝ, (∫ x : ℝ in 0..c, (x : ℂ) ^ r) = (c : ℂ) ^ (r + 1) / (r + 1) - (0 : ℂ) ^ (r + 1) / (r + 1) by @@ -140,7 +140,7 @@ theorem integral_cpow {r : ℂ} (h : -1 < r.re ∨ r ≠ -1 ∧ (0 : ℝ) ∉ [[ · rcases le_total c 0 with (hc | hc) · rw [max_eq_left hc] at hx; exact hx.2.ne · rw [min_eq_left hc] at hx; exact hx.1.ne' - · contrapose! hr; rw [hr]; ring + · contrapose hr; rw [hr]; ring · exact intervalIntegrable_cpow' h set_option backward.isDefEq.respectTransparency false in @@ -379,7 +379,7 @@ theorem integral_mul_cpow_one_add_sq {t : ℂ} (ht : t ≠ -1) : (∫ x : ℝ in a..b, (x : ℂ) * ((1 : ℂ) + ↑x ^ 2) ^ t) = ((1 : ℂ) + (b : ℂ) ^ 2) ^ (t + 1) / (2 * (t + ↑1)) - ((1 : ℂ) + (a : ℂ) ^ 2) ^ (t + 1) / (2 * (t + ↑1)) := by - have : t + 1 ≠ 0 := by contrapose! ht; rwa [add_eq_zero_iff_eq_neg] at ht + have : t + 1 ≠ 0 := by contrapose ht; rwa [add_eq_zero_iff_eq_neg] at ht apply integral_eq_sub_of_hasDerivAt · intro x _ have f : HasDerivAt (fun y : ℂ => 1 + y ^ 2) (2 * x : ℂ) x := by diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/ChebyshevGauss.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/ChebyshevGauss.lean index 90147d10a1ce70..da283c90645e32 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/ChebyshevGauss.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/ChebyshevGauss.lean @@ -39,7 +39,7 @@ open Complex (exp I) private lemma exp_sub_one_ne_zero {n : ℕ} {k : ℤ} (hn : n ≠ 0) (hk : ¬ (2 * n : ℤ) ∣ k) : exp (k / n * π * I) ≠ 1 := by - contrapose! hk + contrapose hk obtain ⟨m, hx⟩ := Complex.exp_eq_one_iff.mp hk have h : k = 2 * n * m := by apply (@Int.cast_inj ℂ _ _).mp diff --git a/Mathlib/CategoryTheory/Filtered/Basic.lean b/Mathlib/CategoryTheory/Filtered/Basic.lean index 86555191353ef6..ebda68a87d1b12 100644 --- a/Mathlib/CategoryTheory/Filtered/Basic.lean +++ b/Mathlib/CategoryTheory/Filtered/Basic.lean @@ -259,7 +259,7 @@ theorem sup_exists : grind [coeq_condition] · rw [@w' _ _ mX' mY' f' _] apply Finset.mem_of_mem_insert_of_ne mf' - contrapose! h + contrapose h obtain ⟨rfl, h⟩ := h trivial @@ -788,7 +788,7 @@ theorem inf_exists : grind [eq_condition] · rw [@w' _ _ mX' mY' f' _] apply Finset.mem_of_mem_insert_of_ne mf' - contrapose! h + contrapose h obtain ⟨rfl, h⟩ := h trivial diff --git a/Mathlib/Combinatorics/Enumerative/DyckWord.lean b/Mathlib/Combinatorics/Enumerative/DyckWord.lean index 7e5508cbd0a109..7156246494fdaf 100644 --- a/Mathlib/Combinatorics/Enumerative/DyckWord.lean +++ b/Mathlib/Combinatorics/Enumerative/DyckWord.lean @@ -468,7 +468,7 @@ lemma monotone_semilength : Monotone semilength := fun p q pq ↦ by lemma strictMono_semilength : StrictMono semilength := fun p q pq ↦ by obtain ⟨plq, pnq⟩ := lt_iff_le_and_ne.mp pq apply lt_of_le_of_ne (monotone_semilength plq) - contrapose! pnq + contrapose pnq replace pnq := congr(2 * $(pnq)) simp_rw [two_mul_semilength_eq_length] at pnq exact DyckWord.ext ((infix_of_le plq).eq_of_length pnq) diff --git a/Mathlib/Combinatorics/Enumerative/InclusionExclusion.lean b/Mathlib/Combinatorics/Enumerative/InclusionExclusion.lean index 0ecbb7678c102d..f7e31563ffc173 100644 --- a/Mathlib/Combinatorics/Enumerative/InclusionExclusion.lean +++ b/Mathlib/Combinatorics/Enumerative/InclusionExclusion.lean @@ -75,7 +75,7 @@ lemma indicator_biUnion_eq_sum_powerset (s : Finset ι) (S : ι → Set α) (f : intro t hts ht rw [Set.indicator_of_notMem] · simp - · contrapose! ha + · contrapose ha simp only [Set.mem_iInter] at ha rcases ht with ⟨i, hi⟩ simp only [Set.mem_iUnion, exists_prop] diff --git a/Mathlib/Combinatorics/Enumerative/Partition/GenFun.lean b/Mathlib/Combinatorics/Enumerative/Partition/GenFun.lean index 50c17055565681..15d1857dae5a36 100644 --- a/Mathlib/Combinatorics/Enumerative/Partition/GenFun.lean +++ b/Mathlib/Combinatorics/Enumerative/Partition/GenFun.lean @@ -96,18 +96,18 @@ private theorem aux_dvd_of_coeff_ne_zero {f : ℕ → ℕ → R} {d : ℕ} {s : x ∣ g x := by by_cases hx : x ∈ s · specialize hprod x hx - contrapose! hprod + contrapose hprod have hx0 : x ≠ 0 := fun h ↦ hs0 (h ▸ hx) rw [map_add, (summable_genFun_term' f hx0).map_tsum _ (WithPiTopology.continuous_coeff _ _)] rw [show (0 : R) = 0 + ∑' (i : ℕ), 0 by simp] congrm (?_ + ∑' (i : ℕ), ?_) · suffices g x ≠ 0 by simp [this] - contrapose! hprod + contrapose hprod simp [hprod] · rw [map_smul, coeff_X_pow] apply smul_eq_zero_of_right suffices g x ≠ x * (i + 1) by simp [this] - contrapose! hprod + contrapose hprod simp [hprod] · suffices g x = 0 by simp [this] contrapose! hx @@ -124,7 +124,7 @@ private theorem aux_prod_coeff_eq_zero_of_notMem_range (f : ℕ → ℕ → R) { rw [Set.mem_range] have hgne0 (i : ℕ) : g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i := by refine ⟨fun h ↦ ⟨?_, ?_⟩, by grind⟩ - · contrapose! hs0 with rfl + · contrapose hs0 with rfl exact mem_of_subset (mem_finsuppAntidiag.mp hg).2 (by simpa using h) · exact Nat.le_of_dvd (Nat.pos_of_ne_zero h) <| aux_dvd_of_coeff_ne_zero hs0 hg hprod _ refine ⟨Nat.Partition.mk (Finsupp.mk g.support (fun i ↦ g i / i) ?_).toMultiset ?_ ?_, ?_⟩ diff --git a/Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean b/Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean index ffea420c3163bc..99df79691738ff 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean @@ -602,7 +602,7 @@ end completeMultipartiteGraph /-- If `H` is not `n`-colorable and `G` is `n`-colorable, then `G` is `H.Free`. -/ theorem free_of_colorable {W : Type*} {H : SimpleGraph W} (nhc : ¬H.Colorable n) (hc : G.Colorable n) : H.Free G := by - contrapose! nhc with hc' + contrapose nhc with hc' exact ⟨hc.some.comp hc'.some.toHom⟩ end SimpleGraph diff --git a/Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean b/Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean index 27470b143c6f97..aa43c29edb30d7 100644 --- a/Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean +++ b/Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean @@ -438,7 +438,7 @@ def ofCopy (f : Copy (completeEquipartiteGraph r t) G) : G.CompleteEquipartiteSu rw [← h₁', ← h₂'] apply f.toHom.map_adj simp_rw [completeEquipartiteGraph_adj] - contrapose! hne with heq + contrapose hne with heq simp_rw [← h₁, ← h₂, heq] end CompleteEquipartiteSubgraph diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean index ea34c08a4d1810..90b571f8cb242b 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean @@ -157,7 +157,7 @@ lemma exists_adj_isEdgeReachable_two (hne : u ≠ v) (h : G.IsEdgeReachable 2 u simp only [Walk.getVert_tail, Nat.reduceAdd] at this simpa using hw.getVert_eq_start_iff_of_not_nil (Walk.not_nil_of_ne hne) |>.mp this.symm · refine Walk.reachable <| Walk.cons (deleteEdges_adj.mpr ⟨this, ?_⟩) Walk.nil - contrapose! h' + contrapose h' refine (Set.subsingleton_iff_singleton h').mp ?_ exact Set.encard_le_one_iff_subsingleton.mp (Order.le_of_lt_succ hs) @@ -173,7 +173,7 @@ variable {w : G.Walk u v} private lemma IsTrail.isEdgeReachable_two_of_isEdgeReachable_two_aux (hw : w.IsTrail) (huv : G.IsEdgeReachable 2 u v) (huy : x ∈ w.support) : G.IsEdgeReachable 2 u x := by classical - contrapose! huy + contrapose huy obtain ⟨e, he⟩ := by simpa [isEdgeReachable_two] using huy have he' : ¬ (G.deleteEdges {e}).Reachable v x := fun hvy ↦ he <| (isEdgeReachable_two.1 huv _).trans hvy diff --git a/Mathlib/Combinatorics/SimpleGraph/Diam.lean b/Mathlib/Combinatorics/SimpleGraph/Diam.lean index 304b055ccd2098..12b31a1a8be14c 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Diam.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Diam.lean @@ -64,7 +64,7 @@ lemma eccent_eq_zero_of_subsingleton [Subsingleton α] (u : α) : G.eccent u = 0 lemma eccent_ne_zero [Nontrivial α] (u : α) : G.eccent u ≠ 0 := by obtain ⟨v, huv⟩ := exists_ne ‹_› - contrapose! huv + contrapose huv simp only [eccent, ENat.iSup_eq_zero, edist_eq_zero_iff] at huv exact (huv v).symm @@ -160,7 +160,7 @@ lemma nontrivial_of_ediam_ne_zero (h : G.ediam ≠ 0) : Nontrivial α := by lemma ediam_ne_zero [Nontrivial α] : G.ediam ≠ 0 := by obtain ⟨u, v, huv⟩ := exists_pair_ne ‹_› - contrapose! huv + contrapose huv simp only [ediam, eccent, ENat.iSup_eq_zero, edist_eq_zero_iff] at huv exact huv u v diff --git a/Mathlib/Combinatorics/SimpleGraph/Extremal/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Extremal/Basic.lean index 453ccbc0f888b8..a7fcb5c636b9a2 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Extremal/Basic.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Extremal/Basic.lean @@ -165,7 +165,7 @@ theorem extremalNumber_congr {n₁ n₂ : ℕ} {W₁ W₂ : Type*} {H₁ : Simpl rw [← Fintype.card_fin n₂, extremalNumber_le_iff] intro G _ h apply card_edgeFinset_le_extremalNumber - contrapose! h + contrapose h exact h.trans' ⟨e.toCopy⟩ /-- If `H₁ ≃g H₂`, then `extremalNumber n H₁` equals `extremalNumber n H₂`. -/ @@ -189,7 +189,7 @@ theorem card_edgeFinset_deleteIncidenceSet_le_extremalNumber #(G.deleteIncidenceSet v).edgeFinset ≤ extremalNumber (card V - 1) H := by rw [← card_edgeFinset_induce_compl_singleton, ← @card_unique ({v} : Set V), ← card_compl_set] apply card_edgeFinset_le_extremalNumber - contrapose! h + contrapose h exact h.trans ⟨Copy.induce G {v}ᶜ⟩ end ExtremalNumber diff --git a/Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean b/Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean index fc80ac86a5696c..3f74a28e62c4fa 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean @@ -219,7 +219,7 @@ lemma card_parts_le [DecidableEq V] : #h.finpartition.parts ≤ r := by obtain ⟨z, -, hz⟩ := h.finpartition.exists_subset_part_bijOn have ncf : ¬G.CliqueFree #z := by refine IsNClique.not_cliqueFree ⟨fun v hv w hw hn ↦ ?_, rfl⟩ - contrapose! hn + contrapose hn exact hz.injOn hv hw (by rwa [← h.not_adj_iff_part_eq]) rw [Finset.card_eq_of_equiv hz.equiv] at ncf exact absurd (h.1.mono (Nat.succ_le_of_lt l)) ncf diff --git a/Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean b/Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean index 3c9212eb4c7334..f3c8dda0a5de56 100644 --- a/Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean +++ b/Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean @@ -238,7 +238,7 @@ theorem colorable_iff_isCompleteMultipartite_of_maximal_cliqueFree fun _ ↦ G.colorable_zero_iff.2 <| cliqueFree_one.1 h.1⟩ | r + 1 => refine ⟨fun hc ↦ ?_, fun hc ↦ hc.colorable_of_cliqueFree h.1⟩ - contrapose! hc + contrapose hc obtain ⟨_, _, _, _, _, hw⟩ := exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite h hc exact hw.not_colorable_succ diff --git a/Mathlib/Combinatorics/SimpleGraph/Operations.lean b/Mathlib/Combinatorics/SimpleGraph/Operations.lean index f2aeb6bdee7aff..d474214530793b 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Operations.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Operations.lean @@ -103,7 +103,7 @@ lemma disjoint_sdiff_neighborFinset_image : have : t ∉ e := by rw [mem_sdiff, mem_incidenceFinset] at he obtain ⟨_, h⟩ := he - contrapose! h + contrapose h simp_all [incidenceSet] aesop diff --git a/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean b/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean index ad88bdfb0c4798..4ad99886d99d06 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Subgraph.lean @@ -1119,7 +1119,7 @@ theorem deleteEdges_coe_eq (s : Set (Sym2 G'.verts)) : refine Sym2.ind ?_ rintro ⟨v', hv'⟩ ⟨w', hw'⟩ simp only [Sym2.map_mk, Sym2.eq] - contrapose! + contrapose rintro (_ | _) <;> simpa only [Sym2.eq_swap] · intro h' hs exact h' _ hs rfl diff --git a/Mathlib/Combinatorics/SimpleGraph/Walk/Maps.lean b/Mathlib/Combinatorics/SimpleGraph/Walk/Maps.lean index 3566978ee2f97d..24fd87ee58e088 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Walk/Maps.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Walk/Maps.lean @@ -244,7 +244,7 @@ theorem toDeleteEdges_cons (s : Set (Sym2 V)) {u v w : V} (h : G.Adj u v) (p : G This is an abbreviation for `SimpleGraph.Walk.toDeleteEdges`. -/ abbrev toDeleteEdge (e : Sym2 V) (p : G.Walk v w) (hp : e ∉ p.edges) : (G.deleteEdges {e}).Walk v w := - p.toDeleteEdges {e} (fun _ => by contrapose!; simp +contextual [hp]) + p.toDeleteEdges {e} (fun _ ↦ by contrapose; simp +contextual [hp]) @[simp] theorem map_toDeleteEdges_eq (s : Set (Sym2 V)) {p : G.Walk v w} (hp) : diff --git a/Mathlib/Data/Finset/Insert.lean b/Mathlib/Data/Finset/Insert.lean index 8c35828a7bf9da..fbaa3b4dc10377 100644 --- a/Mathlib/Data/Finset/Insert.lean +++ b/Mathlib/Data/Finset/Insert.lean @@ -433,7 +433,7 @@ instance (i : α) (s : Finset α) : Nonempty ((insert i s : Finset α) : Set α) (Finset.coe_nonempty.mpr (s.insert_nonempty i)).to_subtype theorem ne_insert_of_notMem (s t : Finset α) {a : α} (h : a ∉ s) : s ≠ insert a t := by - contrapose! h + contrapose h simp [h] theorem insert_subset_iff : insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t := by grind diff --git a/Mathlib/Data/Finsupp/Fin.lean b/Mathlib/Data/Finsupp/Fin.lean index b3d27b4921b70c..0f165b6327bf55 100644 --- a/Mathlib/Data/Finsupp/Fin.lean +++ b/Mathlib/Data/Finsupp/Fin.lean @@ -79,11 +79,11 @@ theorem cons_zero_zero : cons 0 (0 : Fin n →₀ M) = 0 := by simp [cons_zero_e variable {s} {y} theorem cons_ne_zero_of_left (h : y ≠ 0) : cons y s ≠ 0 := by - contrapose! h with c + contrapose h with c rw [← cons_zero y s, c, Finsupp.coe_zero, Pi.zero_apply] theorem cons_ne_zero_of_right (h : s ≠ 0) : cons y s ≠ 0 := by - contrapose! h with c + contrapose h with c ext a simp [← cons_succ a y s, c] diff --git a/Mathlib/Data/Finsupp/Option.lean b/Mathlib/Data/Finsupp/Option.lean index 346d28f45ac970..53a2921070925f 100644 --- a/Mathlib/Data/Finsupp/Option.lean +++ b/Mathlib/Data/Finsupp/Option.lean @@ -159,14 +159,14 @@ theorem optionElim_zero (y : M) : (0 : α →₀ M).optionElim y = single none y · simp theorem optionElim_ne_zero_of_left (y : M) (f : α →₀ M) (h : y ≠ 0) : f.optionElim y ≠ 0 := by - contrapose! h with c + contrapose h with c have : f.optionElim y none = (0 : Option α →₀ M) none := by rw [c] simp only [optionElim_apply_eq_elim, Option.elim_none, coe_zero, Pi.zero_apply] at this exact this theorem optionElim_ne_zero_of_right (y : M) (f : α →₀ M) (h : f ≠ 0) : f.optionElim y ≠ 0 := by - contrapose! h with c + contrapose h with c ext a have : f.optionElim y (Option.some a) = (0 : Option α →₀ M) (Option.some a) := by rw [c] diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean index 708545ed3fed6c..52d8710b6f7300 100644 --- a/Mathlib/Data/List/Basic.lean +++ b/Mathlib/Data/List/Basic.lean @@ -591,7 +591,7 @@ theorem succ_idxOf_lt_length_of_mem_dropLast {l : List α} {a : α} (ha : a ∈ theorem idxOf_getLast {l : List α} (hl : l ≠ []) (hl' : l.getLast hl ∉ l.dropLast) : l.idxOf (l.getLast hl) = l.length - 1 := Nat.le_antisymm (Nat.le_pred_of_lt <| l.idxOf_lt_length_of_mem <| getLast_mem hl) <| by - contrapose! hl' + contrapose hl' rwa [mem_dropLast_iff_idxOf_lt <| getLast_mem hl, ← Nat.not_le] end IndexOf diff --git a/Mathlib/Data/NNReal/Defs.lean b/Mathlib/Data/NNReal/Defs.lean index a4e7a49f178474..475f19ddfd64d9 100644 --- a/Mathlib/Data/NNReal/Defs.lean +++ b/Mathlib/Data/NNReal/Defs.lean @@ -450,7 +450,7 @@ theorem coe_sSup (s : Set ℝ≥0) : (↑(sSup s) : ℝ) = sSup (((↑) : ℝ≥ exact (@subset_sSup_of_within ℝ (Set.Ici (0 : ℝ)) _ _ (_) s hs H A).symm · simp only [csSup_of_not_bddAbove H, csSup_empty, bot_eq_zero', NNReal.coe_zero] apply (Real.sSup_of_not_bddAbove ?_).symm - contrapose! H + contrapose H exact bddAbove_coe.1 H @[simp, norm_cast] diff --git a/Mathlib/Data/Nat/Count.lean b/Mathlib/Data/Nat/Count.lean index 5dfad409ee9538..afc61bcf6c07f2 100644 --- a/Mathlib/Data/Nat/Count.lean +++ b/Mathlib/Data/Nat/Count.lean @@ -107,7 +107,7 @@ theorem count_strict_mono {m n : ℕ} (hm : p m) (hmn : m < n) : count p m < cou (count_lt_count_succ_iff.2 hm).trans_le <| count_monotone _ (Nat.succ_le_iff.2 hmn) theorem count_injective {m n : ℕ} (hm : p m) (hn : p n) (heq : count p m = count p n) : m = n := by - by_contra! h : m ≠ n + by_contra h : m ≠ n wlog hmn : m < n · exact this hn hm heq.symm h.symm (by grind) · simpa [heq] using count_strict_mono hm hmn diff --git a/Mathlib/Data/Nat/Digits/Defs.lean b/Mathlib/Data/Nat/Digits/Defs.lean index 5a2b2a1ca17f1d..525657e7632cfc 100644 --- a/Mathlib/Data/Nat/Digits/Defs.lean +++ b/Mathlib/Data/Nat/Digits/Defs.lean @@ -234,7 +234,7 @@ theorem digits_ofDigits (b : ℕ) (h : 1 < b) (L : List ℕ) (w₁ : ∀ l ∈ L left simpa using w₂ · right - contrapose! w₂ + contrapose w₂ refine digits_zero_of_eq_zero h.ne_bot w₂ _ ?_ rw [List.getLast_cons h'] exact List.getLast_mem h' diff --git a/Mathlib/Data/Nat/Factorization/Basic.lean b/Mathlib/Data/Nat/Factorization/Basic.lean index 2c0ac5a056a707..729d67a6199067 100644 --- a/Mathlib/Data/Nat/Factorization/Basic.lean +++ b/Mathlib/Data/Nat/Factorization/Basic.lean @@ -38,7 +38,7 @@ theorem factorization_eq_zero_iff_remainder {p r : ℕ} (i : ℕ) (pp : p.Prime) contrapose! h refine ⟨pp, ?_, ?_⟩ · rwa [← Nat.dvd_add_iff_right (dvd_mul_right p i)] - · contrapose! hr0 + · contrapose hr0 exact (add_eq_zero.1 hr0).2 /-- The only numbers with empty prime factorization are `0` and `1` -/ diff --git a/Mathlib/Data/Nat/Factorization/LCM.lean b/Mathlib/Data/Nat/Factorization/LCM.lean index 3ce1e57a546954..9aa5aa0919dbb5 100644 --- a/Mathlib/Data/Nat/Factorization/LCM.lean +++ b/Mathlib/Data/Nat/Factorization/LCM.lean @@ -60,7 +60,7 @@ lemma coprime_factorizationLCMLeft_factorizationLCMRight : dsimp only; split_ifs with h h' any_goals simp only [coprime_one_right_eq_true, coprime_one_left_eq_true] refine coprime_pow_primes _ _ (prime_of_mem_primeFactors hp) (prime_of_mem_primeFactors hq) ?_ - contrapose! h'; rwa [← h'] + contrapose h'; rwa [← h'] variable {a b} diff --git a/Mathlib/Data/Set/Finite/Basic.lean b/Mathlib/Data/Set/Finite/Basic.lean index d632ba23a921be..9ab9a13a96d5d8 100644 --- a/Mathlib/Data/Set/Finite/Basic.lean +++ b/Mathlib/Data/Set/Finite/Basic.lean @@ -897,7 +897,7 @@ theorem not_injOn_infinite_finite_image {f : α → β} {s : Set α} (h_inf : s. have : Infinite s := infinite_coe_iff.mpr h_inf have h := not_injective_infinite_finite ((f '' s).codRestrict (s.restrict f) fun x => ⟨x, x.property, rfl⟩) - contrapose! h + contrapose h rwa [injective_codRestrict, ← injOn_iff_injective] theorem finite_range_findGreatest {P : α → ℕ → Prop} [∀ x, DecidablePred (P x)] {b : ℕ} : diff --git a/Mathlib/Data/Sym/Sym2.lean b/Mathlib/Data/Sym/Sym2.lean index a3b3153007e9e8..d375f071f5b40e 100644 --- a/Mathlib/Data/Sym/Sym2.lean +++ b/Mathlib/Data/Sym/Sym2.lean @@ -561,7 +561,7 @@ instance decidablePred_mem_diagSet (α : Type u) [DecidableEq α] : DecidablePre IsDiag.decidablePred _ theorem other_ne {a : α} {z : Sym2 α} (hd : ¬IsDiag z) (h : a ∈ z) : Mem.other h ≠ a := by - contrapose! hd + contrapose hd have h' := Sym2.other_spec h rw [hd] at h' rw [← h'] diff --git a/Mathlib/FieldTheory/CardinalEmb.lean b/Mathlib/FieldTheory/CardinalEmb.lean index bbcebcb34b944d..066528edb5da99 100644 --- a/Mathlib/FieldTheory/CardinalEmb.lean +++ b/Mathlib/FieldTheory/CardinalEmb.lean @@ -159,7 +159,7 @@ theorem strictMono_leastExt : StrictMono φ := fun i j h ↦ by theorem adjoin_image_leastExt (i : ι) : E⟮ contrapose! hxy + constructor <;> contrapose hxy · rw [inner_eq_one_iff_of_norm_eq_one hx hy] at hxy simp [hy, hxy] · rw [inner_eq_neg_one_iff_of_norm_eq_one hx hy] at hxy diff --git a/Mathlib/Geometry/Group/Growth/LinearLowerBound.lean b/Mathlib/Geometry/Group/Growth/LinearLowerBound.lean index a6cac4cba9d584..2430a39e7a77a9 100644 --- a/Mathlib/Geometry/Group/Growth/LinearLowerBound.lean +++ b/Mathlib/Geometry/Group/Growth/LinearLowerBound.lean @@ -30,7 +30,7 @@ lemma pow_ssubset_pow_succ_of_pow_ne_closure (hX₁ : (1 : G) ∈ X) (hX : X.Non · simpa [ssubset_iff_subset_not_subset, hX₁, -Finset.subset_singleton_iff] using hX.not_subset_singleton refine (pow_subset_pow_right hX₁ <| n.le_add_right _).ssubset_of_ne ?_ - contrapose! hXclosure with hXn + contrapose hXclosure with hXn rw [← closure_pow (mod_cast hX₁) hn] wlog hn₁ : n = 1 · simp +contextual only [pow_one] at this diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Basic.lean b/Mathlib/Geometry/Manifold/ContMDiff/Basic.lean index adb0510c6aa8e0..e7c869166bc873 100644 --- a/Mathlib/Geometry/Manifold/ContMDiff/Basic.lean +++ b/Mathlib/Geometry/Manifold/ContMDiff/Basic.lean @@ -293,7 +293,7 @@ lemma ContMDiff.piecewise · apply (hg x).congr_of_eventuallyEq filter_upwards [isClosed_closure.isOpen_compl.mem_nhds h'x] with y hy rw [piecewise_eq_of_notMem] - contrapose! hy + contrapose hy simpa using subset_closure hy /-- Given two `C^n` functions `f` and `g` from `ℝ` to a real manifold which coincide locally diff --git a/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean b/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean index cdae29ab9991ac..d38f6ab791ac74 100644 --- a/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean +++ b/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean @@ -563,7 +563,7 @@ lemma mdifferentiableWithinAt_of_mfderivWithin_injective MDifferentiableWithinAt I I' f s x := by nontriviality E have : Nontrivial (TangentSpace I x) := inferInstanceAs (Nontrivial E) - contrapose! hf + contrapose hf rw [mfderivWithin_zero_of_not_mdifferentiableWithinAt hf] exact not_injective_const diff --git a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean index e680faa78794d2..1318a2cadf6146 100644 --- a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean +++ b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean @@ -777,10 +777,10 @@ theorem IsOpen.exists_contMDiff_support_eq {s : Set M} (hs : IsOpen s) : by_cases Hx : x ∈ tsupport (f c) · suffices g c (chartAt H c x) = 0 by simp only [this, mul_zero] rw [← notMem_support, g_supp, ← mem_preimage, preimage_inter] - contrapose! hx + contrapose hx simp only [mem_inter_iff, mem_preimage, (chartAt H c).left_inv (hf c Hx)] at hx exact hx.2 - · have : x ∉ support (f c) := by contrapose! Hx; exact subset_tsupport _ Hx + · have : x ∉ support (f c) := by contrapose Hx; exact subset_tsupport _ Hx rw [notMem_support] at this simp [this] · apply SmoothPartitionOfUnity.contMDiff_finsum_smul @@ -813,7 +813,7 @@ theorem exists_contMDiff_support_eq_eq_one_iff classical apply lt_of_le_of_ne (g_pos x) (Ne.symm ?_) rw [← mem_support, g_supp] - contrapose! xs + contrapose xs exact h.trans f_supp.symm.subset (by simpa using xs) linarith [f_pos x] refine ⟨fun x ↦ f x / (f x + g x), ?_, ?_, ?_, ?_⟩ diff --git a/Mathlib/GroupTheory/Coxeter/Inversion.lean b/Mathlib/GroupTheory/Coxeter/Inversion.lean index e2449ef522bfda..d67bc2f8373bd5 100644 --- a/Mathlib/GroupTheory/Coxeter/Inversion.lean +++ b/Mathlib/GroupTheory/Coxeter/Inversion.lean @@ -95,14 +95,14 @@ theorem odd_length : Odd (ℓ t) := by theorem length_mul_left_ne (w : W) : ℓ (w * t) ≠ ℓ w := by suffices cs.lengthParity (w * t) ≠ cs.lengthParity w by - contrapose! this + contrapose this simp only [lengthParity_eq_ofAdd_length, this] rcases ht with ⟨w, i, rfl⟩ simp [lengthParity_simple] theorem length_mul_right_ne (w : W) : ℓ (t * w) ≠ ℓ w := by suffices cs.lengthParity (t * w) ≠ cs.lengthParity w by - contrapose! this + contrapose this simp only [lengthParity_eq_ofAdd_length, this] rcases ht with ⟨w, i, rfl⟩ simp [lengthParity_simple] diff --git a/Mathlib/GroupTheory/Coxeter/Length.lean b/Mathlib/GroupTheory/Coxeter/Length.lean index 1e58fc48f6a9fa..f7c45b59a03552 100644 --- a/Mathlib/GroupTheory/Coxeter/Length.lean +++ b/Mathlib/GroupTheory/Coxeter/Length.lean @@ -256,7 +256,7 @@ theorem not_isReduced_alternatingWord (i i' : B) {m : ℕ} (hM : M i i' ≠ 0) ( _ ≤ M i i' := Nat.sub_le _ _ _ < M i i' + 1 := Nat.lt_succ_self _ | step m ih => -- Inductive step - contrapose! ih + contrapose ih rw [alternatingWord_succ'] at ih apply IsReduced.drop (j := 1) at ih simpa using ih diff --git a/Mathlib/GroupTheory/DoubleCoset.lean b/Mathlib/GroupTheory/DoubleCoset.lean index 0af52ea6bf44c9..0807db7726cfff 100644 --- a/Mathlib/GroupTheory/DoubleCoset.lean +++ b/Mathlib/GroupTheory/DoubleCoset.lean @@ -148,7 +148,7 @@ lemma mem_quotToDoubleCoset_iff {H K : Subgroup G} (i : Quotient (H : Set G) K) lemma disjoint_out {H K : Subgroup G} {a b : Quotient H K} : a ≠ b → Disjoint (doubleCoset a.out H K) (doubleCoset b.out (H : Set G) K) := by - contrapose! + contrapose intro h simpa [out_eq'] using mk_eq_of_doubleCoset_eq (eq_of_not_disjoint h) @@ -251,7 +251,7 @@ lemma iUnion_finset_leftRel_eq_univ_of_leftRel {H K : Subgroup G} {t : Finset (Q refine (Set.ne_univ_iff_exists_notMem _).mpr ⟨Quot.mk (leftRel K) x, ?_⟩ simp only [Set.mem_iUnion, Set.mem_image, exists_prop, not_exists, not_and] intro y hy q hq - contrapose! hx + contrapose hx simp only [Set.mem_iUnion, exists_prop] refine ⟨y, hy, ?_⟩ rw [← doubleCoset_eq_of_mem hq, mem_doubleCoset] @@ -268,7 +268,7 @@ lemma iUnion_finset_rightRel_eq_univ_of_rightRel {H K : Subgroup G} {t : Finset refine (Set.ne_univ_iff_exists_notMem _).mpr ⟨Quot.mk (rightRel H) x, ?_⟩ simp only [Set.mem_iUnion, Set.mem_image, exists_prop, not_exists, not_and] intro y hy q hq - contrapose! hx + contrapose hx simp only [Set.mem_iUnion, exists_prop] refine ⟨y, hy, ?_⟩ rw [← doubleCoset_eq_of_mem hq, mem_doubleCoset] diff --git a/Mathlib/GroupTheory/GroupAction/FixedPoints.lean b/Mathlib/GroupTheory/GroupAction/FixedPoints.lean index 17a79f2c8556dd..ecb6e5dfad05f4 100644 --- a/Mathlib/GroupTheory/GroupAction/FixedPoints.lean +++ b/Mathlib/GroupTheory/GroupAction/FixedPoints.lean @@ -262,7 +262,7 @@ is disjoint from `(fixedBy α g)ᶜ`, then `g` and `h` cannot commute. is disjoint from `(fixedBy α g)ᶜ`, then `g` and `h` cannot commute. -/] theorem not_commute_of_disjoint_movedBy_preimage {g h : G} (ne_one : g ≠ 1) (disjoint : Disjoint (fixedBy α g)ᶜ (h • (fixedBy α g)ᶜ)) : ¬Commute g h := by - contrapose! ne_one with comm + contrapose ne_one with comm rwa [movedBy_mem_fixedBy_of_commute comm, disjoint_self, Set.bot_eq_empty, ← Set.compl_univ, compl_inj_iff, fixedBy_eq_univ_iff_eq_one] at disjoint diff --git a/Mathlib/GroupTheory/GroupAction/SubMulAction/Combination.lean b/Mathlib/GroupTheory/GroupAction/SubMulAction/Combination.lean index c61ec1cfbf3091..bba2b35b27c918 100644 --- a/Mathlib/GroupTheory/GroupAction/SubMulAction/Combination.lean +++ b/Mathlib/GroupTheory/GroupAction/SubMulAction/Combination.lean @@ -86,7 +86,7 @@ theorem addAction_faithful {G : Type*} [AddGroup G] [AddAction G α] {n : ℕ} obtain ⟨s, has, has'⟩ := exists_mem_notMem hn hα (Ne.symm ha) rw [Equiv.ext_iff, not_forall] use s - contrapose! has' + contrapose has' simp only [AddAction.toPerm_apply, coe_one, id_eq] at has' rw [← has'] simpa [← mem_coe_iff] @@ -114,7 +114,7 @@ theorem mulAction_faithful (hn : 1 ≤ n) (hα : n < ENat.card α) {g : G} : obtain ⟨s, has, has'⟩ := exists_mem_notMem hn hα (Ne.symm ha) rw [Equiv.ext_iff, not_forall] use s - contrapose! has' + contrapose has' simp only [MulAction.toPerm_apply, coe_one, id_eq] at has' rw [← has'] simpa only [coe_smul, smul_mem_smul_finset_iff, ← mem_coe_iff] diff --git a/Mathlib/GroupTheory/OrderOfElement.lean b/Mathlib/GroupTheory/OrderOfElement.lean index c2ac8b615cb093..f2a6ad313a5809 100644 --- a/Mathlib/GroupTheory/OrderOfElement.lean +++ b/Mathlib/GroupTheory/OrderOfElement.lean @@ -622,7 +622,7 @@ theorem infinite_not_isOfFinOrder {x : G} (h : ¬IsOfFinOrder x) : contrapose! h have : ¬Injective fun n : ℕ => x ^ n := by have := Set.not_injOn_infinite_finite_image (Set.Ioi_infinite 0) h - contrapose! this + contrapose this exact Set.injOn_of_injective this rwa [injective_pow_iff_not_isOfFinOrder, Classical.not_not] at this @@ -704,7 +704,7 @@ theorem infinite_not_isOfFinOrder {x : G} (h : ¬IsOfFinOrder x) : contrapose! h have : ¬Function.Injective fun n : ℕ => x ^ n := by have := Set.not_injOn_infinite_finite_image (Set.Ioi_infinite 0) h - contrapose! this + contrapose this exact Set.injOn_of_injective this rwa [injective_pow_iff_not_isOfFinOrder, Classical.not_not] at this diff --git a/Mathlib/GroupTheory/PGroup.lean b/Mathlib/GroupTheory/PGroup.lean index fa98d228019dfc..86024127dfa148 100644 --- a/Mathlib/GroupTheory/PGroup.lean +++ b/Mathlib/GroupTheory/PGroup.lean @@ -196,7 +196,7 @@ theorem nonempty_fixed_point_of_prime_not_dvd_card (α) [MulAction G α] (hpα : @Set.Nonempty.of_subtype _ _ (by rw [← Finite.card_pos_iff, pos_iff_ne_zero] - contrapose! hpα + contrapose hpα rw [← Nat.modEq_zero_iff_dvd, ← hpα] exact hG.card_modEq_card_fixedPoints α) diff --git a/Mathlib/GroupTheory/Perm/Centralizer.lean b/Mathlib/GroupTheory/Perm/Centralizer.lean index 3115abba2f1464..844239413c0f3f 100644 --- a/Mathlib/GroupTheory/Perm/Centralizer.lean +++ b/Mathlib/GroupTheory/Perm/Centralizer.lean @@ -500,7 +500,7 @@ theorem kerParam_apply {u : Perm (Function.fixedPoints g)} rw [kerParam, MonoidHom.noncommCoprod_apply', mul_apply, ofSubtype_apply_of_not_mem u hx', noncommPiCoprod_apply, ← Finset.noncommProd_erase_mul _ (Finset.mem_univ ⟨g.cycleOf x, hx⟩), mul_apply, ← notMem_support] - contrapose! hx' + contrapose hx' obtain ⟨a, ha1, ha2⟩ := mem_support_of_mem_noncommProd_support hx' simp only [Finset.mem_erase, Finset.mem_univ, and_true, Ne, Subtype.ext_iff] at ha1 have key := cycleFactorsFinset_pairwise_disjoint g a.2 hx ha1 @@ -512,7 +512,7 @@ theorem kerParam_apply {u : Perm (Function.fixedPoints g)} · rw [cycleOf_mem_cycleFactorsFinset_iff] at hx rw [kerParam, MonoidHom.noncommCoprod_apply, mul_apply, Equiv.apply_eq_iff_eq, ← notMem_support] - contrapose! hx + contrapose hx obtain ⟨a, -, ha⟩ := mem_support_of_mem_noncommProd_support (comm := fun a ha b hb h ↦ g.pairwise_commute_of_mem_zpowers h (v a) (v b) (v a).2 (v b).2) hx exact support_zpowers_of_mem_cycleFactorsFinset_le (v a) ha diff --git a/Mathlib/GroupTheory/Perm/ClosureSwap.lean b/Mathlib/GroupTheory/Perm/ClosureSwap.lean index f8d96dc6d8dddc..295a60aefc331e 100644 --- a/Mathlib/GroupTheory/Perm/ClosureSwap.lean +++ b/Mathlib/GroupTheory/Perm/ClosureSwap.lean @@ -49,7 +49,7 @@ theorem exists_smul_notMem_of_subset_orbit_closure (S : Set G) (T : Set α) {a : have key0 : ¬ closure S ≤ stabilizer G T := by have ⟨b, hb⟩ := nonempty obtain ⟨σ, rfl⟩ := subset hb - contrapose! notMem with h + contrapose notMem with h exact smul_mem_smul_set_iff.mp ((h σ.2).symm ▸ hb) contrapose! key0 refine (closure_le _).mpr fun σ hσ ↦ ?_ diff --git a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean index 837d6e688be692..32d0ab199b8011 100644 --- a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean +++ b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean @@ -518,7 +518,7 @@ theorem IsCycle.support_pow_eq_iff (hf : IsCycle f) {n : ℕ} : · intro H apply le_antisymm (support_pow_le _ n) _ intro x hx - contrapose! H + contrapose H ext z by_cases hz : f z = z · rw [pow_apply_eq_self_of_apply_eq_self hz, one_apply] @@ -1018,7 +1018,7 @@ theorem IsCycle.commute_iff' {g c : Perm α} (hc : c.IsCycle) : subtypePerm_apply_zpow_of_mem] at hix exact hix.symm · rw [notMem_support.mp hx, eq_comm, ← notMem_support] - contrapose! hx + contrapose hx exact (hc' x).mp hx /-- A permutation `g` commutes with a cycle `c` if and only if diff --git a/Mathlib/GroupTheory/Perm/Cycle/Factors.lean b/Mathlib/GroupTheory/Perm/Cycle/Factors.lean index 95f433d05c5ef0..4f0a76b60ed3af 100644 --- a/Mathlib/GroupTheory/Perm/Cycle/Factors.lean +++ b/Mathlib/GroupTheory/Perm/Cycle/Factors.lean @@ -177,7 +177,7 @@ theorem cycleOf_mul_of_apply_right_eq_self [DecidableRel f.SameCycle] rw [cycleOf_apply_apply_zpow_self] simp [h.mul_zpow, zpow_apply_eq_self_of_apply_eq_self hx] · rw [cycleOf_apply_of_not_sameCycle hxy, cycleOf_apply_of_not_sameCycle] - contrapose! hxy + contrapose hxy obtain ⟨z, rfl⟩ := hxy refine ⟨z, ?_⟩ simp [h.mul_zpow, zpow_apply_eq_self_of_apply_eq_self hx] @@ -552,7 +552,7 @@ theorem cycleOf_mem_cycleFactorsFinset_iff {f : Perm α} {x : α} : rw [mem_cycleFactorsFinset_iff] constructor · rintro ⟨hc, _⟩ - contrapose! hc + contrapose hc rw [notMem_support, ← cycleOf_eq_one_iff] at hc simp [hc] · intro hx diff --git a/Mathlib/GroupTheory/Perm/MaximalSubgroups.lean b/Mathlib/GroupTheory/Perm/MaximalSubgroups.lean index a356671eafae10..929f4ee0d6ad0f 100644 --- a/Mathlib/GroupTheory/Perm/MaximalSubgroups.lean +++ b/Mathlib/GroupTheory/Perm/MaximalSubgroups.lean @@ -214,7 +214,7 @@ lemma _root_.Subgroup.isPretransitive_of_stabilizer_lt obtain ⟨g, hg, rfl⟩ := moves a ha b hb rw [stabilizer_compl] at hg exact ⟨⟨g, hG.le hg⟩, rfl⟩ - · contrapose! hG + · contrapose hG apply not_lt_of_ge -- `G ≤ stabilizer (Equiv.Perm α) s` have : G = Subgroup.map G.subtype ⊤ := by @@ -410,7 +410,7 @@ theorem isCoatom_stabilizer {s : Set α} IsCoatom (stabilizer (Perm α) s) := by obtain h | h | h := Nat.lt_trichotomy s.ncard sᶜ.ncard · exact isCoatom_stabilizer_of_ncard_lt_ncard_compl hs_nonempty h - · contrapose! hα + · contrapose hα rw [← Set.ncard_add_ncard_compl s, two_mul, ← h] · rw [← stabilizer_compl] apply isCoatom_stabilizer_of_ncard_lt_ncard_compl hsc_nonempty diff --git a/Mathlib/GroupTheory/SpecificGroups/Alternating.lean b/Mathlib/GroupTheory/SpecificGroups/Alternating.lean index ca9655387bac24..a8f681aff1e6a7 100644 --- a/Mathlib/GroupTheory/SpecificGroups/Alternating.lean +++ b/Mathlib/GroupTheory/SpecificGroups/Alternating.lean @@ -521,7 +521,7 @@ theorem eq_alternatingGroup_of_index_eq_two {G : Subgroup (Equiv.Perm α)} (hG : refine swap_induction_on g (iff_of_true G.one_mem <| map_one _) fun g x y hxy ih ↦ ?_ rw [mul_mem_iff_of_index_two hG, mul_mem_iff_of_index_two alternatingGroup.index_eq_two, ih] refine iff_congr (iff_of_false ?_ (by cases (sign_swap hxy).symm.trans ·)) Iff.rfl - contrapose! habG + contrapose habG rw [← (isConj_iff.mp <| isConj_swap hxy hab).choose_spec] exact (normal_of_index_eq_two hG).conj_mem _ habG _ diff --git a/Mathlib/GroupTheory/SpecificGroups/ZGroup.lean b/Mathlib/GroupTheory/SpecificGroups/ZGroup.lean index 6c206ec2007a10..f31aa7aa08076b 100644 --- a/Mathlib/GroupTheory/SpecificGroups/ZGroup.lean +++ b/Mathlib/GroupTheory/SpecificGroups/ZGroup.lean @@ -96,7 +96,7 @@ theorem commutator_lt [Finite G] [IsZGroup G] [Nontrivial G] : commutator G < let f := MonoidHom.transferSylow P (hP.normalizer_le_centralizer rfl) refine lt_of_le_of_lt (Abelianization.commutator_subset_ker f) ?_ have h := P.ne_bot_of_dvd_card (Nat.card G).minFac_dvd - contrapose! h + contrapose h rw [← Subgroup.isComplement'_top_left, ← (not_lt_top_iff.mp h)] exact hP.isComplement' rfl diff --git a/Mathlib/LinearAlgebra/AffineSpace/Simplex/Basic.lean b/Mathlib/LinearAlgebra/AffineSpace/Simplex/Basic.lean index 33f0aa15954352..ea6b5944d86dc0 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/Simplex/Basic.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/Simplex/Basic.lean @@ -432,7 +432,7 @@ lemma setInterior_map (I : Set k) {n : ℕ} (s : Simplex k P n) {f : P →ᵃ[k] simp [Affine.Simplex.affineCombination_mem_setInterior_iff hw1] · apply iff_of_false · exact fun h ↦ hp (Set.mem_of_mem_of_subset h (s.map f hf).setInterior_subset_affineSpan) - · contrapose! hp + · contrapose hp obtain ⟨q, hq, hqp⟩ := hp rw [s.map_points, Set.range_comp, ← AffineSubspace.map_span, AffineSubspace.mem_map] exact ⟨q, (Set.mem_of_mem_of_subset hq s.setInterior_subset_affineSpan), hqp⟩ diff --git a/Mathlib/LinearAlgebra/Determinant.lean b/Mathlib/LinearAlgebra/Determinant.lean index b54dceab5224bf..11661dabaf74b5 100644 --- a/Mathlib/LinearAlgebra/Determinant.lean +++ b/Mathlib/LinearAlgebra/Determinant.lean @@ -308,7 +308,7 @@ theorem det_conj {N : Type*} [AddCommGroup N] [Module A N] (f : M →ₗ[A] M) ( · rw [← toMatrix_comp, LinearEquiv.comp_coe, e.self_trans_symm, LinearEquiv.refl_toLinearMap, toMatrix_id] · have H' : ¬∃ t : Finset N, Nonempty (Basis t A N) := by - contrapose! H + contrapose H rcases H with ⟨s, ⟨b⟩⟩ exact ⟨_, ⟨(b.map e.symm).reindexFinsetRange⟩⟩ simp only [coe_det, H, H', MonoidHom.one_apply, dif_neg, not_false_eq_true] diff --git a/Mathlib/LinearAlgebra/Eigenspace/Basic.lean b/Mathlib/LinearAlgebra/Eigenspace/Basic.lean index 38f623028f5092..998a3b33b78496 100644 --- a/Mathlib/LinearAlgebra/Eigenspace/Basic.lean +++ b/Mathlib/LinearAlgebra/Eigenspace/Basic.lean @@ -307,7 +307,7 @@ lemma HasUnifEigenvalue.le {f : End R M} {μ : R} {k m : ℕ∞} (hm : k ≤ m) (hk : f.HasUnifEigenvalue μ k) : f.HasUnifEigenvalue μ m := by unfold HasUnifEigenvalue at * - contrapose! hk + contrapose hk rw [← le_bot_iff, ← hk] exact (f.genEigenspace _).monotone hm diff --git a/Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean b/Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean index 12e076085966a6..e802198a5800c1 100644 --- a/Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean +++ b/Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean @@ -272,7 +272,7 @@ theorem linearCombination_onFinset {s : Finset α} {f : α → R} (g : α → M) simp only [linearCombination_apply, Finsupp.sum, Finsupp.onFinset_apply, Finsupp.support_onFinset] rw [Finset.sum_filter_of_ne] intro x _ h - contrapose! h + contrapose h simp [h] variable [Module S M] [SMulCommClass R S M] diff --git a/Mathlib/LinearAlgebra/Finsupp/Pi.lean b/Mathlib/LinearAlgebra/Finsupp/Pi.lean index 1d41160156e4c9..1325a6d2926a92 100644 --- a/Mathlib/LinearAlgebra/Finsupp/Pi.lean +++ b/Mathlib/LinearAlgebra/Finsupp/Pi.lean @@ -214,7 +214,7 @@ theorem range_mapRange_linearMap (f : M →ₗ[R] N) (hf : LinearMap.ker f = ⊥ choose y hy using hx refine ⟨⟨x.support, y, fun i => ?_⟩, by ext; simp_all⟩ constructor - <;> contrapose! + <;> contrapose <;> simp_all +contextual [← hy, map_zero, LinearMap.ker_eq_bot'.1 hf] end Finsupp diff --git a/Mathlib/LinearAlgebra/LinearIndependent/Defs.lean b/Mathlib/LinearAlgebra/LinearIndependent/Defs.lean index b96ac332ec96b5..d64a21bd54dab2 100644 --- a/Mathlib/LinearAlgebra/LinearIndependent/Defs.lean +++ b/Mathlib/LinearAlgebra/LinearIndependent/Defs.lean @@ -239,7 +239,7 @@ theorem linearIndependent_iff'ₛ : refine _root_.by_contradiction fun hni ↦ hni <| hv (f.support ∪ g.support) f g ?_ _ ?_ · rwa [← sum_subset subset_union_left, ← sum_subset subset_union_right] <;> rintro i - hi <;> rw [Finsupp.notMem_support_iff.mp hi, zero_smul] - · contrapose! hni + · contrapose hni simp_rw [notMem_union, Finsupp.notMem_support_iff] at hni rw [hni.1, hni.2]⟩ diff --git a/Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean b/Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean index 35b5d3745413f0..66b6beb66750b7 100644 --- a/Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean +++ b/Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean @@ -485,7 +485,7 @@ theorem det_eq_zero_of_not_linearIndependent_rows [IsDomain R] {A : Matrix m m R theorem linearIndependent_rows_of_det_ne_zero [IsDomain R] {A : Matrix m m R} (hA : A.det ≠ 0) : LinearIndependent R (fun i ↦ A i) := by - contrapose! hA + contrapose hA exact det_eq_zero_of_not_linearIndependent_rows hA theorem linearIndependent_cols_of_det_ne_zero [IsDomain R] {A : Matrix m m R} (hA : A.det ≠ 0) : diff --git a/Mathlib/LinearAlgebra/Matrix/Gershgorin.lean b/Mathlib/LinearAlgebra/Matrix/Gershgorin.lean index c51c1c67efddb8..a5cd489c9ccf92 100644 --- a/Mathlib/LinearAlgebra/Matrix/Gershgorin.lean +++ b/Mathlib/LinearAlgebra/Matrix/Gershgorin.lean @@ -35,7 +35,7 @@ theorem eigenvalue_mem_ball {μ : K} (hμ : Module.End.HasEigenvalue (Matrix.toL · obtain ⟨v, h_eg, h_nz⟩ := hμ.exists_hasEigenvector obtain ⟨i, -, h_i⟩ := Finset.exists_mem_eq_sup' Finset.univ_nonempty (fun i => ‖v i‖) have h_nz : v i ≠ 0 := by - contrapose! h_nz + contrapose h_nz ext j rw [Pi.zero_apply, ← norm_le_zero_iff] refine (h_i ▸ Finset.le_sup' (fun i => ‖v i‖) (Finset.mem_univ j)).trans ?_ diff --git a/Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean b/Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean index d09385e4922a4a..0200dcf3c44bfd 100644 --- a/Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean @@ -49,7 +49,7 @@ lemma detp_neg_one_diagonal (d : n → R) : detp (-1) (diagonal d) = 0 := by rw [detp, sum_eq_zero] intro σ hσ have hσ1 : σ ≠ 1 := by - contrapose! hσ + contrapose hσ rw [hσ, mem_ofSign, sign_one] decide obtain ⟨i, hi⟩ := not_forall.mp (mt Perm.ext_iff.mpr hσ1) @@ -94,7 +94,7 @@ theorem detp_mul : conv_rhs => rw [add_assoc] refine congr_arg₂ (· + ·) (sum_congr rfl fun σ hσ ↦ ?_) (add_comm _ _) replace hσ : ¬ Function.Injective σ := by - contrapose! hσ + contrapose hσ rw [notMem_compl, mem_map, ofSign_disjUnion] exact ⟨Equiv.ofBijective σ hσ.bijective_of_finite, mem_univ _, rfl⟩ obtain ⟨i, j, hσ, hij⟩ := Function.not_injective_iff.mp hσ diff --git a/Mathlib/LinearAlgebra/Matrix/ZPow.lean b/Mathlib/LinearAlgebra/Matrix/ZPow.lean index bc46e0f48d750a..6276c51a81c673 100644 --- a/Mathlib/LinearAlgebra/Matrix/ZPow.lean +++ b/Mathlib/LinearAlgebra/Matrix/ZPow.lean @@ -249,7 +249,7 @@ theorem coe_units_zpow (u : Mˣ) : ∀ n : ℤ, ((u ^ n : Mˣ) : M) = (u : M) ^ theorem zpow_ne_zero_of_isUnit_det [Nonempty n'] [Nontrivial R] {A : M} (ha : IsUnit A.det) (z : ℤ) : A ^ z ≠ 0 := by have := ha.det_zpow z - contrapose! this + contrapose this rw [this, det_zero ‹_›] exact not_isUnit_zero diff --git a/Mathlib/LinearAlgebra/PID.lean b/Mathlib/LinearAlgebra/PID.lean index 2d85ae07c6c27b..359397a738a7cc 100644 --- a/Mathlib/LinearAlgebra/PID.lean +++ b/Mathlib/LinearAlgebra/PID.lean @@ -42,7 +42,7 @@ lemma trace_restrict_eq_of_forall_mem [IsDomain R] [IsPrincipalIdealRing R] set A : Matrix (Fin n) (Fin n) R := toMatrix snf.bN snf.bN (f.restrict hf') set B : Matrix ι ι R := toMatrix snf.bM snf.bM f have aux : ∀ i, B i i ≠ 0 → i ∈ Set.range snf.f := fun i hi ↦ by - contrapose! hi; exact snf.repr_eq_zero_of_notMem_range ⟨_, (hf _)⟩ hi + contrapose hi; exact snf.repr_eq_zero_of_notMem_range ⟨_, (hf _)⟩ hi change ∑ i, A i i = ∑ i, B i i rw [← Finset.sum_filter_of_ne (p := fun j ↦ j ∈ Set.range snf.f) (by simpa using aux)] simp [A, B, hf, Finset.sum_image snf.f.injective.injOn] diff --git a/Mathlib/LinearAlgebra/Projectivization/Cardinality.lean b/Mathlib/LinearAlgebra/Projectivization/Cardinality.lean index dc3c3915d70e4d..513701b01148ac 100644 --- a/Mathlib/LinearAlgebra/Projectivization/Cardinality.lean +++ b/Mathlib/LinearAlgebra/Projectivization/Cardinality.lean @@ -111,7 +111,7 @@ lemma card_of_finrank [Finite k] {n : ℕ} (h : Module.finrank k V = n) : have : n = 0 := by rw [← h] apply Module.finrank_of_not_finite - contrapose! hf + contrapose hf simpa using Module.finite_of_finite k simp [this] have : 1 < Nat.card k := Finite.one_lt_card diff --git a/Mathlib/LinearAlgebra/Projectivization/Independence.lean b/Mathlib/LinearAlgebra/Projectivization/Independence.lean index e8b2c918433569..1802d0080df0af 100644 --- a/Mathlib/LinearAlgebra/Projectivization/Independence.lean +++ b/Mathlib/LinearAlgebra/Projectivization/Independence.lean @@ -81,7 +81,7 @@ representatives are linearly dependent. -/ theorem dependent_iff : Dependent f ↔ ¬LinearIndependent K (Projectivization.rep ∘ f) := by refine ⟨?_, fun h => ?_⟩ · rintro ⟨ff, hff, hh1⟩ - contrapose! hh1 + contrapose hh1 choose a ha using fun i : ι => exists_smul_eq_mk_rep K (ff i) (hff i) convert hh1.units_smul a⁻¹ ext i diff --git a/Mathlib/LinearAlgebra/RootSystem/Base.lean b/Mathlib/LinearAlgebra/RootSystem/Base.lean index 3421deb5ef6f56..e3c8d35417f093 100644 --- a/Mathlib/LinearAlgebra/RootSystem/Base.lean +++ b/Mathlib/LinearAlgebra/RootSystem/Base.lean @@ -222,7 +222,7 @@ lemma pos_or_neg_of_sum_smul_root_mem (f : ι → ℤ) by_cases hi : i ∈ b.support · change 0 ≤ f' ⟨i, hi⟩ simp [← hc] - · replace hi : i ∉ f.support := by contrapose! hi; exact hf₀ hi + · replace hi : i ∉ f.support := by contrapose hi; exact hf₀ hi simp_all refine Pi.lt_def.mpr ⟨aux, ?_⟩ by_contra! contra diff --git a/Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean b/Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean index ad21bbe14821d4..5f6d9bf5bb259d 100644 --- a/Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean +++ b/Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean @@ -178,7 +178,7 @@ lemma induction_on_cartanMatrix [P.IsReduced] [P.IsIrreducible] have hq₀ : q ≠ ⊥ := q.ne_bot_iff.mpr ⟨P.root i, subset_span <| by simpa, P.ne_zero i⟩ have hq_mem (k : b.support) : P.root k ∈ q ↔ p k := by refine ⟨fun hk ↦ ?_, fun hk ↦ subset_span <| by simpa⟩ - contrapose! hk + contrapose hk exact b.linearIndepOn_root.linearIndependent.notMem_span_image hk have hq_notMem (k : b.support) (hk : P.root k ∉ q) : q ≤ LinearMap.ker (P.coroot' k) := by refine fun x hx ↦ LinearMap.mem_ker.mpr ?_ diff --git a/Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean b/Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean index a3bebfbb528050..2a859b897c6159 100644 --- a/Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean +++ b/Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean @@ -230,7 +230,7 @@ lemma root_add_root_mem_of_pairingIn_neg (h : P.pairingIn ℤ i j < 0) (h' : α α i + α j ∈ Φ := by let _i := P.indexNeg replace h : 0 < P.pairingIn ℤ i (-j) := by simpa - replace h' : i ≠ -j := by contrapose! h'; simp [h'] + replace h' : i ≠ -j := by contrapose h'; simp [h'] simpa using P.root_sub_root_mem_of_pairingIn_pos h h' lemma pairingIn_eq_zero_of_add_notMem_of_sub_notMem (hp : i ≠ j) (hn : α i ≠ -α j) @@ -300,7 +300,7 @@ lemma apply_eq_or (i j : ι) : B.form (α j) (α j) = 3 * B.form (α i) (α i) := by obtain ⟨j', h₁, h₂⟩ := P.exists_form_eq_form_and_form_ne_zero B i j suffices P.pairingIn ℤ i j' ≠ 0 by simp only [← h₁, B.apply_eq_or_aux i j' this] - contrapose! h₂ + contrapose h₂ replace h₂ : P.pairing i j' = 0 := by rw [← P.algebraMap_pairingIn ℤ, h₂, map_zero] exact (B.apply_root_root_zero_iff i j').mpr h₂ diff --git a/Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean b/Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean index a32c529e9e01b4..cda390f3c2669f 100644 --- a/Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean +++ b/Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean @@ -436,7 +436,7 @@ lemma eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero {x : M} lemma rootForm_pos_of_ne_zero {x : M} (hx : x ∈ P.rootSpan R) (h : x ≠ 0) : 0 < P.RootForm x x := by apply (P.zero_le_rootForm x).lt_of_ne - contrapose! h + contrapose h exact P.eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero hx h.symm lemma rootForm_anisotropic [P.IsRootSystem] : diff --git a/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Lemmas.lean b/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Lemmas.lean index 33513d59325d6c..78dcfd684d021f 100644 --- a/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Lemmas.lean +++ b/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Lemmas.lean @@ -67,7 +67,7 @@ lemma root_sub_root_mem_of_mem_of_mem (hk : α k + α i - α j ∈ Φ) exact P.ne_zero _ hk'.choose_spec have aux (h : P.pairingIn ℤ i k = -2) : ¬P.pairingIn ℤ k i = -2 := by have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap - contrapose! hk'; exact (P.pairingIn_neg_two_neg_two_iff ℤ i k).mp ⟨h, hk'⟩ + contrapose hk'; exact (P.pairingIn_neg_two_neg_two_iff ℤ i k).mp ⟨h, hk'⟩ have := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i k aesop -- https://github.com/leanprover-community/mathlib4/issues/24551 (this should be faster) replace hki : P.pairing k i = -1 := by rw [← P.algebraMap_pairingIn ℤ, hki]; simp @@ -92,7 +92,7 @@ lemma root_add_root_mem_of_mem_of_mem (hk : α k + α i - α j ∈ Φ) simp only [indexNeg_neg, root_reflectionPerm, reflection_apply_self] module rw [← neg_mem_range_root_iff] - convert b.root_sub_root_mem_of_mem_of_mem j i (-k) hij.symm hj hi hk (by contrapose! hkj; aesop) + convert b.root_sub_root_mem_of_mem_of_mem j i (-k) hij.symm hj hi hk (by contrapose hkj; aesop) (by convert P.neg_mem_range_root_iff.mpr hk' using 1; simp [neg_add_eq_sub]) using 1 simp only [indexNeg_neg, root_reflectionPerm, reflection_apply_self] module @@ -280,7 +280,7 @@ private lemma chainBotCoeff_mul_chainTopCoeff.aux_2 have hlj_mem : P.root l - P.root j ∈ range P.root := by rwa [← h₁] /- It is sufficient to prove that two key pairings vanish. -/ suffices ¬ (P.pairingIn ℤ m i = 0 ∧ P.pairingIn ℤ l j ≠ 0) by - contrapose! this + contrapose this rcases ne_or_eq (P.pairingIn ℤ m i) 0 with hmi | hmi · simpa [hmi, this.1, P.pairingIn_eq_zero_iff (i := i)] using chainBotCoeff_if_one_zero him_mem refine ⟨hmi, fun hlj ↦ ?_⟩ diff --git a/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Semisimple.lean b/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Semisimple.lean index fe832b4af82ed2..e56ded4bca6605 100644 --- a/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Semisimple.lean +++ b/Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Semisimple.lean @@ -131,7 +131,7 @@ lemma isNilpotent_e : apply P.nsmul_notMem_range_root (n := P.chainTopCoeff i i + 2) (i := i) convert hk₁ using 1 module - · contrapose! hij + · contrapose hij rw [root_eq_neg_iff] at hij rw [hij, ← indexNeg_neg, neg_neg] rw [root_add_nsmul_mem_range_iff_le_chainTopCoeff hij'] at hk₁ @@ -361,7 +361,7 @@ instance instIsIrreducible [Nonempty ι] : suffices ∃ i, v b i ∈ U by obtain ⟨i, hi⟩ := this; exact instIsIrreducible_aux₂ hi let U' : LieSubmodule K H (b.support ⊕ ι → K) := { U with lie_mem := U.lie_mem } apply instIsIrreducible_aux₁ U' - contrapose! hU + contrapose hU replace hU : U ≤ span K (range (u (b := b))) := by rwa [← coe_genWeightSpace_zero_eq_span_range_u] refine (LieSubmodule.eq_bot_iff _).mpr fun x hx ↦ ?_ obtain ⟨c, hc⟩ : ∃ c : b.support → K, ∑ i, c i • u i = x := diff --git a/Mathlib/LinearAlgebra/RootSystem/Reduced.lean b/Mathlib/LinearAlgebra/RootSystem/Reduced.lean index 4a0a7a989c491d..58fc7fe12dc861 100644 --- a/Mathlib/LinearAlgebra/RootSystem/Reduced.lean +++ b/Mathlib/LinearAlgebra/RootSystem/Reduced.lean @@ -183,7 +183,7 @@ lemma linearIndependent_iff_coxeterWeight_ne_four : LinearIndependent R ![P.root i, P.root j] ↔ P.coxeterWeight i j ≠ 4 := by have : IsAddTorsionFree M := .of_isTorsionFree R M refine ⟨coxeterWeight_ne_four_of_linearIndependent P, fun h ↦ ?_⟩ - contrapose! h + contrapose h have h₁ := P.pairing_smul_root_eq_of_not_linearIndependent h rw [LinearIndependent.pair_symm_iff] at h have h₂ := P.pairing_smul_root_eq_of_not_linearIndependent h diff --git a/Mathlib/MeasureTheory/Function/ContinuousMapDense.lean b/Mathlib/MeasureTheory/Function/ContinuousMapDense.lean index 292bff25fd73ef..3995e5cbafa6f1 100644 --- a/Mathlib/MeasureTheory/Function/ContinuousMapDense.lean +++ b/Mathlib/MeasureTheory/Function/ContinuousMapDense.lean @@ -183,7 +183,7 @@ theorem MemLp.exists_hasCompactSupport_eLpNorm_sub_le simp only [sub_add_sub_cancel] refine ⟨f, I3, f_cont, f_mem, HasCompactSupport.intro k_compact fun x hx => ?_⟩ rw [← Function.notMem_support] - contrapose! hx + contrapose hx exact interior_subset (f_support hx) diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean index 859b622e81eb85..8680d36fda8b27 100644 --- a/Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean +++ b/Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean @@ -150,7 +150,7 @@ lemma MemLp.mono_exponent_of_measure_support_ne_top {p q : ℝ≥0∞} {f : α have : (toMeasurable μ s).indicator f = f := by apply Set.indicator_eq_self.2 apply Function.support_subset_iff'.2 fun x hx ↦ hf x ?_ - contrapose! hx + contrapose hx exact subset_toMeasurable μ s hx rw [← this, memLp_indicator_iff_restrict (measurableSet_toMeasurable μ s)] at hfq ⊢ have : Fact (μ (toMeasurable μ s) < ∞) := ⟨by simpa [lt_top_iff_ne_top] using hs⟩ diff --git a/Mathlib/MeasureTheory/Group/Measure.lean b/Mathlib/MeasureTheory/Group/Measure.lean index e4199b378a0a54..9a7e8b97877b15 100644 --- a/Mathlib/MeasureTheory/Group/Measure.lean +++ b/Mathlib/MeasureTheory/Group/Measure.lean @@ -580,7 +580,7 @@ any open set. -/] theorem isOpenPosMeasure_of_mulLeftInvariant_of_compact (K : Set G) (hK : IsCompact K) (h : μ K ≠ 0) : IsOpenPosMeasure μ := by refine ⟨fun U hU hne => ?_⟩ - contrapose! h + contrapose h rw [← nonpos_iff_eq_zero] rw [← hU.interior_eq] at hne obtain ⟨t, hKt⟩ : ∃ t : Finset G, K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h : G => g * h) ⁻¹' U := diff --git a/Mathlib/MeasureTheory/Integral/Bochner/Set.lean b/Mathlib/MeasureTheory/Integral/Bochner/Set.lean index 2c76538aa136db..e052f6f99c0052 100644 --- a/Mathlib/MeasureTheory/Integral/Bochner/Set.lean +++ b/Mathlib/MeasureTheory/Integral/Bochner/Set.lean @@ -336,7 +336,7 @@ theorem setIntegral_eq_zero_of_ae_eq_zero (ht_eq : ∀ᵐ x ∂μ, x ∈ t → f ∫ x in t, f x ∂μ = 0 := by by_cases hf : AEStronglyMeasurable f (μ.restrict t); swap · rw [integral_undef] - contrapose! hf + contrapose hf exact hf.1 have : ∫ x in t, hf.mk f x ∂μ = 0 := by refine integral_eq_zero_of_ae ?_ @@ -589,7 +589,7 @@ theorem norm_setIntegral_le_of_norm_le_const_ae' {C : ℝ} (hs : μ s < ∞) · rw [integral_non_aestronglyMeasurable hfm] have : ∃ᵐ (x : X) ∂μ, x ∈ s := by apply frequently_ae_mem_iff.mpr - contrapose! hfm + contrapose hfm simp [Measure.restrict_eq_zero.mpr hfm] rcases (this.and_eventually hC).exists with ⟨x, hx, h'x⟩ have : 0 ≤ C := (norm_nonneg _).trans (h'x hx) diff --git a/Mathlib/MeasureTheory/Integral/IntegrableOn.lean b/Mathlib/MeasureTheory/Integral/IntegrableOn.lean index be11e7d4eac624..36d43625c3bc24 100644 --- a/Mathlib/MeasureTheory/Integral/IntegrableOn.lean +++ b/Mathlib/MeasureTheory/Integral/IntegrableOn.lean @@ -829,7 +829,7 @@ theorem integrableOn_Icc_iff_integrableOn_Ioc' by_cases hab : a ≤ b · rw [← Ioc_union_left hab, integrableOn_union, eq_true (integrableOn_singleton ha'), and_true] · rw [Icc_eq_empty hab, Ioc_eq_empty] - contrapose! hab + contrapose hab exact hab.le theorem integrableOn_Icc_iff_integrableOn_Ico' @@ -838,7 +838,7 @@ theorem integrableOn_Icc_iff_integrableOn_Ico' by_cases hab : a ≤ b · rw [← Ico_union_right hab, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true] · rw [Icc_eq_empty hab, Ico_eq_empty] - contrapose! hab + contrapose hab exact hab.le theorem integrableOn_Ico_iff_integrableOn_Ioo' diff --git a/Mathlib/MeasureTheory/Integral/Layercake.lean b/Mathlib/MeasureTheory/Integral/Layercake.lean index eff92dc79ba712..cd6ddd00faf986 100644 --- a/Mathlib/MeasureTheory/Integral/Layercake.lean +++ b/Mathlib/MeasureTheory/Integral/Layercake.lean @@ -268,7 +268,7 @@ theorem lintegral_comp_eq_lintegral_meas_le_mul_of_measurable (μ : Measure α) sets `{ω | f ω > uₙ}` for `uₙ` a sequence decreasing to `M`. Therefore, this case follows from the case where the measure is sigma-finite, applied to `ν`. -/ have M_bdd : BddAbove {s : ℝ | g =ᵐ[volume.restrict (Ioc (0 : ℝ) s)] 0} := by - contrapose! H1 + contrapose H1 have : ∀ (n : ℕ), g =ᵐ[volume.restrict (Ioc (0 : ℝ) n)] 0 := by intro n rcases not_bddAbove_iff.1 H1 n with ⟨s, hs, ns⟩ diff --git a/Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean b/Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean index f8783a14b7be02..d8ead455ce55b7 100644 --- a/Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean +++ b/Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean @@ -486,7 +486,7 @@ theorem lintegral_indicator_le (f : α → ℝ≥0∞) (s : Set α) : congr with x simp only [mem_preimage, mem_singleton_iff, mem_inter_iff, iff_self_and] rintro rfl - contrapose! H + contrapose H simpa [H] using hg x @[simp] diff --git a/Mathlib/MeasureTheory/Measure/AEMeasurable.lean b/Mathlib/MeasureTheory/Measure/AEMeasurable.lean index 0b479d63acf55b..eefd2a9376d897 100644 --- a/Mathlib/MeasureTheory/Measure/AEMeasurable.lean +++ b/Mathlib/MeasureTheory/Measure/AEMeasurable.lean @@ -107,7 +107,7 @@ theorem sum_measure [Countable ι] {μ : ι → Measure α} (h : ∀ i, AEMeasur rw [hs _ _ hi] exact fun h => ⟨i, h, hi⟩ · refine measure_mono_null (fun x (hx : f x ≠ g x) => ?_) (hsμ i) - contrapose! hx + contrapose hx refine (piecewise_eq_of_notMem _ _ _ ?_).symm exact fun h => hx (mem_iInter.1 h i) @@ -210,7 +210,7 @@ theorem exists_ae_eq_range_subset (H : AEMeasurable f μ) {t : Set β} (ht : ∀ by_cases hx : x ∈ s · simpa [g, hx] using h₀.some_mem · simp only [g, hx, piecewise_eq_of_notMem, not_false_iff] - contrapose! hx + contrapose hx apply subset_toMeasurable simp +contextual only [hx, mem_compl_iff, mem_setOf_eq, not_and, not_false_iff, imp_true_iff] diff --git a/Mathlib/MeasureTheory/Measure/EverywherePos.lean b/Mathlib/MeasureTheory/Measure/EverywherePos.lean index 72e0111a3df2f5..64741e31bac0ad 100644 --- a/Mathlib/MeasureTheory/Measure/EverywherePos.lean +++ b/Mathlib/MeasureTheory/Measure/EverywherePos.lean @@ -265,7 +265,7 @@ lemma IsEverywherePos.IsGdelta_of_isMulLeftInvariant apply inter_mem_nhdsWithin k apply IsOpen.mem_nhds (by simpa using h'k.smul _) push _ ∈ _ - contrapose! H + contrapose H simpa [mem_smul_set_iff_inv_smul_mem] using H have : 0 < μ (k \ ((z * x⁻¹) • k)) := h z zk _ this exact lt_irrefl _ (C.le.trans_lt this) diff --git a/Mathlib/MeasureTheory/Measure/Haar/Extension.lean b/Mathlib/MeasureTheory/Measure/Haar/Extension.lean index 1ee37893955edd..5b48903ac5d26f 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/Extension.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/Extension.lean @@ -123,7 +123,7 @@ noncomputable def pushforward : · refine ENNReal.toReal_lt_of_lt_ofReal ((setLIntegral_mono measurable_const h).trans_lt ?_) rwa [lintegral_const, restrict_apply_univ] · intro y hy - contrapose! hy + contrapose hy rw [Function.notMem_support, hS htb hy, hS (mem_of_mem_nhds hb) hy, edist_self] } map_add' f g := by ext c diff --git a/Mathlib/MeasureTheory/Measure/Haar/Unique.lean b/Mathlib/MeasureTheory/Measure/Haar/Unique.lean index b40539a128167c..10afcab099b9c8 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/Unique.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/Unique.lean @@ -168,7 +168,7 @@ lemma integral_isMulLeftInvariant_isMulRightInvariant_combo · simp [image_eq_zero_of_notMem_tsupport H] have : g (y⁻¹ * x) = 0 := by apply image_eq_zero_of_notMem_tsupport - contrapose! hxy + contrapose hxy simp only [mem_prod, H, true_and] apply subset_closure simp only [M, mem_image, mem_prod, Prod.exists] @@ -200,7 +200,7 @@ lemma integral_isMulLeftInvariant_isMulRightInvariant_combo · simp [image_eq_zero_of_notMem_tsupport H] have : f (y * x) = 0 := by apply image_eq_zero_of_notMem_tsupport - contrapose! hxy + contrapose hxy simp only [mem_prod, H, true_and] apply subset_closure simp only [M, mem_image, mem_prod, Prod.exists] diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean index 4cb3ccb004b5f6..f179a5ae566126 100644 --- a/Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean +++ b/Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean @@ -117,6 +117,6 @@ theorem integral_comp_abs {f : ℝ → ℝ} : refine setIntegral_congr_fun measurableSet_Iic (fun _ hx => ?_) rw [abs_eq_neg_self.mpr (by exact hx)] · have : ¬ Integrable (fun x => f |x|) := by - contrapose! hf + contrapose hf exact hf.integrableOn rw [← eq, integral_undef hf, integral_undef this, mul_zero] diff --git a/Mathlib/MeasureTheory/Measure/Prod.lean b/Mathlib/MeasureTheory/Measure/Prod.lean index 487fe7fd620c50..8ceecb66a24d8d 100644 --- a/Mathlib/MeasureTheory/Measure/Prod.lean +++ b/Mathlib/MeasureTheory/Measure/Prod.lean @@ -1122,7 +1122,7 @@ theorem fst_map_prodMk₀ {X : α → β} {Y : α → γ} {μ : Measure α} Measure.map_apply_of_aemeasurable hX hs, ← prod_univ, mk_preimage_prod, preimage_univ, inter_univ] · have : ¬AEMeasurable (fun x ↦ (X x, Y x)) μ := by - contrapose! hX + contrapose hX exact measurable_fst.comp_aemeasurable hX simp [map_of_not_aemeasurable, hX, this] @@ -1184,7 +1184,7 @@ theorem snd_map_prodMk₀ {X : α → β} {Y : α → γ} {μ : Measure α} (hX Measure.map_apply_of_aemeasurable hY hs, ← univ_prod, mk_preimage_prod, preimage_univ, univ_inter] · have : ¬AEMeasurable (fun x ↦ (X x, Y x)) μ := by - contrapose! hY + contrapose hY exact measurable_snd.comp_aemeasurable hY simp [map_of_not_aemeasurable, hY, this] diff --git a/Mathlib/ModelTheory/Satisfiability.lean b/Mathlib/ModelTheory/Satisfiability.lean index 9fdf6d1181a384..f0ff75d836b059 100644 --- a/Mathlib/ModelTheory/Satisfiability.lean +++ b/Mathlib/ModelTheory/Satisfiability.lean @@ -305,7 +305,7 @@ theorem models_iff_not_satisfiable (φ : L.Sentence) : T ⊨ᵇ φ ↔ ¬IsSatis (Set.subset_union_right (Set.mem_singleton _))) (h1 (h2.some.subtheoryModel Set.subset_union_left)), fun h M => ?_⟩ - contrapose! h + contrapose h rw [← Sentence.realize_not] at h refine ⟨{ Carrier := M @@ -316,7 +316,7 @@ theorem models_iff_not_satisfiable (φ : L.Sentence) : T ⊨ᵇ φ ↔ ¬IsSatis theorem ModelsBoundedFormula.realize_sentence {φ : L.Sentence} (h : T ⊨ᵇ φ) (M : Type*) [L.Structure M] [M ⊨ T] [Nonempty M] : M ⊨ φ := by rw [models_iff_not_satisfiable] at h - contrapose! h + contrapose h have : M ⊨ T ∪ {Formula.not φ} := by simp only [Set.union_singleton, model_iff, Set.mem_insert_iff, forall_eq_or_imp, Sentence.realize_not] diff --git a/Mathlib/NumberTheory/ArithmeticFunction/LFunction.lean b/Mathlib/NumberTheory/ArithmeticFunction/LFunction.lean index c3e3173b676083..34e5b3be175e68 100644 --- a/Mathlib/NumberTheory/ArithmeticFunction/LFunction.lean +++ b/Mathlib/NumberTheory/ArithmeticFunction/LFunction.lean @@ -124,7 +124,7 @@ noncomputable def ofPowerSeries (q : ℕ) : PowerSeries R →ₐ[R] ArithmeticFu · obtain ⟨k, rfl⟩ := hn simp [(Nat.pow_right_injective hq).extend_apply, one_apply, hq.ne'] · rw [Function.extend_apply' _ _ _ hn, Pi.zero_apply, smul_map, one_apply_ne, smul_zero] - contrapose! hn + contrapose hn exact ⟨0, by simp [hn]⟩ · simp diff --git a/Mathlib/NumberTheory/ArithmeticFunction/Moebius.lean b/Mathlib/NumberTheory/ArithmeticFunction/Moebius.lean index 1a9395ad961cbe..25f147992e3153 100644 --- a/Mathlib/NumberTheory/ArithmeticFunction/Moebius.lean +++ b/Mathlib/NumberTheory/ArithmeticFunction/Moebius.lean @@ -68,7 +68,7 @@ theorem moebius_apply_one : μ 1 = 1 := by simp theorem moebius_ne_zero_iff_squarefree {n : ℕ} : μ n ≠ 0 ↔ Squarefree n := by constructor <;> intro h - · contrapose! h + · contrapose h simp [h] · simp [h] diff --git a/Mathlib/NumberTheory/Bertrand.lean b/Mathlib/NumberTheory/Bertrand.lean index 9e3752f2717234..dc809c44a95dbf 100644 --- a/Mathlib/NumberTheory/Bertrand.lean +++ b/Mathlib/NumberTheory/Bertrand.lean @@ -168,7 +168,7 @@ theorem centralBinom_le_of_no_bertrand_prime (n : ℕ) (n_large : 2 < n) let f x := x ^ n.centralBinom.factorization x have : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x := by refine Finset.prod_filter_of_ne fun p _ h => ?_ - contrapose! h; dsimp only [f] + contrapose h; dsimp only [f] rw [factorization_eq_zero_of_not_prime n.centralBinom h, _root_.pow_zero] rw [centralBinom_factorization_small n n_large no_prime, ← this, ← Finset.prod_filter_mul_prod_filter_not S (· ≤ sqrt (2 * n))] diff --git a/Mathlib/NumberTheory/DirichletCharacter/Basic.lean b/Mathlib/NumberTheory/DirichletCharacter/Basic.lean index 19dacec6f1a25d..86cc33517d7b97 100644 --- a/Mathlib/NumberTheory/DirichletCharacter/Basic.lean +++ b/Mathlib/NumberTheory/DirichletCharacter/Basic.lean @@ -315,7 +315,7 @@ lemma primitiveCharacter_one [NeZero n] : (1 : DirichletCharacter R n).primitive theorem conductor_dvd_of_mem_conductorSet {d : ℕ} [NeZero n] (hd : d ∈ χ.conductorSet) : χ.conductor ∣ d := by have : NeZero d := ⟨by - contrapose! hd + contrapose hd exact hd ▸ zero_ne_mem_conductorSet χ⟩ suffices d.gcd χ.conductor ∈ χ.conductorSet by have : χ.conductor ≤ d.gcd χ.conductor := Nat.sInf_le this diff --git a/Mathlib/NumberTheory/Height/Basic.lean b/Mathlib/NumberTheory/Height/Basic.lean index fce53c8206a860..b2604b01e28d73 100644 --- a/Mathlib/NumberTheory/Height/Basic.lean +++ b/Mathlib/NumberTheory/Height/Basic.lean @@ -170,7 +170,7 @@ lemma logHeight₁_eq (x : K) : rw [mulHeight₁_eq] at H have : ∀ a ∈ archAbsVal.map (fun v ↦ max (v x) 1), a ≠ 0 := by intro a ha - contrapose! ha + contrapose ha rw [ha] exact Multiset.prod_eq_zero_iff.not.mp <| left_ne_zero_of_mul H rw [log_mul (left_ne_zero_of_mul H) (right_ne_zero_of_mul H), log_multiset_prod this, diff --git a/Mathlib/NumberTheory/MahlerMeasure.lean b/Mathlib/NumberTheory/MahlerMeasure.lean index 1126b672cccbec..8241c4d16e1028 100644 --- a/Mathlib/NumberTheory/MahlerMeasure.lean +++ b/Mathlib/NumberTheory/MahlerMeasure.lean @@ -224,7 +224,7 @@ theorem cyclotomic_dvd_of_mahlerMeasure_eq_one (hX : ¬ X ∣ p) (hpdeg : p.degr obtain ⟨z, _⟩ := Splits.exists_eval_eq_zero (IsAlgClosed.splits <| p.map (castRingHom ℂ)) hpdegC have hz₀ : z ≠ 0 := by - contrapose! hX + contrapose hX simp_all [X_dvd_iff, coeff_zero_eq_aeval_zero] have h_z_root : z ∈ p.aroots ℂ := by aesop obtain ⟨m, h_m_pos, h_prim⟩ := isPrimitiveRoot_of_mahlerMeasure_eq_one h hz₀ h_z_root diff --git a/Mathlib/NumberTheory/Modular.lean b/Mathlib/NumberTheory/Modular.lean index ef90aca9f7d417..6968d0831a1add 100644 --- a/Mathlib/NumberTheory/Modular.lean +++ b/Mathlib/NumberTheory/Modular.lean @@ -728,7 +728,7 @@ lemma stabilizer_of_ne (hz : z ∈ 𝒟) (hg : g • z = z) have : T⁻¹ • z ≠ z := by rwa [ne_eq, inv_smul_eq_iff, eq_comm] have : (z : ℂ) ≠ -I := by grind [neg_im, coe_I, Complex.I_im, z.coe_im_pos] have : S • z ≠ z := by - contrapose! hzI + contrapose hzI rw [UpperHalfPlane.ext_iff, modular_S_smul, coe_mk, ← mul_one (_ : ℂ)⁻¹, inv_mul_eq_iff_eq_mul₀ (neg_ne_zero.mpr z.ne_zero), neg_mul, ← neg_eq_iff_eq_neg, ← I_sq, ← sq, sq_eq_sq_iff_eq_or_eq_neg, ← coe_I, ← UpperHalfPlane.ext_iff] at hzI diff --git a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean index 8a536f39c49a1d..9e3b16905ff965 100644 --- a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean +++ b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean @@ -47,7 +47,7 @@ def gammaSet := {v : Fin 2 → ℤ | (↑) ∘ v = a ∧ (v 0).gcd (v 1) = r} open scoped Function in -- required for scoped `on` notation lemma pairwise_disjoint_gammaSet : Pairwise (Disjoint on gammaSet N r) := by refine fun u v huv ↦ ?_ - contrapose! huv + contrapose huv obtain ⟨f, hf⟩ := Set.not_disjoint_iff.mp huv exact hf.1.1.symm.trans hf.2.1 diff --git a/Mathlib/NumberTheory/ModularForms/NormTrace.lean b/Mathlib/NumberTheory/ModularForms/NormTrace.lean index 406cd16c780cdd..965caf37aaf3e5 100644 --- a/Mathlib/NumberTheory/ModularForms/NormTrace.lean +++ b/Mathlib/NumberTheory/ModularForms/NormTrace.lean @@ -122,7 +122,7 @@ protected def ModularForm.norm [ℋ.HasDetPlusMinusOne] [ModularFormClass F 𝒢 variable {f} in lemma ModularForm.norm_ne_zero [ℋ.HasDetPlusMinusOne] [ModularFormClass F 𝒢 k] (hf : (f : ℍ → ℂ) ≠ 0) : ModularForm.norm ℋ f ≠ 0 := by - contrapose! hf + contrapose hf rw [← DFunLike.coe_injective.eq_iff, coe_norm, coe_zero, prod_eq_zero_iff] at hf · simpa [QuotientGroup.exists_mk] using hf · exact Quotient.forall.mpr fun r _ ↦ (translate f r.val⁻¹).holo' diff --git a/Mathlib/NumberTheory/MulChar/Duality.lean b/Mathlib/NumberTheory/MulChar/Duality.lean index 18b2a55c546b93..b16320a20d07df 100644 --- a/Mathlib/NumberTheory/MulChar/Duality.lean +++ b/Mathlib/NumberTheory/MulChar/Duality.lean @@ -41,9 +41,9 @@ instance finite [Finite Mˣ] [IsDomain R] : Finite (MulChar M R) := .of_equiv _ lemma exists_apply_ne_one_iff_exists_monoidHom (a : Mˣ) : (∃ χ : MulChar M R, χ a ≠ 1) ↔ ∃ φ : Mˣ →* Rˣ, φ a ≠ 1 := by refine ⟨fun ⟨χ, hχ⟩ ↦ ⟨χ.toUnitHom, ?_⟩, fun ⟨φ, hφ⟩ ↦ ⟨ofUnitHom φ, ?_⟩⟩ - · contrapose! hχ + · contrapose hχ rwa [Units.ext_iff, coe_toUnitHom] at hχ - · contrapose! hφ + · contrapose hφ simpa only [ofUnitHom_eq, equivToUnitHom_symm_coe, Units.val_eq_one] using hφ variable (M R) @@ -57,7 +57,7 @@ theorem exists_apply_ne_one_of_hasEnoughRootsOfUnity [Nontrivial R] {a : M} (ha by_cases hu : IsUnit a · refine (exists_apply_ne_one_iff_exists_monoidHom hu.unit).mpr ?_ refine CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity Mˣ R ?_ - contrapose! ha + contrapose ha rw [← hu.unit_spec, ha, Units.val_eq_one] · exact ⟨1, by simpa only [map_nonunit _ hu] using zero_ne_one⟩ diff --git a/Mathlib/NumberTheory/Multiplicity.lean b/Mathlib/NumberTheory/Multiplicity.lean index 7f8ae3e1ccd5e9..75eceb399d1a85 100644 --- a/Mathlib/NumberTheory/Multiplicity.lean +++ b/Mathlib/NumberTheory/Multiplicity.lean @@ -307,7 +307,7 @@ theorem Int.two_pow_sub_pow' {x y : ℤ} (n : ℕ) (hxy : 4 ∣ x - y) (hx : ¬2 · simpa only [even_iff_two_dvd] using hx_odd.pow.sub_odd hy_odd.pow · simpa only [even_iff_two_dvd, ← Int.not_even_iff_odd] using hx_odd.pow norm_cast - contrapose! hpn + contrapose hpn rw [pow_succ] conv_rhs => rw [hk] exact mul_dvd_mul_left _ hpn diff --git a/Mathlib/NumberTheory/NumberField/CMField.lean b/Mathlib/NumberTheory/NumberField/CMField.lean index 97a749daefd35f..91832e9ee88db2 100644 --- a/Mathlib/NumberTheory/NumberField/CMField.lean +++ b/Mathlib/NumberTheory/NumberField/CMField.lean @@ -468,7 +468,7 @@ theorem eq_maximalRealSubfield (E : Subfield K) [IsTotallyReal E] [IsQuadraticEx have := ((IntermediateField.isSimpleOrder_of_finrank_prime E K (IsQuadraticExtension.finrank_eq_two E K ▸ Nat.prime_two)).eq_bot_or_eq_top L).resolve_left ?_ · simpa [L] using congr_arg IntermediateField.toSubfield this - · contrapose! h + · contrapose h rw [← SetLike.coe_set_eq, Subfield.coe_toIntermediateField] at h rw [← sup_eq_left, ← SetLike.coe_set_eq, h, IntermediateField.coe_bot] aesop diff --git a/Mathlib/NumberTheory/NumberField/ClassNumber.lean b/Mathlib/NumberTheory/NumberField/ClassNumber.lean index d897f56c59b4f1..edad7fac09958b 100644 --- a/Mathlib/NumberTheory/NumberField/ClassNumber.lean +++ b/Mathlib/NumberTheory/NumberField/ClassNumber.lean @@ -82,7 +82,7 @@ theorem exists_ideal_in_class_of_norm_le (C : ClassGroup (𝓞 K)) : exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr K (FractionalIdeal.mk0 K J) obtain ⟨I₀, hI⟩ := dvd_iff_le.mpr ((span_singleton_le_iff_mem J).mpr (by exact ha)) have : I₀ ≠ 0 := by - contrapose! h_nz + contrapose h_nz rw [h_nz, mul_zero, zero_eq_bot, span_singleton_eq_bot] at hI rw [Algebra.linearMap_apply, hI, map_zero] let I := (⟨I₀, mem_nonZeroDivisors_iff_ne_zero.mpr this⟩ : (Ideal (𝓞 K))⁰) diff --git a/Mathlib/NumberTheory/NumberField/Completion/InfinitePlace.lean b/Mathlib/NumberTheory/NumberField/Completion/InfinitePlace.lean index d7ecfc9f798a98..50c18ccd04ded9 100644 --- a/Mathlib/NumberTheory/NumberField/Completion/InfinitePlace.lean +++ b/Mathlib/NumberTheory/NumberField/Completion/InfinitePlace.lean @@ -151,7 +151,7 @@ theorem isClosed_image_extensionEmbeddingOfIsReal {v : InfinitePlace K} (hv : Is theorem subfield_ne_real_of_isComplex {v : InfinitePlace K} (hv : IsComplex v) : (extensionEmbedding v).fieldRange ≠ Complex.ofRealHom.fieldRange := by - contrapose! hv + contrapose hv simp only [not_isComplex_iff_isReal, isReal_iff] ext x obtain ⟨r, hr⟩ := hv ▸ RingHom.mem_fieldRange_self (extensionEmbedding v) (x : v.Completion) diff --git a/Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean b/Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean index 4de2e92d4e5bc1..cec0529d8c0bf9 100644 --- a/Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean +++ b/Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean @@ -202,7 +202,7 @@ theorem isComplex_iff {w : InfinitePlace K} : IsComplex w ↔ ¬ComplexEmbedding.IsReal (embedding w) := by refine ⟨?_, fun h => ⟨embedding w, h, mk_embedding w⟩⟩ rintro ⟨φ, ⟨hφ, rfl⟩⟩ - contrapose! hφ + contrapose hφ cases mk_eq_iff.mp (mk_embedding (mk φ)) with | inl h => rwa [h] at hφ | inr h => rwa [← ComplexEmbedding.isReal_conjugate_iff, h] at hφ @@ -247,7 +247,7 @@ theorem norm_embedding_of_isReal {w : InfinitePlace K} (hw : IsReal w) (x : K) : @[simp] theorem isReal_of_mk_isReal {φ : K →+* ℂ} (h : IsReal (mk φ)) : ComplexEmbedding.IsReal φ := by - contrapose! h + contrapose h rw [not_isReal_iff_isComplex] exact ⟨φ, h, rfl⟩ diff --git a/Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean b/Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean index 2ad063a9e142f2..a9ba9a5f4335cf 100644 --- a/Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean +++ b/Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean @@ -252,7 +252,7 @@ theorem IsRamified.ne_conjugate {w₁ w₂ : InfinitePlace K} (h : w₂.IsRamifi by_cases h_eq : w₁ = w₂ · rw [isRamified_iff, isComplex_iff] at h exact Ne.symm (h_eq ▸ h.1) - · contrapose! h_eq + · contrapose h_eq rw [← mk_embedding w₁, h_eq, mk_conjugate_eq, mk_embedding] lemma IsRamified.comap_embedding {w : InfinitePlace K} (h : w.IsRamified k) : diff --git a/Mathlib/NumberTheory/Padics/PadicIntegers.lean b/Mathlib/NumberTheory/Padics/PadicIntegers.lean index 49bdfa2e9c67d7..bb26b5291c7eab 100644 --- a/Mathlib/NumberTheory/Padics/PadicIntegers.lean +++ b/Mathlib/NumberTheory/Padics/PadicIntegers.lean @@ -458,7 +458,7 @@ theorem mem_span_pow_iff_le_valuation (x : ℤ_[p]) (hx : x ≠ 0) (n : ℕ) : suffices c ≠ 0 by rw [valuation_p_pow_mul _ _ this] exact le_self_add - contrapose! hx + contrapose hx rw [hx, mul_zero] · nth_rewrite 2 [unitCoeff_spec hx] simpa [Units.isUnit, IsUnit.dvd_mul_left] using pow_dvd_pow _ diff --git a/Mathlib/NumberTheory/Padics/PadicNumbers.lean b/Mathlib/NumberTheory/Padics/PadicNumbers.lean index fa59c5669e7bd3..134d05c71ac54f 100644 --- a/Mathlib/NumberTheory/Padics/PadicNumbers.lean +++ b/Mathlib/NumberTheory/Padics/PadicNumbers.lean @@ -1055,7 +1055,7 @@ theorem norm_eq_zpow_neg_valuation {x : ℚ_[p]} : x ≠ 0 → ‖x‖ = (p : rw [PadicSeq.norm_eq_zpow_neg_valuation] · rw [Rat.cast_zpow, Rat.cast_natCast] · apply CauSeq.not_limZero_of_not_congr_zero - contrapose! hf + contrapose hf apply Quotient.sound simpa using hf diff --git a/Mathlib/NumberTheory/PythagoreanTriples.lean b/Mathlib/NumberTheory/PythagoreanTriples.lean index 40eb1cb34ada09..b48468311a88ab 100644 --- a/Mathlib/NumberTheory/PythagoreanTriples.lean +++ b/Mathlib/NumberTheory/PythagoreanTriples.lean @@ -438,7 +438,7 @@ theorem isPrimitiveClassified_of_coprime_of_odd_of_pos (hc : Int.gcd x y = 1) (h norm_cast have hvz : v ≠ 0 := by simp [field, v, -mul_eq_zero, -div_eq_zero_iff, h0] have hw1 : w ≠ -1 := by - contrapose! hvz with hw1 + contrapose hvz with hw1 rw [hw1, neg_sq, one_pow, add_eq_right] at hq exact eq_zero_of_pow_eq_zero hq have hQ : ∀ x : ℚ, 1 + x ^ 2 ≠ 0 := by diff --git a/Mathlib/NumberTheory/RamificationInertia/Basic.lean b/Mathlib/NumberTheory/RamificationInertia/Basic.lean index 3647094d89385b..a46d9cf0cc38cb 100644 --- a/Mathlib/NumberTheory/RamificationInertia/Basic.lean +++ b/Mathlib/NumberTheory/RamificationInertia/Basic.lean @@ -189,7 +189,7 @@ theorem FinrankQuotientMap.linearIndependent_of_nontrivial [IsDedekindDomain R] (hRS : RingHom.ker (algebraMap R S) ≠ ⊤) (F : V'' →ₗ[R] V) (hf : Function.Injective F) (f' : V'' →ₗ[R] V') {ι : Type*} {b : ι → V''} (hb' : LinearIndependent S (f' ∘ b)) : LinearIndependent K (F ∘ b) := by - contrapose! hb' with hb + contrapose hb' with hb -- Informally, if we have a nontrivial linear dependence with coefficients `g` in `K`, -- then we can find a linear dependence with coefficients `I.Quotient.mk g'` in `R/I`, -- where `I = ker (algebraMap R S)`. diff --git a/Mathlib/NumberTheory/RatFunc/Ostrowski.lean b/Mathlib/NumberTheory/RatFunc/Ostrowski.lean index 08ff29932ebd25..0a87f87db92b13 100644 --- a/Mathlib/NumberTheory/RatFunc/Ostrowski.lean +++ b/Mathlib/NumberTheory/RatFunc/Ostrowski.lean @@ -40,7 +40,7 @@ lemma valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X {f : RatFunc | f p q hq => rw [intDegree_div (by grind only) (by grind only), v.map_div, zpow_sub₀ (ne_zero_of_lt hlt)] simp_rw [intDegree_polynomial, zpow_natCast, ← coePolynomial_eq_algebraMap] - have hp : p ≠ 0 := by contrapose! hf; simp [hf] + have hp : p ≠ 0 := by contrapose hf; simp [hf] rw [valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X _ hlt hp, valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X _ hlt hq] diff --git a/Mathlib/Order/Cofinal.lean b/Mathlib/Order/Cofinal.lean index c310ca77de8774..bb75e366ea630b 100644 --- a/Mathlib/Order/Cofinal.lean +++ b/Mathlib/Order/Cofinal.lean @@ -145,7 +145,7 @@ theorem BddAbove.of_not_isCofinal {s : Set α} (h : ¬ IsCofinal s) : BddAbove s exact ⟨x, fun y hy ↦ (h y hy).le⟩ theorem IsCofinal.of_not_bddAbove {s : Set α} (h : ¬ BddAbove s) : IsCofinal s := by - contrapose! h + contrapose h exact .of_not_isCofinal h /-- In a linear order with no maximum, cofinal sets are the same as unbounded sets. -/ diff --git a/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean b/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean index 4ffb5feb1ed40b..8da4d06f32a1fe 100644 --- a/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean +++ b/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean @@ -419,7 +419,7 @@ theorem csInf_lt_iff (hb : BddBelow s) (hs : s.Nonempty) : sInf s < a ↔ ∃ b lemma csSup_eq_univ_of_not_bddAbove (hs : ¬BddAbove s) : sSup s = sSup univ := by rw [csSup_of_not_bddAbove hs, csSup_of_not_bddAbove (s := univ)] - contrapose! hs + contrapose hs exact hs.mono (subset_univ _) lemma ciSup_eq_univ_of_not_bddAbove (hf : ¬BddAbove (range f)) : ⨆ i, f i = sSup univ := diff --git a/Mathlib/Order/Filter/Map.lean b/Mathlib/Order/Filter/Map.lean index 099b49d4a775e0..00411c48b6d246 100644 --- a/Mathlib/Order/Filter/Map.lean +++ b/Mathlib/Order/Filter/Map.lean @@ -442,7 +442,7 @@ theorem comap_bot : comap m ⊥ = ⊥ := theorem neBot_of_comap (h : (comap m g).NeBot) : g.NeBot := by rw [neBot_iff] at * - contrapose! h + contrapose h rw [h] exact comap_bot diff --git a/Mathlib/Order/Partition/Basic.lean b/Mathlib/Order/Partition/Basic.lean index 9e27a5acfbf5a9..886c32b71e9842 100644 --- a/Mathlib/Order/Partition/Basic.lean +++ b/Mathlib/Order/Partition/Basic.lean @@ -214,7 +214,7 @@ lemma existsUnique_of_mem_le (h : P ≤ Q) (hx : x ∈ P) : obtain ⟨y, hy, hxy⟩ := h hx refine ⟨y, ⟨hy, hxy⟩, fun z ⟨hz, hxz⟩ => Q.eq_of_not_disjoint hz hy ?_⟩ have := P.ne_bot_of_mem hx - contrapose! this + contrapose this exact le_bot_iff.mp (this hxz hxy) /-- The top partition of `s` is the partition with the single part `s`. -/ diff --git a/Mathlib/Order/PrimeSeparator.lean b/Mathlib/Order/PrimeSeparator.lean index 4033aa645095a6..33aac280ab96f3 100644 --- a/Mathlib/Order/PrimeSeparator.lean +++ b/Mathlib/Order/PrimeSeparator.lean @@ -120,7 +120,7 @@ theorem prime_ideal_of_disjoint_filter_ideal (hFI : Disjoint (F : Set α) (I : S have ba₁a₂F : b ⊔ (a₁ ⊓ a₂) ∈ F := PFilter.mem_of_le ineq (PFilter.inf_mem c₁F c₂F) -- Now, if we would have a₁ ⊓ a₂ ∈ J, then, since J is an ideal and b ∈ J, we would also get -- b ⊔ (a₁ ⊓ a₂) ∈ J. But this contradicts that J is disjoint from F. - contrapose! JF with ha₁a₂ + contrapose JF with ha₁a₂ rw [Set.not_disjoint_iff] use b ⊔ (a₁ ⊓ a₂) exact ⟨ba₁a₂F, sup_mem bJ ha₁a₂⟩ diff --git a/Mathlib/Order/SuccPred/Archimedean.lean b/Mathlib/Order/SuccPred/Archimedean.lean index f76ad099596d09..d406b48db35a82 100644 --- a/Mathlib/Order/SuccPred/Archimedean.lean +++ b/Mathlib/Order/SuccPred/Archimedean.lean @@ -247,7 +247,7 @@ lemma SuccOrder.forall_ne_bot_iff (∀ i, i ≠ ⊥ → P i) ↔ (∀ i, P (SuccOrder.succ i)) := by refine ⟨fun h i ↦ h _ (Order.succ_ne_bot i), fun h i hi ↦ ?_⟩ obtain ⟨j, rfl⟩ := exists_succ_iterate_of_le (bot_le : ⊥ ≤ i) - have hj : 0 < j := by apply Nat.pos_of_ne_zero; contrapose! hi; simp [hi] + have hj : 0 < j := by apply Nat.pos_of_ne_zero; contrapose hi; simp [hi] rw [← Nat.succ_pred_eq_of_pos hj] simp only [Function.iterate_succ', Function.comp_apply] apply h diff --git a/Mathlib/Order/SuccPred/IntervalSucc.lean b/Mathlib/Order/SuccPred/IntervalSucc.lean index 08e30747f85a75..aef822576df67e 100644 --- a/Mathlib/Order/SuccPred/IntervalSucc.lean +++ b/Mathlib/Order/SuccPred/IntervalSucc.lean @@ -40,7 +40,7 @@ theorem biUnion_Ici_Ico_map_succ [SuccOrder α] [IsSuccArchimedean α] [LinearOr apply subset_antisymm <| iUnion₂_subset fun i hi ↦ Ico_subset_Ico_left (hf i hi) |>.trans Ico_subset_Ici_self intro b hb - contrapose! h2f + contrapose h2f use b simp only [upperBounds, mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] exact Succ.rec (P := fun i _ ↦ f i ≤ b) hb (by simp_all) @@ -53,7 +53,7 @@ theorem biUnion_Ici_Ioc_map_succ [SuccOrder α] [IsSuccArchimedean α] [LinearOr apply subset_antisymm <| iUnion₂_subset fun i hi ↦ Ioc_subset_Ioc_left (hf i hi) |>.trans Ioc_subset_Ioi_self intro b hb - contrapose! h2f + contrapose h2f suffices ∀ i, a ≤ i → f i < b from ⟨b, by aesop (add simp [upperBounds, le_of_lt])⟩ exact Succ.rec (P := fun i _ ↦ f i < b) hb (by simp_all) diff --git a/Mathlib/Order/SuccPred/Tree.lean b/Mathlib/Order/SuccPred/Tree.lean index cb6dccb7be2ab5..4a01e31ae22cf1 100644 --- a/Mathlib/Order/SuccPred/Tree.lean +++ b/Mathlib/Order/SuccPred/Tree.lean @@ -196,7 +196,7 @@ lemma RootedTree.mem_subtrees_disjoint_iff {t₁ t₂ : SubRootedTree t} exact t₁.root_ne_bot_of_mem_subtrees ht₁ this mpr h := by rw [SubRootedTree.mem_iff] at h₁ h₂ - contrapose! h + contrapose h rw [disjoint_iff, ← ne_eq, ← bot_lt_iff_ne_bot] at h rcases lt_or_le_of_directed (by simp : v₁ ⊓ v₂ ≤ v₁) h₁ with oh | oh · simp_all [RootedTree.subtrees, IsAtom.lt_iff] diff --git a/Mathlib/Probability/Density.lean b/Mathlib/Probability/Density.lean index 656f5b69b194ee..1e01e3122c18be 100644 --- a/Mathlib/Probability/Density.lean +++ b/Mathlib/Probability/Density.lean @@ -139,14 +139,14 @@ theorem pdf_of_not_haveLebesgueDecomposition {_ : MeasurableSpace Ω} {ℙ : Mea theorem aemeasurable_of_pdf_ne_zero {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} (X : Ω → E) (h : ¬pdf X ℙ μ =ᵐ[μ] 0) : AEMeasurable X ℙ := by - contrapose! h + contrapose h exact pdf_of_not_aemeasurable h theorem hasPDF_of_pdf_ne_zero {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} {X : Ω → E} (hac : map X ℙ ≪ μ) (hpdf : ¬pdf X ℙ μ =ᵐ[μ] 0) : HasPDF X ℙ μ := by refine ⟨?_, ?_, hac⟩ · exact aemeasurable_of_pdf_ne_zero X hpdf - · contrapose! hpdf + · contrapose hpdf have := pdf_of_not_haveLebesgueDecomposition hpdf filter_upwards using congrFun this diff --git a/Mathlib/Probability/Kernel/Basic.lean b/Mathlib/Probability/Kernel/Basic.lean index b1098ee54922a5..ebb76243496389 100644 --- a/Mathlib/Probability/Kernel/Basic.lean +++ b/Mathlib/Probability/Kernel/Basic.lean @@ -411,7 +411,7 @@ lemma exists_ae_eq_isMarkovKernel {μ : Measure α} refine ⟨toMeasurable μ {a | ¬ IsProbabilityMeasure (κ a)}, measurableSet_toMeasurable _ _, by simpa [measure_toMeasurable] using h, ?_⟩ intro a ha - contrapose! ha + contrapose ha exact subset_toMeasurable _ _ ha obtain ⟨a, ha⟩ : sᶜ.Nonempty := by contrapose! h'; simpa [μs, h'] using measure_univ_le_add_compl s (μ := μ) diff --git a/Mathlib/Probability/Kernel/Composition/MapComap.lean b/Mathlib/Probability/Kernel/Composition/MapComap.lean index d99d07d86f0cb6..d639924e23fab4 100644 --- a/Mathlib/Probability/Kernel/Composition/MapComap.lean +++ b/Mathlib/Probability/Kernel/Composition/MapComap.lean @@ -457,7 +457,7 @@ lemma fst_map_prod (κ : Kernel α β) {f : β → γ} {g : β → δ} (hg : Mea · simp only [Set.preimage, Set.mem_setOf] · exact measurable_fst hs · have : ¬ Measurable (fun x ↦ (f x, g x)) := by - contrapose! hf; exact hf.fst + contrapose hf; exact hf.fst simp [map_of_not_measurable _ hf, map_of_not_measurable _ this] lemma fst_map_id_prod (κ : Kernel α β) {f : β → γ} (hf : Measurable f) : @@ -519,7 +519,7 @@ lemma snd_map_prod (κ : Kernel α β) {f : β → γ} {g : β → δ} (hf : Mea · simp only [Set.preimage, Set.mem_setOf] · exact measurable_snd hs · have : ¬ Measurable (fun x ↦ (f x, g x)) := by - contrapose! hg; exact hg.snd + contrapose hg; exact hg.snd simp [map_of_not_measurable _ hg, map_of_not_measurable _ this] lemma snd_map_prod_id (κ : Kernel α β) {f : β → γ} (hf : Measurable f) : diff --git a/Mathlib/Probability/Kernel/CondDistrib.lean b/Mathlib/Probability/Kernel/CondDistrib.lean index 3a8c1ba8d3f380..60cbf03ca84038 100644 --- a/Mathlib/Probability/Kernel/CondDistrib.lean +++ b/Mathlib/Probability/Kernel/CondDistrib.lean @@ -410,7 +410,7 @@ theorem _root_.MeasureTheory.AEStronglyMeasurable.comp_snd_map_prodMk {Ω F} {m · exact measurable_snd hs · rw [Measure.map_of_not_aemeasurable] · simp - · contrapose! hX; exact measurable_fst.comp_aemeasurable hX + · contrapose hX; exact measurable_fst.comp_aemeasurable hX theorem _root_.MeasureTheory.Integrable.comp_snd_map_prodMk {Ω} {mΩ : MeasurableSpace Ω} (X : Ω → β) {μ : Measure Ω} {f : Ω → F} (hf_int : Integrable f μ) : @@ -422,7 +422,7 @@ theorem _root_.MeasureTheory.Integrable.comp_snd_map_prodMk exact hf_int.2 · rw [Measure.map_of_not_aemeasurable] · simp - · contrapose! hX; exact measurable_fst.comp_aemeasurable hX + · contrapose hX; exact measurable_fst.comp_aemeasurable hX theorem aestronglyMeasurable_comp_snd_map_prodMk_iff {Ω F} {_ : MeasurableSpace Ω} [TopologicalSpace F] {X : Ω → β} {μ : Measure Ω} (hX : Measurable X) {f : Ω → F} : diff --git a/Mathlib/Probability/Kernel/Disintegration/Basic.lean b/Mathlib/Probability/Kernel/Disintegration/Basic.lean index 1d7e289ce314eb..0dd09d494ad4cf 100644 --- a/Mathlib/Probability/Kernel/Disintegration/Basic.lean +++ b/Mathlib/Probability/Kernel/Disintegration/Basic.lean @@ -63,7 +63,7 @@ variable [ρ.IsCondKernel ρCond] lemma disintegrate : ρ.fst ⊗ₘ ρCond = ρ := IsCondKernel.disintegrate lemma IsCondKernel.isSFiniteKernel (hρ : ρ ≠ 0) : IsSFiniteKernel ρCond := by - contrapose! hρ; rwa [← ρ.disintegrate ρCond, Measure.compProd_of_not_isSFiniteKernel] + contrapose hρ; rwa [← ρ.disintegrate ρCond, Measure.compProd_of_not_isSFiniteKernel] variable [IsFiniteMeasure ρ] diff --git a/Mathlib/Probability/Martingale/OptionalSampling.lean b/Mathlib/Probability/Martingale/OptionalSampling.lean index 961147f7d106b5..06b2a90e3cdc2c 100644 --- a/Mathlib/Probability/Martingale/OptionalSampling.lean +++ b/Mathlib/Probability/Martingale/OptionalSampling.lean @@ -70,7 +70,7 @@ theorem condExp_stopping_time_ae_eq_restrict_eq_const_of_le_const (h : Martingal · suffices {x : Ω | τ x = i} = ∅ by simp [this]; norm_cast ext1 x simp only [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false] - contrapose! hin + contrapose hin exact_mod_cast hin ▸ hτ_le x variable [Nonempty ι] diff --git a/Mathlib/Probability/Moments/CovarianceBilin.lean b/Mathlib/Probability/Moments/CovarianceBilin.lean index a4b52c07c15b0a..5da2e1c05237ba 100644 --- a/Mathlib/Probability/Moments/CovarianceBilin.lean +++ b/Mathlib/Probability/Moments/CovarianceBilin.lean @@ -136,7 +136,7 @@ lemma covarianceBilin_map_const_add [CompleteSpace E] [IsProbabilityMeasure μ] · ext rw [covarianceBilin_of_not_memLp, covarianceBilin_of_not_memLp h] rw [(measurableEmbedding_addLeft _).memLp_map_measure_iff.not] - contrapose! h + contrapose h convert (memLp_const (-c)).add h ext; simp diff --git a/Mathlib/Probability/Moments/CovarianceBilinDual.lean b/Mathlib/Probability/Moments/CovarianceBilinDual.lean index 7a04df4f77b5bc..0f07dd3368cba0 100644 --- a/Mathlib/Probability/Moments/CovarianceBilinDual.lean +++ b/Mathlib/Probability/Moments/CovarianceBilinDual.lean @@ -270,7 +270,7 @@ lemma _root_.MeasureTheory.memLp_id_of_self_sub_integral {p : ℝ≥0∞} apply (integrable_norm_rpow_iff (by fun_prop) hp0 hptop).1 have I : Integrable (fun (x : E) ↦ ‖x‖) μ := by apply Integrable.norm - contrapose! hx + contrapose hx exact integral_undef hx have := (h_Lp.integrable_norm_rpow hp0 hptop).const_mul (2 ^ p.toReal) apply (((I.const_mul (2 * ‖c‖ ^ (p.toReal - 1))).add this)).mono' (by fun_prop) @@ -308,7 +308,7 @@ lemma covarianceBilinDual_of_not_memLp' (h : ¬ MemLp (fun x ↦ x - ∫ y, y lemma covarianceBilinDual_of_not_memLp (h : ¬ MemLp id 2 μ) (L₁ L₂ : StrongDual ℝ E) : covarianceBilinDual μ L₁ L₂ = 0 := by apply covarianceBilinDual_of_not_memLp' - contrapose! h + contrapose h exact memLp_id_of_self_sub_integral h @[simp] diff --git a/Mathlib/Probability/Moments/Variance.lean b/Mathlib/Probability/Moments/Variance.lean index eec6b11abcd6df..7ecc3e14f1d84e 100644 --- a/Mathlib/Probability/Moments/Variance.lean +++ b/Mathlib/Probability/Moments/Variance.lean @@ -134,7 +134,7 @@ lemma variance_of_not_memLp [IsFiniteMeasure μ] (hX : AEStronglyMeasurable X μ lemma memLp_two_of_variance_ne_zero [IsFiniteMeasure μ] (hX : AEStronglyMeasurable X μ) (h : Var[X; μ] ≠ 0) : MemLp X 2 μ := by - contrapose! h + contrapose h exact variance_of_not_memLp hX h theorem ofReal_variance [IsFiniteMeasure μ] (hX : MemLp X 2 μ) : diff --git a/Mathlib/RepresentationTheory/FiniteIndex.lean b/Mathlib/RepresentationTheory/FiniteIndex.lean index ef2494695f817b..edcd99bb921ce7 100644 --- a/Mathlib/RepresentationTheory/FiniteIndex.lean +++ b/Mathlib/RepresentationTheory/FiniteIndex.lean @@ -162,7 +162,7 @@ lemma indToCoind_coindToInd : A.coindToInd ∘ₗ A.indToCoind = LinearMap.id := rw [coindToInd_of_support_subset_orbit g] · simp · intro x hx - contrapose! hx + contrapose hx simpa using indToCoindAux_of_not_rel g x a hx /-- Let `S ≤ G` be a finite index subgroup, `g₁, ..., gₙ` a set of right coset representatives of diff --git a/Mathlib/RingTheory/Algebraic/Basic.lean b/Mathlib/RingTheory/Algebraic/Basic.lean index 08ce307a2f1cd2..d8786723e0bf6c 100644 --- a/Mathlib/RingTheory/Algebraic/Basic.lean +++ b/Mathlib/RingTheory/Algebraic/Basic.lean @@ -120,7 +120,7 @@ theorem Algebra.isAlgebraic_of_not_injective (h : ¬ Function.Injective (algebra theorem Algebra.injective_of_transcendental [h : Algebra.Transcendental R A] : Function.Injective (algebraMap R A) := by rw [transcendental_iff_not_isAlgebraic] at h - contrapose! h + contrapose h exact isAlgebraic_of_not_injective h end diff --git a/Mathlib/RingTheory/Algebraic/Integral.lean b/Mathlib/RingTheory/Algebraic/Integral.lean index 0117efb5d15c50..013f62c2144576 100644 --- a/Mathlib/RingTheory/Algebraic/Integral.lean +++ b/Mathlib/RingTheory/Algebraic/Integral.lean @@ -123,7 +123,7 @@ theorem transcendental_aeval_iff {r : A} {f : K[X]} : Transcendental K (Polynomial.aeval r f) ↔ Transcendental K r ∧ Transcendental K f := by refine ⟨fun h ↦ ⟨?_, h.of_aeval⟩, fun ⟨h1, h2⟩ ↦ h1.aeval_of_transcendental h2⟩ rw [Transcendental] at h ⊢ - contrapose! h + contrapose h rw [isAlgebraic_iff_isIntegral] at h ⊢ exact .of_mem_of_fg _ h.fg_adjoin_singleton _ (aeval_mem_adjoin_singleton _ _) diff --git a/Mathlib/RingTheory/Algebraic/MvPolynomial.lean b/Mathlib/RingTheory/Algebraic/MvPolynomial.lean index 338dc1662ab3fd..1eca307e7f69aa 100644 --- a/Mathlib/RingTheory/Algebraic/MvPolynomial.lean +++ b/Mathlib/RingTheory/Algebraic/MvPolynomial.lean @@ -82,7 +82,7 @@ theorem transcendental_supported_polynomial_aeval_X_iff i ∉ s ∧ Transcendental R f := by refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨h, hf⟩ ↦ transcendental_supported_polynomial_aeval_X R h hf⟩ · rw [Transcendental] at h - contrapose! h + contrapose h refine isAlgebraic_algebraMap (⟨Polynomial.aeval (X i) f, ?_⟩ : supported R s) exact Algebra.adjoin_mono (Set.singleton_subset_iff.2 (Set.mem_image_of_mem _ h)) (Polynomial.aeval_mem_adjoin_singleton _ _) diff --git a/Mathlib/RingTheory/Artinian/Module.lean b/Mathlib/RingTheory/Artinian/Module.lean index 3ac44944cc6451..d478653c67316d 100644 --- a/Mathlib/RingTheory/Artinian/Module.lean +++ b/Mathlib/RingTheory/Artinian/Module.lean @@ -161,7 +161,7 @@ open Function /-- Any injective endomorphism of an Artinian module is surjective. -/ theorem surjective_of_injective_endomorphism (f : M →ₗ[R] M) (s : Injective f) : Surjective f := by - have h := ‹IsArtinian R M›; contrapose! h + have h := ‹IsArtinian R M›; contrapose h rw [IsArtinian, WellFoundedLT, isWellFounded_iff] refine (RelEmbedding.natGT (LinearMap.range <| f ^ ·) ?_).not_wellFounded intro n diff --git a/Mathlib/RingTheory/ClassGroup.lean b/Mathlib/RingTheory/ClassGroup.lean index 64eb77aa65bbfc..d39be3cd05f639 100644 --- a/Mathlib/RingTheory/ClassGroup.lean +++ b/Mathlib/RingTheory/ClassGroup.lean @@ -293,7 +293,7 @@ theorem ClassGroup.mk0_eq_mk0_iff [IsDedekindDomain R] {I J : (Ideal R)⁰} : · rintro ⟨x, y, hx, hy, h⟩ have hy' : y ∈ R⁰ := mem_nonZeroDivisors_iff_ne_zero.mpr hy refine ⟨IsLocalization.mk' _ x ⟨y, hy'⟩, ?_, ?_⟩ - · contrapose! hx + · contrapose hx rwa [mk'_eq_iff_eq_mul, zero_mul, ← (algebraMap R (FractionRing R)).map_zero, (IsFractionRing.injective R (FractionRing R)).eq_iff] at hx · exact (FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal _ hy').mpr h diff --git a/Mathlib/RingTheory/DedekindDomain/Different.lean b/Mathlib/RingTheory/DedekindDomain/Different.lean index f76cbabd874ec9..66c2af83650970 100644 --- a/Mathlib/RingTheory/DedekindDomain/Different.lean +++ b/Mathlib/RingTheory/DedekindDomain/Different.lean @@ -929,12 +929,12 @@ theorem not_dvd_differentIdeal_iff · rw [Algebra.isUnramifiedAt_iff_map_eq (p := P.under A)] constructor · suffices Algebra.IsSeparable (A ⧸ P.under A) (B ⧸ P) by infer_instance - contrapose! H + contrapose H exact dvd_differentIdeal_of_not_isSeparable A hp P H · rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff hPbot Ideal.map_comap_le] apply Ideal.ramificationIdx_spec · simp [Ideal.map_le_iff_le_comap] - · contrapose! H + · contrapose H rw [← pow_one P, show 1 = 2 - 1 by simp] apply pow_sub_one_dvd_differentIdeal _ _ _ hp simpa [Ideal.dvd_iff_le] using H diff --git a/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean b/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean index a2b234c7a502c2..7075dea9501b7b 100644 --- a/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean +++ b/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean @@ -764,7 +764,7 @@ theorem Ideal.count_associates_eq' (Associates.mk (span {x})).count (Associates.mk (span {a})).factors = n := by obtain ⟨q, hq⟩ := hle apply Ideal.count_associates_eq hx _ hq - contrapose! hlt with hdvd + contrapose hlt with hdvd obtain ⟨q', hq'⟩ := hdvd use q' rw [hq, hq'] diff --git a/Mathlib/RingTheory/DualNumber.lean b/Mathlib/RingTheory/DualNumber.lean index 700a6d70de45c3..b713af1231514a 100644 --- a/Mathlib/RingTheory/DualNumber.lean +++ b/Mathlib/RingTheory/DualNumber.lean @@ -116,7 +116,7 @@ lemma ideal_trichotomy [DivisionRing K] (I : Ideal K[ε]) : have : ε * r = (fst r) • ε := by ext <;> simp rw [this] at hxI hx0 ⊢ have hr : fst r ≠ 0 := by - contrapose! hx0 + contrapose hx0 simp [hx0] refine ⟨r⁻¹, ?_⟩ simp [TrivSqZeroExt.ext_iff, inv_mul_cancel₀ hr] diff --git a/Mathlib/RingTheory/FractionalIdeal/Extended.lean b/Mathlib/RingTheory/FractionalIdeal/Extended.lean index abec5ebf7f5bd3..c61c8e7eac45d4 100644 --- a/Mathlib/RingTheory/FractionalIdeal/Extended.lean +++ b/Mathlib/RingTheory/FractionalIdeal/Extended.lean @@ -212,14 +212,14 @@ theorem coe_extendedHomₐ_eq_span (I : FractionalIdeal A⁰ K) : rfl theorem le_one_of_extendedHomₐ_le_one [IsIntegrallyClosed A] [IsIntegrallyClosed B] - (hI : extendedHomₐ L B I ≤ 1) : I ≤ 1 := by - contrapose! hI + (hI : extendedHomₐ L B I ≤ 1) : I ≤ 1 := by + contrapose hI rw [SetLike.not_le_iff_exists] at hI ⊢ obtain ⟨x, hx₁, hx₂⟩ := hI refine ⟨algebraMap K L x, ?_, ?_⟩ · simpa [← FractionalIdeal.mem_coe, IsLocalization.algebraMap_eq_map_map_submonoid A⁰ B K L] using subset_span <| Set.mem_image_of_mem _ hx₁ - · contrapose! hx₂ + · contrapose hx₂ rw [mem_one_iff, ← IsIntegrallyClosed.isIntegral_iff] at hx₂ ⊢ exact IsIntegral.tower_bot_of_field <| isIntegral_trans _ hx₂ diff --git a/Mathlib/RingTheory/FractionalIdeal/Operations.lean b/Mathlib/RingTheory/FractionalIdeal/Operations.lean index 021f1b055b1636..850d72496b7d4f 100644 --- a/Mathlib/RingTheory/FractionalIdeal/Operations.lean +++ b/Mathlib/RingTheory/FractionalIdeal/Operations.lean @@ -297,7 +297,7 @@ theorem exists_ne_zero_mem_isInteger [Nontrivial R] (hI : I ≠ 0) : theorem map_ne_zero [Nontrivial R] (hI : I ≠ 0) : I.map h ≠ 0 := by obtain ⟨x, x_ne_zero, hx⟩ := exists_ne_zero_mem_isInteger hI - contrapose! x_ne_zero with map_eq_zero + contrapose x_ne_zero with map_eq_zero refine IsFractionRing.to_map_eq_zero_iff.mp (eq_zero_iff.mp map_eq_zero _ (mem_map.mpr ?_)) exact ⟨algebraMap R K x, hx, h.commutes x⟩ diff --git a/Mathlib/RingTheory/HahnSeries/Basic.lean b/Mathlib/RingTheory/HahnSeries/Basic.lean index ab3d2de2bfdf0d..790f74e9cfa765 100644 --- a/Mathlib/RingTheory/HahnSeries/Basic.lean +++ b/Mathlib/RingTheory/HahnSeries/Basic.lean @@ -454,7 +454,7 @@ theorem embDomain_coeff {f : Γ ↪o Γ'} {x : R⟦Γ⟧} {a : Γ} : · rw [dif_pos (Set.mem_image_of_mem f ha)] exact congr rfl (f.injective (Classical.choose_spec (Set.mem_image_of_mem f ha)).2) · rw [dif_neg, Classical.not_not.1 fun c => ha ((mem_support _ _).2 c)] - contrapose! ha + contrapose ha obtain ⟨b, hb1, hb2⟩ := (Set.mem_image _ _ _).1 ha rwa [f.injective hb2] at hb1 diff --git a/Mathlib/RingTheory/HahnSeries/Binomial.lean b/Mathlib/RingTheory/HahnSeries/Binomial.lean index ef8f1c2cd91936..46ec61006315cc 100644 --- a/Mathlib/RingTheory/HahnSeries/Binomial.lean +++ b/Mathlib/RingTheory/HahnSeries/Binomial.lean @@ -117,7 +117,7 @@ theorem coeff_toOrderTopSubOnePos_pow {g : Γ} (hg : 0 < g) (r s : R) (k : ℕ) intro n hn rw [binomialFamily_apply, add_sub_cancel_left, coeff_smul, single_pow, coeff_single_of_ne, smul_zero] - · contrapose! hn + · contrapose hn apply (StrictMono.injective (nsmul_left_strictMono hg)) hn.symm · by_cases hr : r = 0 <;> simp [hr, hg] diff --git a/Mathlib/RingTheory/HahnSeries/Lex.lean b/Mathlib/RingTheory/HahnSeries/Lex.lean index 43648c8219e500..24fc842b4477a6 100644 --- a/Mathlib/RingTheory/HahnSeries/Lex.lean +++ b/Mathlib/RingTheory/HahnSeries/Lex.lean @@ -408,7 +408,7 @@ def embDomainOrderEmbedding [Zero R] : Lex R⟦Γ⟧ ↪o Lex R⟦Γ'⟧ where constructor · rintro (⟨i, hj, hi⟩ | heq) · have himem : i ∈ Set.range f := by - contrapose! hi + contrapose hi simp [embDomain_notin_range hi] obtain ⟨k, rfl⟩ := himem refine Or.inl ⟨k, fun j hjk ↦ ?_, by simpa using hi⟩ diff --git a/Mathlib/RingTheory/HahnSeries/Summable.lean b/Mathlib/RingTheory/HahnSeries/Summable.lean index 2abf8b35259c8b..1428aafab18e6d 100644 --- a/Mathlib/RingTheory/HahnSeries/Summable.lean +++ b/Mathlib/RingTheory/HahnSeries/Summable.lean @@ -581,7 +581,7 @@ def ofFinsupp (f : α →₀ R⟦Γ⟧) : SummableFamily Γ R α where finite_co_support' g := by refine f.support.finite_toSet.subset fun a ha => ?_ simp only [mem_coe, Finsupp.mem_support_iff, Ne] - contrapose! ha + contrapose ha simp [ha] @[simp] @@ -596,7 +596,7 @@ theorem hsum_ofFinsupp {f : α →₀ R⟦Γ⟧} : (ofFinsupp f).hsum = f.sum fu rw [map_sum, finsum_eq_sum_of_support_subset] intro x h simp only [mem_coe, Finsupp.mem_support_iff, Ne] - contrapose! h + contrapose h simp [h] end OfFinsupp diff --git a/Mathlib/RingTheory/Henselian.lean b/Mathlib/RingTheory/Henselian.lean index 063af0fa8d9eef..7ca21e2494141e 100644 --- a/Mathlib/RingTheory/Henselian.lean +++ b/Mathlib/RingTheory/Henselian.lean @@ -144,7 +144,7 @@ theorem HenselianLocalRing.TFAE (R : Type u) [CommRing R] [IsLocalRing R] : have H := HenselianLocalRing.is_henselian f hf a₀ simp only [← ker_eq_maximalIdeal φ hφ, eval₂_at_apply, RingHom.mem_ker] at H h₁ h₂ obtain ⟨a, ha₁, ha₂⟩ := H h₁ (by - contrapose! h₂ + contrapose h₂ rwa [← mem_nonunits_iff, ← mem_maximalIdeal, ← ker_eq_maximalIdeal φ hφ, RingHom.mem_ker] at h₂) refine ⟨a, ha₁, ?_⟩ @@ -160,7 +160,7 @@ instance (R : Type*) [CommRing R] [hR : HenselianLocalRing R] : is_henselian := by intro f hf a₀ h₁ h₂ refine HenselianLocalRing.is_henselian f hf a₀ h₁ ?_ - contrapose! h₂ + contrapose h₂ rw [← mem_nonunits_iff, ← IsLocalRing.mem_maximalIdeal, ← Ideal.Quotient.eq_zero_iff_mem] at h₂ rw [h₂] exact not_isUnit_zero diff --git a/Mathlib/RingTheory/Ideal/Basic.lean b/Mathlib/RingTheory/Ideal/Basic.lean index f20ae5688482cf..2d538798e3794b 100644 --- a/Mathlib/RingTheory/Ideal/Basic.lean +++ b/Mathlib/RingTheory/Ideal/Basic.lean @@ -270,7 +270,7 @@ theorem exists_maximal_of_not_isField [Nontrivial R] (h : ¬ IsField R) : theorem not_isField_of_ne_of_ne [Nontrivial R] {I : Ideal R} (h_bot : I ≠ ⊥) (h_top : I ≠ ⊤) : ¬ IsField R := by - contrapose! h_bot + contrapose h_bot exact ((isField_iff_maximal_bot.mp h_bot).eq_of_le h_top bot_le).symm theorem not_isField_iff_exists_ideal_bot_lt_and_lt_top [Nontrivial R] : diff --git a/Mathlib/RingTheory/Ideal/Int.lean b/Mathlib/RingTheory/Ideal/Int.lean index 231a35a4ce7353..b42f61ed4a0f41 100644 --- a/Mathlib/RingTheory/Ideal/Int.lean +++ b/Mathlib/RingTheory/Ideal/Int.lean @@ -124,7 +124,7 @@ theorem Nat.absNorm_under_prime (P : Ideal R) [P.IsPrime] [NeZero P] : · infer_instance · refine Int.natCast_ne_zero.mpr <| absNorm_eq_zero_iff.not.mpr ?_ have : P ≠ ⊥ := NeZero.ne _ - contrapose! this + contrapose this exact eq_bot_of_comap_eq_bot this end CommRing diff --git a/Mathlib/RingTheory/Ideal/IsPrincipalPowQuotient.lean b/Mathlib/RingTheory/Ideal/IsPrincipalPowQuotient.lean index 6240683dbc6b06..505d48a32388d6 100644 --- a/Mathlib/RingTheory/Ideal/IsPrincipalPowQuotient.lean +++ b/Mathlib/RingTheory/Ideal/IsPrincipalPowQuotient.lean @@ -65,7 +65,7 @@ def quotEquivPowQuotPowSucc (h : I.IsPrincipal) (h' : I ≠ ⊥) (n : ℕ) : rw [mul_comm, pow_succ, mul_assoc, mul_right_inj' (pow_ne_zero _ _)] at hy · rw [hI, Ideal.mem_span_singleton] exact ⟨y, hy⟩ - · contrapose! h' + · contrapose h' rw [hI, h', Ideal.span_singleton_eq_bot] let e : (R ⧸ I) ≃ₗ[R] R ⧸ (LinearMap.ker (f.comp g)) := Submodule.quotEquivOfEq I (LinearMap.ker (f ∘ₗ g)) this diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime/Colon.lean b/Mathlib/RingTheory/Ideal/MinimalPrime/Colon.lean index 9ecd208c7666f6..96c9fc3a99afe8 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime/Colon.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime/Colon.lean @@ -39,7 +39,7 @@ theorem exists_eq_colon_of_mem_minimalPrimes [IsNoetherianRing R] have key : ∃ n ≠ 0, ∃ J : Ideal R, I ^ n * J ≤ ann ∧ ¬ J ≤ I := by -- let `n` be large enough so that `ann.radical ^ n ≤ ann` (uses Noetherian) obtain ⟨n, hn⟩ := ann.exists_radical_pow_le_of_fg ann.radical.fg_of_isNoetherianRing - have hn0 : n ≠ 0 := by contrapose! hn; simpa [hn, ann] + have hn0 : n ≠ 0 := by contrapose hn; simpa [hn, ann] -- then take `J` to be the product of the other minimal primes raised to the `n`th power have h := ann.finite_minimalPrimes_of_isNoetherianRing R rw [← ann.sInf_minimalPrimes, ← h.coe_toFinset, ← h.toFinset.inf_id_eq_sInf, diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime/Noetherian.lean b/Mathlib/RingTheory/Ideal/MinimalPrime/Noetherian.lean index 095b86bfd5f042..8934e7b4381811 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime/Noetherian.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime/Noetherian.lean @@ -29,8 +29,8 @@ lemma Ideal.finite_minimalPrimes_of_isNoetherianRing (I : Ideal R) : obtain ⟨I : Ideal R, hI : ¬ I.minimalPrimes.Finite, hmax⟩ := set_has_maximal_iff_noetherian.mpr hR {I : Ideal R | ¬ I.minimalPrimes.Finite} ⟨I, hI⟩ simp only [Set.mem_setOf_eq, not_imp_not] at hmax - have h1 : ¬ I.IsPrime := by contrapose! hI; simp [minimalPrimes_eq_subsingleton_self] - have h2 : I ≠ ⊤ := by contrapose! hI; simp [hI, minimalPrimes_top] + have h1 : ¬ I.IsPrime := by contrapose hI; simp [minimalPrimes_eq_subsingleton_self] + have h2 : I ≠ ⊤ := by contrapose hI; simp [hI, minimalPrimes_top] obtain ⟨x, hx, y, hy, h⟩ := (not_isPrime_iff.mp h1).resolve_left h2 rw [← Ideal.span_singleton_le_iff_mem, ← left_lt_sup] at hx hy refine hI (((hmax _ hx).union (hmax _ hy)).subset fun p ⟨⟨hp, hI⟩, hmin⟩ ↦ ?_) diff --git a/Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean b/Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean index 07befae4818479..5f82d14c60acb5 100644 --- a/Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean +++ b/Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean @@ -125,7 +125,7 @@ theorem Ideal.exists_mul_add_mem_pow_succ [IsDedekindDomain S] (hP : P ≠ ⊥) refine (Ideal.eq_prime_pow_of_succ_lt_of_le hP (lt_of_le_of_ne le_sup_right ?_) (sup_le (Ideal.span_le.mpr (Set.singleton_subset_iff.mpr a_mem)) (Ideal.pow_succ_lt_pow hP i).le)).symm - contrapose! a_notMem with this + contrapose a_notMem with this rw [this] exact mem_sup.mpr ⟨a, mem_span_singleton_self a, 0, by simp, by simp⟩ diff --git a/Mathlib/RingTheory/Ideal/Over.lean b/Mathlib/RingTheory/Ideal/Over.lean index 67976afee03664..1448938c2c5cdc 100644 --- a/Mathlib/RingTheory/Ideal/Over.lean +++ b/Mathlib/RingTheory/Ideal/Over.lean @@ -241,7 +241,7 @@ instance bot_liesOver_bot : (⊥ : Ideal B).LiesOver (⊥ : Ideal A) where variable {A B} in theorem ne_bot_of_liesOver_of_ne_bot (hp : p ≠ ⊥) (P : Ideal B) [P.LiesOver p] : P ≠ ⊥ := by - contrapose! hp + contrapose hp rw [over_def P p, hp, under_bot] end CommRing diff --git a/Mathlib/RingTheory/Ideal/Prod.lean b/Mathlib/RingTheory/Ideal/Prod.lean index 86a5e27fcceb58..a35ddec7659af5 100644 --- a/Mathlib/RingTheory/Ideal/Prod.lean +++ b/Mathlib/RingTheory/Ideal/Prod.lean @@ -146,7 +146,7 @@ theorem prod_eq_top_iff {I : Ideal R} {J : Ideal S} : theorem isPrime_of_isPrime_prod_top {I : Ideal R} (h : (Ideal.prod I (⊤ : Ideal S)).IsPrime) : I.IsPrime := by constructor - · contrapose! h + · contrapose h rw [h, prod_top_top, isPrime_iff] simp · intro x y hxy diff --git a/Mathlib/RingTheory/IntegralDomain.lean b/Mathlib/RingTheory/IntegralDomain.lean index 4b2545d2e432a7..952c02b282160e 100644 --- a/Mathlib/RingTheory/IntegralDomain.lean +++ b/Mathlib/RingTheory/IntegralDomain.lean @@ -188,7 +188,7 @@ theorem sum_hom_units_eq_zero (f : G →* R) (hf : f ≠ 1) : ∑ g : G, f g = 0 obtain ⟨x, hx⟩ := IsCyclic.exists_monoid_generator (α := MonoidHom.range f.toHomUnits) have hx1 : (x.1 : R) - 1 ≠ 0 := by rw [sub_ne_zero] - contrapose! hf + contrapose hf ext g obtain ⟨n, hn⟩ := hx ⟨f.toHomUnits g, g, rfl⟩ simpa [hf, Subtype.ext_iff, Units.ext_iff] using hn.symm diff --git a/Mathlib/RingTheory/Lasker.lean b/Mathlib/RingTheory/Lasker.lean index bb80fd158689ff..cab9a51f60ed4c 100644 --- a/Mathlib/RingTheory/Lasker.lean +++ b/Mathlib/RingTheory/Lasker.lean @@ -81,7 +81,7 @@ lemma isPrimary_decomposition_pairwise_ne_radical {N : Submodule R M} obtain ⟨I', hI', hI⟩ := hI obtain ⟨J', hJ', hJ⟩ := hJ simp only [Function.onFun, ne_eq] - contrapose! hIJ + contrapose hIJ suffices (I'.colon Set.univ).radical = (J'.colon Set.univ).radical by rw [← hI, ← hJ, this] · rw [← hI, colon_finsetInf, @@ -182,7 +182,7 @@ lemma comap_localized₀_eq_ite apply (hqp.mem_or_mem hb).resolve_right grind [Submonoid.mem_iInf, mem_primeCompl_iff] · replace hq : ¬ (q.colon Set.univ : Set R) ⊆ ⋃ r ∈ s₀, r := by - contrapose! hp + contrapose hp obtain ⟨r, hrs, h⟩ := (subset_union_prime p p fun i _ _ _ ↦ i.2.1).mp hp rw [← r.2.1.radical_le_iff, hq] at h exact hs₀ h hrs @@ -190,7 +190,7 @@ lemma comap_localized₀_eq_ite replace hy2 : y ∈ S := by simp only [Submonoid.mem_iInf, Ideal.mem_primeCompl_iff, Subtype.forall, S] intro r hrI hrs - contrapose! hy2 + contrapose hy2 exact Set.mem_biUnion hrs hy2 rw [eq_top_iff, ← map_le_iff_le_comap, map_top] rintro - ⟨x, rfl⟩ diff --git a/Mathlib/RingTheory/LaurentSeries.lean b/Mathlib/RingTheory/LaurentSeries.lean index 3d335ed7e0b7f9..fb4748f995b01c 100644 --- a/Mathlib/RingTheory/LaurentSeries.lean +++ b/Mathlib/RingTheory/LaurentSeries.lean @@ -244,7 +244,7 @@ theorem single_order_mul_powerSeriesPart (x : R⸨X⸩) : · rw [ofPowerSeries_apply, embDomain_notin_range] · contrapose! h exact order_le_of_coeff_ne_zero h.symm - · contrapose! h + · contrapose h simp only [Set.mem_range, RelEmbedding.coe_mk, Function.Embedding.coeFn_mk] at h lia diff --git a/Mathlib/RingTheory/Localization/Ideal.lean b/Mathlib/RingTheory/Localization/Ideal.lean index 31f13f3d32b68d..bccbd896981b84 100644 --- a/Mathlib/RingTheory/Localization/Ideal.lean +++ b/Mathlib/RingTheory/Localization/Ideal.lean @@ -145,7 +145,7 @@ theorem comap_map_of_isPrimary_disjoint {I : Ideal R} (hI : I.IsPrimary) (hM : Disjoint (M : Set R) I) : Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I) = I := by have key : Disjoint (M : Set R) I.radical := by - contrapose! hM + contrapose hM rw [Set.not_disjoint_iff] at hM ⊢ obtain ⟨a, ha, k, hk⟩ := hM exact ⟨a ^ k, pow_mem ha k, hk⟩ diff --git a/Mathlib/RingTheory/MvPolynomial/Homogeneous.lean b/Mathlib/RingTheory/MvPolynomial/Homogeneous.lean index 757478c05113ab..d21fb0529a180c 100644 --- a/Mathlib/RingTheory/MvPolynomial/Homogeneous.lean +++ b/Mathlib/RingTheory/MvPolynomial/Homogeneous.lean @@ -386,7 +386,7 @@ lemma exists_eval_ne_zero_of_coeff_finSuccEquiv_ne_zero_aux {N : ℕ} {F : MvPolynomial (Fin (Nat.succ N)) R} {n : ℕ} (hF : IsHomogeneous F n) (hFn : ((finSuccEquiv R N) F).coeff n ≠ 0) : ∃ r, eval r F ≠ 0 := by - have hF₀ : F ≠ 0 := by contrapose! hFn; simp [hFn] + have hF₀ : F ≠ 0 := by contrapose hFn; simp [hFn] have hdeg : natDegree (finSuccEquiv R N F) < n + 1 := by linarith [natDegree_finSuccEquiv F, degreeOf_le_totalDegree F 0, hF.totalDegree hF₀] use Fin.cons 1 0 @@ -399,7 +399,7 @@ lemma exists_eval_ne_zero_of_coeff_finSuccEquiv_ne_zero_aux exact hi.symm simp_rw [eval_eq_eval_mv_eval', eval_one_map, Polynomial.eval_eq_sum_range' hdeg, eval_zero, one_pow, mul_one, map_sum, Finset.sum_range_succ, Finset.sum_eq_zero aux, zero_add] - contrapose! hFn + contrapose hFn ext d rw [coeff_zero] obtain rfl | hd := eq_or_ne d 0 @@ -428,7 +428,7 @@ lemma exists_eval_ne_zero_of_totalDegree_le_card_aux {N : ℕ} {F : MvPolynomial induction N generalizing n with | zero => use 0 - contrapose! hF₀ + contrapose hF₀ ext d simpa only [Subsingleton.elim d 0, eval_zero, coeff_zero] using hF₀ | succ N IH => diff --git a/Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean b/Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean index 39421e5080769f..dc1b54b571ceb3 100644 --- a/Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean +++ b/Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean @@ -872,7 +872,7 @@ lemma sPolynomial_def (f g : MvPolynomial σ R) : lemma degree_ne_zero_of_sub_leadingTerm_ne_zero {f : MvPolynomial σ R} (h : f - m.leadingTerm f ≠ 0) : m.degree f ≠ 0 := by - contrapose! h + contrapose h rw [m.degree_eq_zero_iff.mp h, leadingTerm_C, sub_eq_zero] @[simp] @@ -976,7 +976,7 @@ lemma degree_sPolynomial (f g : MvPolynomial σ R) : intro hs apply (m.degree_sPolynomial_le f g).lt_of_ne apply m.toSyn.injective.ne - contrapose! hs + contrapose hs rw [← m.coeff_degree_eq_zero_iff, hs, m.coeff_sPolynomial_sup_eq_zero] lemma degree_sPolynomial_lt_sup_degree {f g : MvPolynomial σ R} (h : m.sPolynomial f g ≠ 0) : diff --git a/Mathlib/RingTheory/MvPowerSeries/Expand.lean b/Mathlib/RingTheory/MvPowerSeries/Expand.lean index f2d722124e3ec3..ea210feed7115a 100644 --- a/Mathlib/RingTheory/MvPowerSeries/Expand.lean +++ b/Mathlib/RingTheory/MvPowerSeries/Expand.lean @@ -199,7 +199,7 @@ theorem trunc'_expand [DecidableEq σ] {n : σ →₀ ℕ} (φ : MvPowerSeries by_cases! h : ∀ i, p ∣ d i · obtain ⟨m, hm⟩ : ∃ m, p • m = d := ⟨d.mapRange (fun a ↦ a / p) (by simp), by ext i; simp [(Nat.mul_div_cancel' (h i))]⟩ - by_cases! h_le : m ≤ n + by_cases h_le : m ≤ n · rw [← hm, coeff_trunc', if_pos (nsmul_le_nsmul_right h_le p), coeff_expand_smul, MvPolynomial.coeff_expand_smul _ hp, coeff_trunc', if_pos h_le] · have not_le : ¬ p • m ≤ p • n := by @@ -213,7 +213,7 @@ theorem trunc'_expand [DecidableEq σ] {n : σ →₀ ℕ} (φ : MvPowerSeries if_neg h_le] · obtain ⟨i, hi⟩ := h rw [MvPolynomial.coeff_expand_of_not_dvd _ hi] - by_cases! hd : d ≤ p • n + by_cases hd : d ≤ p • n · rw [coeff_trunc', if_pos hd, coeff_expand_of_not_dvd _ hp _ hi] rw [coeff_trunc', if_neg hd] diff --git a/Mathlib/RingTheory/MvPowerSeries/PiTopology.lean b/Mathlib/RingTheory/MvPowerSeries/PiTopology.lean index c5d1db4e66a1c6..0672dcc87d9d6b 100644 --- a/Mathlib/RingTheory/MvPowerSeries/PiTopology.lean +++ b/Mathlib/RingTheory/MvPowerSeries/PiTopology.lean @@ -336,7 +336,7 @@ theorem summable_prod_of_tendsto_weightedOrder_atTop_nhds_top {w : σ → ℕ} apply (Finset.Iio i).powerset.finite_toSet.subset suffices ∀ s : Finset ι, coeff d (∏ i ∈ s, f i) ≠ 0 → ↑s ⊆ Set.Iio i by simpa intro s hs - contrapose! hs + contrapose hs obtain ⟨x, hxs, hxi⟩ := Set.not_subset.mp hs rw [Set.mem_Iio, not_lt] at hxi refine coeff_eq_zero_of_lt_weightedOrder w <| (hi x hxi).trans_le <| ?_ diff --git a/Mathlib/RingTheory/MvPowerSeries/Trunc.lean b/Mathlib/RingTheory/MvPowerSeries/Trunc.lean index 2d547abfec783e..5823179e5f8fff 100644 --- a/Mathlib/RingTheory/MvPowerSeries/Trunc.lean +++ b/Mathlib/RingTheory/MvPowerSeries/Trunc.lean @@ -149,7 +149,7 @@ theorem truncFinset_truncFinset_pow (hs : IsLowerSet (s : Set (σ →₀ ℕ))) simp [coeff_truncFinset_eq_zero _ hx] theorem support_truncFinset_subset (p : MvPowerSeries σ R) : (truncFinset R s p).support ⊆ s := by - intro; contrapose! + intro; contrapose simpa using coeff_truncFinset_eq_zero p lemma totalDegree_truncFinset (p : MvPowerSeries σ R) : @@ -299,7 +299,7 @@ theorem coeff_truncTotal_eq_zero (p : MvPowerSeries σ R) {x : σ →₀ ℕ} (h : n ≤ degree x) : (truncTotal R n p).coeff x = 0 := coeff_truncFinset_eq_zero p (by simpa) lemma truncTotal_one (h : n ≠ 0) : truncTotal R n (1 : MvPowerSeries σ R) = 1 := - truncFinset_one (by revert h; contrapose!; simp) + truncFinset_one (by revert h; contrapose; simp) lemma coeff_truncTotal_mul_truncTotal_eq_coeff_mul {x : σ →₀ ℕ} (p q : MvPowerSeries σ R) (hx : degree x < n) : MvPolynomial.coeff x ((truncTotal R n) p * (truncTotal R n) q) = diff --git a/Mathlib/RingTheory/Norm/Basic.lean b/Mathlib/RingTheory/Norm/Basic.lean index eda9b7589fe7ea..4797f839f4a90e 100644 --- a/Mathlib/RingTheory/Norm/Basic.lean +++ b/Mathlib/RingTheory/Norm/Basic.lean @@ -105,7 +105,7 @@ theorem norm_eq_zero_iff [IsDomain R] [IsDomain S] [Module.Free R S] [Module.Fin leftMulMatrix_mulVec_repr] at hv refine (mul_eq_zero.mp (b.ext_elem fun i => ?_)).resolve_right (show ∑ i, v i • b i ≠ 0 from ?_) · simpa only [map_zero, Pi.zero_apply] using congr_fun hv i - · contrapose! v_ne with sum_eq + · contrapose v_ne with sum_eq apply b.equivFun.symm.injective rw [b.equivFun_symm_apply, sum_eq, map_zero] @@ -141,7 +141,7 @@ section IntermediateField theorem _root_.IntermediateField.AdjoinSimple.norm_gen_eq_one {x : L} (hx : ¬IsIntegral K x) : norm K (AdjoinSimple.gen K x) = 1 := by rw [norm_eq_one_of_not_exists_basis] - contrapose! hx + contrapose hx obtain ⟨s, ⟨b⟩⟩ := hx refine .of_mem_of_fg K⟮x⟯.toSubalgebra ?_ x ?_ · exact (Submodule.fg_iff_finiteDimensional _).mpr (b.finiteDimensional_of_finite) diff --git a/Mathlib/RingTheory/Polynomial/Content.lean b/Mathlib/RingTheory/Polynomial/Content.lean index c4a812aa2fa78f..d2bc3c3cc753fa 100644 --- a/Mathlib/RingTheory/Polynomial/Content.lean +++ b/Mathlib/RingTheory/Polynomial/Content.lean @@ -389,7 +389,7 @@ theorem exists_primitive_lcm_of_isPrimitive {p q : R[X]} (hp : p.IsPrimitive) (h by_contra! con rcases Nat.find_spec con with ⟨s, sdeg, ⟨ps, qs⟩, rs⟩ have s0 : s ≠ 0 := by - contrapose! rs + contrapose rs simp [rs] have hs := Nat.find_min' h diff --git a/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean b/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean index b5ab12beb913d5..7c09104a687c62 100644 --- a/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean +++ b/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean @@ -254,7 +254,7 @@ theorem cyclotomic_eval_lt_add_one_pow_totient {n : ℕ} {q : ℝ} (hn' : 3 ≤ · rw [← Complex.arg_eq_pi_iff, hζ.arg_eq_pi_iff hn.ne'] at this rw [this] at hζ linarith [hζ.unique <| IsPrimitiveRoot.neg_one 0 two_ne_zero.symm] - · contrapose! hζ₀ + · contrapose hζ₀ apply Complex.ext <;> simp [hζ₀, h.2] have : ¬eval (↑q) (cyclotomic n ℂ) = 0 := by simpa using (cyclotomic_pos' n hq').ne.symm suffices Units.mk0 ‖(cyclotomic n ℂ).eval ↑q‖₊ (by simp_all) < diff --git a/Mathlib/RingTheory/Polynomial/GaussLemma.lean b/Mathlib/RingTheory/Polynomial/GaussLemma.lean index d4389cc1548fff..39af4196f09f96 100644 --- a/Mathlib/RingTheory/Polynomial/GaussLemma.lean +++ b/Mathlib/RingTheory/Polynomial/GaussLemma.lean @@ -322,7 +322,7 @@ theorem IsPrimitive.dvd_of_fraction_map_dvd_fraction_map {p q : R[X]} (hp : p.Is iterate 2 apply mul_ne_zero hq.ne_zero rw [Ne, C_eq_zero] - contrapose! s0 + contrapose s0 simp [s0, mem_nonZeroDivisors_iff_ne_zero] variable (K) diff --git a/Mathlib/RingTheory/Polynomial/ScaleRoots.lean b/Mathlib/RingTheory/Polynomial/ScaleRoots.lean index 9e2e3010f00a7a..cf3db2ec59b8fc 100644 --- a/Mathlib/RingTheory/Polynomial/ScaleRoots.lean +++ b/Mathlib/RingTheory/Polynomial/ScaleRoots.lean @@ -333,7 +333,7 @@ lemma rootMultiplicity_scaleRoots (p : R[X]) {r a : R} (hr : IsLeftRegular r) : obtain rfl | hp := eq_or_ne p 0 · simp obtain ⟨q, e, hq⟩ := exists_eq_pow_rootMultiplicity_mul_and_not_dvd p hp a - have hq0 : q ≠ 0 := by contrapose! hp; simp_all + have hq0 : q ≠ 0 := by contrapose hp; simp_all conv_lhs => rw [e] rw [mul_scaleRoots', pow_scaleRoots', X_sub_C_scaleRoots, mul_comm, mul_comm _ (q.scaleRoots r), rootMultiplicity_mul_X_sub_C_pow (q.scaleRoots_ne_zero hq0 _)] diff --git a/Mathlib/RingTheory/PowerSeries/PiTopology.lean b/Mathlib/RingTheory/PowerSeries/PiTopology.lean index 97d0c7b7dfd67b..ef0d0b8f5043e5 100644 --- a/Mathlib/RingTheory/PowerSeries/PiTopology.lean +++ b/Mathlib/RingTheory/PowerSeries/PiTopology.lean @@ -207,7 +207,7 @@ theorem summable_prod_of_tendsto_order_atTop_nhds_top apply (Finset.Iio i).powerset.finite_toSet.subset suffices ∀ s : Finset ι, coeff n (∏ i ∈ s, f i) ≠ 0 → ↑s ⊆ Set.Iio i by simpa intro s hs - contrapose! hs + contrapose hs obtain ⟨x, hxs, hxi⟩ := Set.not_subset.mp hs rw [Set.mem_Iio, not_lt] at hxi refine coeff_of_lt_order _ <| (hi x hxi).trans_le <| le_trans ?_ (le_order_prod _ _) diff --git a/Mathlib/RingTheory/PowerSeries/Substitution.lean b/Mathlib/RingTheory/PowerSeries/Substitution.lean index 33048fd8aa0f98..180123fdedb515 100644 --- a/Mathlib/RingTheory/PowerSeries/Substitution.lean +++ b/Mathlib/RingTheory/PowerSeries/Substitution.lean @@ -248,12 +248,12 @@ theorem coeff_subst_X_pow {k : ℕ} (hk : k ≠ 0) (f : PowerSeries R) (n : ℕ) coeff_X_pow_self, Algebra.algebraMap_eq_smul_one] intro j hj rw [← pow_mul, coeff_X_pow, if_neg, smul_zero] - contrapose! hj + contrapose hj rw [hj, Nat.mul_div_cancel_left j hk.pos] · rw [coeff_subst' (.X_pow hk), finsum_eq_zero_of_forall_eq_zero] intro j rw [← pow_mul, coeff_X_pow, if_neg, smul_zero] - contrapose! h + contrapose h use j @[simp] diff --git a/Mathlib/RingTheory/PowerSeries/WeierstrassPreparation.lean b/Mathlib/RingTheory/PowerSeries/WeierstrassPreparation.lean index 67852ff8cc136f..1c410073241183 100644 --- a/Mathlib/RingTheory/PowerSeries/WeierstrassPreparation.lean +++ b/Mathlib/RingTheory/PowerSeries/WeierstrassPreparation.lean @@ -183,7 +183,7 @@ theorem IsWeierstrassDivisor.of_map_ne_zero [IsLocalRing A] (hg : g.map (IsLocalRing.residue A) ≠ 0) : g.IsWeierstrassDivisor := by rw [IsWeierstrassDivisor, IsWeierstrassDivisorAt, ← IsLocalRing.notMem_maximalIdeal] have h := coeff_order hg - contrapose! h + contrapose h rwa [coeff_map, IsLocalRing.residue_eq_zero_iff] theorem _root_.Polynomial.IsDistinguishedAt.isWeierstrassDivisorAt {g : A[X]} {I : Ideal A} @@ -672,7 +672,7 @@ theorem degree_eq_coe_lift_order_map_of_ne_top (hI : I ≠ ⊤) : f.degree = (g.map (Ideal.Quotient.mk I)).order.lift (order_finite_iff_ne_zero.2 (H.map_ne_zero_of_ne_top hI)) := by refine H.isDistinguishedAt.degree_eq_coe_lift_order_map g h ?_ H.eq_mul - contrapose! hI + contrapose hI exact Ideal.eq_top_of_isUnit_mem _ hI (isUnit_iff_constantCoeff.1 H.isUnit) theorem natDegree_eq_toNat_order_map_of_ne_top (hI : I ≠ ⊤) : @@ -746,7 +746,7 @@ theorem IsWeierstrassDivision.isUnit_of_map_ne_zero · rw [zero_mul] · rw [← ENat.lt_lift_iff (h := order_finite_iff_ne_zero.2 hg), ENat.lift_eq_toNat_of_lt_top] refine (Finset.antidiagonal.fst_le hp).lt_of_ne ?_ - contrapose! hnotMem + contrapose hnotMem rwa [Finset.mem_singleton, Finset.antidiagonal_congr hp (by simp)] theorem IsWeierstrassDivision.isWeierstrassFactorization diff --git a/Mathlib/RingTheory/Radical/Basic.lean b/Mathlib/RingTheory/Radical/Basic.lean index 91fef888800c66..b706f493c294f1 100644 --- a/Mathlib/RingTheory/Radical/Basic.lean +++ b/Mathlib/RingTheory/Radical/Basic.lean @@ -75,7 +75,7 @@ lemma pairwise_primeFactors_isRelPrime : intro x hx y hy hxy simp only [Finset.mem_coe, mem_primeFactors, mem_normalizedFactors_iff' ha₀] at hx hy rw [hx.1.isRelPrime_iff_not_dvd] - contrapose! hxy + contrapose hxy have : Associated x y := hx.1.associated_of_dvd hy.1 hxy exact this.eq_of_normalized hx.2.1 hy.2.1 diff --git a/Mathlib/RingTheory/Regular/Depth.lean b/Mathlib/RingTheory/Regular/Depth.lean index adc857d4320502..0bcb3f8785655a 100644 --- a/Mathlib/RingTheory/Regular/Depth.lean +++ b/Mathlib/RingTheory/Regular/Depth.lean @@ -103,7 +103,7 @@ lemma subsingleton_linearMap_iff [IsNoetherianRing R] [Module.Finite R M] [Modul simp [eq0] absurd hom0 let _ := Module.finitePresentation_of_finite R N - contrapose! f_ne0 + contrapose f_ne0 exact (Module.FinitePresentation.linearEquivMapExtendScalars p'.asIdeal.primeCompl).symm.map_eq_zero_iff.mp (Subsingleton.eq_zero _) diff --git a/Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean b/Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean index ffccb51203c5e3..86ea593086cd71 100644 --- a/Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean +++ b/Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean @@ -847,7 +847,7 @@ lemma IsCyclic.exists_apply_ne_one {G G' : Type*} [Group G] [IsCyclic G] [Finite have hφg : IsPrimitiveRoot (φ g) (Nat.card G) := by rwa [monoidHomOfForallMemZpowers_apply_gen hg hζg] use φ - contrapose! ha + contrapose ha specialize hg a rw [← mem_powers_iff_mem_zpowers, Submonoid.mem_powers_iff] at hg obtain ⟨k, hk⟩ := hg diff --git a/Mathlib/RingTheory/Spectrum/Prime/Jacobson.lean b/Mathlib/RingTheory/Spectrum/Prime/Jacobson.lean index 7451288be91601..0abbf001e224f7 100644 --- a/Mathlib/RingTheory/Spectrum/Prime/Jacobson.lean +++ b/Mathlib/RingTheory/Spectrum/Prime/Jacobson.lean @@ -54,7 +54,7 @@ instance [IsJacobsonRing R] : JacobsonSpace (PrimeSpectrum R) := by simp only [Set.nonempty_iff_ne_empty, ne_eq, Set.inter_assoc, ← Set.disjoint_iff_inter_eq_empty, Set.disjoint_compl_left_iff_subset, zeroLocus_subset_zeroLocus_iff, Ideal.radical_eq_jacobson, Ideal.jacobson, le_sInf_iff] at hS ⊢ - contrapose! hS + contrapose hS rintro x ⟨hJx, hx⟩ exact @hS ⟨x, hx.isPrime⟩ ⟨hJx, (isClosed_singleton_iff_isMaximal _).mpr hx⟩ diff --git a/Mathlib/RingTheory/Trace/Basic.lean b/Mathlib/RingTheory/Trace/Basic.lean index 993e4096ded6c1..1b450e941853d0 100644 --- a/Mathlib/RingTheory/Trace/Basic.lean +++ b/Mathlib/RingTheory/Trace/Basic.lean @@ -101,7 +101,7 @@ open IntermediateField theorem trace_gen_eq_zero {x : L} (hx : ¬IsIntegral K x) : Algebra.trace K K⟮x⟯ (AdjoinSimple.gen K x) = 0 := by rw [trace_eq_zero_of_not_exists_basis, LinearMap.zero_apply] - contrapose! hx + contrapose hx obtain ⟨s, ⟨b⟩⟩ := hx refine .of_mem_of_fg K⟮x⟯.toSubalgebra ?_ x ?_ · exact (Submodule.fg_iff_finiteDimensional _).mpr (b.finiteDimensional_of_finite) diff --git a/Mathlib/RingTheory/TwoSidedIdeal/Basic.lean b/Mathlib/RingTheory/TwoSidedIdeal/Basic.lean index 134eddd50697f5..76662f764e151d 100644 --- a/Mathlib/RingTheory/TwoSidedIdeal/Basic.lean +++ b/Mathlib/RingTheory/TwoSidedIdeal/Basic.lean @@ -51,7 +51,7 @@ variable {R : Type*} [NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) instance [Nontrivial R] : Nontrivial (TwoSidedIdeal R) := by obtain ⟨I, J, h⟩ : Nontrivial (RingCon R) := inferInstance - exact ⟨⟨I⟩, ⟨J⟩, by contrapose! h; aesop⟩ + exact ⟨⟨I⟩, ⟨J⟩, by contrapose h; aesop⟩ instance setLike : SetLike (TwoSidedIdeal R) R where coe t := {r | t.ringCon r 0} diff --git a/Mathlib/RingTheory/UniqueFactorizationDomain/ClassGroup.lean b/Mathlib/RingTheory/UniqueFactorizationDomain/ClassGroup.lean index c131045ab52d0d..e02e1d48fad720 100644 --- a/Mathlib/RingTheory/UniqueFactorizationDomain/ClassGroup.lean +++ b/Mathlib/RingTheory/UniqueFactorizationDomain/ClassGroup.lean @@ -62,7 +62,7 @@ lemma isPrincipal_of_exists_mul_ne_zero_isPrincipal obtain ⟨y, hyJ, rfl⟩ := (Ideal.mem_mul_span_singleton).1 hxJg rw [← span_singleton_mul_span_singleton, span_singleton_mul_left_inj] at this · exact ⟨y, this⟩ - · contrapose! hx0 + · contrapose hx0 rw [hx0, mul_zero] -- Show `J * (g) ≤ (x)` by proving `x ∣ b * g` for all `b ∈ J`. refine le_antisymm diff --git a/Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean b/Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean index 930937a54a7d5b..69adbbe9251048 100644 --- a/Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean +++ b/Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean @@ -199,7 +199,7 @@ theorem factors'_cong {a b : α} (h : a ~ᵤ b) : factors' a = factors' b := by · rw [associated_zero_iff_eq_zero] at h rw [h] have ha : a ≠ 0 := by - contrapose! hb with ha + contrapose hb with ha rw [← associated_zero_iff_eq_zero, ← ha] exact h.symm rw [← Multiset.map_eq_map Subtype.coe_injective, map_subtype_coe_factors', @@ -393,7 +393,7 @@ open Classical in theorem exists_prime_dvd_of_not_inf_one {a b : α} (ha : a ≠ 0) (hb : b ≠ 0) (h : Associates.mk a ⊓ Associates.mk b ≠ 1) : ∃ p : α, Prime p ∧ p ∣ a ∧ p ∣ b := by have hz : factors (Associates.mk a) ⊓ factors (Associates.mk b) ≠ 0 := by - contrapose! h with hf + contrapose h with hf change (factors (Associates.mk a) ⊓ factors (Associates.mk b)).prod = 1 rw [hf] exact Multiset.prod_zero diff --git a/Mathlib/RingTheory/Valuation/ValuationRing.lean b/Mathlib/RingTheory/Valuation/ValuationRing.lean index c77af59613a0ea..5e8bdf33ea37d5 100644 --- a/Mathlib/RingTheory/Valuation/ValuationRing.lean +++ b/Mathlib/RingTheory/Valuation/ValuationRing.lean @@ -191,7 +191,7 @@ noncomputable instance linearOrderedCommGroupWithZero : mul_lt_mul_of_pos_left := by simp_rw [← not_le] rintro ⟨a⟩ ha ⟨b⟩ ⟨c⟩ hbc - contrapose! hbc + contrapose hbc obtain ⟨d, hd⟩ := hbc simp only [Algebra.smul_def, mul_left_comm, mul_eq_mul_left_iff] at hd obtain rfl | rfl := hd diff --git a/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean b/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean index 162e0f42544bc5..86d0de6b04f7ea 100644 --- a/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean +++ b/Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean @@ -310,7 +310,7 @@ lemma left_cancel_posSubmonoid (x y : R) (u : posSubmonoid R) : lemma val_posSubmonoid_ne_zero (x : posSubmonoid R) : (x : R) ≠ 0 := by have := x.prop rw [posSubmonoid_def] at this - contrapose! this + contrapose this simp [this] variable (R) in diff --git a/Mathlib/RingTheory/WittVector/DiscreteValuationRing.lean b/Mathlib/RingTheory/WittVector/DiscreteValuationRing.lean index 950d98a39f6ae8..ef571e47200128 100644 --- a/Mathlib/RingTheory/WittVector/DiscreteValuationRing.lean +++ b/Mathlib/RingTheory/WittVector/DiscreteValuationRing.lean @@ -124,7 +124,7 @@ theorem exists_eq_pow_p_mul (a : 𝕎 k) (ha : a ≠ 0) : simp only [Function.comp_apply] at this rw [← this] at hcm refine ⟨m, b, ?_, ?_⟩ - · contrapose! hc + · contrapose hc simp [hc, zero_pow <| pow_ne_zero _ hp.out.ne_zero] · simp_rw [← mul_left_iterate (p : 𝕎 k) m] convert hcm using 2 diff --git a/Mathlib/RingTheory/ZMod/UnitsCyclic.lean b/Mathlib/RingTheory/ZMod/UnitsCyclic.lean index f43d3602cf9fbe..79e5082f07e949 100644 --- a/Mathlib/RingTheory/ZMod/UnitsCyclic.lean +++ b/Mathlib/RingTheory/ZMod/UnitsCyclic.lean @@ -313,7 +313,7 @@ theorem isCyclic_units_iff_of_odd {n : ℕ} (hn : Odd n) : refine not_isCyclic_units_of_mul_coprime _ _ (hn.of_dvd_nat this) ?_ (hn.of_dvd_nat (Nat.div_dvd_of_dvd this)) ?_ ((Nat.coprime_ordCompl hp hn0).pow_left ..) · simpa [(hp.factorization_pos_of_dvd hn0 dvd).ne'] using hp.ne_one - · contrapose! hnp + · contrapose hnp conv_lhs => rw [← Nat.div_mul_cancel this, hnp, one_mul] rintro ⟨q, m, hq, -, rfl⟩ cases (Nat.prime_dvd_prime_iff_eq hp hq).mp (hp.dvd_of_dvd_pow dvd) diff --git a/Mathlib/SetTheory/Cardinal/Order.lean b/Mathlib/SetTheory/Cardinal/Order.lean index a2f753c4748b1c..4c53f247b3c7b2 100644 --- a/Mathlib/SetTheory/Cardinal/Order.lean +++ b/Mathlib/SetTheory/Cardinal/Order.lean @@ -552,7 +552,7 @@ lemma exists_eq_of_iSup_eq_of_not_isSuccPrelimit (h : ⨆ i : ι, f i = ω) : ∃ i, f i = ω := by subst h suffices BddAbove (range f) from (isLUB_csSup' this).mem_of_not_isSuccPrelimit hω - contrapose! hω with hf + contrapose hω with hf rw [iSup, csSup_of_not_bddAbove hf, csSup_empty] exact isSuccPrelimit_bot diff --git a/Mathlib/Tactic/ComputeAsymptotics/Multiseries/Corecursion.lean b/Mathlib/Tactic/ComputeAsymptotics/Multiseries/Corecursion.lean index c9d2f4fad802a9..dfde0e05295698 100644 --- a/Mathlib/Tactic/ComputeAsymptotics/Multiseries/Corecursion.lean +++ b/Mathlib/Tactic/ComputeAsymptotics/Multiseries/Corecursion.lean @@ -151,7 +151,7 @@ theorem dist_eq_one_of_head {s t : Seq α} (h : s.head ≠ t.head) : dist s t = intro h' simpa [Stream'.cons] · rw [Subtype.coe_ne_coe] - contrapose! h + contrapose h simp [h] theorem dist_cons_cons_eq_one {x y : α} {s t : Seq α} (h : x ≠ y) : diff --git a/Mathlib/Tactic/NormNum/Irrational.lean b/Mathlib/Tactic/NormNum/Irrational.lean index b833158537eda5..a12691f7195d97 100644 --- a/Mathlib/Tactic/NormNum/Irrational.lean +++ b/Mathlib/Tactic/NormNum/Irrational.lean @@ -132,7 +132,7 @@ private theorem not_power_rat_of_num {a b d : ℕ} rcases d.even_or_odd with (h_even | h_odd) · have := not_power_rat_of_num_aux h_coprime (q := -q) ha (by linarith) rwa [h_even.neg_pow] at this - · contrapose! hq + · contrapose hq rw [← h_odd.pow_nonneg_iff, ← hq] positivity diff --git a/Mathlib/Tactic/Order/ToInt.lean b/Mathlib/Tactic/Order/ToInt.lean index 8ae8bdb2c62c6a..ed2453c993de03 100644 --- a/Mathlib/Tactic/Order/ToInt.lean +++ b/Mathlib/Tactic/Order/ToInt.lean @@ -60,7 +60,7 @@ theorem exists_translation : ∃ tr : Fin n → ℤ, ∀ i j, val i ≤ val j · contrapose! h exact lt_of_le_of_ne (by simpa using (this hj.choose hi.choose (by simpa))) (fun h ↦ h_eq (h.symm)) - · simpa using this hi.choose hj.choose (by apply lt_of_le_of_ne h; contrapose! h_eq; simp [h_eq]) + · simpa using this hi.choose hj.choose (by apply lt_of_le_of_ne h; contrapose h_eq; simp [h_eq]) /-- Auxiliary definition used by the `order` tactic to transfer facts in a linear order to `ℤ`. -/ noncomputable def toInt (k : Fin n) : ℤ := diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean index 5f733e02efa1a2..cd2568f0ba7934 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean @@ -256,7 +256,7 @@ lemma Topology.IsClosedEmbedding.map_tprod {ι α α' G : Type*} · by_cases h : Multipliable f L · exact h.map_tprod g hge.continuous · rw [tprod_eq_one_of_not_multipliable h, tprod_eq_one_of_not_multipliable, map_one] - contrapose! h + contrapose h -- need to show `g ∘ f` multipliable implies `g` multipliable simp only [Multipliable, HasProd] at h ⊢ obtain ⟨b, hb⟩ := h diff --git a/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean b/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean index 866eb11ec210e5..e843d1dadc01fe 100644 --- a/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean +++ b/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean @@ -282,7 +282,7 @@ instance Subgroup.isClosed_of_discrete [T2Space G] {H : Subgroup G} [DiscreteTop have : (fun p : G × G => p.2 * p.1⁻¹) ⁻¹' V ∈ 𝓤 G := preimage_mem_comap V_in apply isClosed_of_spaced_out this intro h h_in h' h'_in - contrapose! + contrapose simp only [Set.mem_preimage] rintro (hyp : h' * h⁻¹ ∈ V) have : h' * h⁻¹ ∈ ({1} : Set G) := VH ▸ Set.mem_inter hyp (H.mul_mem h'_in (H.inv_mem h_in)) diff --git a/Mathlib/Topology/Algebra/Module/Equiv.lean b/Mathlib/Topology/Algebra/Module/Equiv.lean index fc3f2b89fc288e..af51d37ab81471 100644 --- a/Mathlib/Topology/Algebra/Module/Equiv.lean +++ b/Mathlib/Topology/Algebra/Module/Equiv.lean @@ -1208,7 +1208,7 @@ theorem inverse_eq_ringInverse (e : M ≃L[R] M₂) (f : M →L[R] M₂) : ext simp · suffices ¬IsUnit ((e.symm : M₂ →L[R] M).comp f) by simp [this, h₁] - contrapose! h₁ + contrapose h₁ rcases h₁ with ⟨F, hF⟩ use (ContinuousLinearEquiv.unitsEquiv _ _ F).trans e ext diff --git a/Mathlib/Topology/ContinuousMap/CompactlySupported.lean b/Mathlib/Topology/ContinuousMap/CompactlySupported.lean index 365f2d07707381..e291c160e0235e 100644 --- a/Mathlib/Topology/ContinuousMap/CompactlySupported.lean +++ b/Mathlib/Topology/ContinuousMap/CompactlySupported.lean @@ -679,7 +679,7 @@ protected lemma exists_add_of_le {f₁ f₂ : C_c(α, ℝ≥0)} (h : f₁ ≤ f rw [tsupport, tsupport, ← closure_union] apply closure_mono intro x hx - contrapose! hx + contrapose hx simp only [ContinuousMap.toFun_eq_coe, coe_toContinuousMap, Set.mem_union, Function.mem_support, ne_eq, not_or, Decidable.not_not, ContinuousMap.coe_sub, Pi.sub_apply] at hx ⊢ simp [hx.1, hx.2] diff --git a/Mathlib/Topology/EMetricSpace/Paracompact.lean b/Mathlib/Topology/EMetricSpace/Paracompact.lean index 0d74d27057b1c0..e252e9c771e572 100644 --- a/Mathlib/Topology/EMetricSpace/Paracompact.lean +++ b/Mathlib/Topology/EMetricSpace/Paracompact.lean @@ -137,7 +137,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) (hm : m ≤ n + k) : Set.Subsingleton { j | (D m j ∩ B).Nonempty } := by rintro 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_gt.resolve_left h) rcases memD.1 hyD with ⟨y', rfl, hsuby, -, hdisty⟩ diff --git a/Mathlib/Topology/ExtremallyDisconnected.lean b/Mathlib/Topology/ExtremallyDisconnected.lean index 17290ca9388660..47b42abaa711dc 100644 --- a/Mathlib/Topology/ExtremallyDisconnected.lean +++ b/Mathlib/Topology/ExtremallyDisconnected.lean @@ -150,7 +150,7 @@ lemma exists_compact_surjective_zorn_subset [T1Space A] [CompactSpace D] {X : D obtain ⟨E_closed, E_surj⟩ := E_min.prop refine ⟨E, isCompact_iff_compactSpace.mp E_closed.isCompact, E_surj, ?_⟩ intro E₀ E₀_min E₀_closed - contrapose! E₀_min + contrapose E₀_min exact eq_univ_of_image_val_eq <| E_min.eq_of_subset ⟨E₀_closed.trans E_closed, image_image_val_eq_restrict_image ▸ E₀_min⟩ image_val_subset diff --git a/Mathlib/Topology/Instances/AddCircle/DenseSubgroup.lean b/Mathlib/Topology/Instances/AddCircle/DenseSubgroup.lean index 6ce056cea1713d..d3d80dc8aec63d 100644 --- a/Mathlib/Topology/Instances/AddCircle/DenseSubgroup.lean +++ b/Mathlib/Topology/Instances/AddCircle/DenseSubgroup.lean @@ -41,7 +41,7 @@ theorem dense_addSubgroupClosure_pair_iff {a b : ℝ} : · simp [field, mul_div_left_comm _ b, ← Rat.cast_def, hr] · simp [field] · intro h - contrapose! h + contrapose h rcases (AddSubgroup.dense_or_cyclic _).resolve_left h with ⟨c, hc⟩ have : {a, b} ⊆ range (· • c : ℤ → ℝ) := by rw [← AddSubgroup.coe_zmultiples, AddSubgroup.zmultiples_eq_closure, ← hc] diff --git a/Mathlib/Topology/Instances/RatLemmas.lean b/Mathlib/Topology/Instances/RatLemmas.lean index 7a2bad9ac13f12..471cce12b549ce 100644 --- a/Mathlib/Topology/Instances/RatLemmas.lean +++ b/Mathlib/Topology/Instances/RatLemmas.lean @@ -78,7 +78,7 @@ theorem not_secondCountableTopology_opc : ¬SecondCountableTopology ℚ∞ := by instance : TotallyDisconnectedSpace ℚ := by clear p s 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 · apply this s hs y hy x hx H.symm <| H.lt_or_gt.resolve_left hlt rcases exists_irrational_btwn (Rat.cast_lt.2 hlt) with ⟨z, hz, hxz, hzy⟩ diff --git a/Mathlib/Topology/LocallyFinsupp.lean b/Mathlib/Topology/LocallyFinsupp.lean index cf3f80921be7bf..80612fc9ca39a6 100644 --- a/Mathlib/Topology/LocallyFinsupp.lean +++ b/Mathlib/Topology/LocallyFinsupp.lean @@ -268,7 +268,7 @@ protected def addSubmonoid [AddMonoid Y] : AddSubmonoid (X → Y) where add_mem' {f g} hf hg := by constructor · intro x hx - contrapose! hx + contrapose hx simp [notMem_support.1 fun a ↦ hx (hf.1 a), notMem_support.1 fun a ↦ hx (hg.1 a)] · intro z hz obtain ⟨t₁, ht₁⟩ := hf.2 z hz diff --git a/Mathlib/Topology/Separation/CompletelyRegular.lean b/Mathlib/Topology/Separation/CompletelyRegular.lean index 7c6b1d5df49a9d..51bae435b3e41f 100644 --- a/Mathlib/Topology/Separation/CompletelyRegular.lean +++ b/Mathlib/Topology/Separation/CompletelyRegular.lean @@ -212,7 +212,7 @@ theorem CompletelyRegularSpace.isTopologicalBasis_clopens_of_cardinalMk_lt_conti refine ⟨f ⁻¹' Iio r, ⟨hrclopen ▸ isClosed_Iic.preimage hfc, isOpen_Iio.preimage hfc⟩, ?_, ?_⟩ · simp [hf₀, hrclopen] · refine preimage_subset_iff.mpr (fun x ↦ ?_) - contrapose!; intro hxs + contrapose; intro hxs simpa [hf₁ hxs] using le_one' /-- A T₃.₅ space is a completely regular space that is also T₀. -/ diff --git a/Mathlib/Topology/UrysohnsLemma.lean b/Mathlib/Topology/UrysohnsLemma.lean index d1c368702c8a19..7f6d44d94a3b5d 100644 --- a/Mathlib/Topology/UrysohnsLemma.lean +++ b/Mathlib/Topology/UrysohnsLemma.lean @@ -413,7 +413,7 @@ theorem exists_continuous_one_zero_of_isCompact [RegularSpace X] [LocallyCompact · apply HasCompactSupport.intro' k_comp k_closed (fun x hx ↦ ?_) simp only [ContinuousMap.coe_mk, sub_eq_zero] apply (hft _).symm - contrapose! hx + contrapose hx simp only [mem_compl_iff, not_not] at hx exact interior_subset hx · have : 0 ≤ f x ∧ f x ≤ 1 := by simpa using h'f x