From 483848e8afb952d25f51f5ab865b4b3525c086b9 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Thu, 4 Apr 2024 22:42:55 +0000 Subject: [PATCH] chore: tidy various files (#11624) --- Archive/Wiedijk100Theorems/CubingACube.lean | 2 +- Mathlib/Algebra/Divisibility/Units.lean | 5 +++-- .../Module/Submodule/RestrictScalars.lean | 2 +- Mathlib/Algebra/Order/Monoid/MinMax.lean | 2 +- Mathlib/Algebra/Ring/InjSurj.lean | 2 +- Mathlib/AlgebraicGeometry/AffineScheme.lean | 8 ++----- .../InnerProductSpace/Projection.lean | 3 --- .../Analysis/Normed/Group/CocompactMap.lean | 6 ++--- Mathlib/CategoryTheory/Sites/Equivalence.lean | 4 ++-- Mathlib/Data/Polynomial/Eval.lean | 4 ++-- Mathlib/Data/Real/EReal.lean | 8 +++---- Mathlib/Data/Set/Lattice.lean | 2 +- Mathlib/FieldTheory/Minpoly/Field.lean | 13 ++++++----- Mathlib/FieldTheory/Perfect.lean | 6 +++-- .../Geometry/Manifold/PartitionOfUnity.lean | 5 ++--- Mathlib/GroupTheory/Perm/Cycle/Factors.lean | 5 ++--- Mathlib/LinearAlgebra/Dual.lean | 2 +- Mathlib/LinearAlgebra/Matrix/ToLin.lean | 20 ++++++++--------- .../LinearAlgebra/TensorProduct/Basic.lean | 14 ++++++------ Mathlib/Logic/Function/Basic.lean | 2 +- .../Function/ConditionalExpectation/Real.lean | 5 +++-- .../Integral/BoundedContinuousFunction.lean | 10 ++++----- .../MeasurableSpace/CountablyGenerated.lean | 12 ++++------ Mathlib/MeasureTheory/Measure/Count.lean | 4 ---- .../Measure/LevyProkhorovMetric.lean | 22 +++++++++---------- Mathlib/NumberTheory/SmoothNumbers.lean | 3 +-- .../Kernel/Disintegration/Density.lean | 10 ++++----- Mathlib/RingTheory/AlgebraTower.lean | 3 +-- Mathlib/RingTheory/Binomial.lean | 2 +- Mathlib/RingTheory/Coprime/Lemmas.lean | 2 +- Mathlib/RingTheory/Finiteness.lean | 3 +-- Mathlib/RingTheory/Polynomial/Pochhammer.lean | 4 ++-- Mathlib/RingTheory/PowerSeries/Order.lean | 10 ++------- Mathlib/RingTheory/PrincipalIdealDomain.lean | 6 ++--- Mathlib/SetTheory/Cardinal/Basic.lean | 2 +- Mathlib/SetTheory/Ordinal/Basic.lean | 11 +++++----- Mathlib/Topology/Compactness/Lindelof.lean | 6 ++--- Mathlib/Topology/UniformSpace/Basic.lean | 2 +- Mathlib/Topology/UniformSpace/Separation.lean | 2 +- 39 files changed, 105 insertions(+), 129 deletions(-) diff --git a/Archive/Wiedijk100Theorems/CubingACube.lean b/Archive/Wiedijk100Theorems/CubingACube.lean index 6606b2f0dba71..744556b41831d 100644 --- a/Archive/Wiedijk100Theorems/CubingACube.lean +++ b/Archive/Wiedijk100Theorems/CubingACube.lean @@ -573,7 +573,7 @@ theorem cannot_cube_a_cube : ∀ {s : Set (Cube n)}, s.Finite → -- given a finite collection of (hyper)cubes s.Nontrivial → -- containing at least two elements s.PairwiseDisjoint Cube.toSet → -- which is pairwise disjoint - ⋃ c ∈ s, Cube.toSet c = unitCube.toSet → -- whose union is the unit cube + ⋃ c ∈ s, Cube.toSet c = unitCube.toSet → -- whose union is the unit cube InjOn Cube.w s → -- such that the widths of all cubes are different False := by -- then we can derive a contradiction intro n hn s hfin h2 hd hU hinj diff --git a/Mathlib/Algebra/Divisibility/Units.lean b/Mathlib/Algebra/Divisibility/Units.lean index 9b86f26ebfe0e..a3e7460e606f1 100644 --- a/Mathlib/Algebra/Divisibility/Units.lean +++ b/Mathlib/Algebra/Divisibility/Units.lean @@ -251,8 +251,9 @@ theorem IsRelPrime.mul_left (H1 : IsRelPrime x z) (H2 : IsRelPrime y z) : IsRelP obtain ⟨a, b, ha, hb, rfl⟩ := exists_dvd_and_dvd_of_dvd_mul h exact (H1 ha <| (dvd_mul_right a b).trans hz).mul (H2 hb <| (dvd_mul_left b a).trans hz) -theorem IsRelPrime.mul_right (H1 : IsRelPrime x y) (H2 : IsRelPrime x z) : IsRelPrime x (y * z) := - by rw [isRelPrime_comm] at H1 H2 ⊢; exact H1.mul_left H2 +theorem IsRelPrime.mul_right (H1 : IsRelPrime x y) (H2 : IsRelPrime x z) : + IsRelPrime x (y * z) := by + rw [isRelPrime_comm] at H1 H2 ⊢; exact H1.mul_left H2 theorem IsRelPrime.mul_left_iff : IsRelPrime (x * y) z ↔ IsRelPrime x z ∧ IsRelPrime y z := ⟨fun H ↦ ⟨H.of_mul_left_left, H.of_mul_left_right⟩, fun ⟨H1, H2⟩ ↦ H1.mul_left H2⟩ diff --git a/Mathlib/Algebra/Module/Submodule/RestrictScalars.lean b/Mathlib/Algebra/Module/Submodule/RestrictScalars.lean index 4d695134ccf88..c9130a29620d6 100644 --- a/Mathlib/Algebra/Module/Submodule/RestrictScalars.lean +++ b/Mathlib/Algebra/Module/Submodule/RestrictScalars.lean @@ -25,7 +25,7 @@ namespace Submodule variable (S : Type*) {R M : Type*} [Semiring R] [AddCommMonoid M] [Semiring S] [Module S M] [Module R M] [SMul S R] [IsScalarTower S R M] -/-- `V.restrict_scalars S` is the `S`-submodule of the `S`-module given by restriction of scalars, +/-- `V.restrictScalars S` is the `S`-submodule of the `S`-module given by restriction of scalars, corresponding to `V`, an `R`-submodule of the original `R`-module. -/ def restrictScalars (V : Submodule R M) : Submodule S M where diff --git a/Mathlib/Algebra/Order/Monoid/MinMax.lean b/Mathlib/Algebra/Order/Monoid/MinMax.lean index 7deead61e0f12..48f85459e3b73 100644 --- a/Mathlib/Algebra/Order/Monoid/MinMax.lean +++ b/Mathlib/Algebra/Order/Monoid/MinMax.lean @@ -21,7 +21,7 @@ variable {α β : Type*} rules relating them. -/ section CommSemigroup -variable[LinearOrder α] [CommSemigroup α] [CommSemigroup β] +variable [LinearOrder α] [CommSemigroup α] [CommSemigroup β] @[to_additive] lemma fn_min_mul_fn_max (f : α → β) (a b : α) : f (min a b) * f (max a b) = f a * f b := by diff --git a/Mathlib/Algebra/Ring/InjSurj.lean b/Mathlib/Algebra/Ring/InjSurj.lean index 5bd9a68fbd480..cc410ccc8c960 100644 --- a/Mathlib/Algebra/Ring/InjSurj.lean +++ b/Mathlib/Algebra/Ring/InjSurj.lean @@ -304,7 +304,7 @@ protected def Function.Injective.commSemiring [CommSemiring α] (f : β → α) __ := hf.commSemigroup f mul #align function.injective.comm_semiring Function.Injective.commSemiring -/-- Pushforward a `NonAssocSemiring` instance along a surjective function. -/ +/-- Pushforward a `CommSemiring` instance along a surjective function. -/ @[reducible] -- See note [reducible non-instances] protected def Function.Surjective.commSemiring [CommSemiring α] (f : α → β) (hf : Surjective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) diff --git a/Mathlib/AlgebraicGeometry/AffineScheme.lean b/Mathlib/AlgebraicGeometry/AffineScheme.lean index 550bca2881f1d..a15f41914b5fd 100644 --- a/Mathlib/AlgebraicGeometry/AffineScheme.lean +++ b/Mathlib/AlgebraicGeometry/AffineScheme.lean @@ -569,9 +569,7 @@ theorem basicOpen_union_eq_self_iff (s : Set (X.presheaf.obj <| op U)) : intro x _ exact X.basicOpen_le x · simp only [Opens.iSup_def, Subtype.coe_mk, Set.preimage_iUnion] - -- Porting note: need an extra rewrite here, after simp, it is in `↔` form - rw [iff_iff_eq] - congr 3 + congr! 1 · refine congr_arg (Set.iUnion ·) ?_ ext1 x exact congr_arg Opens.carrier (hU.fromSpec_map_basicOpen _) @@ -614,9 +612,7 @@ theorem of_affine_open_cover {X : Scheme} (V : X.affineOpens) (S : Set X.affineO have : ∀ (x : V.1), ∃ f : X.presheaf.obj <| op V.1, ↑x ∈ X.basicOpen f ∧ P (X.affineBasicOpen f) := by intro x - have : ↑x ∈ (Set.univ : Set X) := trivial - rw [← hS] at this - obtain ⟨W, hW⟩ := Set.mem_iUnion.mp this + obtain ⟨W, hW⟩ := Set.mem_iUnion.mp (by simpa only [← hS] using Set.mem_univ (x : X)) obtain ⟨f, g, e, hf⟩ := exists_basicOpen_le_affine_inter V.prop W.1.prop x ⟨x.prop, hW⟩ refine' ⟨f, hf, _⟩ convert hP₁ _ g (hS' W) using 1 diff --git a/Mathlib/Analysis/InnerProductSpace/Projection.lean b/Mathlib/Analysis/InnerProductSpace/Projection.lean index 0645ed5c1d26c..4d7ae8e530725 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection.lean @@ -54,10 +54,7 @@ variable {𝕜 E F : Type*} [RCLike 𝕜] variable [NormedAddCommGroup E] [NormedAddCommGroup F] variable [InnerProductSpace 𝕜 E] [InnerProductSpace ℝ F] --- mathport name: «expr⟪ , ⟫» local notation "⟪" x ", " y "⟫" => @inner 𝕜 _ _ x y - --- mathport name: exprabsR local notation "absR" => abs /-! ### Orthogonal projection in inner product spaces -/ diff --git a/Mathlib/Analysis/Normed/Group/CocompactMap.lean b/Mathlib/Analysis/Normed/Group/CocompactMap.lean index 314ecf84d0305..919f345193ef6 100644 --- a/Mathlib/Analysis/Normed/Group/CocompactMap.lean +++ b/Mathlib/Analysis/Normed/Group/CocompactMap.lean @@ -27,7 +27,7 @@ variable [NormedAddCommGroup E] [NormedAddCommGroup F] [ProperSpace E] [ProperSp variable {f : 𝓕} theorem CocompactMapClass.norm_le [FunLike 𝓕 E F] [CocompactMapClass 𝓕 E F] (ε : ℝ) : - ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), ε < ‖f x‖ := by + ∃ r : ℝ, ∀ x : E, r < ‖x‖ → ε < ‖f x‖ := by have h := cocompact_tendsto f rw [tendsto_def] at h specialize h (Metric.closedBall 0 ε)ᶜ (mem_cocompact_of_closedBall_compl_subset 0 ⟨ε, rfl.subset⟩) @@ -39,7 +39,7 @@ theorem CocompactMapClass.norm_le [FunLike 𝓕 E F] [CocompactMapClass 𝓕 E F simp [hx] theorem Filter.tendsto_cocompact_cocompact_of_norm {f : E → F} - (h : ∀ ε : ℝ, ∃ r : ℝ, ∀ (x : E) (_hx : r < ‖x‖), ε < ‖f x‖) : + (h : ∀ ε : ℝ, ∃ r : ℝ, ∀ x : E, r < ‖x‖ → ε < ‖f x‖) : Tendsto f (cocompact E) (cocompact F) := by rw [tendsto_def] intro s hs @@ -53,6 +53,6 @@ theorem Filter.tendsto_cocompact_cocompact_of_norm {f : E → F} simp [hr x hx] theorem ContinuousMapClass.toCocompactMapClass_of_norm [FunLike 𝓕 E F] [ContinuousMapClass 𝓕 E F] - (h : ∀ (f : 𝓕) (ε : ℝ), ∃ r : ℝ, ∀ (x : E) (_hx : r < ‖x‖), ε < ‖f x‖) : + (h : ∀ (f : 𝓕) (ε : ℝ), ∃ r : ℝ, ∀ x : E, r < ‖x‖ → ε < ‖f x‖) : CocompactMapClass 𝓕 E F where cocompact_tendsto := (tendsto_cocompact_cocompact_of_norm <| h ·) diff --git a/Mathlib/CategoryTheory/Sites/Equivalence.lean b/Mathlib/CategoryTheory/Sites/Equivalence.lean index cf34f844e6f4e..c1d083cadbf76 100644 --- a/Mathlib/CategoryTheory/Sites/Equivalence.lean +++ b/Mathlib/CategoryTheory/Sites/Equivalence.lean @@ -77,7 +77,7 @@ theorem coverPreserving : CoverPreserving J (e.locallyCoverDense J).inducedTopol simpa using S.downward_closed hg _ · intro hf exact ⟨_, e.unitInv.app Z ≫ f ≫ e.unitInv.app U, S.downward_closed hf _, - e.unit.app Z ≫ e.unit.app _, (by simp)⟩ + e.unit.app Z ≫ e.unit.app _, by simp⟩ instance : IsCoverDense e.functor (e.locallyCoverDense J).inducedTopology where is_cover U := by @@ -87,7 +87,7 @@ instance : IsCoverDense e.functor (e.locallyCoverDense J).inducedTopology where simp only [Sieve.functorPushforward_apply, Presieve.functorPushforward, exists_and_left, Sieve.top_apply, iff_true] exact ⟨e.functor.obj Y, (Adjunction.homEquiv e.toAdjunction _ _).symm f, - Presieve.in_coverByImage _ _, e.unit.app _, (by simp)⟩ + Presieve.in_coverByImage _ _, e.unit.app _, by simp⟩ instance : IsCoverDense e.inverse J where is_cover U := by diff --git a/Mathlib/Data/Polynomial/Eval.lean b/Mathlib/Data/Polynomial/Eval.lean index d99e281bf076d..adef01a6bf428 100644 --- a/Mathlib/Data/Polynomial/Eval.lean +++ b/Mathlib/Data/Polynomial/Eval.lean @@ -1094,8 +1094,8 @@ theorem eval₂_pow' (n : ℕ) : theorem eval₂_comp' : eval₂ (algebraMap R S) x (p.comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) p := by induction p using Polynomial.induction_on' with - | h_add r s hr hs => simp only [add_comp, eval₂_add, hr, hs] - | h_monomial n a => simp only [monomial_comp, eval₂_mul', eval₂_C, eval₂_monomial, eval₂_pow'] + | h_add r s hr hs => simp only [add_comp, eval₂_add, hr, hs] + | h_monomial n a => simp only [monomial_comp, eval₂_mul', eval₂_C, eval₂_monomial, eval₂_pow'] end Algebra diff --git a/Mathlib/Data/Real/EReal.lean b/Mathlib/Data/Real/EReal.lean index 3ae3942ebe7db..0770355995adb 100644 --- a/Mathlib/Data/Real/EReal.lean +++ b/Mathlib/Data/Real/EReal.lean @@ -450,10 +450,10 @@ theorem eq_bot_iff_forall_lt (x : EReal) : x = ⊥ ↔ ∀ y : ℝ, x < (y : ERe lemma exists_between_coe_real {x z : EReal} (h : x < z) : ∃ y : ℝ, x < y ∧ y < z := by obtain ⟨a, ha₁, ha₂⟩ := exists_between h - induction' a using EReal.rec with a₀ - · exact (not_lt_bot ha₁).elim - · exact ⟨a₀, by exact_mod_cast ha₁, by exact_mod_cast ha₂⟩ - · exact (not_top_lt ha₂).elim + induction a using EReal.rec with + | h_bot => exact (not_lt_bot ha₁).elim + | h_real a₀ => exact ⟨a₀, ha₁, ha₂⟩ + | h_top => exact (not_top_lt ha₂).elim @[simp] lemma image_coe_Icc (x y : ℝ) : Real.toEReal '' Icc x y = Icc ↑x ↑y := by diff --git a/Mathlib/Data/Set/Lattice.lean b/Mathlib/Data/Set/Lattice.lean index 9ff06b86e7abf..766a1c2b4b4e1 100644 --- a/Mathlib/Data/Set/Lattice.lean +++ b/Mathlib/Data/Set/Lattice.lean @@ -31,7 +31,7 @@ for `Set α`, and some more set constructions. `f ⁻¹ y ⊆ s`. * `Set.seq`: Union of the image of a set under a **seq**uence of functions. `seq s t` is the union of `f '' t` over all `f ∈ s`, where `t : Set α` and `s : Set (α → β)`. -* `Set.iUnion_eq_sigma_of_disjoint`: Equivalence between `⋃ i, t i` and `Σ i, t i`, where `t` is an +* `Set.unionEqSigmaOfDisjoint`: Equivalence between `⋃ i, t i` and `Σ i, t i`, where `t` is an indexed family of disjoint sets. ## Naming convention diff --git a/Mathlib/FieldTheory/Minpoly/Field.lean b/Mathlib/FieldTheory/Minpoly/Field.lean index 6f82d9c3c2679..6dc847b5ce13a 100644 --- a/Mathlib/FieldTheory/Minpoly/Field.lean +++ b/Mathlib/FieldTheory/Minpoly/Field.lean @@ -300,11 +300,12 @@ lemma minpoly_algEquiv_toLinearMap (σ : L ≃ₐ[K] L) (hσ : IsOfFinOrder σ) lemma minpoly_algHom_toLinearMap (σ : L →ₐ[K] L) (hσ : IsOfFinOrder σ) : minpoly K σ.toLinearMap = X ^ (orderOf σ) - C 1 := by have : orderOf σ = orderOf (AlgEquiv.algHomUnitsEquiv _ _ hσ.unit) := by - erw [orderOf_injective (AlgEquiv.algHomUnitsEquiv K L) - (AlgEquiv.algHomUnitsEquiv K L).injective] - rw [← orderOf_units] - rfl - rw [this, ← minpoly_algEquiv_toLinearMap]; rfl - rwa [← orderOf_pos_iff, ← this, orderOf_pos_iff] + rw [← MonoidHom.coe_coe, orderOf_injective (AlgEquiv.algHomUnitsEquiv K L) + (AlgEquiv.algHomUnitsEquiv K L).injective, ← orderOf_units, IsOfFinOrder.val_unit] + rw [this, ← minpoly_algEquiv_toLinearMap] + · apply congr_arg + ext + simp + · rwa [← orderOf_pos_iff, ← this, orderOf_pos_iff] end AlgHom diff --git a/Mathlib/FieldTheory/Perfect.lean b/Mathlib/FieldTheory/Perfect.lean index a06d6c24d5199..43a3f223242de 100644 --- a/Mathlib/FieldTheory/Perfect.lean +++ b/Mathlib/FieldTheory/Perfect.lean @@ -375,7 +375,8 @@ It's given by `x ↦ x ^ p`, see `rootsExpandEquivRoots_apply`. -/ noncomputable def rootsExpandEquivRoots : (expand R p f).roots.toFinset ≃ f.roots.toFinset := ((frobeniusEquiv R p).image _).trans <| .Set.ofEq <| show _ '' (setOf _) = setOf _ by classical simp_rw [← roots_expand_image_frobenius (p := p) (f := f), Finset.mem_val, - Finset.setOf_mem, Finset.coe_image]; rfl + Finset.setOf_mem, Finset.coe_image, RingEquiv.toEquiv_eq_coe, EquivLike.coe_coe, + frobeniusEquiv_apply] @[simp] theorem rootsExpandEquivRoots_apply (x) : (rootsExpandEquivRoots p f x : R) = x ^ p := rfl @@ -387,7 +388,8 @@ noncomputable def rootsExpandPowEquivRoots (n : ℕ) : (expand R (p ^ n) f).roots.toFinset ≃ f.roots.toFinset := ((iterateFrobeniusEquiv R p n).image _).trans <| .Set.ofEq <| show _ '' (setOf _) = setOf _ by classical simp_rw [← roots_expand_image_iterateFrobenius (p := p) (f := f) (n := n), - Finset.mem_val, Finset.setOf_mem, Finset.coe_image]; rfl + Finset.mem_val, Finset.setOf_mem, Finset.coe_image, RingEquiv.toEquiv_eq_coe, + EquivLike.coe_coe, iterateFrobeniusEquiv_apply] @[simp] theorem rootsExpandPowEquivRoots_apply (n : ℕ) (x) : diff --git a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean index 5d07cfeffb8d9..a1e3058b9f280 100644 --- a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean +++ b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean @@ -271,14 +271,13 @@ theorem finite_tsupport : {i | x₀ ∈ tsupport (ρ i)}.Finite := /-- The tsupport of a partition of unity at a point `x₀` as a `Finset`. This is the set of `i : ι` such that `x₀ ∈ tsupport f i`. -/ -def fintsupport (x : M ): Finset ι := +def fintsupport (x : M) : Finset ι := (ρ.finite_tsupport x).toFinset theorem mem_fintsupport_iff (i : ι) : i ∈ ρ.fintsupport x₀ ↔ x₀ ∈ tsupport (ρ i) := Finite.mem_toFinset _ -theorem eventually_fintsupport_subset : - ∀ᶠ y in 𝓝 x₀, ρ.fintsupport y ⊆ ρ.fintsupport x₀ := +theorem eventually_fintsupport_subset : ∀ᶠ y in 𝓝 x₀, ρ.fintsupport y ⊆ ρ.fintsupport x₀ := ρ.toPartitionOfUnity.eventually_fintsupport_subset _ theorem finsupport_subset_fintsupport : ρ.finsupport x₀ ⊆ ρ.fintsupport x₀ := diff --git a/Mathlib/GroupTheory/Perm/Cycle/Factors.lean b/Mathlib/GroupTheory/Perm/Cycle/Factors.lean index 4f63d2d91129c..222496acec54e 100644 --- a/Mathlib/GroupTheory/Perm/Cycle/Factors.lean +++ b/Mathlib/GroupTheory/Perm/Cycle/Factors.lean @@ -313,7 +313,7 @@ end CycleOf section cycleFactors open scoped List in -/-- Given a list `l : List α` and a permutation `f : perm α` whose nonfixed points are all in `l`, +/-- Given a list `l : List α` and a permutation `f : Perm α` whose nonfixed points are all in `l`, recursively factors `f` into cycles. -/ def cycleFactorsAux [DecidableEq α] [Fintype α] : ∀ (l : List α) (f : Perm α), @@ -352,8 +352,7 @@ def cycleFactorsAux [DecidableEq α] [Fintype α] : have hgm : (g::m.erase g) ~ m := List.cons_perm_iff_perm_erase.2 ⟨hg, List.Perm.refl _⟩ have : ∀ h ∈ m.erase g, Disjoint g h := - (List.pairwise_cons.1 - ((hgm.pairwise_iff @fun a b (h : Disjoint a b) => h.symm).2 hm₃)).1 + (List.pairwise_cons.1 ((hgm.pairwise_iff Disjoint.symm).2 hm₃)).1 by_cases id fun hgy : g y ≠ y => (disjoint_prod_right _ this y).resolve_right <| by have hsc : SameCycle f⁻¹ x (f y) := by diff --git a/Mathlib/LinearAlgebra/Dual.lean b/Mathlib/LinearAlgebra/Dual.lean index 891907a42b6f2..00078c5ade191 100644 --- a/Mathlib/LinearAlgebra/Dual.lean +++ b/Mathlib/LinearAlgebra/Dual.lean @@ -662,7 +662,7 @@ def evalEquiv : M ≃ₗ[R] Dual R (Dual R M) := /-- The dual of a reflexive module is reflexive. -/ instance Dual.instIsReflecive : IsReflexive R (Dual R M) := -⟨by simpa only [← symm_dualMap_evalEquiv] using (evalEquiv R M).dualMap.symm.bijective⟩ + ⟨by simpa only [← symm_dualMap_evalEquiv] using (evalEquiv R M).dualMap.symm.bijective⟩ /-- The isomorphism `Module.evalEquiv` induces an order isomorphism on subspaces. -/ def mapEvalEquiv : Submodule R M ≃o Submodule R (Dual R (Dual R M)) := diff --git a/Mathlib/LinearAlgebra/Matrix/ToLin.lean b/Mathlib/LinearAlgebra/Matrix/ToLin.lean index ec08452ef1086..906a0100d0056 100644 --- a/Mathlib/LinearAlgebra/Matrix/ToLin.lean +++ b/Mathlib/LinearAlgebra/Matrix/ToLin.lean @@ -655,8 +655,8 @@ theorem LinearMap.toMatrix_reindexRange [DecidableEq M₁] [DecidableEq M₂] (f (i : n) : LinearMap.toMatrix v₁.reindexRange v₂.reindexRange f ⟨v₂ k, Set.mem_range_self k⟩ ⟨v₁ i, Set.mem_range_self i⟩ = - LinearMap.toMatrix v₁ v₂ f k i := - by simp_rw [LinearMap.toMatrix_apply, Basis.reindexRange_self, Basis.reindexRange_repr] + LinearMap.toMatrix v₁ v₂ f k i := by + simp_rw [LinearMap.toMatrix_apply, Basis.reindexRange_self, Basis.reindexRange_repr] #align linear_map.to_matrix_reindex_range LinearMap.toMatrix_reindexRange variable {M₃ : Type*} [AddCommMonoid M₃] [Module R M₃] (v₃ : Basis l R M₃) @@ -812,14 +812,14 @@ theorem Matrix.toLinAlgEquiv_one : Matrix.toLinAlgEquiv v₁ 1 = LinearMap.id := theorem LinearMap.toMatrixAlgEquiv_reindexRange [DecidableEq M₁] (f : M₁ →ₗ[R] M₁) (k i : n) : LinearMap.toMatrixAlgEquiv v₁.reindexRange f ⟨v₁ k, Set.mem_range_self k⟩ ⟨v₁ i, Set.mem_range_self i⟩ = - LinearMap.toMatrixAlgEquiv v₁ f k i := - by simp_rw [LinearMap.toMatrixAlgEquiv_apply, Basis.reindexRange_self, Basis.reindexRange_repr] + LinearMap.toMatrixAlgEquiv v₁ f k i := by + simp_rw [LinearMap.toMatrixAlgEquiv_apply, Basis.reindexRange_self, Basis.reindexRange_repr] #align linear_map.to_matrix_alg_equiv_reindex_range LinearMap.toMatrixAlgEquiv_reindexRange theorem LinearMap.toMatrixAlgEquiv_comp (f g : M₁ →ₗ[R] M₁) : LinearMap.toMatrixAlgEquiv v₁ (f.comp g) = - LinearMap.toMatrixAlgEquiv v₁ f * LinearMap.toMatrixAlgEquiv v₁ g := - by simp [LinearMap.toMatrixAlgEquiv, LinearMap.toMatrix_comp v₁ v₁ v₁ f g] + LinearMap.toMatrixAlgEquiv v₁ f * LinearMap.toMatrixAlgEquiv v₁ g := by + simp [LinearMap.toMatrixAlgEquiv, LinearMap.toMatrix_comp v₁ v₁ v₁ f g] #align linear_map.to_matrix_alg_equiv_comp LinearMap.toMatrixAlgEquiv_comp theorem LinearMap.toMatrixAlgEquiv_mul (f g : M₁ →ₗ[R] M₁) : @@ -830,15 +830,15 @@ theorem LinearMap.toMatrixAlgEquiv_mul (f g : M₁ →ₗ[R] M₁) : theorem Matrix.toLinAlgEquiv_mul (A B : Matrix n n R) : Matrix.toLinAlgEquiv v₁ (A * B) = - (Matrix.toLinAlgEquiv v₁ A).comp (Matrix.toLinAlgEquiv v₁ B) := - by convert Matrix.toLin_mul v₁ v₁ v₁ A B + (Matrix.toLinAlgEquiv v₁ A).comp (Matrix.toLinAlgEquiv v₁ B) := by + convert Matrix.toLin_mul v₁ v₁ v₁ A B #align matrix.to_lin_alg_equiv_mul Matrix.toLinAlgEquiv_mul @[simp] theorem Matrix.toLin_finTwoProd_apply (a b c d : R) (x : R × R) : Matrix.toLin (Basis.finTwoProd R) (Basis.finTwoProd R) !![a, b; c, d] x = - (a * x.fst + b * x.snd, c * x.fst + d * x.snd) := - by simp [Matrix.toLin_apply, Matrix.mulVec, Matrix.dotProduct] + (a * x.fst + b * x.snd, c * x.fst + d * x.snd) := by + simp [Matrix.toLin_apply, Matrix.mulVec, Matrix.dotProduct] #align matrix.to_lin_fin_two_prod_apply Matrix.toLin_finTwoProd_apply theorem Matrix.toLin_finTwoProd (a b c d : R) : diff --git a/Mathlib/LinearAlgebra/TensorProduct/Basic.lean b/Mathlib/LinearAlgebra/TensorProduct/Basic.lean index 0161d8d01c903..e2b6ff6ceaf0b 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Basic.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Basic.lean @@ -334,13 +334,13 @@ protected theorem add_smul (r s : R'') (x : M ⊗[R] N) : (r + s) • x = r • #align tensor_product.add_smul TensorProduct.add_smul instance addMonoid : AddMonoid (M ⊗[R] N) := -{ TensorProduct.addZeroClass _ _ with - toAddSemigroup := TensorProduct.addSemigroup _ _ - toZero := (TensorProduct.addZeroClass _ _).toZero - nsmul := fun n v => n • v - nsmul_zero := by simp [TensorProduct.zero_smul] - nsmul_succ := by simp only [TensorProduct.one_smul, TensorProduct.add_smul, add_comm, - forall_const] } + { TensorProduct.addZeroClass _ _ with + toAddSemigroup := TensorProduct.addSemigroup _ _ + toZero := (TensorProduct.addZeroClass _ _).toZero + nsmul := fun n v => n • v + nsmul_zero := by simp [TensorProduct.zero_smul] + nsmul_succ := by simp only [TensorProduct.one_smul, TensorProduct.add_smul, add_comm, + forall_const] } instance addCommMonoid : AddCommMonoid (M ⊗[R] N) := { TensorProduct.addCommSemigroup _ _ with diff --git a/Mathlib/Logic/Function/Basic.lean b/Mathlib/Logic/Function/Basic.lean index d7bd273a321c6..9f7eaf071cb4c 100644 --- a/Mathlib/Logic/Function/Basic.lean +++ b/Mathlib/Logic/Function/Basic.lean @@ -806,7 +806,7 @@ namespace FactorsThrough protected theorem rfl {f : α → β} : FactorsThrough f f := fun _ _ ↦ id -theorem comp_left {f : α → β} {g : α → γ} (h : FactorsThrough g f) (g' : γ → δ) : +theorem comp_left {f : α → β} {g : α → γ} (h : FactorsThrough g f) (g' : γ → δ) : FactorsThrough (g' ∘ g) f := fun _x _y hxy ↦ congr_arg g' (h hxy) diff --git a/Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean b/Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean index 36fc3b57df8cc..b158dc267bb2f 100644 --- a/Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean +++ b/Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean @@ -131,7 +131,7 @@ theorem set_integral_abs_condexp_le {s : Set α} (hs : MeasurableSet[m] s) (f : (condexp_indicator hfint hs).fun_comp abs refine' EventuallyEq.trans (eventually_of_forall fun x => _) this.symm rw [← Real.norm_eq_abs, norm_indicator_eq_indicator_norm] - rfl + simp only [Real.norm_eq_abs] rw [this, ← integral_indicator (hnm _ hs)] refine' (integral_abs_condexp_le _).trans (le_of_eq <| integral_congr_ae <| eventually_of_forall fun x => _) @@ -229,7 +229,8 @@ theorem condexp_stronglyMeasurable_simpleFunc_mul (hm : m ≤ m0) (f : @SimpleFu intro s c f ext1 x by_cases hx : x ∈ s - · simp only [hx, Pi.mul_apply, Set.indicator_of_mem, Pi.smul_apply, Algebra.id.smul_eq_mul]; rfl + · simp only [hx, Pi.mul_apply, Set.indicator_of_mem, Pi.smul_apply, Algebra.id.smul_eq_mul, + Function.const_apply] · simp only [hx, Pi.mul_apply, Set.indicator_of_not_mem, not_false_iff, zero_mul] apply @SimpleFunc.induction _ _ m _ (fun f => _) (fun c s hs => ?_) (fun g₁ g₂ _ h_eq₁ h_eq₂ => ?_) f diff --git a/Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean b/Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean index 15a98476ed6d0..94a3ec42e5b17 100644 --- a/Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean +++ b/Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean @@ -40,16 +40,14 @@ theorem measurable_coe_ennreal_comp (f : X →ᵇ ℝ≥0) : variable (μ : Measure X) [IsFiniteMeasure μ] -theorem lintegral_lt_top_of_nnreal (f : X →ᵇ ℝ≥0) : - (∫⁻ x, f x ∂μ) < ∞ := by +theorem lintegral_lt_top_of_nnreal (f : X →ᵇ ℝ≥0) : ∫⁻ x, f x ∂μ < ∞ := by apply IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal refine ⟨nndist f 0, fun x ↦ ?_⟩ have key := BoundedContinuousFunction.NNReal.upper_bound f x rwa [ENNReal.coe_le_coe] #align measure_theory.lintegral_lt_top_of_bounded_continuous_to_nnreal BoundedContinuousFunction.lintegral_lt_top_of_nnreal -theorem integrable_of_nnreal (f : X →ᵇ ℝ≥0) : - Integrable (((↑) : ℝ≥0 → ℝ) ∘ ⇑f) μ := by +theorem integrable_of_nnreal (f : X →ᵇ ℝ≥0) : Integrable (((↑) : ℝ≥0 → ℝ) ∘ ⇑f) μ := by refine' ⟨(NNReal.continuous_coe.comp f.continuous).measurable.aestronglyMeasurable, _⟩ simp only [HasFiniteIntegral, Function.comp_apply, NNReal.nnnorm_eq] exact lintegral_lt_top_of_nnreal _ f @@ -59,11 +57,11 @@ theorem integral_eq_integral_nnrealPart_sub (f : X →ᵇ ℝ) : ∫ x, f x ∂μ = (∫ x, (f.nnrealPart x : ℝ) ∂μ) - ∫ x, ((-f).nnrealPart x : ℝ) ∂μ := by simp only [f.self_eq_nnrealPart_sub_nnrealPart_neg, Pi.sub_apply, integral_sub, integrable_of_nnreal] - rfl + simp only [Function.comp_apply] #align bounded_continuous_function.integral_eq_integral_nnreal_part_sub BoundedContinuousFunction.integral_eq_integral_nnrealPart_sub theorem lintegral_of_real_lt_top (f : X →ᵇ ℝ) : - (∫⁻ x, ENNReal.ofReal (f x) ∂μ) < ∞ := lintegral_lt_top_of_nnreal _ f.nnrealPart + ∫⁻ x, ENNReal.ofReal (f x) ∂μ < ∞ := lintegral_lt_top_of_nnreal _ f.nnrealPart #align measure_theory.finite_measure.lintegral_lt_top_of_bounded_continuous_to_real BoundedContinuousFunction.lintegral_of_real_lt_top theorem toReal_lintegral_coe_eq_integral (f : X →ᵇ ℝ≥0) (μ : Measure X) : diff --git a/Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean b/Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean index f5d0dca71cfe3..dadb3ec19c6aa 100644 --- a/Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean +++ b/Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean @@ -290,14 +290,10 @@ lemma measurableSet_generateFrom_memPartition_iff (t : ℕ → Set α) (n : ℕ) exact diff_subset _ _ · simp only [Finset.coe_sdiff, coe_toFinset] refine (IsCompl.eq_compl ⟨?_, ?_⟩).symm - · rw [disjoint_iff_inter_eq_empty] - ext x - simp only [mem_inter_iff, mem_sUnion, mem_diff, Finset.mem_coe, mem_empty_iff_false, - iff_false, not_and, not_exists, forall_exists_index, and_imp] - intro u hu huS hxu v hvS - have huv : u ≠ v := fun h_eq ↦ absurd hvS (h_eq ▸ huS) - have : Disjoint u v := disjoint_memPartition t n hu (hS_subset hvS) huv - exact fun hxv ↦ absurd rfl (this.ne_of_mem hxu hxv) + · refine Set.disjoint_sUnion_right.mpr fun u huS => ?_ + refine Set.disjoint_sUnion_left.mpr fun v huV => ?_ + refine disjoint_memPartition t n (mem_of_mem_diff huV) (hS_subset huS) ?_ + exact ne_of_mem_of_not_mem huS (not_mem_of_mem_diff huV) |>.symm · rw [codisjoint_iff] simp only [sup_eq_union, top_eq_univ] rw [← sUnion_memPartition t n, union_comm, ← sUnion_union, union_diff_cancel hS_subset] diff --git a/Mathlib/MeasureTheory/Measure/Count.lean b/Mathlib/MeasureTheory/Measure/Count.lean index 1a2d103f4ba50..1e1deefcbe23d 100644 --- a/Mathlib/MeasureTheory/Measure/Count.lean +++ b/Mathlib/MeasureTheory/Measure/Count.lean @@ -51,7 +51,6 @@ theorem count_apply_finset' {s : Finset α} (s_mble : MeasurableSet (s : Set α) count (↑s : Set α) = ∑' i : (↑s : Set α), 1 := count_apply s_mble _ = ∑ i in s, 1 := (s.tsum_subtype 1) _ = s.card := by simp - #align measure_theory.measure.count_apply_finset' MeasureTheory.Measure.count_apply_finset' @[simp] @@ -79,7 +78,6 @@ theorem count_apply_infinite (hs : s.Infinite) : count s = ∞ := by _ = ∑' i : (t : Set α), 1 := (t.tsum_subtype 1).symm _ ≤ count (t : Set α) := le_count_apply _ ≤ count s := measure_mono ht - #align measure_theory.measure.count_apply_infinite MeasureTheory.Measure.count_apply_infinite @[simp] @@ -104,7 +102,6 @@ theorem count_apply_lt_top' (s_mble : MeasurableSet s) : count s < ∞ ↔ s.Fin count s < ∞ ↔ count s ≠ ∞ := lt_top_iff_ne_top _ ↔ ¬s.Infinite := (not_congr (count_apply_eq_top' s_mble)) _ ↔ s.Finite := Classical.not_not - #align measure_theory.measure.count_apply_lt_top' MeasureTheory.Measure.count_apply_lt_top' @[simp] @@ -113,7 +110,6 @@ theorem count_apply_lt_top [MeasurableSingletonClass α] : count s < ∞ ↔ s.F count s < ∞ ↔ count s ≠ ∞ := lt_top_iff_ne_top _ ↔ ¬s.Infinite := (not_congr count_apply_eq_top) _ ↔ s.Finite := Classical.not_not - #align measure_theory.measure.count_apply_lt_top MeasureTheory.Measure.count_apply_lt_top theorem empty_of_count_eq_zero' (s_mble : MeasurableSet s) (hsc : count s = 0) : s = ∅ := by diff --git a/Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean b/Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean index bb5032f3d2b0e..e66871f6c50fd 100644 --- a/Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean +++ b/Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean @@ -299,7 +299,7 @@ lemma BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt (μ ν : Me <| measure_mono (subset_univ _) apply le_trans (set_integral_mono (s := Ioc 0 ‖f‖) ?_ ?_ key) rw [integral_add] - · apply add_le_add rfl.le + · apply add_le_add_left simp only [integral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter, Real.volume_Ioc, sub_zero, norm_nonneg, toReal_ofReal, smul_eq_mul, (mul_comm _ ε).le] @@ -371,17 +371,15 @@ lemma continuous_levyProkhorov_to_probabilityMeasure : have bound := BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt (Ps n) P (ε := dist (μs n) ν + εs n) ?_ ?_ f ?_ · refine bound.trans ?_ - apply (add_le_add hn.le rfl.le).trans + apply (add_le_add_right hn.le _).trans rw [BoundedContinuousFunction.integral_eq_integral_meas_le] · simp only [ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure] - rw [add_assoc] - have also : (dist (μs n) ν + εs n) * ‖f‖ ≤ δ/2 := by - rw [mul_comm] - apply (mul_le_mul (a := ‖f‖) rfl.le hn'.le - (by positivity) (by exact norm_nonneg f)).trans (le_of_eq _) - field_simp - ring - apply add_le_add rfl.le <| (add_le_add rfl.le also).trans <| by linarith + rw [add_assoc, mul_comm] + gcongr + calc + δ / 2 + ‖f‖ * (dist (μs n) ν + εs n) + _ ≤ δ / 2 + ‖f‖ * (‖f‖⁻¹ * δ / 2) := by gcongr + _ = δ := by field_simp; ring · exact eventually_of_forall f_nn · positivity · rw [ENNReal.ofReal_add (by positivity) (by positivity), ← add_zero (levyProkhorovEDist _ _)] @@ -389,11 +387,11 @@ lemma continuous_levyProkhorov_to_probabilityMeasure : (le_of_eq ?_) (ofReal_pos.mpr εs_pos) rw [LevyProkhorov.dist_def, levyProkhorovDist, ofReal_toReal (levyProkhorovEDist_ne_top _ _)] - rfl + simp only [Ps, P, LevyProkhorov.probabilityMeasure] · exact eventually_of_forall f_nn · simp only [IsCoboundedUnder, IsCobounded, eventually_map, eventually_atTop, ge_iff_le, forall_exists_index] - refine ⟨0, fun a i hia ↦ le_trans (integral_nonneg f_nn) (hia i rfl.le)⟩ + refine ⟨0, fun a i hia ↦ le_trans (integral_nonneg f_nn) (hia i le_rfl)⟩ /-- The topology of the Lévy-Prokhorov metric is finer than the topology of convergence in distribution. -/ diff --git a/Mathlib/NumberTheory/SmoothNumbers.lean b/Mathlib/NumberTheory/SmoothNumbers.lean index b02f5c1db362d..88a8a38f56a5b 100644 --- a/Mathlib/NumberTheory/SmoothNumbers.lean +++ b/Mathlib/NumberTheory/SmoothNumbers.lean @@ -187,8 +187,7 @@ def equivProdNatSmoothNumbers {p : ℕ} (hp: p.Prime) : simp only [not_lt, le_iff_eq_or_lt, H, or_false, eq_comm, true_eq_decide_iff] refine prod_eq <| (filter_eq m.factors p).symm ▸ this ▸ perm_append_comm.trans ?_ convert filter_append_perm .. - simp only [not_lt] - simp only [decide_not, Bool.not_not, lt_iff_not_ge] + simp only [not_lt, decide_not, Bool.not_not, lt_iff_not_ge] @[simp] lemma equivProdNatSmoothNumbers_apply {p e m : ℕ} (hp: p.Prime) (hm : m ∈ p.smoothNumbers) : diff --git a/Mathlib/Probability/Kernel/Disintegration/Density.lean b/Mathlib/Probability/Kernel/Disintegration/Density.lean index b34cc4335b51f..b222665c88edc 100644 --- a/Mathlib/Probability/Kernel/Disintegration/Density.lean +++ b/Mathlib/Probability/Kernel/Disintegration/Density.lean @@ -50,10 +50,10 @@ However, we can't turn those functions for each `a` into a measurable function o In order to obtain measurability through countability, we use the fact that the measurable space `γ` is countably generated. For each `n : ℕ`, we define (in the file -Probability/Process/PartitionFiltration) a finite partition of `γ`, such that those partitions are -finer as `n` grows, and the σ-algebra generated by the union of all partitions is the σ-algebra -of `γ`. For `x : γ`, `countablePartitionSet n x` denotes the set in the partition such that -`x ∈ countablePartitionSet n x`. +`Mathlib.Probability.Process.PartitionFiltration`) a finite partition of `γ`, such that those +partitions are finer as `n` grows, and the σ-algebra generated by the union of all partitions is the +σ-algebra of `γ`. For `x : γ`, `countablePartitionSet n x` denotes the set in the partition such +that `x ∈ countablePartitionSet n x`. For a given `n`, the function `densityProcess κ ν n : α → γ → Set β → ℝ` defined by `fun a x s ↦ (κ a (countablePartitionSet n x ×ˢ s) / ν a (countablePartitionSet n x)).toReal` has @@ -772,7 +772,7 @@ lemma tendsto_density_fst_atTop_ae_of_monotone [IsFiniteKernel κ] · rw [MeasureTheory.integral_const, smul_eq_mul, mul_one] convert tendsto_integral_density_of_monotone (κ := κ) le_rfl a seq hseq hseq_iUnion hseq_meas rw [fst_apply' _ _ MeasurableSet.univ] - rfl + simp only [mem_univ, setOf_true] · exact ae_of_all _ (fun c n m hnm ↦ density_mono_set le_rfl a c (hseq hnm)) · exact ae_of_all _ (fun x m ↦ density_le_one le_rfl a x (seq m)) diff --git a/Mathlib/RingTheory/AlgebraTower.lean b/Mathlib/RingTheory/AlgebraTower.lean index 715c8afbf8839..f3481e5083987 100644 --- a/Mathlib/RingTheory/AlgebraTower.lean +++ b/Mathlib/RingTheory/AlgebraTower.lean @@ -149,8 +149,7 @@ noncomputable def Basis.smul {ι : Type v₁} {ι' : Type w₁} (b : Basis ι R @[simp] theorem Basis.smul_repr {ι : Type v₁} {ι' : Type w₁} (b : Basis ι R S) (c : Basis ι' S A) (x ij) : (b.smul c).repr x ij = b.repr (c.repr x ij.2) ij.1 := by - set_option tactic.skipAssignedInstances false in - simp [Basis.smul]; rfl + simp [Basis.smul] #align basis.smul_repr Basis.smul_repr theorem Basis.smul_repr_mk {ι : Type v₁} {ι' : Type w₁} (b : Basis ι R S) (c : Basis ι' S A) diff --git a/Mathlib/RingTheory/Binomial.lean b/Mathlib/RingTheory/Binomial.lean index 97563b07f43ed..14077da2cfb4c 100644 --- a/Mathlib/RingTheory/Binomial.lean +++ b/Mathlib/RingTheory/Binomial.lean @@ -120,7 +120,7 @@ theorem choose_nat_cast (n k : ℕ) : choose (n : R) k = Nat.choose n k := by refine nsmul_right_injective (Nat.factorial k) (Nat.factorial_ne_zero k) ?_ simp only rw [← descPochhammer_eq_factorial_smul_choose, nsmul_eq_mul, ← Nat.cast_mul, - ← Nat.descFactorial_eq_factorial_mul_choose, ← descPochhammer_eval_eq_descFactorial] + ← Nat.descFactorial_eq_factorial_mul_choose, ← descPochhammer_eval_eq_descFactorial] end Ring diff --git a/Mathlib/RingTheory/Coprime/Lemmas.lean b/Mathlib/RingTheory/Coprime/Lemmas.lean index 6ae93d4c8b9ef..78dc1146da016 100644 --- a/Mathlib/RingTheory/Coprime/Lemmas.lean +++ b/Mathlib/RingTheory/Coprime/Lemmas.lean @@ -18,7 +18,7 @@ These lemmas are in a separate file to the definition of `IsCoprime` or `IsRelPr as they require more imports. Notably, this includes lemmas about `Finset.prod` as this requires importing BigOperators, and -lemmas about `HasPow` since these are easiest to prove via `Finset.prod`. +lemmas about `Pow` since these are easiest to prove via `Finset.prod`. -/ diff --git a/Mathlib/RingTheory/Finiteness.lean b/Mathlib/RingTheory/Finiteness.lean index 5c1b77b83728f..1bead432a4827 100644 --- a/Mathlib/RingTheory/Finiteness.lean +++ b/Mathlib/RingTheory/Finiteness.lean @@ -651,8 +651,7 @@ instance bot : Module.Finite R (⊥ : Submodule R M) := iff_fg.mpr fg_bot instance top [Finite R M] : Module.Finite R (⊤ : Submodule R M) := iff_fg.mpr out -variable {R M} -variable (R) +variable {M} /-- The submodule generated by a finite set is `R`-finite. -/ theorem span_of_finite {A : Set M} (hA : Set.Finite A) : diff --git a/Mathlib/RingTheory/Polynomial/Pochhammer.lean b/Mathlib/RingTheory/Polynomial/Pochhammer.lean index 2bae692f55639..ce66c1e195096 100644 --- a/Mathlib/RingTheory/Polynomial/Pochhammer.lean +++ b/Mathlib/RingTheory/Polynomial/Pochhammer.lean @@ -376,8 +376,8 @@ theorem descPochhammer_eval_eq_descFactorial (n k : ℕ) : rw [descPochhammer_succ_right, Nat.descFactorial_succ, mul_sub, eval_sub, eval_mul_X, ← Nat.cast_comm k, eval_nat_cast_mul, ← Nat.cast_comm n, ← sub_mul, ih] by_cases h : n < k - rw [Nat.descFactorial_eq_zero_iff_lt.mpr h, Nat.cast_zero, mul_zero, mul_zero, Nat.cast_zero] - rw [Nat.cast_mul, Nat.cast_sub <| not_lt.mp h] + · rw [Nat.descFactorial_eq_zero_iff_lt.mpr h, Nat.cast_zero, mul_zero, mul_zero, Nat.cast_zero] + · rw [Nat.cast_mul, Nat.cast_sub <| not_lt.mp h] theorem descPochhammer_int_eq_ascFactorial (a b : ℕ) : (descPochhammer ℤ b).eval (a + b : ℤ) = (a + 1).ascFactorial b := by diff --git a/Mathlib/RingTheory/PowerSeries/Order.lean b/Mathlib/RingTheory/PowerSeries/Order.lean index 0e6fc931c32ff..ea5d27f1443f2 100644 --- a/Mathlib/RingTheory/PowerSeries/Order.lean +++ b/Mathlib/RingTheory/PowerSeries/Order.lean @@ -98,14 +98,8 @@ theorem coeff_of_lt_order (n : ℕ) (h : ↑n < order φ) : coeff R n φ = 0 := /-- The `0` power series is the unique power series with infinite order.-/ @[simp] -theorem order_eq_top {φ : R⟦X⟧} : φ.order = ⊤ ↔ φ = 0 := by - constructor - · intro h - ext n - rw [(coeff R n).map_zero, coeff_of_lt_order] - simp [h] - · rintro rfl - exact order_zero +theorem order_eq_top {φ : R⟦X⟧} : φ.order = ⊤ ↔ φ = 0 := + PartENat.not_dom_iff_eq_top.symm.trans order_finite_iff_ne_zero.not_left #align power_series.order_eq_top PowerSeries.order_eq_top /-- The order of a formal power series is at least `n` if diff --git a/Mathlib/RingTheory/PrincipalIdealDomain.lean b/Mathlib/RingTheory/PrincipalIdealDomain.lean index a826159abad7e..9acbe6900a245 100644 --- a/Mathlib/RingTheory/PrincipalIdealDomain.lean +++ b/Mathlib/RingTheory/PrincipalIdealDomain.lean @@ -161,8 +161,8 @@ section variable [Ring R] -instance span_pair_isPrincipal [IsBezout R] (x y : R) : (Ideal.span {x, y}).IsPrincipal := - by classical exact isPrincipal_of_FG (Ideal.span {x, y}) ⟨{x, y}, by simp⟩ +instance span_pair_isPrincipal [IsBezout R] (x y : R) : (Ideal.span {x, y}).IsPrincipal := by + classical exact isPrincipal_of_FG (Ideal.span {x, y}) ⟨{x, y}, by simp⟩ #align is_bezout.span_pair_is_principal IsBezout.span_pair_isPrincipal variable (x y : R) [(Ideal.span {x, y}).IsPrincipal] @@ -212,7 +212,7 @@ theorem _root_.isRelPrime_iff_isCoprime : IsRelPrime x y ↔ IsCoprime x y := variable (R) -/-- Any bezout domain is a GCD domain. This is not an instance since `GCDMonoid` contains data, +/-- Any Bézout domain is a GCD domain. This is not an instance since `GCDMonoid` contains data, and this might not be how we would like to construct it. -/ noncomputable def toGCDDomain [IsBezout R] [IsDomain R] [DecidableEq R] : GCDMonoid R := gcdMonoidOfGCD (gcd · ·) (gcd_dvd_left · ·) (gcd_dvd_right · ·) dvd_gcd diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean index a36b8b0ad55db..e2dd65087a197 100644 --- a/Mathlib/SetTheory/Cardinal/Basic.lean +++ b/Mathlib/SetTheory/Cardinal/Basic.lean @@ -60,7 +60,7 @@ We define cardinal numbers as a quotient of types under the equivalence relation `Cardinal.{u} : Type (u + 1)` is the quotient of types in `Type u`. The operation `Cardinal.lift` lifts cardinal numbers to a higher level. * Cardinal arithmetic specifically for infinite cardinals (like `κ * κ = κ`) is in the file - `SetTheory/Cardinal/Ordinal.lean`. + `Mathlib/SetTheory/Cardinal/Ordinal.lean`. * There is an instance `Pow Cardinal`, but this will only fire if Lean already knows that both the base and the exponent live in the same universe. As a workaround, you can add ``` diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean index 98c856dad7ab1..945969d24b126 100644 --- a/Mathlib/SetTheory/Ordinal/Basic.lean +++ b/Mathlib/SetTheory/Ordinal/Basic.lean @@ -37,10 +37,11 @@ initial segment (or, equivalently, in any way). This total order is well founded universe). In some cases the universe level has to be given explicitly. * `o₁ + o₂` is the order on the disjoint union of `o₁` and `o₂` obtained by declaring that - every element of `o₁` is smaller than every element of `o₂`. The main properties of addition - (and the other operations on ordinals) are stated and proved in `Ordinal/Arithmetic.lean`. Here, - we only introduce it and prove its basic properties to deduce the fact that the order on ordinals - is total (and well founded). + every element of `o₁` is smaller than every element of `o₂`. + The main properties of addition (and the other operations on ordinals) are stated and proved in + `Mathlib/SetTheory/Ordinal/Arithmetic.lean`. + Here, we only introduce it and prove its basic properties to deduce the fact that the order on + ordinals is total (and well founded). * `succ o` is the successor of the ordinal `o`. * `Cardinal.ord c`: when `c` is a cardinal, `ord c` is the smallest ordinal with this cardinality. It is the canonical way to represent a cardinal with an ordinal. @@ -861,7 +862,7 @@ theorem lift_omega : lift ω = ω := In this paragraph, we introduce the addition on ordinals, and prove just enough properties to deduce that the order on ordinals is total (and therefore well-founded). Further properties of the addition, together with properties of the other operations, are proved in -`Ordinal/Arithmetic.lean`. +`Mathlib/SetTheory/Ordinal/Arithmetic.lean`. -/ diff --git a/Mathlib/Topology/Compactness/Lindelof.lean b/Mathlib/Topology/Compactness/Lindelof.lean index b49c6ed659610..fbe2a716bd056 100644 --- a/Mathlib/Topology/Compactness/Lindelof.lean +++ b/Mathlib/Topology/Compactness/Lindelof.lean @@ -719,13 +719,13 @@ instance SecondCountableTopology.ofPseudoMetrizableSpaceLindelofSpace [PseudoMet intro z have : IsOpen (U z) := Metric.isOpen_ball refine IsOpen.mem_nhds this ?hx - simp_all only [U, gt_iff_lt, Metric.mem_ball, dist_self, zero_lt_two, mul_pos_iff_of_pos_left] + simp only [U, Metric.mem_ball, dist_self, hpos] have ⟨t, hct, huniv⟩ := LindelofSpace.elim_nhds_subcover U hU refine ⟨t, hct, ?_⟩ intro z have ⟨y, ht, hzy⟩ : ∃ y ∈ t, z ∈ U y := exists_set_mem_of_union_eq_top t (fun i ↦ U i) huniv z - use y, ht - exact LT.lt.le hzy + simp only [Metric.mem_ball, U] at hzy + exact ⟨y, ht, hzy.le⟩ exact Metric.secondCountable_of_almost_dense_set h_dense lemma eq_open_union_countable [HereditarilyLindelofSpace X] {ι : Type u} (U : ι → Set X) diff --git a/Mathlib/Topology/UniformSpace/Basic.lean b/Mathlib/Topology/UniformSpace/Basic.lean index 0fe9c2b600b3e..151cfa150076e 100644 --- a/Mathlib/Topology/UniformSpace/Basic.lean +++ b/Mathlib/Topology/UniformSpace/Basic.lean @@ -349,7 +349,7 @@ def UniformSpace.ofCore {α : Type u} (u : UniformSpace.Core α) : UniformSpace .ofCoreEq u _ rfl #align uniform_space.of_core UniformSpace.ofCore -/-- Construct a `UniformSpace.core` from a `UniformSpace`. -/ +/-- Construct a `UniformSpace.Core` from a `UniformSpace`. -/ @[reducible] def UniformSpace.toCore (u : UniformSpace α) : UniformSpace.Core α where __ := u diff --git a/Mathlib/Topology/UniformSpace/Separation.lean b/Mathlib/Topology/UniformSpace/Separation.lean index 2c9f11151e371..b19e8e67bce27 100644 --- a/Mathlib/Topology/UniformSpace/Separation.lean +++ b/Mathlib/Topology/UniformSpace/Separation.lean @@ -250,7 +250,7 @@ instance instUniformSpace : UniformSpace (SeparationQuotient α) where exact @hUt (x, z) ⟨y', this.mem_open (UniformSpace.isOpen_ball _ hUo) hxyU, hyzU⟩ nhds_eq_comap_uniformity := surjective_mk.forall.2 fun x ↦ comap_injective surjective_mk <| by conv_lhs => rw [comap_mk_nhds_mk, nhds_eq_comap_uniformity, ← comap_map_mk_uniformity] - simp only [Filter.comap_comap]; rfl + simp only [Filter.comap_comap, Function.comp, Prod_map] theorem uniformity_eq : 𝓤 (SeparationQuotient α) = (𝓤 α).map (Prod.map mk mk) := rfl #align uniform_space.uniformity_quotient SeparationQuotient.uniformity_eq