From be0b59d276020004e21109a79cab71f259755349 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Tue, 26 Dec 2023 16:00:04 +0000 Subject: [PATCH] =?UTF-8?q?chore(*):=20use=20`=E2=88=80=20s=20=E2=8A=86=20?= =?UTF-8?q?t,=20=5F`=20etc=20(#9276)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Changes in this PR shouldn't change the public API. The only changes about `∃ x ∈ s, _` is inside a proof. Co-authored-by: Jeremy Tan Jie Rui --- Archive/Imo/Imo2021Q1.lean | 2 +- Mathlib/Algebra/Function/Support.lean | 2 +- Mathlib/Analysis/Calculus/TangentCone.lean | 2 +- .../Analysis/InnerProductSpace/Projection.lean | 5 ++--- Mathlib/Analysis/NormedSpace/lpSpace.lean | 5 ++--- .../Combinatorics/Additive/PluenneckeRuzsa.lean | 8 ++++---- Mathlib/Computability/Partrec.lean | 5 ++--- Mathlib/Computability/Primrec.lean | 5 ++--- Mathlib/Data/Nat/Prime.lean | 2 +- Mathlib/GroupTheory/Submonoid/Membership.lean | 2 +- Mathlib/GroupTheory/Subsemigroup/Membership.lean | 2 +- Mathlib/LinearAlgebra/Eigenspace/Basic.lean | 2 +- Mathlib/LinearAlgebra/LinearIndependent.lean | 2 +- Mathlib/MeasureTheory/Measure/VectorMeasure.lean | 2 +- .../NumberTheory/DiophantineApproximation.lean | 3 +-- Mathlib/RingTheory/DedekindDomain/Dvr.lean | 4 ++-- Mathlib/RingTheory/DedekindDomain/Ideal.lean | 4 ++-- .../Category/TopCat/Limits/Cofiltered.lean | 2 +- Mathlib/Topology/Semicontinuous.lean | 16 ++++++++-------- Mathlib/Topology/ShrinkingLemma.lean | 2 +- 20 files changed, 36 insertions(+), 41 deletions(-) diff --git a/Archive/Imo/Imo2021Q1.lean b/Archive/Imo/Imo2021Q1.lean index dbb1f65c63224..3a56e305e2b2f 100644 --- a/Archive/Imo/Imo2021Q1.lean +++ b/Archive/Imo/Imo2021Q1.lean @@ -110,7 +110,7 @@ end Imo2021Q1 open Imo2021Q1 theorem imo2021_q1 : - ∀ n : ℕ, 100 ≤ n → ∀ (A) (_ : A ⊆ Finset.Icc n (2 * n)), + ∀ n : ℕ, 100 ≤ n → ∀ A ⊆ Finset.Icc n (2 * n), (∃ a ∈ A, ∃ b ∈ A, a ≠ b ∧ ∃ k : ℕ, a + b = k ^ 2) ∨ ∃ a ∈ Finset.Icc n (2 * n) \ A, ∃ b ∈ Finset.Icc n (2 * n) \ A, a ≠ b ∧ ∃ k : ℕ, a + b = k ^ 2 := by diff --git a/Mathlib/Algebra/Function/Support.lean b/Mathlib/Algebra/Function/Support.lean index dab474ff28353..7aa21a278e370 100644 --- a/Mathlib/Algebra/Function/Support.lean +++ b/Mathlib/Algebra/Function/Support.lean @@ -70,7 +70,7 @@ theorem mulSupport_subset_iff {f : α → M} {s : Set α} : mulSupport f ⊆ s @[to_additive] theorem mulSupport_subset_iff' {f : α → M} {s : Set α} : - mulSupport f ⊆ s ↔ ∀ (x) (_ : x ∉ s), f x = 1 := + mulSupport f ⊆ s ↔ ∀ x ∉ s, f x = 1 := forall_congr' fun _ => not_imp_comm #align function.mul_support_subset_iff' Function.mulSupport_subset_iff' #align function.support_subset_iff' Function.support_subset_iff' diff --git a/Mathlib/Analysis/Calculus/TangentCone.lean b/Mathlib/Analysis/Calculus/TangentCone.lean index f78ccdb03a5bd..34e2f39c5bbb6 100644 --- a/Mathlib/Analysis/Calculus/TangentCone.lean +++ b/Mathlib/Analysis/Calculus/TangentCone.lean @@ -184,7 +184,7 @@ theorem subset_tangentCone_prod_right {t : Set F} {y : F} (hs : x ∈ closure s) /-- The tangent cone of a product contains the tangent cone of each factor. -/ theorem mapsTo_tangentCone_pi {ι : Type*} [DecidableEq ι] {E : ι → Type*} [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)] {s : ∀ i, Set (E i)} {x : ∀ i, E i} - {i : ι} (hi : ∀ (j) (_ : j ≠ i), x j ∈ closure (s j)) : + {i : ι} (hi : ∀ j ≠ i, x j ∈ closure (s j)) : MapsTo (LinearMap.single i : E i →ₗ[𝕜] ∀ j, E j) (tangentConeAt 𝕜 (s i) (x i)) (tangentConeAt 𝕜 (Set.pi univ s) x) := by rintro w ⟨c, d, hd, hc, hy⟩ diff --git a/Mathlib/Analysis/InnerProductSpace/Projection.lean b/Mathlib/Analysis/InnerProductSpace/Projection.lean index fae9a45834782..9d301c71a6cf5 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection.lean @@ -1387,7 +1387,7 @@ open FiniteDimensional Submodule Set /-- An orthonormal set in an `InnerProductSpace` is maximal, if and only if the orthogonal complement of its span is empty. -/ theorem maximal_orthonormal_iff_orthogonalComplement_eq_bot (hv : Orthonormal 𝕜 ((↑) : v → E)) : - (∀ (u) (_ : u ⊇ v), Orthonormal 𝕜 ((↑) : u → E) → u = v) ↔ (span 𝕜 v)ᗮ = ⊥ := by + (∀ u ⊇ v, Orthonormal 𝕜 ((↑) : u → E) → u = v) ↔ (span 𝕜 v)ᗮ = ⊥ := by rw [Submodule.eq_bot_iff] constructor · contrapose! @@ -1453,8 +1453,7 @@ variable [FiniteDimensional 𝕜 E] /-- An orthonormal set in a finite-dimensional `InnerProductSpace` is maximal, if and only if it is a basis. -/ theorem maximal_orthonormal_iff_basis_of_finiteDimensional (hv : Orthonormal 𝕜 ((↑) : v → E)) : - (∀ (u) (_ : u ⊇ v), Orthonormal 𝕜 ((↑) : u → E) → u = v) ↔ - ∃ b : Basis v 𝕜 E, ⇑b = ((↑) : v → E) := by + (∀ u ⊇ v, Orthonormal 𝕜 ((↑) : u → E) → u = v) ↔ ∃ b : Basis v 𝕜 E, ⇑b = ((↑) : v → E) := by haveI := proper_isROrC 𝕜 (span 𝕜 v) rw [maximal_orthonormal_iff_orthogonalComplement_eq_bot hv] rw [Submodule.orthogonal_eq_bot_iff] diff --git a/Mathlib/Analysis/NormedSpace/lpSpace.lean b/Mathlib/Analysis/NormedSpace/lpSpace.lean index b88d4fc8f2f99..4e63558c7b96c 100644 --- a/Mathlib/Analysis/NormedSpace/lpSpace.lean +++ b/Mathlib/Analysis/NormedSpace/lpSpace.lean @@ -185,7 +185,7 @@ theorem of_exponent_ge {p q : ℝ≥0∞} {f : ∀ i, E i} (hfq : Memℓp f q) ( · simp [hi] · exact (hC ⟨i, hi, rfl⟩).trans (le_max_right _ _) · apply memℓp_gen - have : ∀ (i) (_ : i ∉ hfq.finite_dsupport.toFinset), ‖f i‖ ^ p.toReal = 0 := by + have : ∀ i ∉ hfq.finite_dsupport.toFinset, ‖f i‖ ^ p.toReal = 0 := by intro i hi have : f i = 0 := by simpa using hi simp [this, Real.zero_rpow hp.ne'] @@ -1039,8 +1039,7 @@ protected theorem norm_sum_single (hp : 0 < p.toReal) (f : ∀ i, E i) (s : Fins ‖∑ i in s, lp.single p i (f i)‖ ^ p.toReal = ∑ i in s, ‖f i‖ ^ p.toReal := by refine' (hasSum_norm hp (∑ i in s, lp.single p i (f i))).unique _ simp only [lp.single_apply, coeFn_sum, Finset.sum_apply, Finset.sum_dite_eq] - have h : ∀ (i) (_ : i ∉ s), ‖ite (i ∈ s) (f i) 0‖ ^ p.toReal = 0 := by - intro i hi + have h : ∀ i ∉ s, ‖ite (i ∈ s) (f i) 0‖ ^ p.toReal = 0 := fun i hi ↦ by simp [if_neg hi, Real.zero_rpow hp.ne'] have h' : ∀ i ∈ s, ‖f i‖ ^ p.toReal = ‖ite (i ∈ s) (f i) 0‖ ^ p.toReal := by intro i hi diff --git a/Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean b/Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean index c94eb43a1ace6..0b3eb306ed10f 100644 --- a/Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean +++ b/Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean @@ -87,7 +87,7 @@ theorem card_mul_mul_le_card_mul_mul_card_div (A B C : Finset α) : @[to_additive] theorem mul_pluennecke_petridis (C : Finset α) - (hA : ∀ (A') (_ : A' ⊆ A), (A * B).card * A'.card ≤ (A' * B).card * A.card) : + (hA : ∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card) : (A * B * C).card * A.card ≤ (A * B).card * (A * C).card := by induction' C using Finset.induction_on with x C _ ih · simp @@ -123,7 +123,7 @@ theorem mul_pluennecke_petridis (C : Finset α) @[to_additive] private theorem mul_aux (hA : A.Nonempty) (hAB : A ⊆ B) (h : ∀ A' ∈ B.powerset.erase ∅, ((A * C).card : ℚ≥0) / ↑A.card ≤ (A' * C).card / ↑A'.card) : - ∀ (A') (_ : A' ⊆ A), (A * C).card * A'.card ≤ (A' * C).card * A.card := by + ∀ A' ⊆ A, (A * C).card * A'.card ≤ (A' * C).card * A.card := by rintro A' hAA' obtain rfl | hA' := A'.eq_empty_or_nonempty · simp @@ -180,7 +180,7 @@ theorem card_div_mul_le_card_div_mul_card_mul (A B C : Finset α) : #align finset.card_div_mul_le_card_div_mul_card_mul Finset.card_div_mul_le_card_div_mul_card_mul theorem card_add_nsmul_le {α : Type*} [AddCommGroup α] [DecidableEq α] {A B : Finset α} - (hAB : ∀ (A') (_ : A' ⊆ A), (A + B).card * A'.card ≤ (A' + B).card * A.card) (n : ℕ) : + (hAB : ∀ A' ⊆ A, (A + B).card * A'.card ≤ (A' + B).card * A.card) (n : ℕ) : (A + n • B).card ≤ ((A + B).card / A.card : ℚ≥0) ^ n * A.card := by obtain rfl | hA := A.eq_empty_or_nonempty · simp @@ -195,7 +195,7 @@ theorem card_add_nsmul_le {α : Type*} [AddCommGroup α] [DecidableEq α] {A B : #align finset.card_add_nsmul_le Finset.card_add_nsmul_le @[to_additive existing] -theorem card_mul_pow_le (hAB : ∀ (A') (_ : A' ⊆ A), (A * B).card * A'.card ≤ (A' * B).card * A.card) +theorem card_mul_pow_le (hAB : ∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card) (n : ℕ) : (A * B ^ n).card ≤ ((A * B).card / A.card : ℚ≥0) ^ n * A.card := by obtain rfl | hA := A.eq_empty_or_nonempty · simp diff --git a/Mathlib/Computability/Partrec.lean b/Mathlib/Computability/Partrec.lean index 9c3c8dde19db6..e7e4130c6fe31 100644 --- a/Mathlib/Computability/Partrec.lean +++ b/Mathlib/Computability/Partrec.lean @@ -828,9 +828,8 @@ theorem fix_aux {α σ} (f : α →. Sum σ α) (a : α) (b : σ) : · cases' h₁ (Nat.lt_succ_self _) with a' h injection mem_unique h h₂ · exact this _ _ am' (PFun.mem_fix_iff.2 (Or.inl fa')) - · suffices - ∀ (a') (_ : b ∈ PFun.fix f a') (k) (_ : Sum.inr a' ∈ F a k), - ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, ∀ (_ : k ≤ m), ∃ a₂, Sum.inr a₂ ∈ F a m by + · suffices ∀ a', b ∈ PFun.fix f a' → ∀ k, Sum.inr a' ∈ F a k → + ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m by rcases this _ h 0 (by simp) with ⟨n, hn₁, hn₂⟩ exact ⟨_, ⟨⟨_, hn₁⟩, fun {m} mn => hn₂ m mn (Nat.zero_le _)⟩, hn₁⟩ intro a₁ h₁ diff --git a/Mathlib/Computability/Primrec.lean b/Mathlib/Computability/Primrec.lean index 09b38d22f97d7..eec9bbc1a0dcd 100644 --- a/Mathlib/Computability/Primrec.lean +++ b/Mathlib/Computability/Primrec.lean @@ -971,9 +971,8 @@ instance list : Primcodable (List α) := intro n IH; simp cases' @decode α _ n.unpair.1 with a; · rfl simp only [decode_eq_ofNat, Option.some.injEq, Option.some_bind, Option.map_some'] - suffices : - ∀ (o : Option (List ℕ)) (p) (_ : encode o = encode p), - encode (Option.map (List.cons (encode a)) o) = encode (Option.map (List.cons a) p) + suffices : ∀ (o : Option (List ℕ)) (p), encode o = encode p → + encode (Option.map (List.cons (encode a)) o) = encode (Option.map (List.cons a) p) exact this _ _ (IH _ (Nat.unpair_right_le n)) intro o p IH cases o <;> cases p diff --git a/Mathlib/Data/Nat/Prime.lean b/Mathlib/Data/Nat/Prime.lean index 52562e5efe8af..b0c086aa962c9 100644 --- a/Mathlib/Data/Nat/Prime.lean +++ b/Mathlib/Data/Nat/Prime.lean @@ -95,7 +95,7 @@ theorem Prime.eq_one_or_self_of_dvd {p : ℕ} (pp : p.Prime) (m : ℕ) (hm : m rw [hn, mul_one] #align nat.prime.eq_one_or_self_of_dvd Nat.Prime.eq_one_or_self_of_dvd -theorem prime_def_lt'' {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ∀ (m) (_ : m ∣ p), m = 1 ∨ m = p := by +theorem prime_def_lt'' {p : ℕ} : Prime p ↔ 2 ≤ p ∧ ∀ m, m ∣ p → m = 1 ∨ m = p := by refine' ⟨fun h => ⟨h.two_le, h.eq_one_or_self_of_dvd⟩, fun h => _⟩ -- Porting note: needed to make ℕ explicit have h1 := (@one_lt_two ℕ ..).trans_le h.1 diff --git a/Mathlib/GroupTheory/Submonoid/Membership.lean b/Mathlib/GroupTheory/Submonoid/Membership.lean index 65e5e5ce0cfdb..c815ce3f0b156 100644 --- a/Mathlib/GroupTheory/Submonoid/Membership.lean +++ b/Mathlib/GroupTheory/Submonoid/Membership.lean @@ -580,7 +580,7 @@ theorem map_powers {N : Type*} {F : Type*} [Monoid N] [MonoidHomClass F M N] (f @[to_additive "If all the elements of a set `s` commute, then `closure s` forms an additive commutative monoid."] -def closureCommMonoidOfComm {s : Set M} (hcomm : ∀ (a) (_ : a ∈ s) (b) (_ : b ∈ s), a * b = b * a) : +def closureCommMonoidOfComm {s : Set M} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) : CommMonoid (closure s) := { (closure s).toMonoid with mul_comm := fun x y => by diff --git a/Mathlib/GroupTheory/Subsemigroup/Membership.lean b/Mathlib/GroupTheory/Subsemigroup/Membership.lean index a46be74b9a2c0..5fbf1f8cc37ad 100644 --- a/Mathlib/GroupTheory/Subsemigroup/Membership.lean +++ b/Mathlib/GroupTheory/Subsemigroup/Membership.lean @@ -119,7 +119,7 @@ then it holds for all elements of the supremum of `S`. -/ elements of `S i` for all `i`, and is preserved under addition, then it holds for all elements of the supremum of `S`."] theorem iSup_induction (S : ι → Subsemigroup M) {C : M → Prop} {x₁ : M} (hx₁ : x₁ ∈ ⨆ i, S i) - (hp : ∀ (i) (x₂ : M) (_hxS : x₂ ∈ S i), C x₂) (hmul : ∀ x y, C x → C y → C (x * y)) : C x₁ := by + (hp : ∀ i, ∀ x₂ ∈ S i, C x₂) (hmul : ∀ x y, C x → C y → C (x * y)) : C x₁ := by rw [iSup_eq_closure] at hx₁ refine' closure_induction hx₁ (fun x₂ hx₂ => _) hmul obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx₂ diff --git a/Mathlib/LinearAlgebra/Eigenspace/Basic.lean b/Mathlib/LinearAlgebra/Eigenspace/Basic.lean index c5b30f32b3f3d..b0c4ba710772c 100644 --- a/Mathlib/LinearAlgebra/Eigenspace/Basic.lean +++ b/Mathlib/LinearAlgebra/Eigenspace/Basic.lean @@ -358,7 +358,7 @@ lemma injOn_generalizedEigenspace [NoZeroSMulDivisors R M] (f : End R M) : theorem independent_generalizedEigenspace [NoZeroSMulDivisors R M] (f : End R M) : CompleteLattice.Independent (fun μ ↦ ⨆ k, f.generalizedEigenspace μ k) := by classical - suffices ∀ μ (s : Finset R) (_ : μ ∉ s), Disjoint (⨆ k, f.generalizedEigenspace μ k) + suffices ∀ μ (s : Finset R), μ ∉ s → Disjoint (⨆ k, f.generalizedEigenspace μ k) (s.sup fun μ ↦ ⨆ k, f.generalizedEigenspace μ k) by simp_rw [CompleteLattice.independent_iff_supIndep_of_injOn f.injOn_generalizedEigenspace, Finset.supIndep_iff_disjoint_erase] diff --git a/Mathlib/LinearAlgebra/LinearIndependent.lean b/Mathlib/LinearAlgebra/LinearIndependent.lean index ce6061878003c..e2818f02d8c9b 100644 --- a/Mathlib/LinearAlgebra/LinearIndependent.lean +++ b/Mathlib/LinearAlgebra/LinearIndependent.lean @@ -1005,7 +1005,7 @@ theorem exists_maximal_independent' (s : ι → M) : theorem exists_maximal_independent (s : ι → M) : ∃ I : Set ι, (LinearIndependent R fun x : I => s x) ∧ - ∀ (i) (_ : i ∉ I), ∃ a : R, a ≠ 0 ∧ a • s i ∈ span R (s '' I) := by + ∀ i ∉ I, ∃ a : R, a ≠ 0 ∧ a • s i ∈ span R (s '' I) := by classical rcases exists_maximal_independent' R s with ⟨I, hIlinind, hImaximal⟩ use I, hIlinind diff --git a/Mathlib/MeasureTheory/Measure/VectorMeasure.lean b/Mathlib/MeasureTheory/Measure/VectorMeasure.lean index 32f40dfef6f7e..065e55fffb0bf 100644 --- a/Mathlib/MeasureTheory/Measure/VectorMeasure.lean +++ b/Mathlib/MeasureTheory/Measure/VectorMeasure.lean @@ -1167,7 +1167,7 @@ namespace MutuallySingular variable {v v₁ v₂ : VectorMeasure α M} {w w₁ w₂ : VectorMeasure α N} theorem mk (s : Set α) (hs : MeasurableSet s) (h₁ : ∀ t ⊆ s, MeasurableSet t → v t = 0) - (h₂ : ∀ (t) (_ : t ⊆ sᶜ), MeasurableSet t → w t = 0) : v ⟂ᵥ w := by + (h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → w t = 0) : v ⟂ᵥ w := by refine' ⟨s, hs, fun t hst => _, fun t hst => _⟩ <;> by_cases ht : MeasurableSet t · exact h₁ t hst ht · exact not_measurable v ht diff --git a/Mathlib/NumberTheory/DiophantineApproximation.lean b/Mathlib/NumberTheory/DiophantineApproximation.lean index 9ea505ff15bdf..f5af3c4ba8849 100644 --- a/Mathlib/NumberTheory/DiophantineApproximation.lean +++ b/Mathlib/NumberTheory/DiophantineApproximation.lean @@ -122,11 +122,10 @@ theorem exists_int_int_abs_mul_sub_le (ξ : ℝ) {n : ℕ} (n_pos : 0 < n) : have hwd : ∀ m : ℤ, m ∈ D → f m ∈ Ico (0 : ℤ) n := fun x hx => mem_Ico.mpr ⟨floor_nonneg.mpr (mul_nonneg (fract_nonneg (ξ * x)) hn.le), Ne.lt_of_le (H x hx) (hfu' x)⟩ - have : ∃ (x : ℤ) (_ : x ∈ D) (y : ℤ) (_ : y ∈ D), x < y ∧ f x = f y := by + obtain ⟨x, hx, y, hy, x_lt_y, hxy⟩ : ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y := by obtain ⟨x, hx, y, hy, x_ne_y, hxy⟩ := exists_ne_map_eq_of_card_lt_of_maps_to hD hwd rcases lt_trichotomy x y with (h | h | h) exacts [⟨x, hx, y, hy, h, hxy⟩, False.elim (x_ne_y h), ⟨y, hy, x, hx, h, hxy.symm⟩] - obtain ⟨x, hx, y, hy, x_lt_y, hxy⟩ := this refine' ⟨⌊ξ * y⌋ - ⌊ξ * x⌋, y - x, sub_pos_of_lt x_lt_y, sub_le_iff_le_add.mpr <| le_add_of_le_of_nonneg (mem_Icc.mp hy).2 (mem_Icc.mp hx).1, _⟩ diff --git a/Mathlib/RingTheory/DedekindDomain/Dvr.lean b/Mathlib/RingTheory/DedekindDomain/Dvr.lean index 6dcbeb736b11c..b32fe71a7be3e 100644 --- a/Mathlib/RingTheory/DedekindDomain/Dvr.lean +++ b/Mathlib/RingTheory/DedekindDomain/Dvr.lean @@ -59,8 +59,8 @@ TODO: prove the equivalence. -/ structure IsDedekindDomainDvr : Prop where isNoetherianRing : IsNoetherianRing A - is_dvr_at_nonzero_prime : - ∀ (P) (_ : P ≠ (⊥ : Ideal A)) (_ : P.IsPrime), DiscreteValuationRing (Localization.AtPrime P) + is_dvr_at_nonzero_prime : ∀ P ≠ (⊥ : Ideal A), ∀ _ : P.IsPrime, + DiscreteValuationRing (Localization.AtPrime P) #align is_dedekind_domain_dvr IsDedekindDomainDvr /-- Localizing a domain of Krull dimension `≤ 1` gives another ring of Krull dimension `≤ 1`. diff --git a/Mathlib/RingTheory/DedekindDomain/Ideal.lean b/Mathlib/RingTheory/DedekindDomain/Ideal.lean index 1be9caa7c604c..ed723c0b17f4a 100644 --- a/Mathlib/RingTheory/DedekindDomain/Ideal.lean +++ b/Mathlib/RingTheory/DedekindDomain/Ideal.lean @@ -245,7 +245,7 @@ assuming `IsDedekindDomain A`, which implies `IsDedekindDomainInv`. For **integr `IsDedekindDomain`(`_inv`) implies only `Ideal.cancelCommMonoidWithZero`. -/ def IsDedekindDomainInv : Prop := - ∀ (I) (_ : I ≠ (⊥ : FractionalIdeal A⁰ (FractionRing A))), I * I⁻¹ = 1 + ∀ I ≠ (⊥ : FractionalIdeal A⁰ (FractionRing A)), I * I⁻¹ = 1 #align is_dedekind_domain_inv IsDedekindDomainInv open FractionalIdeal @@ -253,7 +253,7 @@ open FractionalIdeal variable {R A K} theorem isDedekindDomainInv_iff [Algebra A K] [IsFractionRing A K] : - IsDedekindDomainInv A ↔ ∀ (I) (_ : I ≠ (⊥ : FractionalIdeal A⁰ K)), I * I⁻¹ = 1 := by + IsDedekindDomainInv A ↔ ∀ I ≠ (⊥ : FractionalIdeal A⁰ K), I * I⁻¹ = 1 := by let h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K := FractionalIdeal.mapEquiv (FractionRing.algEquiv A K) refine h.toEquiv.forall_congr (fun {x} => ?_) diff --git a/Mathlib/Topology/Category/TopCat/Limits/Cofiltered.lean b/Mathlib/Topology/Category/TopCat/Limits/Cofiltered.lean index 1f342f7f6693b..fac47af6971ac 100644 --- a/Mathlib/Topology/Category/TopCat/Limits/Cofiltered.lean +++ b/Mathlib/Topology/Category/TopCat/Limits/Cofiltered.lean @@ -76,7 +76,7 @@ theorem isTopologicalBasis_cofiltered_limit (T : ∀ j, Set (Set (F.obj j))) · simp · rintro ⟨U, G, h1, h2⟩ obtain ⟨j, hj⟩ := IsCofiltered.inf_objs_exists G - let g : ∀ (e) (_he : e ∈ G), j ⟶ e := fun _ he => (hj he).some + let g : ∀ e ∈ G, j ⟶ e := fun _ he => (hj he).some let Vs : J → Set (F.obj j) := fun e => if h : e ∈ G then F.map (g e h) ⁻¹' U e else Set.univ let V : Set (F.obj j) := ⋂ (e : J) (_he : e ∈ G), Vs e refine' ⟨j, V, _, _⟩ diff --git a/Mathlib/Topology/Semicontinuous.lean b/Mathlib/Topology/Semicontinuous.lean index 4ca4fa36d269f..7e7a6811d6e86 100644 --- a/Mathlib/Topology/Semicontinuous.lean +++ b/Mathlib/Topology/Semicontinuous.lean @@ -564,7 +564,7 @@ theorem lowerSemicontinuousWithinAt_iSup {f : ι → α → δ} lowerSemicontinuousWithinAt_ciSup (by simp) h #align lower_semicontinuous_within_at_supr lowerSemicontinuousWithinAt_iSup -theorem lowerSemicontinuousWithinAt_biSup {p : ι → Prop} {f : ∀ (i) (_h : p i), α → δ} +theorem lowerSemicontinuousWithinAt_biSup {p : ι → Prop} {f : ∀ i, p i → α → δ} (h : ∀ i hi, LowerSemicontinuousWithinAt (f i hi) s x) : LowerSemicontinuousWithinAt (fun x' => ⨆ (i) (hi), f i hi x') s x := lowerSemicontinuousWithinAt_iSup fun i => lowerSemicontinuousWithinAt_iSup fun hi => h i hi @@ -583,7 +583,7 @@ theorem lowerSemicontinuousAt_iSup {f : ι → α → δ} (h : ∀ i, LowerSemic lowerSemicontinuousAt_ciSup (by simp) h #align lower_semicontinuous_at_supr lowerSemicontinuousAt_iSup -theorem lowerSemicontinuousAt_biSup {p : ι → Prop} {f : ∀ (i) (_h : p i), α → δ} +theorem lowerSemicontinuousAt_biSup {p : ι → Prop} {f : ∀ i, p i → α → δ} (h : ∀ i hi, LowerSemicontinuousAt (f i hi) x) : LowerSemicontinuousAt (fun x' => ⨆ (i) (hi), f i hi x') x := lowerSemicontinuousAt_iSup fun i => lowerSemicontinuousAt_iSup fun hi => h i hi @@ -600,7 +600,7 @@ theorem lowerSemicontinuousOn_iSup {f : ι → α → δ} (h : ∀ i, LowerSemic lowerSemicontinuousOn_ciSup (by simp) h #align lower_semicontinuous_on_supr lowerSemicontinuousOn_iSup -theorem lowerSemicontinuousOn_biSup {p : ι → Prop} {f : ∀ (i) (_h : p i), α → δ} +theorem lowerSemicontinuousOn_biSup {p : ι → Prop} {f : ∀ i, p i → α → δ} (h : ∀ i hi, LowerSemicontinuousOn (f i hi) s) : LowerSemicontinuousOn (fun x' => ⨆ (i) (hi), f i hi x') s := lowerSemicontinuousOn_iSup fun i => lowerSemicontinuousOn_iSup fun hi => h i hi @@ -616,7 +616,7 @@ theorem lowerSemicontinuous_iSup {f : ι → α → δ} (h : ∀ i, LowerSemicon lowerSemicontinuous_ciSup (by simp) h #align lower_semicontinuous_supr lowerSemicontinuous_iSup -theorem lowerSemicontinuous_biSup {p : ι → Prop} {f : ∀ (i) (_h : p i), α → δ} +theorem lowerSemicontinuous_biSup {p : ι → Prop} {f : ∀ i, p i → α → δ} (h : ∀ i hi, LowerSemicontinuous (f i hi)) : LowerSemicontinuous fun x' => ⨆ (i) (hi), f i hi x' := lowerSemicontinuous_iSup fun i => lowerSemicontinuous_iSup fun hi => h i hi @@ -1006,7 +1006,7 @@ theorem upperSemicontinuousWithinAt_iInf {f : ι → α → δ} @lowerSemicontinuousWithinAt_iSup α _ x s ι δᵒᵈ _ f h #align upper_semicontinuous_within_at_infi upperSemicontinuousWithinAt_iInf -theorem upperSemicontinuousWithinAt_biInf {p : ι → Prop} {f : ∀ (i) (_h : p i), α → δ} +theorem upperSemicontinuousWithinAt_biInf {p : ι → Prop} {f : ∀ i, p i → α → δ} (h : ∀ i hi, UpperSemicontinuousWithinAt (f i hi) s x) : UpperSemicontinuousWithinAt (fun x' => ⨅ (i) (hi), f i hi x') s x := upperSemicontinuousWithinAt_iInf fun i => upperSemicontinuousWithinAt_iInf fun hi => h i hi @@ -1023,7 +1023,7 @@ theorem upperSemicontinuousAt_iInf {f : ι → α → δ} (h : ∀ i, UpperSemic @lowerSemicontinuousAt_iSup α _ x ι δᵒᵈ _ f h #align upper_semicontinuous_at_infi upperSemicontinuousAt_iInf -theorem upperSemicontinuousAt_biInf {p : ι → Prop} {f : ∀ (i) (_h : p i), α → δ} +theorem upperSemicontinuousAt_biInf {p : ι → Prop} {f : ∀ i, p i → α → δ} (h : ∀ i hi, UpperSemicontinuousAt (f i hi) x) : UpperSemicontinuousAt (fun x' => ⨅ (i) (hi), f i hi x') x := upperSemicontinuousAt_iInf fun i => upperSemicontinuousAt_iInf fun hi => h i hi @@ -1040,7 +1040,7 @@ theorem upperSemicontinuousOn_iInf {f : ι → α → δ} (h : ∀ i, UpperSemic upperSemicontinuousWithinAt_iInf fun i => h i x hx #align upper_semicontinuous_on_infi upperSemicontinuousOn_iInf -theorem upperSemicontinuousOn_biInf {p : ι → Prop} {f : ∀ (i) (_h : p i), α → δ} +theorem upperSemicontinuousOn_biInf {p : ι → Prop} {f : ∀ i, p i → α → δ} (h : ∀ i hi, UpperSemicontinuousOn (f i hi) s) : UpperSemicontinuousOn (fun x' => ⨅ (i) (hi), f i hi x') s := upperSemicontinuousOn_iInf fun i => upperSemicontinuousOn_iInf fun hi => h i hi @@ -1055,7 +1055,7 @@ theorem upperSemicontinuous_iInf {f : ι → α → δ} (h : ∀ i, UpperSemicon UpperSemicontinuous fun x' => ⨅ i, f i x' := fun x => upperSemicontinuousAt_iInf fun i => h i x #align upper_semicontinuous_infi upperSemicontinuous_iInf -theorem upperSemicontinuous_biInf {p : ι → Prop} {f : ∀ (i) (_h : p i), α → δ} +theorem upperSemicontinuous_biInf {p : ι → Prop} {f : ∀ i, p i → α → δ} (h : ∀ i hi, UpperSemicontinuous (f i hi)) : UpperSemicontinuous fun x' => ⨅ (i) (hi), f i hi x' := upperSemicontinuous_iInf fun i => upperSemicontinuous_iInf fun hi => h i hi diff --git a/Mathlib/Topology/ShrinkingLemma.lean b/Mathlib/Topology/ShrinkingLemma.lean index 768d8e28e0227..9339ed5884f62 100644 --- a/Mathlib/Topology/ShrinkingLemma.lean +++ b/Mathlib/Topology/ShrinkingLemma.lean @@ -185,7 +185,7 @@ theorem exists_gt (v : PartialRefinement u s) (hs : IsClosed s) (i : ι) (hi : i · intro j rcases eq_or_ne j i with (rfl| hne) <;> simp [*, v.isOpen] · refine' fun x hx => mem_iUnion.2 _ - rcases em (∃ (j : _) (_ : j ≠ i), x ∈ v j) with (⟨j, hji, hj⟩ | h) + rcases em (∃ j ≠ i, x ∈ v j) with (⟨j, hji, hj⟩ | h) · use j rwa [update_noteq hji] · push_neg at h