From 82af17d1e5991b20817f74aef162f13c3504d77d Mon Sep 17 00:00:00 2001 From: damiano Date: Sat, 11 May 2024 14:01:49 +0000 Subject: [PATCH] chore: uncdot various files (#12422) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit These `·` are scoping when there is a single active goal. These were found using a modification of the linter at https://github.com/leanprover-community/mathlib4/pull/12339. --- .../Combinatorics/SimpleGraph/LapMatrix.lean | 8 +-- .../AkraBazzi/GrowsPolynomially.lean | 44 ++++++------ Mathlib/Data/Complex/Exponential.lean | 24 +++---- Mathlib/Data/Finsupp/Multiset.lean | 2 +- Mathlib/Data/Nat/Totient.lean | 6 +- Mathlib/FieldTheory/ChevalleyWarning.lean | 8 +-- Mathlib/FieldTheory/Finite/Basic.lean | 4 +- .../IsAlgClosed/AlgebraicClosure.lean | 8 +-- Mathlib/FieldTheory/IsAlgClosed/Basic.lean | 6 +- Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean | 4 +- Mathlib/FieldTheory/RatFunc.lean | 22 +++--- Mathlib/Geometry/Euclidean/Sphere/Power.lean | 6 +- .../Geometry/Manifold/Instances/Sphere.lean | 4 +- .../Manifold/MFDeriv/SpecificFunctions.lean | 2 +- .../Geometry/RingedSpace/OpenImmersion.lean | 24 +++---- Mathlib/GroupTheory/HNNExtension.lean | 8 +-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean | 4 +- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean | 4 +- Mathlib/GroupTheory/SchurZassenhaus.lean | 2 +- .../GroupTheory/SpecificGroups/Dihedral.lean | 2 +- .../LinearAlgebra/AnnihilatingPolynomial.lean | 2 +- .../Eigenspace/Triangularizable.lean | 4 +- Mathlib/LinearAlgebra/FiniteDimensional.lean | 4 +- Mathlib/LinearAlgebra/Finsupp.lean | 4 +- Mathlib/LinearAlgebra/Lagrange.lean | 2 +- Mathlib/LinearAlgebra/LinearIndependent.lean | 40 +++++------ .../LinearAlgebra/QuadraticForm/Basic.lean | 18 ++--- Mathlib/LinearAlgebra/StdBasis.lean | 38 +++++----- .../Constructions/BorelSpace/Basic.lean | 4 +- .../Constructions/Prod/Basic.lean | 6 +- .../MeasureTheory/Decomposition/Lebesgue.lean | 10 +-- .../Decomposition/SignedLebesgue.lean | 2 +- .../Function/UniformIntegrable.lean | 46 ++++++------ Mathlib/MeasureTheory/Integral/Average.lean | 4 +- .../Integral/BoundedContinuousFunction.lean | 4 +- Mathlib/MeasureTheory/Integral/Lebesgue.lean | 8 +-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean | 12 ++-- .../MeasureTheory/Measure/Haar/Quotient.lean | 10 +-- .../Measure/HasOuterApproxClosed.lean | 22 +++--- .../Measure/LevyProkhorovMetric.lean | 54 +++++++------- Mathlib/ModelTheory/ElementaryMaps.lean | 4 +- Mathlib/ModelTheory/Encoding.lean | 70 +++++++++--------- Mathlib/ModelTheory/Satisfiability.lean | 10 +-- Mathlib/ModelTheory/Substructures.lean | 6 +- Mathlib/NumberTheory/ClassNumber/Finite.lean | 8 +-- Mathlib/NumberTheory/Cyclotomic/Basic.lean | 14 ++-- .../Cyclotomic/PrimitiveRoots.lean | 36 +++++----- Mathlib/NumberTheory/KummerDedekind.lean | 12 ++-- .../LSeries/MellinEqDirichlet.lean | 4 +- .../NumberTheory/Liouville/LiouvilleWith.lean | 6 +- Mathlib/NumberTheory/Modular.lean | 10 +-- Mathlib/NumberTheory/Multiplicity.lean | 18 ++--- .../NumberTheory/NumberField/Embeddings.lean | 14 ++-- Mathlib/NumberTheory/Padics/PadicNumbers.lean | 36 +++++----- Mathlib/NumberTheory/RamificationInertia.lean | 2 +- .../Distributions/Exponential.lean | 2 +- .../Probability/Independence/Conditional.lean | 8 +-- .../Kernel/Disintegration/CdfToKernel.lean | 16 ++--- Mathlib/Probability/Martingale/Basic.lean | 2 +- .../Probability/Martingale/Convergence.lean | 6 +- .../Probability/Martingale/Upcrossing.lean | 30 ++++---- .../GroupCohomology/Resolution.lean | 10 +-- Mathlib/RepresentationTheory/Rep.lean | 4 +- Mathlib/RingTheory/AdicCompletion/Basic.lean | 32 ++++----- Mathlib/RingTheory/Adjoin/PowerBasis.lean | 10 +-- Mathlib/RingTheory/DedekindDomain/Ideal.lean | 10 +-- Mathlib/RingTheory/Finiteness.lean | 4 +- Mathlib/RingTheory/GradedAlgebra/Basic.lean | 20 +++--- Mathlib/RingTheory/HahnSeries/Summable.lean | 2 +- Mathlib/RingTheory/Ideal/MinimalPrime.lean | 8 +-- Mathlib/RingTheory/Ideal/Operations.lean | 2 + Mathlib/RingTheory/IntegrallyClosed.lean | 4 +- Mathlib/RingTheory/IsAdjoinRoot.lean | 6 +- Mathlib/RingTheory/Jacobson.lean | 4 +- .../RingTheory/Localization/FractionRing.lean | 14 ++-- Mathlib/RingTheory/MvPowerSeries/Basic.lean | 22 +++--- Mathlib/RingTheory/Norm.lean | 10 +-- .../Polynomial/Cyclotomic/Expand.lean | 4 +- Mathlib/RingTheory/Polynomial/Dickson.lean | 16 ++--- Mathlib/RingTheory/Polynomial/GaussLemma.lean | 2 +- Mathlib/RingTheory/Polynomial/Vieta.lean | 6 +- Mathlib/RingTheory/PowerSeries/Order.lean | 18 ++--- Mathlib/RingTheory/RootsOfUnity/Basic.lean | 10 +-- Mathlib/RingTheory/RootsOfUnity/Minpoly.lean | 6 +- Mathlib/RingTheory/Trace.lean | 6 +- .../RingTheory/UniqueFactorizationDomain.lean | 12 ++-- .../Valuation/ValuationSubring.lean | 14 ++-- Mathlib/SetTheory/Cardinal/Cofinality.lean | 18 ++--- Mathlib/SetTheory/Surreal/Dyadic.lean | 62 ++++++++-------- Mathlib/Tactic/NormNum/LegendreSymbol.lean | 10 +-- Mathlib/Topology/Algebra/UniformField.lean | 2 +- Mathlib/Topology/Connected/PathConnected.lean | 14 ++-- .../ContinuousFunction/StoneWeierstrass.lean | 2 +- Mathlib/Topology/MetricSpace/Completion.lean | 6 +- .../MetricSpace/HausdorffDistance.lean | 6 +- Mathlib/Topology/Sheaves/LocalPredicate.lean | 20 +++--- .../SheafCondition/PairwiseIntersections.lean | 6 +- Mathlib/Topology/Sheaves/Sheafify.lean | 8 +-- Mathlib/Topology/TietzeExtension.lean | 72 +++++++++---------- 99 files changed, 642 insertions(+), 640 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean b/Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean index fb013218961ca..0fdfdb119678c 100644 --- a/Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean +++ b/Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean @@ -125,10 +125,10 @@ theorem lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable (x : V → Matrix.toLinearMap₂' (G.lapMatrix ℝ) x x = 0 ↔ ∀ i j : V, G.Reachable i j → x i = x j := by rw [lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj] refine ⟨?_, fun h i j hA ↦ h i j hA.reachable⟩ - · intro h i j ⟨w⟩ - induction' w with w i j _ hA _ h' - · rfl - · exact (h i j hA).trans h' + intro h i j ⟨w⟩ + induction' w with w i j _ hA _ h' + · rfl + · exact (h i j hA).trans h' theorem lapMatrix_toLin'_apply_eq_zero_iff_forall_reachable (x : V → ℝ) : Matrix.toLin' (G.lapMatrix ℝ) x = 0 ↔ ∀ i j : V, G.Reachable i j → x i = x j := by diff --git a/Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean b/Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean index d7a31f5bd4ba8..7101a89e02f7b 100644 --- a/Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean +++ b/Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean @@ -333,28 +333,28 @@ protected lemma GrowsPolynomially.mul {f g : ℝ → ℝ} (hf : GrowsPolynomiall simp [abs_of_nonpos hx₁, abs_of_nonpos hx₂] simp only [iff_eventuallyEq hmain, neg_mul] exact this - · intro b hb - have hf := hf.abs b hb - have hg := hg.abs b hb - obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hf⟩ := hf - obtain ⟨c₃, hc₃_mem, c₄, hc₄_mem, hg⟩ := hg - refine ⟨c₁ * c₃, by show 0 < c₁ * c₃; positivity, ?_⟩ - refine ⟨c₂ * c₄, by show 0 < c₂ * c₄; positivity, ?_⟩ - filter_upwards [hf, hg] with x hf hg - intro u hu - refine ⟨?lb, ?ub⟩ - case lb => calc - c₁ * c₃ * (|f x| * |g x|) = (c₁ * |f x|) * (c₃ * |g x|) := by ring - _ ≤ |f u| * |g u| := by - gcongr - · exact (hf u hu).1 - · exact (hg u hu).1 - case ub => calc - |f u| * |g u| ≤ (c₂ * |f x|) * (c₄ * |g x|) := by - gcongr - · exact (hf u hu).2 - · exact (hg u hu).2 - _ = c₂ * c₄ * (|f x| * |g x|) := by ring + intro b hb + have hf := hf.abs b hb + have hg := hg.abs b hb + obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hf⟩ := hf + obtain ⟨c₃, hc₃_mem, c₄, hc₄_mem, hg⟩ := hg + refine ⟨c₁ * c₃, by show 0 < c₁ * c₃; positivity, ?_⟩ + refine ⟨c₂ * c₄, by show 0 < c₂ * c₄; positivity, ?_⟩ + filter_upwards [hf, hg] with x hf hg + intro u hu + refine ⟨?lb, ?ub⟩ + case lb => calc + c₁ * c₃ * (|f x| * |g x|) = (c₁ * |f x|) * (c₃ * |g x|) := by ring + _ ≤ |f u| * |g u| := by + gcongr + · exact (hf u hu).1 + · exact (hg u hu).1 + case ub => calc + |f u| * |g u| ≤ (c₂ * |f x|) * (c₄ * |g x|) := by + gcongr + · exact (hf u hu).2 + · exact (hg u hu).2 + _ = c₂ * c₄ * (|f x| * |g x|) := by ring lemma GrowsPolynomially.const_mul {f : ℝ → ℝ} {c : ℝ} (hf : GrowsPolynomially f) : GrowsPolynomially fun x => c * f x := diff --git a/Mathlib/Data/Complex/Exponential.lean b/Mathlib/Data/Complex/Exponential.lean index 7422dc9052b4b..fcf67aa260995 100644 --- a/Mathlib/Data/Complex/Exponential.lean +++ b/Mathlib/Data/Complex/Exponential.lean @@ -1282,8 +1282,8 @@ theorem sum_div_factorial_le {α : Type*} [LinearOrderedField α] (n j : ℕ) (h _ ≤ ∑ m in range (j - n), ((n.factorial : α) * (n.succ : α) ^ m)⁻¹ := by simp_rw [one_div] gcongr - · rw [← Nat.cast_pow, ← Nat.cast_mul, Nat.cast_le, add_comm] - exact Nat.factorial_mul_pow_le_factorial + rw [← Nat.cast_pow, ← Nat.cast_mul, Nat.cast_le, add_comm] + exact Nat.factorial_mul_pow_le_factorial _ = (n.factorial : α)⁻¹ * ∑ m in range (j - n), (n.succ : α)⁻¹ ^ m := by simp [mul_inv, ← mul_sum, ← sum_mul, mul_comm, inv_pow] _ = ((n.succ : α) - n.succ * (n.succ : α)⁻¹ ^ (j - n)) / (n.factorial * n) := by @@ -1321,8 +1321,8 @@ theorem exp_bound {x : ℂ} (hx : abs x ≤ 1) {n : ℕ} (hn : 0 < n) : _ ≤ ∑ m in filter (fun k => n ≤ k) (range j), abs x ^ n * (1 / m.factorial) := by simp_rw [map_mul, map_pow, map_div₀, abs_natCast] gcongr - · rw [abv_pow abs] - exact pow_le_one _ (abs.nonneg _) hx + rw [abv_pow abs] + exact pow_le_one _ (abs.nonneg _) hx _ = abs x ^ n * ∑ m in (range j).filter fun k => n ≤ k, (1 / m.factorial : ℝ) := by simp [abs_mul, abv_pow abs, abs_div, ← mul_sum] _ ≤ abs x ^ n * (n.succ * (n.factorial * n : ℝ)⁻¹) := by @@ -1351,19 +1351,19 @@ theorem exp_bound' {x : ℂ} {n : ℕ} (hx : abs x / n.succ ≤ 1 / 2) : _ = ∑ i : ℕ in range k, abs x ^ n / n.factorial * (abs x ^ i / (n.succ : ℝ) ^ i) := ?_ _ ≤ abs x ^ n / ↑n.factorial * 2 := ?_ · gcongr - · exact mod_cast Nat.factorial_mul_pow_le_factorial + exact mod_cast Nat.factorial_mul_pow_le_factorial · refine' Finset.sum_congr rfl fun _ _ => _ simp only [pow_add, div_eq_inv_mul, mul_inv, mul_left_comm, mul_assoc] · rw [← mul_sum] gcongr - · simp_rw [← div_pow] - rw [geom_sum_eq, div_le_iff_of_neg] - · trans (-1 : ℝ) - · linarith - · simp only [neg_le_sub_iff_le_add, div_pow, Nat.cast_succ, le_add_iff_nonneg_left] - positivity - · linarith + simp_rw [← div_pow] + rw [geom_sum_eq, div_le_iff_of_neg] + · trans (-1 : ℝ) · linarith + · simp only [neg_le_sub_iff_le_add, div_pow, Nat.cast_succ, le_add_iff_nonneg_left] + positivity + · linarith + · linarith #align complex.exp_bound' Complex.exp_bound' theorem abs_exp_sub_one_le {x : ℂ} (hx : abs x ≤ 1) : abs (exp x - 1) ≤ 2 * abs x := diff --git a/Mathlib/Data/Finsupp/Multiset.lean b/Mathlib/Data/Finsupp/Multiset.lean index f271a28dfc3b4..e8eb30551edda 100644 --- a/Mathlib/Data/Finsupp/Multiset.lean +++ b/Mathlib/Data/Finsupp/Multiset.lean @@ -89,7 +89,7 @@ theorem prod_toMultiset [CommMonoid α] (f : α →₀ ℕ) : · intro a n f _ _ ih rw [toMultiset_add, Multiset.prod_add, ih, toMultiset_single, Multiset.prod_nsmul, Finsupp.prod_add_index' pow_zero pow_add, Finsupp.prod_single_index, Multiset.prod_singleton] - · exact pow_zero a + exact pow_zero a #align finsupp.prod_to_multiset Finsupp.prod_toMultiset @[simp] diff --git a/Mathlib/Data/Nat/Totient.lean b/Mathlib/Data/Nat/Totient.lean index 2f9127c3a3691..117f38bcd064b 100644 --- a/Mathlib/Data/Nat/Totient.lean +++ b/Mathlib/Data/Nat/Totient.lean @@ -347,9 +347,9 @@ theorem totient_gcd_mul_totient_mul (a b : ℕ) : φ (a.gcd b) * φ (a * b) = φ rw [shuffle, shuffle] rotate_left repeat' apply prod_primeFactors_dvd - · simp only [prod_primeFactors_gcd_mul_prod_primeFactors_mul] - rw [eq_comm, mul_comm, ← mul_assoc, ← Nat.mul_div_assoc] - exact mul_dvd_mul (prod_primeFactors_dvd a) (prod_primeFactors_dvd b) + simp only [prod_primeFactors_gcd_mul_prod_primeFactors_mul] + rw [eq_comm, mul_comm, ← mul_assoc, ← Nat.mul_div_assoc] + exact mul_dvd_mul (prod_primeFactors_dvd a) (prod_primeFactors_dvd b) #align nat.totient_gcd_mul_totient_mul Nat.totient_gcd_mul_totient_mul theorem totient_super_multiplicative (a b : ℕ) : φ a * φ b ≤ φ (a * b) := by diff --git a/Mathlib/FieldTheory/ChevalleyWarning.lean b/Mathlib/FieldTheory/ChevalleyWarning.lean index e41a31f25c362..5eadecee5c5a5 100644 --- a/Mathlib/FieldTheory/ChevalleyWarning.lean +++ b/Mathlib/FieldTheory/ChevalleyWarning.lean @@ -93,10 +93,10 @@ theorem MvPolynomial.sum_eval_eq_zero (f : MvPolynomial σ K) _ = a ^ d i * ∏ j, x₀ j ^ d j := congr_arg _ (Fintype.prod_congr _ _ ?_) -- see below _ = (∏ j, x₀ j ^ d j) * a ^ d i := mul_comm _ _ - · -- the remaining step of the calculation above - rintro ⟨j, hj⟩ - show (e a : σ → K) j ^ d j = x₀ ⟨j, hj⟩ ^ d j - rw [Equiv.subtypeEquivCodomain_symm_apply_ne] + -- the remaining step of the calculation above + rintro ⟨j, hj⟩ + show (e a : σ → K) j ^ d j = x₀ ⟨j, hj⟩ ^ d j + rw [Equiv.subtypeEquivCodomain_symm_apply_ne] #align mv_polynomial.sum_eval_eq_zero MvPolynomial.sum_eval_eq_zero variable [DecidableEq K] (p : ℕ) [CharP K p] diff --git a/Mathlib/FieldTheory/Finite/Basic.lean b/Mathlib/FieldTheory/Finite/Basic.lean index 900f2db3ee401..3c08dff7d0ff3 100644 --- a/Mathlib/FieldTheory/Finite/Basic.lean +++ b/Mathlib/FieldTheory/Finite/Basic.lean @@ -625,8 +625,8 @@ theorem unit_isSquare_iff (hF : ringChar F ≠ 2) (a : Fˣ) : · rintro ⟨y, rfl⟩ rw [← pow_two, ← pow_mul, hodd] apply_fun Units.val using Units.ext - · push_cast - exact FiniteField.pow_card_sub_one_eq_one (y : F) (Units.ne_zero y) + push_cast + exact FiniteField.pow_card_sub_one_eq_one (y : F) (Units.ne_zero y) · subst a; intro h have key : 2 * (Fintype.card F / 2) ∣ n * (Fintype.card F / 2) := by rw [← pow_mul] at h diff --git a/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean b/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean index 7027848efdac7..7e0d292000a00 100644 --- a/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean +++ b/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean @@ -142,10 +142,10 @@ theorem AdjoinMonic.isIntegral (z : AdjoinMonic k) : IsIntegral k z := by | h_C => exact isIntegral_algebraMap | h_add _ _ ha hb => exact (ha _ rfl).add (hb _ rfl) | h_X p f ih => - · refine @IsIntegral.mul k _ _ _ _ _ (Ideal.Quotient.mk (maxIdeal k) _) (ih _ rfl) ?_ - refine ⟨f, f.2.1, ?_⟩ - erw [AdjoinMonic.algebraMap, ← hom_eval₂, Ideal.Quotient.eq_zero_iff_mem] - exact le_maxIdeal k (Ideal.subset_span ⟨f, rfl⟩) + refine @IsIntegral.mul k _ _ _ _ _ (Ideal.Quotient.mk (maxIdeal k) _) (ih _ rfl) ?_ + refine ⟨f, f.2.1, ?_⟩ + erw [AdjoinMonic.algebraMap, ← hom_eval₂, Ideal.Quotient.eq_zero_iff_mem] + exact le_maxIdeal k (Ideal.subset_span ⟨f, rfl⟩) #align algebraic_closure.adjoin_monic.is_integral AlgebraicClosure.AdjoinMonic.isIntegral theorem AdjoinMonic.exists_root {f : k[X]} (hfm : f.Monic) (hfi : Irreducible f) : diff --git a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean index 65c5eb794b916..1d209afa66e9b 100644 --- a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean +++ b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean @@ -91,9 +91,9 @@ theorem exists_pow_nat_eq [IsAlgClosed k] (x : k) {n : ℕ} (hn : 0 < n) : ∃ z rw [degree_X_pow_sub_C hn x] exact ne_of_gt (WithBot.coe_lt_coe.2 hn) obtain ⟨z, hz⟩ := exists_root (X ^ n - C x) this - · use z - simp only [eval_C, eval_X, eval_pow, eval_sub, IsRoot.def] at hz - exact sub_eq_zero.1 hz + use z + simp only [eval_C, eval_X, eval_pow, eval_sub, IsRoot.def] at hz + exact sub_eq_zero.1 hz #align is_alg_closed.exists_pow_nat_eq IsAlgClosed.exists_pow_nat_eq theorem exists_eq_mul_self [IsAlgClosed k] (x : k) : ∃ z, x = z * z := by diff --git a/Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean b/Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean index 40aa4b98914e2..2727c61e2e629 100644 --- a/Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean +++ b/Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean @@ -121,8 +121,8 @@ theorem map_polynomial_aeval_of_nonempty [IsAlgClosed 𝕜] (a : A) (p : 𝕜[X] (hnon : (σ a).Nonempty) : σ (aeval a p) = (fun k => eval k p) '' σ a := by nontriviality A refine' Or.elim (le_or_gt (degree p) 0) (fun h => _) (map_polynomial_aeval_of_degree_pos a p) - · rw [eq_C_of_degree_le_zero h] - simp only [Set.image_congr, eval_C, aeval_C, scalar_eq, Set.Nonempty.image_const hnon] + rw [eq_C_of_degree_le_zero h] + simp only [Set.image_congr, eval_C, aeval_C, scalar_eq, Set.Nonempty.image_const hnon] #align spectrum.map_polynomial_aeval_of_nonempty spectrum.map_polynomial_aeval_of_nonempty /-- A specialization of `spectrum.subset_polynomial_aeval` to monic monomials for convenience. -/ diff --git a/Mathlib/FieldTheory/RatFunc.lean b/Mathlib/FieldTheory/RatFunc.lean index 31eaa815c3461..7aad6e553427d 100644 --- a/Mathlib/FieldTheory/RatFunc.lean +++ b/Mathlib/FieldTheory/RatFunc.lean @@ -731,13 +731,13 @@ theorem liftMonoidWithZeroHom_injective [Nontrivial R] (φ : R[X] →*₀ G₀) rintro ⟨x⟩ ⟨y⟩ induction' x using Localization.induction_on with a induction' y using Localization.induction_on with a' - · simp_rw [liftMonoidWithZeroHom_apply_ofFractionRing_mk] - intro h - congr 1 - refine Localization.mk_eq_mk_iff.mpr (Localization.r_of_eq (M := R[X]) ?_) - have := mul_eq_mul_of_div_eq_div _ _ ?_ ?_ h - · rwa [← map_mul, ← map_mul, hφ.eq_iff, mul_comm, mul_comm a'.fst] at this - all_goals exact map_ne_zero_of_mem_nonZeroDivisors _ hφ (SetLike.coe_mem _) + simp_rw [liftMonoidWithZeroHom_apply_ofFractionRing_mk] + intro h + congr 1 + refine Localization.mk_eq_mk_iff.mpr (Localization.r_of_eq (M := R[X]) ?_) + have := mul_eq_mul_of_div_eq_div _ _ ?_ ?_ h + · rwa [← map_mul, ← map_mul, hφ.eq_iff, mul_comm, mul_comm a'.fst] at this + all_goals exact map_ne_zero_of_mem_nonZeroDivisors _ hφ (SetLike.coe_mem _) #align ratfunc.lift_monoid_with_zero_hom_injective RatFunc.liftMonoidWithZeroHom_injective /-- Lift an injective ring homomorphism `R[X] →+* L` to a `RatFunc R →+* L` @@ -810,9 +810,9 @@ instance (R : Type*) [CommSemiring R] [Algebra R K[X]] : Algebra R (RatFunc K) w smul_def' c x := by induction' x using RatFunc.induction_on' with p q hq -- Porting note: the first `rw [...]` was not needed - · rw [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk] - rw [mk_one', ← mk_smul, mk_def_of_ne (c • p) hq, mk_def_of_ne p hq, ← - ofFractionRing_mul, IsLocalization.mul_mk'_eq_mk'_of_mul, Algebra.smul_def] + rw [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk] + rw [mk_one', ← mk_smul, mk_def_of_ne (c • p) hq, mk_def_of_ne p hq, ← + ofFractionRing_mul, IsLocalization.mul_mk'_eq_mk'_of_mul, Algebra.smul_def] commutes' c x := mul_comm _ _ variable {K} @@ -1309,7 +1309,7 @@ theorem denom_dvd {x : RatFunc K} {q : K[X]} (hq : q ≠ 0) : obtain ⟨_hx, hp⟩ := mul_ne_zero_iff.mp hq use num x * p rw [RingHom.map_mul, RingHom.map_mul, ← div_mul_div_comm, div_self, mul_one, num_div_denom] - · exact algebraMap_ne_zero hp + exact algebraMap_ne_zero hp · rintro ⟨p, rfl⟩ exact denom_div_dvd p q #align ratfunc.denom_dvd RatFunc.denom_dvd diff --git a/Mathlib/Geometry/Euclidean/Sphere/Power.lean b/Mathlib/Geometry/Euclidean/Sphere/Power.lean index 7c311572f4ab6..ca5b5b4ab3071 100644 --- a/Mathlib/Geometry/Euclidean/Sphere/Power.lean +++ b/Mathlib/Geometry/Euclidean/Sphere/Power.lean @@ -104,9 +104,9 @@ theorem mul_dist_eq_mul_dist_of_cospherical {a b c d p : P} (h : Cospherical ({a dist a p * dist b p = dist c p * dist d p := by obtain ⟨q, r, h'⟩ := (cospherical_def {a, b, c, d}).mp h obtain ⟨ha, hb, hc, hd⟩ := h' a (by simp), h' b (by simp), h' c (by simp), h' d (by simp) - · rw [← hd] at hc - rw [← hb] at ha - rw [mul_dist_eq_abs_sub_sq_dist hapb ha, hb, mul_dist_eq_abs_sub_sq_dist hcpd hc, hd] + rw [← hd] at hc + rw [← hb] at ha + rw [mul_dist_eq_abs_sub_sq_dist hapb ha, hb, mul_dist_eq_abs_sub_sq_dist hcpd hc, hd] #align euclidean_geometry.mul_dist_eq_mul_dist_of_cospherical EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical /-- **Intersecting Chords Theorem**. -/ diff --git a/Mathlib/Geometry/Manifold/Instances/Sphere.lean b/Mathlib/Geometry/Manifold/Instances/Sphere.lean index d3c2aef8c26ca..b1dae0877c66f 100644 --- a/Mathlib/Geometry/Manifold/Instances/Sphere.lean +++ b/Mathlib/Geometry/Manifold/Instances/Sphere.lean @@ -245,8 +245,8 @@ theorem stereo_left_inv (hv : ‖v‖ = 1) {x : sphere (0 : E) 1} (hx : (x : E) · simp [a, inner_add_right, inner_smul_right, hvy, real_inner_self_eq_norm_mul_norm, hv, mul_smul, mul_pow, Real.norm_eq_abs, sq_abs, norm_smul] -- Porting note: used to be simp only [split, add_comm] but get maxRec errors - · rw [split, add_comm] - ac_rfl + rw [split, add_comm] + ac_rfl -- Porting note: this branch did not exit in ml3 · rw [split, add_comm] congr! diff --git a/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean b/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean index 587cbd6f3b13d..9a495a9615821 100644 --- a/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean +++ b/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean @@ -416,7 +416,7 @@ theorem mfderiv_prod_eq_add {f : M × M' → M''} {p : M × M'} mfderiv_snd, mfderiv_const, mfderiv_const] symm convert ContinuousLinearMap.comp_id <| mfderiv (.prod I I') I'' f (p.1, p.2) - · exact ContinuousLinearMap.coprod_inl_inr + exact ContinuousLinearMap.coprod_inl_inr #align mfderiv_prod_eq_add mfderiv_prod_eq_add end Prod diff --git a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean b/Mathlib/Geometry/RingedSpace/OpenImmersion.lean index 71bc6fb62ceb9..5d6d0893fc5e0 100644 --- a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean +++ b/Mathlib/Geometry/RingedSpace/OpenImmersion.lean @@ -116,12 +116,12 @@ noncomputable def isoRestrict : X ≅ Y.restrict H.base_open := fapply NatIso.ofComponents · intro U refine' asIso (f.c.app (op (H.openFunctor.obj (unop U)))) ≪≫ X.presheaf.mapIso (eqToIso _) - · induction U using Opposite.rec' with | h U => ?_ - cases U - dsimp only [IsOpenMap.functor, Functor.op, Opens.map] - congr 2 - erw [Set.preimage_image_eq _ H.base_open.inj] - rfl + induction U using Opposite.rec' with | h U => ?_ + cases U + dsimp only [IsOpenMap.functor, Functor.op, Opens.map] + congr 2 + erw [Set.preimage_image_eq _ H.base_open.inj] + rfl · intro U V i simp only [CategoryTheory.eqToIso.hom, TopCat.Presheaf.pushforwardObj_map, Category.assoc, Functor.op_map, Iso.trans_hom, asIso_hom, Functor.mapIso_hom, ← X.presheaf.map_comp] @@ -133,12 +133,12 @@ noncomputable def isoRestrict : X ≅ Y.restrict H.base_open := theorem isoRestrict_hom_ofRestrict : H.isoRestrict.hom ≫ Y.ofRestrict _ = f := by -- Porting note: `ext` did not pick up `NatTrans.ext` refine PresheafedSpace.Hom.ext _ _ rfl <| NatTrans.ext _ _ <| funext fun x => ?_ - · simp only [isoRestrict_hom_c_app, NatTrans.comp_app, eqToHom_refl, - ofRestrict_c_app, Category.assoc, whiskerRight_id'] - erw [Category.comp_id, comp_c_app, f.c.naturality_assoc, ← X.presheaf.map_comp] - trans f.c.app x ≫ X.presheaf.map (𝟙 _) - · congr 1 - · erw [X.presheaf.map_id, Category.comp_id] + simp only [isoRestrict_hom_c_app, NatTrans.comp_app, eqToHom_refl, + ofRestrict_c_app, Category.assoc, whiskerRight_id'] + erw [Category.comp_id, comp_c_app, f.c.naturality_assoc, ← X.presheaf.map_comp] + trans f.c.app x ≫ X.presheaf.map (𝟙 _) + · congr 1 + · erw [X.presheaf.map_id, Category.comp_id] #align algebraic_geometry.PresheafedSpace.is_open_immersion.iso_restrict_hom_of_restrict AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict @[simp] diff --git a/Mathlib/GroupTheory/HNNExtension.lean b/Mathlib/GroupTheory/HNNExtension.lean index 21c58a1731913..c90a4361f5415 100644 --- a/Mathlib/GroupTheory/HNNExtension.lean +++ b/Mathlib/GroupTheory/HNNExtension.lean @@ -566,10 +566,10 @@ theorem prod_smul_empty (w : NormalWord d) : erw [(d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1] ext <;> simp -- The next 4 were not needed before leanprover/lean4#2644 - · erw [(d.compl _).equiv_snd_eq_inv_mul] - simp_rw [SetLike.coe_sort_coe] - erw [(d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1] - simp + erw [(d.compl _).equiv_snd_eq_inv_mul] + simp_rw [SetLike.coe_sort_coe] + erw [(d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1] + simp variable (d) /-- The equivalence between elements of the HNN extension and words in normal form. -/ diff --git a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean index 258d1ec316b09..c37ed906c527d 100644 --- a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean +++ b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean @@ -250,8 +250,8 @@ instance [Fintype α] [DecidableEq α] (f : Perm α) : DecidableRel (SameCycle f ⟨fun ⟨n, _, hn⟩ => ⟨n, hn⟩, fun ⟨i, hi⟩ => ⟨(i % orderOf f).natAbs, List.mem_range.2 (Int.ofNat_lt.1 <| by rw [Int.natAbs_of_nonneg (Int.emod_nonneg _ <| Int.natCast_ne_zero.2 (orderOf_pos _).ne')] - · refine' (Int.emod_lt _ <| Int.natCast_ne_zero_iff_pos.2 <| orderOf_pos _).trans_le _ - simp [orderOf_le_card_univ]), + refine' (Int.emod_lt _ <| Int.natCast_ne_zero_iff_pos.2 <| orderOf_pos _).trans_le _ + simp [orderOf_le_card_univ]), by rw [← zpow_natCast, Int.natAbs_of_nonneg (Int.emod_nonneg _ <| Int.natCast_ne_zero_iff_pos.2 <| orderOf_pos _), zpow_mod_orderOf, hi]⟩⟩ diff --git a/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean b/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean index 71239953bbf7e..8678a069c1552 100644 --- a/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean +++ b/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean @@ -409,8 +409,8 @@ def toCycle (f : Perm α) (hf : IsCycle f) : Cycle α := intro x y _ s refine' heq_of_eq _ split_ifs with hx hy hy <;> try rfl - · have hc : SameCycle f x y := IsCycle.sameCycle hf hx hy - exact Quotient.sound' hc.toList_isRotated) + have hc : SameCycle f x y := IsCycle.sameCycle hf hx hy + exact Quotient.sound' hc.toList_isRotated) #align equiv.perm.to_cycle Equiv.Perm.toCycle theorem toCycle_eq_toList (f : Perm α) (hf : IsCycle f) (x : α) (hx : f x ≠ x) : diff --git a/Mathlib/GroupTheory/SchurZassenhaus.lean b/Mathlib/GroupTheory/SchurZassenhaus.lean index 8f5cfc6a8731f..a1b217aa13004 100644 --- a/Mathlib/GroupTheory/SchurZassenhaus.lean +++ b/Mathlib/GroupTheory/SchurZassenhaus.lean @@ -216,7 +216,7 @@ private theorem step2 (K : Subgroup G) [K.Normal] (hK : K ≤ N) : K = ⊥ ∨ K intro hH' rw [comap_injective this hH', isComplement'_top_right, map_eq_bot_iff, QuotientGroup.ker_mk'] at hH - · exact h4.2 (le_antisymm hK hH) + exact h4.2 (le_antisymm hK hH) /-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime` -/ private theorem step3 (K : Subgroup N) [(K.map N.subtype).Normal] : K = ⊥ ∨ K = ⊤ := by diff --git a/Mathlib/GroupTheory/SpecificGroups/Dihedral.lean b/Mathlib/GroupTheory/SpecificGroups/Dihedral.lean index 648376557bdd3..fbd297a43359c 100644 --- a/Mathlib/GroupTheory/SpecificGroups/Dihedral.lean +++ b/Mathlib/GroupTheory/SpecificGroups/Dihedral.lean @@ -199,7 +199,7 @@ theorem exponent : Monoid.exponent (DihedralGroup n) = lcm n 2 := by rintro (m | m) · rw [← orderOf_dvd_iff_pow_eq_one, orderOf_r] refine' Nat.dvd_trans ⟨gcd n m.val, _⟩ (dvd_lcm_left n 2) - · exact (Nat.div_mul_cancel (Nat.gcd_dvd_left n m.val)).symm + exact (Nat.div_mul_cancel (Nat.gcd_dvd_left n m.val)).symm · rw [← orderOf_dvd_iff_pow_eq_one, orderOf_sr] exact dvd_lcm_right n 2 · apply lcm_dvd diff --git a/Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean b/Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean index 80eb4646e5f10..e72cd24238608 100644 --- a/Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean +++ b/Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean @@ -172,7 +172,7 @@ theorem monic_generator_eq_minpoly (a : A) (p : 𝕜[X]) (p_monic : p.Monic) · rw [← span_singleton_annIdealGenerator, Ideal.span_singleton_eq_span_singleton] at p_gen rw [eq_comm] apply eq_of_monic_of_associated p_monic _ p_gen - · apply monic_annIdealGenerator _ _ ((Associated.ne_zero_iff p_gen).mp h) + apply monic_annIdealGenerator _ _ ((Associated.ne_zero_iff p_gen).mp h) #align polynomial.monic_generator_eq_minpoly Polynomial.monic_generator_eq_minpoly theorem span_minpoly_eq_annihilator {M} [AddCommGroup M] [Module 𝕜 M] (f : Module.End 𝕜 M) : diff --git a/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean b/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean index f172877b85f72..28bebcbedace5 100644 --- a/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean +++ b/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean @@ -119,8 +119,8 @@ theorem iSup_generalizedEigenspace_eq_top [IsAlgClosed K] [FiniteDimensional K V -- Since the dimensions of `ER` and `ES` add up to the dimension of `V`, it follows that the -- span of all generalized eigenvectors is all of `V`. show ⨆ (μ : K) (k : ℕ), f.generalizedEigenspace μ k = ⊤ - · rw [← top_le_iff, ← Submodule.eq_top_of_disjoint ER ES h_dim_add h_disjoint] - apply sup_le hER hES + rw [← top_le_iff, ← Submodule.eq_top_of_disjoint ER ES h_dim_add h_disjoint] + apply sup_le hER hES #align module.End.supr_generalized_eigenspace_eq_top Module.End.iSup_generalizedEigenspace_eq_top end Module.End diff --git a/Mathlib/LinearAlgebra/FiniteDimensional.lean b/Mathlib/LinearAlgebra/FiniteDimensional.lean index 4eee3872d702d..4f2114d550131 100644 --- a/Mathlib/LinearAlgebra/FiniteDimensional.lean +++ b/Mathlib/LinearAlgebra/FiniteDimensional.lean @@ -450,8 +450,8 @@ instance finiteDimensional_finset_sup {ι : Type*} (s : Finset ι) (S : ι → S refine' @Finset.sup_induction _ _ _ _ s S (fun i => FiniteDimensional K ↑i) (finiteDimensional_bot K V) _ fun i _ => by infer_instance - · intro S₁ hS₁ S₂ hS₂ - exact Submodule.finiteDimensional_sup S₁ S₂ + intro S₁ hS₁ S₂ hS₂ + exact Submodule.finiteDimensional_sup S₁ S₂ #align submodule.finite_dimensional_finset_sup Submodule.finiteDimensional_finset_sup /-- The submodule generated by a supremum of finite dimensional submodules, indexed by a finite diff --git a/Mathlib/LinearAlgebra/Finsupp.lean b/Mathlib/LinearAlgebra/Finsupp.lean index 3ba8b05b83c44..ba601f5cea244 100644 --- a/Mathlib/LinearAlgebra/Finsupp.lean +++ b/Mathlib/LinearAlgebra/Finsupp.lean @@ -405,8 +405,8 @@ theorem supported_iUnion {δ : Type*} (s : δ → Set α) : · exact zero_mem _ · refine' fun x a l _ _ => add_mem _ by_cases h : ∃ i, x ∈ s i <;> simp [h] - · cases' h with i hi - exact le_iSup (fun i => supported M R (s i)) i (single_mem_supported R _ hi) + cases' h with i hi + exact le_iSup (fun i => supported M R (s i)) i (single_mem_supported R _ hi) #align finsupp.supported_Union Finsupp.supported_iUnion theorem supported_union (s t : Set α) : supported M R (s ∪ t) = supported M R s ⊔ supported M R t := diff --git a/Mathlib/LinearAlgebra/Lagrange.lean b/Mathlib/LinearAlgebra/Lagrange.lean index 5260fd4fd69e4..33961d875fb9b 100644 --- a/Mathlib/LinearAlgebra/Lagrange.lean +++ b/Mathlib/LinearAlgebra/Lagrange.lean @@ -488,7 +488,7 @@ theorem interpolate_eq_add_interpolate_erase (hvs : Set.InjOn v s) (hi : i ∈ s sdiff_singleton_eq_erase, pair_comm, sdiff_insert_insert_of_mem_of_not_mem hj (not_mem_singleton.mpr hij.symm), sdiff_singleton_eq_erase] - · exact insert_subset_iff.mpr ⟨hi, singleton_subset_iff.mpr hj⟩ + exact insert_subset_iff.mpr ⟨hi, singleton_subset_iff.mpr hj⟩ #align lagrange.interpolate_eq_add_interpolate_erase Lagrange.interpolate_eq_add_interpolate_erase end Interpolate diff --git a/Mathlib/LinearAlgebra/LinearIndependent.lean b/Mathlib/LinearAlgebra/LinearIndependent.lean index 47436f55e6a07..f4bcd68edaca4 100644 --- a/Mathlib/LinearAlgebra/LinearIndependent.lean +++ b/Mathlib/LinearAlgebra/LinearIndependent.lean @@ -782,16 +782,16 @@ theorem linearIndependent_sum {v : Sum ι ι' → M} : refine Finset.disjoint_filter.2 fun x _ hx => disjoint_left.1 ?_ hx exact IsCompl.disjoint isCompl_range_inl_range_inr - · rw [← eq_neg_iff_add_eq_zero] at this - rw [disjoint_def'] at hlr - have A := by - refine hlr _ (sum_mem fun i _ => ?_) _ (neg_mem <| sum_mem fun i _ => ?_) this - · exact smul_mem _ _ (subset_span ⟨Sum.inl i, mem_range_self _, rfl⟩) - · exact smul_mem _ _ (subset_span ⟨Sum.inr i, mem_range_self _, rfl⟩) - cases' i with i i - · exact hl _ _ A i (Finset.mem_preimage.2 hi) - · rw [this, neg_eq_zero] at A - exact hr _ _ A i (Finset.mem_preimage.2 hi) + rw [← eq_neg_iff_add_eq_zero] at this + rw [disjoint_def'] at hlr + have A := by + refine hlr _ (sum_mem fun i _ => ?_) _ (neg_mem <| sum_mem fun i _ => ?_) this + · exact smul_mem _ _ (subset_span ⟨Sum.inl i, mem_range_self _, rfl⟩) + · exact smul_mem _ _ (subset_span ⟨Sum.inr i, mem_range_self _, rfl⟩) + cases' i with i i + · exact hl _ _ A i (Finset.mem_preimage.2 hi) + · rw [this, neg_eq_zero] at A + exact hr _ _ A i (Finset.mem_preimage.2 hi) #align linear_independent_sum linearIndependent_sum theorem LinearIndependent.sum_type {v' : ι' → M} (hv : LinearIndependent R v) @@ -1078,11 +1078,11 @@ theorem eq_of_linearIndependent_of_span_subtype [Nontrivial R] {s t : Set M} apply surjective_of_linearIndependent_of_span hs f _ convert hst <;> simp [f, comp] show s = t - · apply Subset.antisymm _ h - intro x hx - rcases h_surj ⟨x, hx⟩ with ⟨y, hy⟩ - convert y.mem - rw [← Subtype.mk.inj hy] + apply Subset.antisymm _ h + intro x hx + rcases h_surj ⟨x, hx⟩ with ⟨y, hy⟩ + convert y.mem + rw [← Subtype.mk.inj hy] #align eq_of_linear_independent_of_span_subtype eq_of_linearIndependent_of_span_subtype open LinearMap @@ -1413,11 +1413,11 @@ theorem exists_linearIndependent_extension (hs : LinearIndependent K ((↑) : s · exact subset_sUnion_of_mem rcases this with ⟨b, ⟨bt, bi⟩, sb, h⟩ - · refine' ⟨b, bt, sb, fun x xt => _, bi⟩ - by_contra hn - apply hn - rw [← h _ ⟨insert_subset_iff.2 ⟨xt, bt⟩, bi.insert hn⟩ (subset_insert _ _)] - exact subset_span (mem_insert _ _) + refine' ⟨b, bt, sb, fun x xt => _, bi⟩ + by_contra hn + apply hn + rw [← h _ ⟨insert_subset_iff.2 ⟨xt, bt⟩, bi.insert hn⟩ (subset_insert _ _)] + exact subset_span (mem_insert _ _) #align exists_linear_independent_extension exists_linearIndependent_extension variable (K t) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index bf6a22dafae19..8d853cc710a48 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -1245,15 +1245,15 @@ theorem exists_orthogonal_basis [hK : Invertible (2 : K)] {B : BilinForm K V} (h rw [IsOrtho, map_smul, smul_apply, map_add, map_smul, smul_eq_mul, smul_eq_mul, div_mul_cancel₀ _ hx, add_neg_self, mul_zero]) refine' ⟨b, _⟩ - · rw [Basis.coe_mkFinCons] - intro j i - refine' Fin.cases _ (fun i => _) i <;> refine' Fin.cases _ (fun j => _) j <;> intro hij <;> - simp only [Function.onFun, Fin.cons_zero, Fin.cons_succ, Function.comp_apply] - · exact (hij rfl).elim - · rw [IsOrtho, ← hB₂] - exact (v' j).prop _ (Submodule.mem_span_singleton_self x) - · exact (v' i).prop _ (Submodule.mem_span_singleton_self x) - · exact hv₁ (ne_of_apply_ne _ hij) + rw [Basis.coe_mkFinCons] + intro j i + refine' Fin.cases _ (fun i => _) i <;> refine' Fin.cases _ (fun j => _) j <;> intro hij <;> + simp only [Function.onFun, Fin.cons_zero, Fin.cons_succ, Function.comp_apply] + · exact (hij rfl).elim + · rw [IsOrtho, ← hB₂] + exact (v' j).prop _ (Submodule.mem_span_singleton_self x) + · exact (v' i).prop _ (Submodule.mem_span_singleton_self x) + · exact hv₁ (ne_of_apply_ne _ hij) #align bilin_form.exists_orthogonal_basis LinearMap.BilinForm.exists_orthogonal_basis end BilinForm diff --git a/Mathlib/LinearAlgebra/StdBasis.lean b/Mathlib/LinearAlgebra/StdBasis.lean index eac1b55f66375..b829e37f629e7 100644 --- a/Mathlib/LinearAlgebra/StdBasis.lean +++ b/Mathlib/LinearAlgebra/StdBasis.lean @@ -181,25 +181,25 @@ theorem linearIndependent_stdBasis [Ring R] [∀ i, AddCommGroup (Ms i)] [∀ i, intro j exact (hs j).map' _ (ker_stdBasis _ _ _) apply linearIndependent_iUnion_finite hs' - · intro j J _ hiJ - have h₀ : - ∀ j, span R (range fun i : ιs j => stdBasis R Ms j (v j i)) ≤ - LinearMap.range (stdBasis R Ms j) := by - intro j - rw [span_le, LinearMap.range_coe] - apply range_comp_subset_range - have h₁ : - span R (range fun i : ιs j => stdBasis R Ms j (v j i)) ≤ - ⨆ i ∈ ({j} : Set _), LinearMap.range (stdBasis R Ms i) := by - rw [@iSup_singleton _ _ _ fun i => LinearMap.range (stdBasis R (Ms) i)] - apply h₀ - have h₂ : - ⨆ j ∈ J, span R (range fun i : ιs j => stdBasis R Ms j (v j i)) ≤ - ⨆ j ∈ J, LinearMap.range (stdBasis R (fun j : η => Ms j) j) := - iSup₂_mono fun i _ => h₀ i - have h₃ : Disjoint (fun i : η => i ∈ ({j} : Set _)) J := by - convert Set.disjoint_singleton_left.2 hiJ using 0 - exact (disjoint_stdBasis_stdBasis _ _ _ _ h₃).mono h₁ h₂ + intro j J _ hiJ + have h₀ : + ∀ j, span R (range fun i : ιs j => stdBasis R Ms j (v j i)) ≤ + LinearMap.range (stdBasis R Ms j) := by + intro j + rw [span_le, LinearMap.range_coe] + apply range_comp_subset_range + have h₁ : + span R (range fun i : ιs j => stdBasis R Ms j (v j i)) ≤ + ⨆ i ∈ ({j} : Set _), LinearMap.range (stdBasis R Ms i) := by + rw [@iSup_singleton _ _ _ fun i => LinearMap.range (stdBasis R (Ms) i)] + apply h₀ + have h₂ : + ⨆ j ∈ J, span R (range fun i : ιs j => stdBasis R Ms j (v j i)) ≤ + ⨆ j ∈ J, LinearMap.range (stdBasis R (fun j : η => Ms j) j) := + iSup₂_mono fun i _ => h₀ i + have h₃ : Disjoint (fun i : η => i ∈ ({j} : Set _)) J := by + convert Set.disjoint_singleton_left.2 hiJ using 0 + exact (disjoint_stdBasis_stdBasis _ _ _ _ h₃).mono h₁ h₂ #align pi.linear_independent_std_basis Pi.linearIndependent_stdBasis variable [Semiring R] [∀ i, AddCommMonoid (Ms i)] [∀ i, Module R (Ms i)] diff --git a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean index 9bb0e19062352..f550866c7621f 100644 --- a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean +++ b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean @@ -802,8 +802,8 @@ theorem ext_of_Ico_finite {α : Type*} [TopologicalSpace α] {m : MeasurableSpac refine' ext_of_generate_finite _ (BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Ico α)) (isPiSystem_Ico (id : α → α) id) _ hμν - · rintro - ⟨a, b, hlt, rfl⟩ - exact h hlt + rintro - ⟨a, b, hlt, rfl⟩ + exact h hlt #align measure_theory.measure.ext_of_Ico_finite MeasureTheory.Measure.ext_of_Ico_finite /-- Two finite measures on a Borel space are equal if they agree on all open-closed intervals. If diff --git a/Mathlib/MeasureTheory/Constructions/Prod/Basic.lean b/Mathlib/MeasureTheory/Constructions/Prod/Basic.lean index 5dd81979ccc3d..b9c9f5202bb8a 100644 --- a/Mathlib/MeasureTheory/Constructions/Prod/Basic.lean +++ b/Mathlib/MeasureTheory/Constructions/Prod/Basic.lean @@ -637,9 +637,9 @@ theorem prod_eq_generateFrom {μ : Measure α} {ν : Measure β} {C : Set (Set (h3C.prod h3D).ext (generateFrom_eq_prod hC hD h3C.isCountablySpanning h3D.isCountablySpanning).symm (h2C.prod h2D) _ - · rintro _ ⟨s, hs, t, ht, rfl⟩ - haveI := h3D.sigmaFinite - rw [h₁ s hs t ht, prod_prod] + rintro _ ⟨s, hs, t, ht, rfl⟩ + haveI := h3D.sigmaFinite + rw [h₁ s hs t ht, prod_prod] #align measure_theory.measure.prod_eq_generate_from MeasureTheory.Measure.prod_eq_generateFrom /- Note that the next theorem is not true for s-finite measures: let `μ = ν = ∞ • Leb` on `[0,1]` diff --git a/Mathlib/MeasureTheory/Decomposition/Lebesgue.lean b/Mathlib/MeasureTheory/Decomposition/Lebesgue.lean index 873bdf8e97303..c85d39541c19e 100644 --- a/Mathlib/MeasureTheory/Decomposition/Lebesgue.lean +++ b/Mathlib/MeasureTheory/Decomposition/Lebesgue.lean @@ -759,8 +759,8 @@ theorem sup_mem_measurableLE {f g : α → ℝ≥0∞} (hf : f ∈ measurableLE have h₂ := hA.inter (measurableSet_lt hg.1 hf.1) rw [set_lintegral_max hf.1 hg.1] refine (add_le_add (hg.2 _ h₁) (hf.2 _ h₂)).trans_eq ?_ - · simp only [← not_le, ← compl_setOf, ← diff_eq] - exact measure_inter_add_diff _ (measurableSet_le hf.1 hg.1) + simp only [← not_le, ← compl_setOf, ← diff_eq] + exact measure_inter_add_diff _ (measurableSet_le hf.1 hg.1) #align measure_theory.measure.lebesgue_decomposition.sup_mem_measurable_le MeasureTheory.Measure.LebesgueDecomposition.sup_mem_measurableLE theorem iSup_succ_eq_sup {α} (f : ℕ → α → ℝ≥0∞) (m : ℕ) (a : α) : @@ -1033,9 +1033,9 @@ instance (priority := 100) haveLebesgueDecomposition_of_sigmaFinite (μ ν : Mea suffices hsumeq : (sum fun i : ℕ ↦ (νn i).restrict (S.set n)) = νn n by rw [hsumeq] ext1 s hs rw [sum_apply _ hs, tsum_eq_single n, hνn, h₁, restrict_restrict (T.set_mem n), inter_self] - · intro m hm - rw [hνn, h₁, restrict_restrict (T.set_mem n), (h₃ hm.symm).inter_eq, restrict_empty, - coe_zero, Pi.zero_apply] + intro m hm + rw [hνn, h₁, restrict_restrict (T.set_mem n), (h₃ hm.symm).inter_eq, restrict_empty, + coe_zero, Pi.zero_apply] · exact fun n ↦ Measurable.indicator (measurable_rnDeriv _ _) (S.set_mem n)⟩ #align measure_theory.measure.have_lebesgue_decomposition_of_sigma_finite MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite diff --git a/Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean b/Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean index ce40d15e6bb82..faa65c9b6e43f 100644 --- a/Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean +++ b/Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean @@ -155,7 +155,7 @@ theorem singularPart_totalVariation (s : SignedMeasure α) (μ : Measure α) : s.toJordanDecomposition.negPart.singularPart μ, singularPart_mutuallySingular s μ⟩ := by refine' JordanDecomposition.toSignedMeasure_injective _ rw [toSignedMeasure_toJordanDecomposition, singularPart, JordanDecomposition.toSignedMeasure] - · rw [totalVariation, this] + rw [totalVariation, this] #align measure_theory.signed_measure.singular_part_total_variation MeasureTheory.SignedMeasure.singularPart_totalVariation nonrec theorem mutuallySingular_singularPart (s : SignedMeasure α) (μ : Measure α) : diff --git a/Mathlib/MeasureTheory/Function/UniformIntegrable.lean b/Mathlib/MeasureTheory/Function/UniformIntegrable.lean index 594cb092211e7..a959943ed9541 100644 --- a/Mathlib/MeasureTheory/Function/UniformIntegrable.lean +++ b/Mathlib/MeasureTheory/Function/UniformIntegrable.lean @@ -354,23 +354,23 @@ theorem Memℒp.snorm_indicator_le' (hp_one : 1 ≤ p) (hp_top : p ≠ ∞) (hf rw [norm_indicator_eq_indicator_norm, Set.indicator_apply] · split_ifs with h exacts [h, hMpos]) - · refine' ⟨δ, hδpos, fun s hs hμs => _⟩ - rw [(_ : f = { x : α | M ≤ ‖f x‖₊ }.indicator f + { x : α | ‖f x‖ < M }.indicator f)] - · rw [snorm_indicator_eq_snorm_restrict hs] - refine' le_trans (snorm_add_le _ _ hp_one) _ - · exact StronglyMeasurable.aestronglyMeasurable - (hmeas.indicator (measurableSet_le measurable_const hmeas.nnnorm.measurable.subtype_coe)) - · exact StronglyMeasurable.aestronglyMeasurable - (hmeas.indicator (measurableSet_lt hmeas.nnnorm.measurable.subtype_coe measurable_const)) - · rw [two_mul] - refine' add_le_add (le_trans (snorm_mono_measure _ Measure.restrict_le_self) hM) _ - rw [← snorm_indicator_eq_snorm_restrict hs] - exact hδ s hs hμs - · ext x - by_cases hx : M ≤ ‖f x‖ - · rw [Pi.add_apply, Set.indicator_of_mem, Set.indicator_of_not_mem, add_zero] <;> simpa - · rw [Pi.add_apply, Set.indicator_of_not_mem, Set.indicator_of_mem, zero_add] <;> - simpa using hx + refine' ⟨δ, hδpos, fun s hs hμs => _⟩ + rw [(_ : f = { x : α | M ≤ ‖f x‖₊ }.indicator f + { x : α | ‖f x‖ < M }.indicator f)] + · rw [snorm_indicator_eq_snorm_restrict hs] + refine' le_trans (snorm_add_le _ _ hp_one) _ + · exact StronglyMeasurable.aestronglyMeasurable + (hmeas.indicator (measurableSet_le measurable_const hmeas.nnnorm.measurable.subtype_coe)) + · exact StronglyMeasurable.aestronglyMeasurable + (hmeas.indicator (measurableSet_lt hmeas.nnnorm.measurable.subtype_coe measurable_const)) + · rw [two_mul] + refine' add_le_add (le_trans (snorm_mono_measure _ Measure.restrict_le_self) hM) _ + rw [← snorm_indicator_eq_snorm_restrict hs] + exact hδ s hs hμs + · ext x + by_cases hx : M ≤ ‖f x‖ + · rw [Pi.add_apply, Set.indicator_of_mem, Set.indicator_of_not_mem, add_zero] <;> simpa + · rw [Pi.add_apply, Set.indicator_of_not_mem, Set.indicator_of_mem, zero_add] <;> + simpa using hx #align measure_theory.mem_ℒp.snorm_indicator_le' MeasureTheory.Memℒp.snorm_indicator_le' /-- This lemma is superceded by `MeasureTheory.Memℒp.snorm_indicator_le` which does not require @@ -808,12 +808,12 @@ theorem uniformIntegrable_of' [IsFiniteMeasure μ] (hp : 1 ≤ p) (hp' : p ≠ ((hf i).indicator ((hf i).nnnorm.measurableSet_lt stronglyMeasurable_const))) (StronglyMeasurable.aestronglyMeasurable ((hf i).indicator (stronglyMeasurable_const.measurableSet_le (hf i).nnnorm))) hp) - · rw [Pi.add_apply, Set.indicator_apply] - split_ifs with hx - · rw [Set.indicator_of_not_mem, add_zero] - simpa using hx - · rw [Set.indicator_of_mem, zero_add] - simpa using hx + rw [Pi.add_apply, Set.indicator_apply] + split_ifs with hx + · rw [Set.indicator_of_not_mem, add_zero] + simpa using hx + · rw [Set.indicator_of_mem, zero_add] + simpa using hx _ ≤ (C : ℝ≥0∞) * μ Set.univ ^ p.toReal⁻¹ + 1 := by have : ∀ᵐ x ∂μ, ‖{ x : α | ‖f i x‖₊ < C }.indicator (f i) x‖₊ ≤ C := by filter_upwards diff --git a/Mathlib/MeasureTheory/Integral/Average.lean b/Mathlib/MeasureTheory/Integral/Average.lean index 07f5002323512..ff29711578889 100644 --- a/Mathlib/MeasureTheory/Integral/Average.lean +++ b/Mathlib/MeasureTheory/Integral/Average.lean @@ -673,8 +673,8 @@ theorem measure_le_setLaverage_pos (hμ : μ s ≠ 0) (hμ₁ : μ s ≠ ∞) rintro x ⟨hfx, hx⟩ dsimp at hfx rwa [← toReal_laverage hf, toReal_le_toReal hx (setLaverage_lt_top h).ne] at hfx - · simp_rw [ae_iff, not_ne_iff] - exact measure_eq_top_of_lintegral_ne_top hf h + simp_rw [ae_iff, not_ne_iff] + exact measure_eq_top_of_lintegral_ne_top hf h #align measure_theory.measure_le_set_laverage_pos MeasureTheory.measure_le_setLaverage_pos /-- **First moment method**. A measurable function is greater than its mean on a set of positive diff --git a/Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean b/Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean index 94a3ec42e5b17..728fd878cffa0 100644 --- a/Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean +++ b/Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean @@ -103,8 +103,8 @@ lemma norm_integral_le_mul_norm [IsFiniteMeasure μ] (f : X →ᵇ E) : _ ≤ ∫ x, ‖f x‖ ∂μ := by exact norm_integral_le_integral_norm _ _ ≤ ∫ _, ‖f‖ ∂μ := ?_ _ = ENNReal.toReal (μ Set.univ) • ‖f‖ := by rw [integral_const] - · apply integral_mono _ (integrable_const ‖f‖) (fun x ↦ f.norm_coe_le_norm x) -- NOTE: `gcongr`? - exact (integrable_norm_iff f.continuous.measurable.aestronglyMeasurable).mpr (f.integrable μ) + apply integral_mono _ (integrable_const ‖f‖) (fun x ↦ f.norm_coe_le_norm x) -- NOTE: `gcongr`? + exact (integrable_norm_iff f.continuous.measurable.aestronglyMeasurable).mpr (f.integrable μ) lemma norm_integral_le_norm [IsProbabilityMeasure μ] (f : X →ᵇ E) : ‖∫ x, f x ∂μ‖ ≤ ‖f‖ := by diff --git a/Mathlib/MeasureTheory/Integral/Lebesgue.lean b/Mathlib/MeasureTheory/Integral/Lebesgue.lean index f9c7f7c66a3fe..a2e1c02fa1893 100644 --- a/Mathlib/MeasureTheory/Integral/Lebesgue.lean +++ b/Mathlib/MeasureTheory/Integral/Lebesgue.lean @@ -393,10 +393,10 @@ theorem lintegral_iSup {f : ℕ → α → ℝ≥0∞} (hf : ∀ n, Measurable ( _ ≤ ⨆ n : ℕ, ((rs.map c).restrict { a | (rs.map c) a ≤ f n a }).lintegral μ := by gcongr with n rw [restrict_lintegral _ (h_meas n)] - · refine' le_of_eq (Finset.sum_congr rfl fun r _ => _) - congr 2 with a - refine' and_congr_right _ - simp (config := { contextual := true }) + refine' le_of_eq (Finset.sum_congr rfl fun r _ => _) + congr 2 with a + refine' and_congr_right _ + simp (config := { contextual := true }) _ ≤ ⨆ n, ∫⁻ a, f n a ∂μ := by gcongr with n rw [← SimpleFunc.lintegral_eq_lintegral] diff --git a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean b/Mathlib/MeasureTheory/Measure/Haar/Basic.lean index 8688faf459444..f983591999d86 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/Basic.lean @@ -273,12 +273,12 @@ theorem mul_left_index_le {K : Set G} (hK : IsCompact K) {V : Set G} (hV : (inte rcases index_elim hK hV with ⟨s, h1s, h2s⟩; rw [← h2s] apply Nat.sInf_le; rw [mem_image] refine' ⟨s.map (Equiv.mulRight g⁻¹).toEmbedding, _, Finset.card_map _⟩ - · simp only [mem_setOf_eq]; refine' Subset.trans (image_subset _ h1s) _ - rintro _ ⟨g₁, ⟨_, ⟨g₂, rfl⟩, ⟨_, ⟨hg₂, rfl⟩, hg₁⟩⟩, rfl⟩ - simp only [mem_preimage] at hg₁; - simp only [exists_prop, mem_iUnion, Finset.mem_map, Equiv.coe_mulRight, - exists_exists_and_eq_and, mem_preimage, Equiv.toEmbedding_apply] - refine' ⟨_, hg₂, _⟩; simp only [mul_assoc, hg₁, inv_mul_cancel_left] + simp only [mem_setOf_eq]; refine' Subset.trans (image_subset _ h1s) _ + rintro _ ⟨g₁, ⟨_, ⟨g₂, rfl⟩, ⟨_, ⟨hg₂, rfl⟩, hg₁⟩⟩, rfl⟩ + simp only [mem_preimage] at hg₁; + simp only [exists_prop, mem_iUnion, Finset.mem_map, Equiv.coe_mulRight, + exists_exists_and_eq_and, mem_preimage, Equiv.toEmbedding_apply] + refine' ⟨_, hg₂, _⟩; simp only [mul_assoc, hg₁, inv_mul_cancel_left] #align measure_theory.measure.haar.mul_left_index_le MeasureTheory.Measure.haar.mul_left_index_le #align measure_theory.measure.haar.add_left_add_index_le MeasureTheory.Measure.haar.add_left_addIndex_le diff --git a/Mathlib/MeasureTheory/Measure/Haar/Quotient.lean b/Mathlib/MeasureTheory/Measure/Haar/Quotient.lean index b005947efccfe..88b2164fbf08c 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/Quotient.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/Quotient.lean @@ -367,11 +367,11 @@ lemma _root_.MeasureTheory.IsFundamentalDomain.absolutelyContinuous_map rw [map_apply meas_π s_meas] at hs ⊢ rw [Measure.restrict_apply] at hs · apply h𝓕.measure_zero_of_invariant _ _ hs - · intro γ - ext g - rw [Set.mem_smul_set_iff_inv_smul_mem, mem_preimage, mem_preimage] - congr! 1 - convert QuotientGroup.mk_mul_of_mem g (γ⁻¹).2 using 1 + intro γ + ext g + rw [Set.mem_smul_set_iff_inv_smul_mem, mem_preimage, mem_preimage] + congr! 1 + convert QuotientGroup.mk_mul_of_mem g (γ⁻¹).2 using 1 exact MeasurableSet.preimage s_meas meas_π attribute [-instance] Quotient.instMeasurableSpace diff --git a/Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean b/Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean index 6d01859b44ded..09a2a5455551c 100644 --- a/Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean +++ b/Mathlib/MeasureTheory/Measure/HasOuterApproxClosed.lean @@ -188,17 +188,17 @@ noncomputable instance (X : Type*) [TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] : HasOuterApproxClosed X := by letI : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X refine ⟨fun F hF ↦ ?_⟩ - · use fun n ↦ thickenedIndicator (δ := (1 : ℝ) / (n + 1)) Nat.one_div_pos_of_nat F - refine ⟨?_, ⟨?_, ?_⟩⟩ - · exact fun n x ↦ thickenedIndicator_le_one Nat.one_div_pos_of_nat F x - · exact fun n x hxF ↦ one_le_thickenedIndicator_apply X Nat.one_div_pos_of_nat hxF - · have key := thickenedIndicator_tendsto_indicator_closure - (δseq := fun (n : ℕ) ↦ (1 : ℝ) / (n + 1)) - (fun _ ↦ Nat.one_div_pos_of_nat) tendsto_one_div_add_atTop_nhds_zero_nat F - rw [tendsto_pi_nhds] at * - intro x - nth_rw 2 [← IsClosed.closure_eq hF] - exact key x + use fun n ↦ thickenedIndicator (δ := (1 : ℝ) / (n + 1)) Nat.one_div_pos_of_nat F + refine ⟨?_, ⟨?_, ?_⟩⟩ + · exact fun n x ↦ thickenedIndicator_le_one Nat.one_div_pos_of_nat F x + · exact fun n x hxF ↦ one_le_thickenedIndicator_apply X Nat.one_div_pos_of_nat hxF + · have key := thickenedIndicator_tendsto_indicator_closure + (δseq := fun (n : ℕ) ↦ (1 : ℝ) / (n + 1)) + (fun _ ↦ Nat.one_div_pos_of_nat) tendsto_one_div_add_atTop_nhds_zero_nat F + rw [tendsto_pi_nhds] at * + intro x + nth_rw 2 [← IsClosed.closure_eq hF] + exact key x namespace MeasureTheory diff --git a/Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean b/Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean index 4a681d0aae206..cfa7d14352d11 100644 --- a/Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean +++ b/Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean @@ -361,34 +361,34 @@ lemma continuous_levyProkhorov_to_probabilityMeasure : linarith [εs_pos n, dist_nonneg (x := μs n) (y := ν)] rw [add_zero] at ε_of_room have key := (tendsto_integral_meas_thickening_le f (A := Ioc 0 ‖f‖) (by simp) P).comp ε_of_room' - · have aux : ∀ (z : ℝ), Iio (z + δ/2) ∈ 𝓝 z := fun z ↦ Iio_mem_nhds (by linarith) - filter_upwards [key (aux _), ε_of_room <| Iio_mem_nhds <| half_pos <| - Real.mul_pos (inv_pos.mpr norm_f_pos) δ_pos] - with n hn hn' - simp only [gt_iff_lt, eventually_atTop, ge_iff_le, ne_eq, mem_map, - mem_atTop_sets, mem_preimage, mem_Iio] at * - specialize εs_pos n - have bound := BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt - (Ps n) P (ε := dist (μs n) ν + εs n) ?_ ?_ f ?_ - · refine bound.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, 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 _ _)] - apply ENNReal.add_lt_add_of_le_of_lt (levyProkhorovEDist_ne_top _ _) - (le_of_eq ?_) (ofReal_pos.mpr εs_pos) - rw [LevyProkhorov.dist_def, levyProkhorovDist, - ofReal_toReal (levyProkhorovEDist_ne_top _ _)] - simp only [Ps, P, LevyProkhorov.probabilityMeasure] + have aux : ∀ (z : ℝ), Iio (z + δ/2) ∈ 𝓝 z := fun z ↦ Iio_mem_nhds (by linarith) + filter_upwards [key (aux _), ε_of_room <| Iio_mem_nhds <| half_pos <| + Real.mul_pos (inv_pos.mpr norm_f_pos) δ_pos] + with n hn hn' + simp only [gt_iff_lt, eventually_atTop, ge_iff_le, ne_eq, mem_map, + mem_atTop_sets, mem_preimage, mem_Iio] at * + specialize εs_pos n + have bound := BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt + (Ps n) P (ε := dist (μs n) ν + εs n) ?_ ?_ f ?_ + · refine bound.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, 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 _ _)] + apply ENNReal.add_lt_add_of_le_of_lt (levyProkhorovEDist_ne_top _ _) + (le_of_eq ?_) (ofReal_pos.mpr εs_pos) + rw [LevyProkhorov.dist_def, levyProkhorovDist, + ofReal_toReal (levyProkhorovEDist_ne_top _ _)] + 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 le_rfl)⟩ diff --git a/Mathlib/ModelTheory/ElementaryMaps.lean b/Mathlib/ModelTheory/ElementaryMaps.lean index 8e1f4b490ada4..a8d2e66326c59 100644 --- a/Mathlib/ModelTheory/ElementaryMaps.lean +++ b/Mathlib/ModelTheory/ElementaryMaps.lean @@ -298,8 +298,8 @@ theorem isElementary_of_exists (f : M ↪[L] N) obtain ⟨b, hb⟩ := htv n φ.not xs a (by rw [BoundedFormula.realize_not, ← Unique.eq_default (f ∘ default)] exact ha) - · refine' ⟨b, fun h => hb (Eq.mp _ ((ih _).2 h))⟩ - rw [Unique.eq_default (f ∘ default), Fin.comp_snoc] + refine' ⟨b, fun h => hb (Eq.mp _ ((ih _).2 h))⟩ + rw [Unique.eq_default (f ∘ default), Fin.comp_snoc] #align first_order.language.embedding.is_elementary_of_exists FirstOrder.Language.Embedding.isElementary_of_exists /-- Bundles an embedding satisfying the Tarski-Vaught test as an elementary embedding. -/ diff --git a/Mathlib/ModelTheory/Encoding.lean b/Mathlib/ModelTheory/Encoding.lean index d1377e256ae26..3aaf040faaf3e 100644 --- a/Mathlib/ModelTheory/Encoding.lean +++ b/Mathlib/ModelTheory/Encoding.lean @@ -141,14 +141,14 @@ theorem card_sigma : #(Σn, L.Term (Sum α (Fin n))) = max ℵ₀ #(Sum α (Σi, · rw [Cardinal.le_def] refine' ⟨⟨Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩) fun F => ⟨1, func F.2 fun _ => var (Sum.inr 0)⟩, _⟩⟩ - · rintro (a | a) (b | b) h - · simp only [Sum.elim_inl, Sigma.mk.inj_iff, heq_eq_eq, var.injEq, Sum.inl.injEq, true_and] - at h - rw [h] - · simp only [Sum.elim_inl, Sum.elim_inr, Sigma.mk.inj_iff, false_and] at h - · simp only [Sum.elim_inr, Sum.elim_inl, Sigma.mk.inj_iff, false_and] at h - · simp only [Sum.elim_inr, Sigma.mk.inj_iff, heq_eq_eq, func.injEq, true_and] at h - rw [Sigma.ext_iff.2 ⟨h.1, h.2.1⟩] + rintro (a | a) (b | b) h + · simp only [Sum.elim_inl, Sigma.mk.inj_iff, heq_eq_eq, var.injEq, Sum.inl.injEq, true_and] + at h + rw [h] + · simp only [Sum.elim_inl, Sum.elim_inr, Sigma.mk.inj_iff, false_and] at h + · simp only [Sum.elim_inr, Sum.elim_inl, Sigma.mk.inj_iff, false_and] at h + · simp only [Sum.elim_inr, Sigma.mk.inj_iff, heq_eq_eq, func.injEq, true_and] at h + rw [Sigma.ext_iff.2 ⟨h.1, h.2.1⟩] #align first_order.language.term.card_sigma FirstOrder.Language.Term.card_sigma instance [Encodable α] [Encodable (Σi, L.Functions i)] : Encodable (L.Term α) := @@ -248,33 +248,33 @@ theorem listDecode_encode_list (l : List (Σn, L.BoundedFormula α n)) : · simp only [eq_mp_eq_cast, cast_eq, eq_self_iff_true, heq_iff_eq, and_self_iff, nil_append] · simp only [eq_self_iff_true, heq_iff_eq, and_self_iff] · rw [listEncode, cons_append, cons_append, singleton_append, cons_append, listDecode] - · have h : ∀ i : Fin φ_l, ((List.map Sum.getLeft? (List.map (fun i : Fin φ_l => - Sum.inl (⟨(⟨φ_n, rel φ_R ts⟩ : Σn, L.BoundedFormula α n).fst, ts i⟩ : - Σn, L.Term (Sum α (Fin n)))) (finRange φ_l) ++ l)).get? ↑i).join = some ⟨_, ts i⟩ := by - intro i - simp only [Option.join, map_append, map_map, Option.bind_eq_some, id, exists_eq_right, - get?_eq_some, length_append, length_map, length_finRange] - refine' ⟨lt_of_lt_of_le i.2 le_self_add, _⟩ - rw [get_append, get_map] - · simp only [Sum.getLeft?, get_finRange, Fin.eta, Function.comp_apply, eq_self_iff_true, - heq_iff_eq, and_self_iff] - · simp only [length_map, length_finRange, is_lt] - rw [dif_pos] - swap - · exact fun i => Option.isSome_iff_exists.2 ⟨⟨_, ts i⟩, h i⟩ - rw [dif_pos] - swap - · intro i - obtain ⟨h1, h2⟩ := Option.eq_some_iff_get_eq.1 (h i) - rw [h2] - simp only [Sigma.mk.inj_iff, heq_eq_eq, rel.injEq, true_and] - refine' ⟨funext fun i => _, _⟩ - · obtain ⟨h1, h2⟩ := Option.eq_some_iff_get_eq.1 (h i) - rw [eq_mp_eq_cast, cast_eq_iff_heq] - exact (Sigma.ext_iff.1 ((Sigma.eta (Option.get _ h1)).trans h2)).2 - rw [List.drop_append_eq_append_drop, length_map, length_finRange, Nat.sub_self, drop, - drop_eq_nil_of_le, nil_append] - rw [length_map, length_finRange] + have h : ∀ i : Fin φ_l, ((List.map Sum.getLeft? (List.map (fun i : Fin φ_l => + Sum.inl (⟨(⟨φ_n, rel φ_R ts⟩ : Σn, L.BoundedFormula α n).fst, ts i⟩ : + Σn, L.Term (Sum α (Fin n)))) (finRange φ_l) ++ l)).get? ↑i).join = some ⟨_, ts i⟩ := by + intro i + simp only [Option.join, map_append, map_map, Option.bind_eq_some, id, exists_eq_right, + get?_eq_some, length_append, length_map, length_finRange] + refine' ⟨lt_of_lt_of_le i.2 le_self_add, _⟩ + rw [get_append, get_map] + · simp only [Sum.getLeft?, get_finRange, Fin.eta, Function.comp_apply, eq_self_iff_true, + heq_iff_eq, and_self_iff] + · simp only [length_map, length_finRange, is_lt] + rw [dif_pos] + swap + · exact fun i => Option.isSome_iff_exists.2 ⟨⟨_, ts i⟩, h i⟩ + rw [dif_pos] + swap + · intro i + obtain ⟨h1, h2⟩ := Option.eq_some_iff_get_eq.1 (h i) + rw [h2] + simp only [Sigma.mk.inj_iff, heq_eq_eq, rel.injEq, true_and] + refine' ⟨funext fun i => _, _⟩ + · obtain ⟨h1, h2⟩ := Option.eq_some_iff_get_eq.1 (h i) + rw [eq_mp_eq_cast, cast_eq_iff_heq] + exact (Sigma.ext_iff.1 ((Sigma.eta (Option.get _ h1)).trans h2)).2 + rw [List.drop_append_eq_append_drop, length_map, length_finRange, Nat.sub_self, drop, + drop_eq_nil_of_le, nil_append] + rw [length_map, length_finRange] · rw [listEncode, List.append_assoc, cons_append, listDecode] simp only [] at * rw [(ih1 _).1, (ih1 _).2, (ih2 _).1, (ih2 _).2, sigmaImp] diff --git a/Mathlib/ModelTheory/Satisfiability.lean b/Mathlib/ModelTheory/Satisfiability.lean index 32b8f42313792..73f5d87151f14 100644 --- a/Mathlib/ModelTheory/Satisfiability.lean +++ b/Mathlib/ModelTheory/Satisfiability.lean @@ -245,11 +245,11 @@ theorem exists_elementaryEmbedding_card_eq_of_ge (M : Type w') [L.Structure M] [ rw [← lift_le.{w'}, lift_lift, lift_lift] at h1 exact ⟨h2, h1⟩) (hN0.trans (by rw [← lift_umax', lift_id])) - · letI := (lhomWithConstants L M).reduct N - haveI h : N ⊨ L.elementaryDiagram M := - (NN0.theory_model_iff (L.elementaryDiagram M)).2 inferInstance - refine' ⟨Bundled.of N, ⟨_⟩, hN⟩ - apply ElementaryEmbedding.ofModelsElementaryDiagram L M N + letI := (lhomWithConstants L M).reduct N + haveI h : N ⊨ L.elementaryDiagram M := + (NN0.theory_model_iff (L.elementaryDiagram M)).2 inferInstance + refine' ⟨Bundled.of N, ⟨_⟩, hN⟩ + apply ElementaryEmbedding.ofModelsElementaryDiagram L M N #align first_order.language.exists_elementary_embedding_card_eq_of_ge FirstOrder.Language.exists_elementaryEmbedding_card_eq_of_ge end diff --git a/Mathlib/ModelTheory/Substructures.lean b/Mathlib/ModelTheory/Substructures.lean index 59adac8dca71f..acfaa17bbc06a 100644 --- a/Mathlib/ModelTheory/Substructures.lean +++ b/Mathlib/ModelTheory/Substructures.lean @@ -302,8 +302,8 @@ theorem coe_closure_eq_range_term_realize : change _ = (S : Set M) rw [← SetLike.ext'_iff] refine' closure_eq_of_le (fun x hx => ⟨var ⟨x, hx⟩, rfl⟩) (le_sInf fun S' hS' => _) - · rintro _ ⟨t, rfl⟩ - exact t.realize_mem _ fun i => hS' i.2 + rintro _ ⟨t, rfl⟩ + exact t.realize_mem _ fun i => hS' i.2 #align first_order.language.substructure.coe_closure_eq_range_term_realize FirstOrder.Language.Substructure.coe_closure_eq_range_term_realize instance small_closure [Small.{u} s] : Small.{u} (closure L s) := by @@ -792,7 +792,7 @@ theorem closure_withConstants_eq : rw [← (L.lhomWithConstants A).substructureReduct.le_iff_le] simp only [subset_closure, reduct_withConstants, closure_le, LHom.coe_substructureReduct, Set.union_subset_iff, and_true_iff] - · exact subset_closure_withConstants + exact subset_closure_withConstants #align first_order.language.substructure.closure_with_constants_eq FirstOrder.Language.Substructure.closure_withConstants_eq end Substructure diff --git a/Mathlib/NumberTheory/ClassNumber/Finite.lean b/Mathlib/NumberTheory/ClassNumber/Finite.lean index 54a77956e0f58..d4b3197dd034f 100644 --- a/Mathlib/NumberTheory/ClassNumber/Finite.lean +++ b/Mathlib/NumberTheory/ClassNumber/Finite.lean @@ -133,10 +133,10 @@ theorem exists_min (I : (Ideal S)⁰) : (by obtain ⟨b, b_mem, b_ne_zero⟩ := (I : Ideal S).ne_bot_iff.mp (nonZeroDivisors.coe_ne_zero I) exact ⟨_, ⟨b, b_mem, b_ne_zero, rfl⟩⟩) - · refine' ⟨b, b_mem, b_ne_zero, _⟩ - intro c hc lt - contrapose! lt with c_ne_zero - exact min _ ⟨c, hc, c_ne_zero, rfl⟩ + refine' ⟨b, b_mem, b_ne_zero, _⟩ + intro c hc lt + contrapose! lt with c_ne_zero + exact min _ ⟨c, hc, c_ne_zero, rfl⟩ #align class_group.exists_min ClassGroup.exists_min section IsAdmissible diff --git a/Mathlib/NumberTheory/Cyclotomic/Basic.lean b/Mathlib/NumberTheory/Cyclotomic/Basic.lean index 13007fc15441e..119ea4c42342c 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Basic.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Basic.lean @@ -143,13 +143,13 @@ theorem trans (C : Type w) [CommRing C] [Algebra A C] [Algebra B C] [IsScalarTow · refine' adjoin_induction (((isCyclotomicExtension_iff T B _).1 hT).2 x) (fun c ⟨n, hn⟩ => subset_adjoin ⟨n, Or.inr hn.1, hn.2⟩) (fun b => _) (fun x y hx hy => Subalgebra.add_mem _ hx hy) fun x y hx hy => Subalgebra.mul_mem _ hx hy - · let f := IsScalarTower.toAlgHom A B C - have hb : f b ∈ (adjoin A {b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1}).map f := - ⟨b, ((isCyclotomicExtension_iff _ _ _).1 hS).2 b, rfl⟩ - rw [IsScalarTower.toAlgHom_apply, ← adjoin_image] at hb - refine' adjoin_mono (fun y hy => _) hb - obtain ⟨b₁, ⟨⟨n, hn⟩, h₁⟩⟩ := hy - exact ⟨n, ⟨mem_union_left T hn.1, by rw [← h₁, ← AlgHom.map_pow, hn.2, AlgHom.map_one]⟩⟩ + let f := IsScalarTower.toAlgHom A B C + have hb : f b ∈ (adjoin A {b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1}).map f := + ⟨b, ((isCyclotomicExtension_iff _ _ _).1 hS).2 b, rfl⟩ + rw [IsScalarTower.toAlgHom_apply, ← adjoin_image] at hb + refine' adjoin_mono (fun y hy => _) hb + obtain ⟨b₁, ⟨⟨n, hn⟩, h₁⟩⟩ := hy + exact ⟨n, ⟨mem_union_left T hn.1, by rw [← h₁, ← AlgHom.map_pow, hn.2, AlgHom.map_one]⟩⟩ #align is_cyclotomic_extension.trans IsCyclotomicExtension.trans @[nontriviality] diff --git a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean index 953e390f23390..9a96ba6e720b1 100644 --- a/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean +++ b/Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean @@ -443,24 +443,24 @@ theorem norm_pow_sub_one_of_prime_pow_ne_two {k s : ℕ} (hζ : IsPrimitiveRoot haveI := IsCyclotomicExtension.finiteDimensional {p ^ (k + 1)} K L haveI := IsCyclotomicExtension.isGalois (p ^ (k + 1)) K L rw [norm_eq_norm_adjoin K] - · have H := hη.sub_one_norm_isPrimePow ?_ hirr₁ htwo - swap; · rw [PNat.pow_coe]; exact hpri.1.isPrimePow.pow (Nat.succ_ne_zero _) - rw [add_sub_cancel_right] at H - rw [H] - congr - · rw [PNat.pow_coe, Nat.pow_minFac, hpri.1.minFac_eq] - exact Nat.succ_ne_zero _ - have := FiniteDimensional.finrank_mul_finrank K K⟮η⟯ L - rw [IsCyclotomicExtension.finrank L hirr, IsCyclotomicExtension.finrank K⟮η⟯ hirr₁, - PNat.pow_coe, PNat.pow_coe, Nat.totient_prime_pow hpri.out (k - s).succ_pos, - Nat.totient_prime_pow hpri.out k.succ_pos, mul_comm _ ((p : ℕ) - 1), mul_assoc, - mul_comm ((p : ℕ) ^ (k.succ - 1))] at this - replace this := mul_left_cancel₀ (tsub_pos_iff_lt.2 hpri.out.one_lt).ne' this - have Hex : k.succ - 1 = (k - s).succ - 1 + s := by - simp only [Nat.succ_sub_succ_eq_sub, tsub_zero] - exact (Nat.sub_add_cancel hs).symm - rw [Hex, pow_add] at this - exact mul_left_cancel₀ (pow_ne_zero _ hpri.out.ne_zero) this + have H := hη.sub_one_norm_isPrimePow ?_ hirr₁ htwo + swap; · rw [PNat.pow_coe]; exact hpri.1.isPrimePow.pow (Nat.succ_ne_zero _) + rw [add_sub_cancel_right] at H + rw [H] + congr + · rw [PNat.pow_coe, Nat.pow_minFac, hpri.1.minFac_eq] + exact Nat.succ_ne_zero _ + have := FiniteDimensional.finrank_mul_finrank K K⟮η⟯ L + rw [IsCyclotomicExtension.finrank L hirr, IsCyclotomicExtension.finrank K⟮η⟯ hirr₁, + PNat.pow_coe, PNat.pow_coe, Nat.totient_prime_pow hpri.out (k - s).succ_pos, + Nat.totient_prime_pow hpri.out k.succ_pos, mul_comm _ ((p : ℕ) - 1), mul_assoc, + mul_comm ((p : ℕ) ^ (k.succ - 1))] at this + replace this := mul_left_cancel₀ (tsub_pos_iff_lt.2 hpri.out.one_lt).ne' this + have Hex : k.succ - 1 = (k - s).succ - 1 + s := by + simp only [Nat.succ_sub_succ_eq_sub, tsub_zero] + exact (Nat.sub_add_cancel hs).symm + rw [Hex, pow_add] at this + exact mul_left_cancel₀ (pow_ne_zero _ hpri.out.ne_zero) this #align is_primitive_root.pow_sub_one_norm_prime_pow_ne_two IsPrimitiveRoot.norm_pow_sub_one_of_prime_pow_ne_two /-- If `Irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is a prime, diff --git a/Mathlib/NumberTheory/KummerDedekind.lean b/Mathlib/NumberTheory/KummerDedekind.lean index a82decd893f1d..2a531c476f364 100644 --- a/Mathlib/NumberTheory/KummerDedekind.lean +++ b/Mathlib/NumberTheory/KummerDedekind.lean @@ -174,12 +174,12 @@ theorem comap_map_eq_map_adjoin_of_coprime_conductor exact Ideal.mul_mem_left (I.map (algebraMap R R)) _ (Ideal.mem_map_of_mem _ hq) refine ⟨fun h => ?_, fun h => (Set.mem_image _ _ _).mpr (Exists.intro ⟨z, hz⟩ ⟨by simp [h], rfl⟩)⟩ - · obtain ⟨x₁, hx₁, hx₂⟩ := (Set.mem_image _ _ _).mp h - have : x₁ = ⟨z, hz⟩ := by - apply h_alg - simp [hx₂] - rfl - rwa [← this] + obtain ⟨x₁, hx₁, hx₂⟩ := (Set.mem_image _ _ _).mp h + have : x₁ = ⟨z, hz⟩ := by + apply h_alg + simp [hx₂] + rfl + rwa [← this] · -- The converse inclusion is trivial have : algebraMap R S = (algebraMap _ S).comp (algebraMap R R) := by ext; rfl rw [this, ← Ideal.map_map] diff --git a/Mathlib/NumberTheory/LSeries/MellinEqDirichlet.lean b/Mathlib/NumberTheory/LSeries/MellinEqDirichlet.lean index 4dbb0d550803b..fe9a56fdf81bc 100644 --- a/Mathlib/NumberTheory/LSeries/MellinEqDirichlet.lean +++ b/Mathlib/NumberTheory/LSeries/MellinEqDirichlet.lean @@ -43,8 +43,8 @@ lemma hasSum_mellin {a : ι → ℂ} {p : ι → ℝ} {F : ℝ → ℂ} {s : ℂ (fun t (ht : 0 < t) ↦ ?_) measurableSet_Ioi).const_mul _ simp_rw [mul_comm (↑(rexp _) : ℂ), ← mul_assoc, neg_mul, ofReal_mul] rw [mul_cpow_ofReal_nonneg hpi.le ht.le, ← mul_assoc, one_div, inv_mul_cancel, one_mul] - · rw [Ne, cpow_eq_zero_iff, not_and_or] - exact Or.inl (ofReal_ne_zero.mpr hpi.ne') + rw [Ne, cpow_eq_zero_iff, not_and_or] + exact Or.inl (ofReal_ne_zero.mpr hpi.ne') · -- summability of integrals of norms apply Summable.of_norm convert h_sum.mul_left (Real.Gamma s.re) using 2 with i diff --git a/Mathlib/NumberTheory/Liouville/LiouvilleWith.lean b/Mathlib/NumberTheory/Liouville/LiouvilleWith.lean index 6b9bb058fc6d7..28626f68f3516 100644 --- a/Mathlib/NumberTheory/Liouville/LiouvilleWith.lean +++ b/Mathlib/NumberTheory/Liouville/LiouvilleWith.lean @@ -246,9 +246,9 @@ protected theorem neg (h : LiouvilleWith p x) : LiouvilleWith p (-x) := by refine ⟨C, hC.mono ?_⟩ rintro n ⟨m, hne, hlt⟩ refine ⟨-m, by simp [neg_div, hne], ?_⟩ - · convert hlt using 1 - rw [abs_sub_comm] - congr! 1; push_cast; ring + convert hlt using 1 + rw [abs_sub_comm] + congr! 1; push_cast; ring #align liouville_with.neg LiouvilleWith.neg @[simp] diff --git a/Mathlib/NumberTheory/Modular.lean b/Mathlib/NumberTheory/Modular.lean index b4622a742a1c5..d954ed7ab5168 100644 --- a/Mathlib/NumberTheory/Modular.lean +++ b/Mathlib/NumberTheory/Modular.lean @@ -311,11 +311,11 @@ theorem exists_row_one_eq_and_min_re {cd : Fin 2 → ℤ} (hcd : IsCoprime (cd 0 ⟨⟨x, hx.2⟩⟩ obtain ⟨g, hg⟩ := Filter.Tendsto.exists_forall_le (tendsto_abs_re_smul z hcd) refine' ⟨g, g.2, _⟩ - · intro g1 hg1 - have : g1 ∈ (fun g : SL(2, ℤ) => (↑ₘg) 1) ⁻¹' {cd} := by - rw [Set.mem_preimage, Set.mem_singleton_iff] - exact Eq.trans hg1.symm (Set.mem_singleton_iff.mp (Set.mem_preimage.mp g.2)) - exact hg ⟨g1, this⟩ + intro g1 hg1 + have : g1 ∈ (fun g : SL(2, ℤ) => (↑ₘg) 1) ⁻¹' {cd} := by + rw [Set.mem_preimage, Set.mem_singleton_iff] + exact Eq.trans hg1.symm (Set.mem_singleton_iff.mp (Set.mem_preimage.mp g.2)) + exact hg ⟨g1, this⟩ #align modular_group.exists_row_one_eq_and_min_re ModularGroup.exists_row_one_eq_and_min_re theorem coe_T_zpow_smul_eq {n : ℤ} : (↑(T ^ n • z) : ℂ) = z + n := by diff --git a/Mathlib/NumberTheory/Multiplicity.lean b/Mathlib/NumberTheory/Multiplicity.lean index f2b99dcd02992..9f948db1af5e7 100644 --- a/Mathlib/NumberTheory/Multiplicity.lean +++ b/Mathlib/NumberTheory/Multiplicity.lean @@ -64,13 +64,13 @@ theorem sq_dvd_add_pow_sub_sub (p x : R) (n : ℕ) : mul_one, Nat.cast_zero, zero_add, Nat.succ_eq_add_one, add_tsub_cancel_left] suffices p ^ 2 ∣ ∑ i : ℕ in range n, x ^ i * p ^ (n + 1 - i) * ↑((n + 1).choose i) by convert this; abel - · apply Finset.dvd_sum - intro y hy - calc - p ^ 2 ∣ p ^ (n + 1 - y) := - pow_dvd_pow p (le_tsub_of_add_le_left (by linarith [Finset.mem_range.mp hy])) - _ ∣ x ^ y * p ^ (n + 1 - y) * ↑((n + 1).choose y) := - dvd_mul_of_dvd_left (dvd_mul_left _ _) _ + apply Finset.dvd_sum + intro y hy + calc + p ^ 2 ∣ p ^ (n + 1 - y) := + pow_dvd_pow p (le_tsub_of_add_le_left (by linarith [Finset.mem_range.mp hy])) + _ ∣ x ^ y * p ^ (n + 1 - y) * ↑((n + 1).choose y) := + dvd_mul_of_dvd_left (dvd_mul_left _ _) _ #align sq_dvd_add_pow_sub_sub sq_dvd_add_pow_sub_sub theorem not_dvd_geom_sum₂ {p : R} (hp : Prime p) (hxy : p ∣ x - y) (hx : ¬p ∣ x) (hn : ¬p ∣ n) : @@ -258,8 +258,8 @@ theorem pow_two_pow_sub_pow_two_pow [CommRing R] {x y : R} (n : ℕ) : · simp only [pow_zero, pow_one, range_zero, prod_empty, one_mul, Nat.zero_eq] · suffices x ^ 2 ^ d.succ - y ^ 2 ^ d.succ = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d) by rw [this, hd, Finset.prod_range_succ, ← mul_assoc, mul_comm (x ^ 2 ^ d + y ^ 2 ^ d)] - · rw [Nat.succ_eq_add_one] - ring + rw [Nat.succ_eq_add_one] + ring #align pow_two_pow_sub_pow_two_pow pow_two_pow_sub_pow_two_pow -- Porting note: simplified proof because `fin_cases` was not available in that case diff --git a/Mathlib/NumberTheory/NumberField/Embeddings.lean b/Mathlib/NumberTheory/NumberField/Embeddings.lean index 3a71f98399c53..0d9e2944c6871 100644 --- a/Mathlib/NumberTheory/NumberField/Embeddings.lean +++ b/Mathlib/NumberTheory/NumberField/Embeddings.lean @@ -121,13 +121,13 @@ theorem pow_eq_one_of_norm_eq_one {x : K} (hxi : IsIntegral ℤ x) (hx : ∀ φ obtain ⟨a, -, b, -, habne, h⟩ := @Set.Infinite.exists_ne_map_eq_of_mapsTo _ _ _ _ (x ^ · : ℕ → K) Set.infinite_univ (by exact fun a _ => ⟨hxi.pow a, fun φ => by simp [hx φ]⟩) (finite_of_norm_le K A (1 : ℝ)) - · wlog hlt : b < a - · exact this K A hxi hx b a habne.symm h.symm (habne.lt_or_lt.resolve_right hlt) - refine ⟨a - b, tsub_pos_of_lt hlt, ?_⟩ - rw [← Nat.sub_add_cancel hlt.le, pow_add, mul_left_eq_self₀] at h - refine h.resolve_right fun hp => ?_ - specialize hx (IsAlgClosed.lift (NumberField.isAlgebraic K)).toRingHom - rw [pow_eq_zero hp, map_zero, norm_zero] at hx; norm_num at hx + wlog hlt : b < a + · exact this K A hxi hx b a habne.symm h.symm (habne.lt_or_lt.resolve_right hlt) + refine ⟨a - b, tsub_pos_of_lt hlt, ?_⟩ + rw [← Nat.sub_add_cancel hlt.le, pow_add, mul_left_eq_self₀] at h + refine h.resolve_right fun hp => ?_ + specialize hx (IsAlgClosed.lift (NumberField.isAlgebraic K)).toRingHom + rw [pow_eq_zero hp, map_zero, norm_zero] at hx; norm_num at hx #align number_field.embeddings.pow_eq_one_of_norm_eq_one NumberField.Embeddings.pow_eq_one_of_norm_eq_one end Bounded diff --git a/Mathlib/NumberTheory/Padics/PadicNumbers.lean b/Mathlib/NumberTheory/Padics/PadicNumbers.lean index e0a62297b77f4..9a2a587ef5a51 100644 --- a/Mathlib/NumberTheory/Padics/PadicNumbers.lean +++ b/Mathlib/NumberTheory/Padics/PadicNumbers.lean @@ -707,21 +707,21 @@ theorem exi_rat_seq_conv_cauchy : IsCauSeq (padicNorm p) (limSeq f) := fun ε h ring_nf at this ⊢ rw [← padicNormE.eq_padic_norm'] exact mod_cast this - · apply lt_of_le_of_lt - · apply padicNormE.add_le - · rw [← add_thirds ε] - apply _root_.add_lt_add - · suffices padicNormE (limSeq f j - f j + (f j - f (max N N2)) : ℚ_[p]) < ε / 3 + ε / 3 by - simpa only [sub_add_sub_cancel] - apply lt_of_le_of_lt - · apply padicNormE.add_le - · apply _root_.add_lt_add - · rw [padicNormE.map_sub] - apply mod_cast hN j - exact le_of_max_le_left hj - · exact hN2 _ (le_of_max_le_right hj) _ (le_max_right _ _) - · apply mod_cast hN (max N N2) - apply le_max_left + apply lt_of_le_of_lt + · apply padicNormE.add_le + · rw [← add_thirds ε] + apply _root_.add_lt_add + · suffices padicNormE (limSeq f j - f j + (f j - f (max N N2)) : ℚ_[p]) < ε / 3 + ε / 3 by + simpa only [sub_add_sub_cancel] + apply lt_of_le_of_lt + · apply padicNormE.add_le + · apply _root_.add_lt_add + · rw [padicNormE.map_sub] + apply mod_cast hN j + exact le_of_max_le_left hj + · exact hN2 _ (le_of_max_le_right hj) _ (le_max_right _ _) + · apply mod_cast hN (max N N2) + apply le_max_left #align padic.exi_rat_seq_conv_cauchy Padic.exi_rat_seq_conv_cauchy private def lim' : PadicSeq p := @@ -903,9 +903,9 @@ theorem norm_rat_le_one : ∀ {q : ℚ} (_ : ¬p ∣ q.den), ‖(q : ℚ_[p])‖ rw [padicNorm.eq_zpow_of_nonzero hnz', padicValRat, neg_sub, padicValNat.eq_zero_of_not_dvd hq, Nat.cast_zero, zero_sub, zpow_neg, zpow_natCast] apply inv_le_one - · norm_cast - apply one_le_pow - exact hp.1.pos + norm_cast + apply one_le_pow + exact hp.1.pos #align padic_norm_e.norm_rat_le_one padicNormE.norm_rat_le_one theorem norm_int_le_one (z : ℤ) : ‖(z : ℚ_[p])‖ ≤ 1 := diff --git a/Mathlib/NumberTheory/RamificationInertia.lean b/Mathlib/NumberTheory/RamificationInertia.lean index 0812be266481c..025b5e82b0381 100644 --- a/Mathlib/NumberTheory/RamificationInertia.lean +++ b/Mathlib/NumberTheory/RamificationInertia.lean @@ -147,7 +147,7 @@ theorem ramificationIdx_eq_normalizedFactors_count (hp0 : map f p ≠ ⊥) (hP : rw [dvd_iff_normalizedFactors_le_normalizedFactors (pow_ne_zero _ hP0) hp0, normalizedFactors_pow, normalizedFactors_irreducible hPirr, normalize_eq, Multiset.nsmul_singleton, ← Multiset.le_count_iff_replicate_le] - · exact (Nat.lt_succ_self _).not_le + exact (Nat.lt_succ_self _).not_le #align ideal.is_dedekind_domain.ramification_idx_eq_normalized_factors_count Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count theorem ramificationIdx_eq_factors_count (hp0 : map f p ≠ ⊥) (hP : P.IsPrime) (hP0 : P ≠ ⊥) : diff --git a/Mathlib/Probability/Distributions/Exponential.lean b/Mathlib/Probability/Distributions/Exponential.lean index e67d27882572c..ab0ec159e99d8 100644 --- a/Mathlib/Probability/Distributions/Exponential.lean +++ b/Mathlib/Probability/Distributions/Exponential.lean @@ -147,7 +147,7 @@ lemma lintegral_exponentialPDF_eq_antiDeriv {r : ℝ} (hr : 0 < r) (x : ℝ) : (f := fun a ↦ -1 * rexp (-(r * a))) _ _] · rw [ENNReal.toReal_ofReal_eq_iff.2 (by set_option tactic.skipAssignedInstances false in norm_num; positivity)] - · norm_num; ring + norm_num; ring · simp only [intervalIntegrable_iff, uIoc_of_le h] exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _ · have : Continuous (fun a ↦ rexp (-(r * a))) := by diff --git a/Mathlib/Probability/Independence/Conditional.lean b/Mathlib/Probability/Independence/Conditional.lean index 7186cc7f4c5ed..f6384e44600a3 100644 --- a/Mathlib/Probability/Independence/Conditional.lean +++ b/Mathlib/Probability/Independence/Conditional.lean @@ -658,10 +658,10 @@ theorem condIndepFun_iff_condexp_inter_preimage_eq_mul {mβ : MeasurableSpace β ∀ s t, MeasurableSet s → MeasurableSet t → (μ⟦f ⁻¹' s ∩ g ⁻¹' t | m'⟧) =ᵐ[μ] fun ω ↦ (μ⟦f ⁻¹' s | m'⟧) ω * (μ⟦g ⁻¹' t | m'⟧) ω := by rw [condIndepFun_iff _ _ _ _ hf hg] - · refine ⟨fun h s t hs ht ↦ ?_, fun h s t ↦ ?_⟩ - · exact h (f ⁻¹' s) (g ⁻¹' t) ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩ - · rintro ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩ - exact h s t hs ht + refine ⟨fun h s t hs ht ↦ ?_, fun h s t ↦ ?_⟩ + · exact h (f ⁻¹' s) (g ⁻¹' t) ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩ + · rintro ⟨s, hs, rfl⟩ ⟨t, ht, rfl⟩ + exact h s t hs ht theorem iCondIndepFun_iff_condexp_inter_preimage_eq_mul {β : ι → Type*} (m : ∀ x, MeasurableSpace (β x)) (f : ∀ i, Ω → β i) (hf : ∀ i, Measurable (f i)) : diff --git a/Mathlib/Probability/Kernel/Disintegration/CdfToKernel.lean b/Mathlib/Probability/Kernel/Disintegration/CdfToKernel.lean index 599f678c19ca5..81f50ef6e6f43 100644 --- a/Mathlib/Probability/Kernel/Disintegration/CdfToKernel.lean +++ b/Mathlib/Probability/Kernel/Disintegration/CdfToKernel.lean @@ -331,14 +331,14 @@ lemma IsRatCondKernelCDFAux.integrable_iInf_rat_gt (hf : IsRatCondKernelCDFAux f refine ⟨(measurable_iInf fun i ↦ hf.measurable_right a _).aestronglyMeasurable, ?_⟩ refine (?_ : _ ≤ (ν a univ : ℝ≥0∞)).trans_lt (measure_lt_top _ _) refine (snorm_le_of_ae_bound (C := 1) ?_).trans (by simp) - · filter_upwards [hf.bddBelow_range a, hf.nonneg a, hf.le_one a] - with t hbdd_below h_nonneg h_le_one - rw [Real.norm_eq_abs, abs_of_nonneg] - · refine ciInf_le_of_le ?_ ?_ ?_ - · exact hbdd_below _ - · exact ⟨q + 1, by simp⟩ - · exact h_le_one _ - · exact le_ciInf fun r ↦ h_nonneg _ + filter_upwards [hf.bddBelow_range a, hf.nonneg a, hf.le_one a] + with t hbdd_below h_nonneg h_le_one + rw [Real.norm_eq_abs, abs_of_nonneg] + · refine ciInf_le_of_le ?_ ?_ ?_ + · exact hbdd_below _ + · exact ⟨q + 1, by simp⟩ + · exact h_le_one _ + · exact le_ciInf fun r ↦ h_nonneg _ lemma _root_.MeasureTheory.Measure.iInf_rat_gt_prod_Iic {ρ : Measure (α × ℝ)} [IsFiniteMeasure ρ] {s : Set α} (hs : MeasurableSet s) (t : ℚ) : diff --git a/Mathlib/Probability/Martingale/Basic.lean b/Mathlib/Probability/Martingale/Basic.lean index 357046f503485..a2a9568d19dd5 100644 --- a/Mathlib/Probability/Martingale/Basic.lean +++ b/Mathlib/Probability/Martingale/Basic.lean @@ -334,7 +334,7 @@ theorem Submartingale.condexp_sub_nonneg {f : ι → Ω → ℝ} (hf : Submartin refine' EventuallyLE.trans _ (condexp_sub (hf.integrable _) (hf.integrable _)).symm.le rw [eventually_sub_nonneg, condexp_of_stronglyMeasurable (ℱ.le _) (hf.adapted _) (hf.integrable _)] - · exact hf.2.1 i j hij + exact hf.2.1 i j hij #align measure_theory.submartingale.condexp_sub_nonneg MeasureTheory.Submartingale.condexp_sub_nonneg theorem submartingale_iff_condexp_sub_nonneg [IsFiniteMeasure μ] {f : ι → Ω → ℝ} : diff --git a/Mathlib/Probability/Martingale/Convergence.lean b/Mathlib/Probability/Martingale/Convergence.lean index a9427d73c4cc4..b9ed1af67cdec 100644 --- a/Mathlib/Probability/Martingale/Convergence.lean +++ b/Mathlib/Probability/Martingale/Convergence.lean @@ -144,9 +144,9 @@ theorem tendsto_of_uncrossing_lt_top (hf₁ : liminf (fun n => (‖f n ω‖₊ by_cases h : IsBoundedUnder (· ≤ ·) atTop fun n => |f n ω| · rw [isBoundedUnder_le_abs] at h refine' tendsto_of_no_upcrossings Rat.denseRange_cast _ h.1 h.2 - · intro a ha b hb hab - obtain ⟨⟨a, rfl⟩, ⟨b, rfl⟩⟩ := ha, hb - exact not_frequently_of_upcrossings_lt_top hab (hf₂ a b (Rat.cast_lt.1 hab)).ne + intro a ha b hb hab + obtain ⟨⟨a, rfl⟩, ⟨b, rfl⟩⟩ := ha, hb + exact not_frequently_of_upcrossings_lt_top hab (hf₂ a b (Rat.cast_lt.1 hab)).ne · obtain ⟨a, b, hab, h₁, h₂⟩ := ENNReal.exists_upcrossings_of_not_bounded_under hf₁.ne h exact False.elim ((hf₂ a b hab).ne (upcrossings_eq_top_of_frequently_lt (Rat.cast_lt.2 hab) h₁ h₂)) diff --git a/Mathlib/Probability/Martingale/Upcrossing.lean b/Mathlib/Probability/Martingale/Upcrossing.lean index 9526c067665ea..8672b66e4a14f 100644 --- a/Mathlib/Probability/Martingale/Upcrossing.lean +++ b/Mathlib/Probability/Martingale/Upcrossing.lean @@ -346,9 +346,9 @@ theorem Adapted.isStoppingTime_crossing (hf : Adapted ℱ f) : exact isStoppingTime_hitting_isStoppingTime ih₂ (fun _ => lowerCrossingTime_le) measurableSet_Ici hf _ refine' ⟨this, _⟩ - · intro n - exact isStoppingTime_hitting_isStoppingTime this (fun _ => upperCrossingTime_le) - measurableSet_Iic hf _ + intro n + exact isStoppingTime_hitting_isStoppingTime this (fun _ => upperCrossingTime_le) + measurableSet_Iic hf _ #align measure_theory.adapted.is_stopping_time_crossing MeasureTheory.Adapted.isStoppingTime_crossing theorem Adapted.isStoppingTime_upperCrossingTime (hf : Adapted ℱ f) : @@ -558,18 +558,18 @@ theorem upcrossingsBefore_lt_of_exists_upcrossing (hab : a < b) {N₁ N₂ : ℕ upcrossingsBefore a b f N ω < upcrossingsBefore a b f (N₂ + 1) ω := by refine' lt_of_lt_of_le (Nat.lt_succ_self _) (le_csSup (upperCrossingTime_lt_bddAbove hab) _) rw [Set.mem_setOf_eq, upperCrossingTime_succ_eq, hitting_lt_iff _ le_rfl] - · refine' ⟨N₂, ⟨_, Nat.lt_succ_self _⟩, hN₂'.le⟩ - rw [lowerCrossingTime, hitting_le_iff_of_lt _ (Nat.lt_succ_self _)] - refine' ⟨N₁, ⟨le_trans _ hN₁, hN₂⟩, hN₁'.le⟩ - by_cases hN : 0 < N - · have : upperCrossingTime a b f N (upcrossingsBefore a b f N ω) ω < N := - Nat.sSup_mem (upperCrossingTime_lt_nonempty hN) (upperCrossingTime_lt_bddAbove hab) - rw [upperCrossingTime_eq_upperCrossingTime_of_lt (hN₁.trans (hN₂.trans <| Nat.le_succ _)) - this] - exact this.le - · rw [not_lt, Nat.le_zero] at hN - rw [hN, upcrossingsBefore_zero, upperCrossingTime_zero] - rfl + refine' ⟨N₂, ⟨_, Nat.lt_succ_self _⟩, hN₂'.le⟩ + rw [lowerCrossingTime, hitting_le_iff_of_lt _ (Nat.lt_succ_self _)] + refine' ⟨N₁, ⟨le_trans _ hN₁, hN₂⟩, hN₁'.le⟩ + by_cases hN : 0 < N + · have : upperCrossingTime a b f N (upcrossingsBefore a b f N ω) ω < N := + Nat.sSup_mem (upperCrossingTime_lt_nonempty hN) (upperCrossingTime_lt_bddAbove hab) + rw [upperCrossingTime_eq_upperCrossingTime_of_lt (hN₁.trans (hN₂.trans <| Nat.le_succ _)) + this] + exact this.le + · rw [not_lt, Nat.le_zero] at hN + rw [hN, upcrossingsBefore_zero, upperCrossingTime_zero] + rfl #align measure_theory.upcrossings_before_lt_of_exists_upcrossing MeasureTheory.upcrossingsBefore_lt_of_exists_upcrossing theorem lowerCrossingTime_lt_of_lt_upcrossingsBefore (hN : 0 < N) (hab : a < b) diff --git a/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean b/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean index 94e1f9f6ffbdc..ec1ea7816e080 100644 --- a/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean +++ b/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean @@ -119,9 +119,9 @@ theorem actionDiagonalSucc_hom_apply {G : Type u} [Group G] {n : ℕ} (f : Fin ( Fin.insertNth_zero'] refine' Fin.cases (Fin.cons_zero _ _) (fun i => _) x · simp only [Fin.cons_succ, mul_left_inj, inv_inj, Fin.castSucc_fin_succ] -/ - · dsimp [actionDiagonalSucc] - erw [hn (fun (j : Fin (n + 1)) => f j.succ)] - exact Fin.cases rfl (fun i => rfl) x + dsimp [actionDiagonalSucc] + erw [hn (fun (j : Fin (n + 1)) => f j.succ)] + exact Fin.cases rfl (fun i => rfl) x set_option linter.uppercaseLean3 false in #align group_cohomology.resolution.Action_diagonal_succ_hom_apply groupCohomology.resolution.actionDiagonalSucc_hom_apply @@ -237,7 +237,7 @@ theorem diagonalSucc_inv_single_left (g : G) (f : Gⁿ →₀ k) (r : k) : -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 erw [diagonalSucc_inv_single_single] rw [sum_single_index, mul_comm] - · rw [zero_mul, single_zero] + rw [zero_mul, single_zero] #align group_cohomology.resolution.diagonal_succ_inv_single_left groupCohomology.resolution.diagonalSucc_inv_single_left theorem diagonalSucc_inv_single_right (g : G →₀ k) (f : Gⁿ) (r : k) : @@ -258,7 +258,7 @@ theorem diagonalSucc_inv_single_right (g : G →₀ k) (f : Gⁿ) (r : k) : -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 erw [diagonalSucc_inv_single_single] rw [sum_single_index] - · rw [zero_mul, single_zero] + rw [zero_mul, single_zero] #align group_cohomology.resolution.diagonal_succ_inv_single_right groupCohomology.resolution.diagonalSucc_inv_single_right end Rep diff --git a/Mathlib/RepresentationTheory/Rep.lean b/Mathlib/RepresentationTheory/Rep.lean index be968c1e2094f..91a3ae6b91ec8 100644 --- a/Mathlib/RepresentationTheory/Rep.lean +++ b/Mathlib/RepresentationTheory/Rep.lean @@ -348,7 +348,7 @@ theorem leftRegularHom_apply {A : Rep k G} (x : A) : -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 erw [leftRegularHom_hom, Finsupp.lift_apply, Finsupp.sum_single_index, one_smul, A.ρ.map_one, LinearMap.one_apply] - · rw [zero_smul] + rw [zero_smul] set_option linter.uppercaseLean3 false in #align Rep.left_regular_hom_apply Rep.leftRegularHom_apply @@ -387,7 +387,7 @@ theorem leftRegularHomEquiv_symm_single {A : Rep k G} (x : A) (g : G) : -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 erw [leftRegularHomEquiv_symm_apply, leftRegularHom_hom, Finsupp.lift_apply, Finsupp.sum_single_index, one_smul] - · rw [zero_smul] + rw [zero_smul] set_option linter.uppercaseLean3 false in #align Rep.left_regular_hom_equiv_symm_single Rep.leftRegularHomEquiv_symm_single diff --git a/Mathlib/RingTheory/AdicCompletion/Basic.lean b/Mathlib/RingTheory/AdicCompletion/Basic.lean index 2417b6a8fe2e4..71e0bbeeab55f 100644 --- a/Mathlib/RingTheory/AdicCompletion/Basic.lean +++ b/Mathlib/RingTheory/AdicCompletion/Basic.lean @@ -506,22 +506,22 @@ theorem le_jacobson_bot [IsAdicComplete I R] : I ≤ (⊥ : Ideal R).jacobson := rw [mul_pow, pow_add, mul_assoc] exact Ideal.mul_mem_right _ (I ^ m) (Ideal.pow_mem_pow hx m) obtain ⟨L, hL⟩ := IsPrecomplete.prec toIsPrecomplete @hf - · rw [isUnit_iff_exists_inv] - use L - rw [← sub_eq_zero, neg_mul] - apply IsHausdorff.haus (toIsHausdorff : IsHausdorff I R) - intro n - specialize hL n - rw [SModEq.sub_mem, Algebra.id.smul_eq_mul, Ideal.mul_top] at hL ⊢ - rw [sub_zero] - suffices (1 - x * y) * f n - 1 ∈ I ^ n by - convert Ideal.sub_mem _ this (Ideal.mul_mem_left _ (1 + -(x * y)) hL) using 1 - ring - cases n - · simp only [Ideal.one_eq_top, pow_zero, Nat.zero_eq, mem_top] - · rw [← neg_sub _ (1 : R), neg_mul, mul_geom_sum, neg_sub, sub_sub, add_comm, ← sub_sub, - sub_self, zero_sub, @neg_mem_iff, mul_pow] - exact Ideal.mul_mem_right _ (I ^ _) (Ideal.pow_mem_pow hx _) + rw [isUnit_iff_exists_inv] + use L + rw [← sub_eq_zero, neg_mul] + apply IsHausdorff.haus (toIsHausdorff : IsHausdorff I R) + intro n + specialize hL n + rw [SModEq.sub_mem, Algebra.id.smul_eq_mul, Ideal.mul_top] at hL ⊢ + rw [sub_zero] + suffices (1 - x * y) * f n - 1 ∈ I ^ n by + convert Ideal.sub_mem _ this (Ideal.mul_mem_left _ (1 + -(x * y)) hL) using 1 + ring + cases n + · simp only [Ideal.one_eq_top, pow_zero, Nat.zero_eq, mem_top] + · rw [← neg_sub _ (1 : R), neg_mul, mul_geom_sum, neg_sub, sub_sub, add_comm, ← sub_sub, + sub_self, zero_sub, @neg_mem_iff, mul_pow] + exact Ideal.mul_mem_right _ (I ^ _) (Ideal.pow_mem_pow hx _) #align is_adic_complete.le_jacobson_bot IsAdicComplete.le_jacobson_bot end IsAdicComplete diff --git a/Mathlib/RingTheory/Adjoin/PowerBasis.lean b/Mathlib/RingTheory/Adjoin/PowerBasis.lean index 2260f3f9779eb..7521e4eabae4c 100644 --- a/Mathlib/RingTheory/Adjoin/PowerBasis.lean +++ b/Mathlib/RingTheory/Adjoin/PowerBasis.lean @@ -45,11 +45,11 @@ noncomputable def adjoin.powerBasisAux {x : S} (hx : IsIntegral K x) : have := hx'.mem_span_pow (y := ⟨y, hy⟩) rw [← minpoly.algebraMap_eq hST] at this apply this - · rw [adjoin_singleton_eq_range_aeval] at hy - obtain ⟨f, rfl⟩ := (aeval x).mem_range.mp hy - use f - ext - exact aeval_algebraMap_apply S (⟨x, _⟩ : adjoin K {x}) _ + rw [adjoin_singleton_eq_range_aeval] at hy + obtain ⟨f, rfl⟩ := (aeval x).mem_range.mp hy + use f + ext + exact aeval_algebraMap_apply S (⟨x, _⟩ : adjoin K {x}) _ #align algebra.adjoin.power_basis_aux Algebra.adjoin.powerBasisAux /-- The power basis `1, x, ..., x ^ (d - 1)` for `K[x]`, diff --git a/Mathlib/RingTheory/DedekindDomain/Ideal.lean b/Mathlib/RingTheory/DedekindDomain/Ideal.lean index cc2179dd14a74..60b23ec5f715d 100644 --- a/Mathlib/RingTheory/DedekindDomain/Ideal.lean +++ b/Mathlib/RingTheory/DedekindDomain/Ideal.lean @@ -821,11 +821,11 @@ theorem Ideal.exist_integer_multiples_not_mem {J : Ideal A} (hJ : J ≠ ⊤) {ι ↑J / I = ↑J * I⁻¹ := div_eq_mul_inv (↑J) I _ < 1 * I⁻¹ := mul_right_strictMono (inv_ne_zero hI0) ?_ _ = I⁻¹ := one_mul _ - · rw [← coeIdeal_top] - -- And multiplying by `I⁻¹` is indeed strictly monotone. - exact - strictMono_of_le_iff_le (fun _ _ => (coeIdeal_le_coeIdeal K).symm) - (lt_top_iff_ne_top.mpr hJ) + rw [← coeIdeal_top] + -- And multiplying by `I⁻¹` is indeed strictly monotone. + exact + strictMono_of_le_iff_le (fun _ _ => (coeIdeal_le_coeIdeal K).symm) + (lt_top_iff_ne_top.mpr hJ) #align ideal.exist_integer_multiples_not_mem Ideal.exist_integer_multiples_not_mem section Gcd diff --git a/Mathlib/RingTheory/Finiteness.lean b/Mathlib/RingTheory/Finiteness.lean index 6d1d64e421ab8..98a698d45b1c3 100644 --- a/Mathlib/RingTheory/Finiteness.lean +++ b/Mathlib/RingTheory/Finiteness.lean @@ -784,8 +784,8 @@ instance finite_finset_sup {ι : Type*} (s : Finset ι) (S : ι → Submodule R refine' @Finset.sup_induction _ _ _ _ s S (fun i => Module.Finite R ↑i) (Module.Finite.bot R V) _ fun i _ => by infer_instance - · intro S₁ hS₁ S₂ hS₂ - exact Submodule.finite_sup S₁ S₂ + intro S₁ hS₁ S₂ hS₂ + exact Submodule.finite_sup S₁ S₂ /-- The submodule generated by a supremum of finite dimensional submodules, indexed by a finite sort is finite-dimensional. -/ diff --git a/Mathlib/RingTheory/GradedAlgebra/Basic.lean b/Mathlib/RingTheory/GradedAlgebra/Basic.lean index ab842cb46376d..743250c5e8b96 100644 --- a/Mathlib/RingTheory/GradedAlgebra/Basic.lean +++ b/Mathlib/RingTheory/GradedAlgebra/Basic.lean @@ -282,16 +282,16 @@ def GradedRing.projZeroRingHom : A →+* A where refine' DirectSum.Decomposition.inductionOn 𝒜 _ _ _ · simp only [mul_zero, decompose_zero, zero_apply, ZeroMemClass.coe_zero] · rintro j ⟨c', hc'⟩ - · simp only [Subtype.coe_mk] - by_cases h : i + j = 0 - · rw [decompose_of_mem_same 𝒜 - (show c * c' ∈ 𝒜 0 from h ▸ SetLike.GradedMul.mul_mem hc hc'), - decompose_of_mem_same 𝒜 (show c ∈ 𝒜 0 from (add_eq_zero_iff.mp h).1 ▸ hc), - decompose_of_mem_same 𝒜 (show c' ∈ 𝒜 0 from (add_eq_zero_iff.mp h).2 ▸ hc')] - · rw [decompose_of_mem_ne 𝒜 (SetLike.GradedMul.mul_mem hc hc') h] - cases' show i ≠ 0 ∨ j ≠ 0 by rwa [add_eq_zero_iff, not_and_or] at h with h' h' - · simp only [decompose_of_mem_ne 𝒜 hc h', zero_mul] - · simp only [decompose_of_mem_ne 𝒜 hc' h', mul_zero] + simp only [Subtype.coe_mk] + by_cases h : i + j = 0 + · rw [decompose_of_mem_same 𝒜 + (show c * c' ∈ 𝒜 0 from h ▸ SetLike.GradedMul.mul_mem hc hc'), + decompose_of_mem_same 𝒜 (show c ∈ 𝒜 0 from (add_eq_zero_iff.mp h).1 ▸ hc), + decompose_of_mem_same 𝒜 (show c' ∈ 𝒜 0 from (add_eq_zero_iff.mp h).2 ▸ hc')] + · rw [decompose_of_mem_ne 𝒜 (SetLike.GradedMul.mul_mem hc hc') h] + cases' show i ≠ 0 ∨ j ≠ 0 by rwa [add_eq_zero_iff, not_and_or] at h with h' h' + · simp only [decompose_of_mem_ne 𝒜 hc h', zero_mul] + · simp only [decompose_of_mem_ne 𝒜 hc' h', mul_zero] · intro _ _ hd he simp only at hd he -- Porting note: added simp only [mul_add, decompose_add, add_apply, AddMemClass.coe_add, hd, he] diff --git a/Mathlib/RingTheory/HahnSeries/Summable.lean b/Mathlib/RingTheory/HahnSeries/Summable.lean index 351e36368fc03..3114f305c4bbe 100644 --- a/Mathlib/RingTheory/HahnSeries/Summable.lean +++ b/Mathlib/RingTheory/HahnSeries/Summable.lean @@ -545,7 +545,7 @@ theorem unit_aux (x : HahnSeries Γ R) {r : R} (hr : r * x.coeff x.order = 1) : rw [addVal_apply_of_ne x0, addVal_apply_of_ne (single_ne_zero h10), addVal_apply_of_ne _, order_C, order_single h10, WithTop.coe_zero, zero_add, ← WithTop.coe_add, neg_add_self, WithTop.coe_zero] - · exact C_ne_zero (left_ne_zero_of_mul_eq_one hr) + exact C_ne_zero (left_ne_zero_of_mul_eq_one hr) · rw [addVal_apply, ← WithTop.coe_zero] split_ifs with h · apply WithTop.coe_ne_top diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean index c25494266170c..31732576e61ae 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime.lean @@ -80,11 +80,11 @@ theorem Ideal.radical_minimalPrimes : I.radical.minimalPrimes = I.minimalPrimes ext p refine' ⟨_, _⟩ <;> rintro ⟨⟨a, ha⟩, b⟩ · refine' ⟨⟨a, a.radical_le_iff.1 ha⟩, _⟩ - · simp only [Set.mem_setOf_eq, and_imp] at * - exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.2 h3) h4 + simp only [Set.mem_setOf_eq, and_imp] at * + exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.2 h3) h4 · refine' ⟨⟨a, a.radical_le_iff.2 ha⟩, _⟩ - · simp only [Set.mem_setOf_eq, and_imp] at * - exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.1 h3) h4 + simp only [Set.mem_setOf_eq, and_imp] at * + exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.1 h3) h4 #align ideal.radical_minimal_primes Ideal.radical_minimalPrimes @[simp] diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean index dba1683177de7..0b2c9de8d0fe1 100644 --- a/Mathlib/RingTheory/Ideal/Operations.lean +++ b/Mathlib/RingTheory/Ideal/Operations.lean @@ -1300,6 +1300,8 @@ end Dvd end MulAndRadical + + section Total variable (ι : Type*) diff --git a/Mathlib/RingTheory/IntegrallyClosed.lean b/Mathlib/RingTheory/IntegrallyClosed.lean index cb3609ee933e3..55e378dabd099 100644 --- a/Mathlib/RingTheory/IntegrallyClosed.lean +++ b/Mathlib/RingTheory/IntegrallyClosed.lean @@ -156,8 +156,8 @@ theorem integralClosure_eq_bot_iff (hRA : Function.Injective (algebraMap R A)) : constructor · intro h refine ⟨ hRA, fun hx => Set.mem_range.mp (Algebra.mem_bot.mp (h hx)), ?_⟩ - · rintro ⟨y, rfl⟩ - apply isIntegral_algebraMap + rintro ⟨y, rfl⟩ + apply isIntegral_algebraMap · intro h x hx rw [Algebra.mem_bot, Set.mem_range] exact isIntegral_iff.mp hx diff --git a/Mathlib/RingTheory/IsAdjoinRoot.lean b/Mathlib/RingTheory/IsAdjoinRoot.lean index cfca3760b5d64..330258944f8de 100644 --- a/Mathlib/RingTheory/IsAdjoinRoot.lean +++ b/Mathlib/RingTheory/IsAdjoinRoot.lean @@ -221,14 +221,14 @@ def lift (h : IsAdjoinRoot S f) : S →+* T where map_add' z w := by dsimp only -- Porting note (#10752): added `dsimp only` rw [h.eval₂_repr_eq_eval₂_of_map_eq hx _ (h.repr z + h.repr w), eval₂_add] - · rw [map_add, map_repr, map_repr] + rw [map_add, map_repr, map_repr] map_one' := by beta_reduce -- Porting note (#12129): additional beta reduction needed rw [h.eval₂_repr_eq_eval₂_of_map_eq hx _ _ (map_one _), eval₂_one] map_mul' z w := by dsimp only -- Porting note (#10752): added `dsimp only` rw [h.eval₂_repr_eq_eval₂_of_map_eq hx _ (h.repr z * h.repr w), eval₂_mul] - · rw [map_mul, map_repr, map_repr] + rw [map_mul, map_repr, map_repr] #align is_adjoin_root.lift IsAdjoinRoot.lift variable {i x} @@ -429,7 +429,7 @@ def basis (h : IsAdjoinRootMonic S f) : Basis (Fin (natDegree f)) R S := refine coeff_eq_zero_of_natDegree_lt (lt_of_lt_of_le ?_ hi) dsimp -- Porting note (#11227):added a `dsimp` rw [natDegree_lt_natDegree_iff hx] - · exact degree_modByMonic_lt _ h.Monic + exact degree_modByMonic_lt _ h.Monic right_inv := fun g => by nontriviality R ext i diff --git a/Mathlib/RingTheory/Jacobson.lean b/Mathlib/RingTheory/Jacobson.lean index 6743358c1deeb..ee8bac3d3f343 100644 --- a/Mathlib/RingTheory/Jacobson.lean +++ b/Mathlib/RingTheory/Jacobson.lean @@ -576,8 +576,8 @@ theorem quotient_mk_comp_C_isIntegral_of_jacobson : (fun h => absurd (_root_.trans (h ▸ hPJ : P = comap f ⊤) comap_top : P = ⊤) hP.ne_top) id apply quotient_mk_comp_C_isIntegral_of_jacobson' _ ?_ (fun x hx => ?_) any_goals exact Ideal.isJacobson_quotient - · obtain ⟨z, rfl⟩ := Quotient.mk_surjective x - rwa [Quotient.eq_zero_iff_mem, mem_comap, hPJ, mem_comap, coe_mapRingHom, map_C] + obtain ⟨z, rfl⟩ := Quotient.mk_surjective x + rwa [Quotient.eq_zero_iff_mem, mem_comap, hPJ, mem_comap, coe_mapRingHom, map_C] set_option linter.uppercaseLean3 false in #align ideal.polynomial.quotient_mk_comp_C_is_integral_of_jacobson Ideal.Polynomial.quotient_mk_comp_C_isIntegral_of_jacobson diff --git a/Mathlib/RingTheory/Localization/FractionRing.lean b/Mathlib/RingTheory/Localization/FractionRing.lean index 83b8e46fa66b3..947d0e431352b 100644 --- a/Mathlib/RingTheory/Localization/FractionRing.lean +++ b/Mathlib/RingTheory/Localization/FractionRing.lean @@ -181,17 +181,17 @@ set_option backward.synthInstance.canonInstances false in -- See https://github. theorem mk'_eq_zero_iff_eq_zero [Algebra R K] [IsFractionRing R K] {x : R} {y : nonZeroDivisors R} : mk' K x y = 0 ↔ x = 0 := by refine' ⟨fun hxy => _, fun h => by rw [h, mk'_zero]⟩ - · simp_rw [mk'_eq_zero_iff, mul_left_coe_nonZeroDivisors_eq_zero_iff] at hxy - exact (exists_const _).mp hxy + simp_rw [mk'_eq_zero_iff, mul_left_coe_nonZeroDivisors_eq_zero_iff] at hxy + exact (exists_const _).mp hxy #align is_fraction_ring.mk'_eq_zero_iff_eq_zero IsFractionRing.mk'_eq_zero_iff_eq_zero theorem mk'_eq_one_iff_eq {x : A} {y : nonZeroDivisors A} : mk' K x y = 1 ↔ x = y := by refine' ⟨_, fun hxy => by rw [hxy, mk'_self']⟩ - · intro hxy - have hy : (algebraMap A K) ↑y ≠ (0 : K) := - IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors y.property - rw [IsFractionRing.mk'_eq_div, div_eq_one_iff_eq hy] at hxy - exact IsFractionRing.injective A K hxy + intro hxy + have hy : (algebraMap A K) ↑y ≠ (0 : K) := + IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors y.property + rw [IsFractionRing.mk'_eq_div, div_eq_one_iff_eq hy] at hxy + exact IsFractionRing.injective A K hxy #align is_fraction_ring.mk'_eq_one_iff_eq IsFractionRing.mk'_eq_one_iff_eq open Function diff --git a/Mathlib/RingTheory/MvPowerSeries/Basic.lean b/Mathlib/RingTheory/MvPowerSeries/Basic.lean index e0df81466081f..a9273bf3f3150 100644 --- a/Mathlib/RingTheory/MvPowerSeries/Basic.lean +++ b/Mathlib/RingTheory/MvPowerSeries/Basic.lean @@ -701,17 +701,17 @@ theorem coeff_prod [DecidableEq σ] | @insert a s ha ih => rw [piAntidiagonal_insert ha, prod_insert ha, coeff_mul, sum_biUnion] · apply Finset.sum_congr rfl - · simp only [mem_antidiagonal, sum_map, Function.Embedding.coeFn_mk, coe_update, Prod.forall] - rintro u v rfl - rw [ih, Finset.mul_sum, ← Finset.sum_attach] - apply Finset.sum_congr rfl - simp only [mem_attach, Finset.prod_insert ha, Function.update_same, forall_true_left, - Subtype.forall] - rintro x - - rw [Finset.prod_congr rfl] - intro i hi - rw [Function.update_noteq] - exact ne_of_mem_of_not_mem hi ha + simp only [mem_antidiagonal, sum_map, Function.Embedding.coeFn_mk, coe_update, Prod.forall] + rintro u v rfl + rw [ih, Finset.mul_sum, ← Finset.sum_attach] + apply Finset.sum_congr rfl + simp only [mem_attach, Finset.prod_insert ha, Function.update_same, forall_true_left, + Subtype.forall] + rintro x - + rw [Finset.prod_congr rfl] + intro i hi + rw [Function.update_noteq] + exact ne_of_mem_of_not_mem hi ha · simp only [Set.PairwiseDisjoint, Set.Pairwise, mem_coe, mem_antidiagonal, ne_eq, disjoint_left, mem_map, mem_attach, Function.Embedding.coeFn_mk, true_and, Subtype.exists, exists_prop, not_exists, not_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, diff --git a/Mathlib/RingTheory/Norm.lean b/Mathlib/RingTheory/Norm.lean index ed47c1c034c50..4f08edff993ce 100644 --- a/Mathlib/RingTheory/Norm.lean +++ b/Mathlib/RingTheory/Norm.lean @@ -134,7 +134,7 @@ theorem PowerBasis.norm_gen_eq_prod_roots [Algebra R F] (pb : PowerBasis R S) ← coeff_map, prod_roots_eq_coeff_zero_of_monic_of_split (this.map _) ((splits_id_iff_splits _).2 hf), this.natDegree_map, map_pow, ← mul_assoc, ← mul_pow] - · simp only [map_neg, _root_.map_one, neg_mul, neg_neg, one_pow, one_mul] + simp only [map_neg, _root_.map_one, neg_mul, neg_neg, one_pow, one_mul] #align algebra.power_basis.norm_gen_eq_prod_roots Algebra.PowerBasis.norm_gen_eq_prod_roots end EqProdRoots @@ -385,10 +385,10 @@ theorem norm_norm [Algebra L F] [IsScalarTower K L F] [IsSeparable K F] (x : F) haveI := σ.toRingHom.toAlgebra ∏ π : F →ₐ[L] A, π x = σ (norm L x) by simp_rw [← Finset.univ_sigma_univ, Finset.prod_sigma, this, norm_eq_prod_embeddings] - · intro σ - letI : Algebra L A := σ.toRingHom.toAlgebra - rw [← norm_eq_prod_embeddings L A (_ : F)] - rfl + intro σ + letI : Algebra L A := σ.toRingHom.toAlgebra + rw [← norm_eq_prod_embeddings L A (_ : F)] + rfl · rw [norm_eq_one_of_not_module_finite hKF] by_cases hKL : FiniteDimensional K L · have hLF : ¬FiniteDimensional L F := by diff --git a/Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean b/Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean index 4b719fdf6bb32..66fceb01a9788 100644 --- a/Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean +++ b/Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean @@ -90,8 +90,8 @@ theorem cyclotomic_expand_eq_cyclotomic {p n : ℕ} (hp : Nat.Prime p) (hdiv : p refine' minpoly.isIntegrallyClosed_dvd (hprim.isIntegral hpos) _ rw [aeval_def, ← eval_map, map_expand, map_cyclotomic, expand_eval, ← IsRoot.def, @isRoot_cyclotomic_iff] - · convert IsPrimitiveRoot.pow_of_dvd hprim hp.ne_zero (dvd_mul_left p n) - rw [Nat.mul_div_cancel _ hp.pos] + convert IsPrimitiveRoot.pow_of_dvd hprim hp.ne_zero (dvd_mul_left p n) + rw [Nat.mul_div_cancel _ hp.pos] · rw [natDegree_expand, natDegree_cyclotomic, natDegree_cyclotomic, mul_comm n, Nat.totient_mul_of_prime_of_dvd hp hdiv, mul_comm] #align polynomial.cyclotomic_expand_eq_cyclotomic Polynomial.cyclotomic_expand_eq_cyclotomic diff --git a/Mathlib/RingTheory/Polynomial/Dickson.lean b/Mathlib/RingTheory/Polynomial/Dickson.lean index 4b01e9bf5e91a..91c4d10ce90d0 100644 --- a/Mathlib/RingTheory/Polynomial/Dickson.lean +++ b/Mathlib/RingTheory/Polynomial/Dickson.lean @@ -250,14 +250,14 @@ theorem dickson_one_one_zmod_p (p : ℕ) [Fact p.Prime] : dickson 1 (1 : ZMod p) apply eq_iff_eq_cancel_right.mpr ring -- Finally, we prove the claim that our finite union of finite sets covers all of `K`. - · apply (Set.eq_univ_of_forall _).symm - intro x - simp only [exists_prop, Set.mem_iUnion, Set.bind_def, Ne, Set.mem_setOf_eq] - by_cases hx : x = 0 - · simp only [hx, and_true_iff, eq_self_iff_true, inv_zero, or_true_iff] - exact ⟨_, 1, rfl, one_ne_zero⟩ - · simp only [hx, or_false_iff, exists_eq_right] - exact ⟨_, rfl, hx⟩ + apply (Set.eq_univ_of_forall _).symm + intro x + simp only [exists_prop, Set.mem_iUnion, Set.bind_def, Ne, Set.mem_setOf_eq] + by_cases hx : x = 0 + · simp only [hx, and_true_iff, eq_self_iff_true, inv_zero, or_true_iff] + exact ⟨_, 1, rfl, one_ne_zero⟩ + · simp only [hx, or_false_iff, exists_eq_right] + exact ⟨_, rfl, hx⟩ #align polynomial.dickson_one_one_zmod_p Polynomial.dickson_one_one_zmod_p theorem dickson_one_one_charP (p : ℕ) [Fact p.Prime] [CharP R p] : dickson 1 (1 : R) p = X ^ p := by diff --git a/Mathlib/RingTheory/Polynomial/GaussLemma.lean b/Mathlib/RingTheory/Polynomial/GaussLemma.lean index 924ed66eafa3c..616e4c524b41e 100644 --- a/Mathlib/RingTheory/Polynomial/GaussLemma.lean +++ b/Mathlib/RingTheory/Polynomial/GaussLemma.lean @@ -64,7 +64,7 @@ theorem integralClosure.mem_lifts_of_monic_of_dvd_map {f : R[X]} (hf : f.Monic) obtain ⟨p, hp, he⟩ := SetLike.mem_coe.mp (this n); use p, hp rw [IsScalarTower.algebraMap_eq R K, coeff_map, ← eval₂_map, eval₂_at_apply] at he rw [eval₂_eq_eval_map]; apply (injective_iff_map_eq_zero _).1 _ _ he - · apply RingHom.injective + apply RingHom.injective rw [aroots_def, IsScalarTower.algebraMap_eq R K _, ← map_map] refine' Multiset.mem_of_le (roots.le_of_dvd ((hf.map _).map _).ne_zero _) ha exact map_dvd (algebraMap K g.SplittingField) hd diff --git a/Mathlib/RingTheory/Polynomial/Vieta.lean b/Mathlib/RingTheory/Polynomial/Vieta.lean index c41e6bda67d0d..fd1b94a66bf58 100644 --- a/Mathlib/RingTheory/Polynomial/Vieta.lean +++ b/Mathlib/RingTheory/Polynomial/Vieta.lean @@ -64,9 +64,9 @@ theorem prod_X_add_C_coeff (s : Multiset R) {k : ℕ} (h : k ≤ Multiset.card s · rw [if_pos (Nat.sub_sub_self h).symm] · intro j hj1 hj2 suffices k ≠ card s - j by rw [if_neg this] - · intro hn - rw [hn, Nat.sub_sub_self (Nat.lt_succ_iff.mp (Finset.mem_range.mp hj1))] at hj2 - exact Ne.irrefl hj2 + intro hn + rw [hn, Nat.sub_sub_self (Nat.lt_succ_iff.mp (Finset.mem_range.mp hj1))] at hj2 + exact Ne.irrefl hj2 · rw [Finset.mem_range] exact Nat.lt_succ_of_le (Nat.sub_le (Multiset.card s) k) set_option linter.uppercaseLean3 false in diff --git a/Mathlib/RingTheory/PowerSeries/Order.lean b/Mathlib/RingTheory/PowerSeries/Order.lean index c6590155af6d4..0f438e43fc9cb 100644 --- a/Mathlib/RingTheory/PowerSeries/Order.lean +++ b/Mathlib/RingTheory/PowerSeries/Order.lean @@ -169,15 +169,15 @@ private theorem order_add_of_order_eq.aux (φ ψ : R⟦X⟧) (_h : order φ ≠ suffices order (φ + ψ) = order φ by rw [le_inf_iff, this] exact ⟨le_rfl, le_of_lt H⟩ - · rw [order_eq] - constructor - · intro i hi - rw [← hi] at H - rw [(coeff _ _).map_add, coeff_of_lt_order i H, add_zero] - exact (order_eq_nat.1 hi.symm).1 - · intro i hi - rw [(coeff _ _).map_add, coeff_of_lt_order i hi, coeff_of_lt_order i (lt_trans hi H), - zero_add] + rw [order_eq] + constructor + · intro i hi + rw [← hi] at H + rw [(coeff _ _).map_add, coeff_of_lt_order i H, add_zero] + exact (order_eq_nat.1 hi.symm).1 + · intro i hi + rw [(coeff _ _).map_add, coeff_of_lt_order i hi, coeff_of_lt_order i (lt_trans hi H), + zero_add] -- #align power_series.order_add_of_order_eq.aux power_series.order_add_of_order_eq.aux /-- The order of the sum of two formal power series diff --git a/Mathlib/RingTheory/RootsOfUnity/Basic.lean b/Mathlib/RingTheory/RootsOfUnity/Basic.lean index 2ccfdfc7714a1..d14e46037ad71 100644 --- a/Mathlib/RingTheory/RootsOfUnity/Basic.lean +++ b/Mathlib/RingTheory/RootsOfUnity/Basic.lean @@ -209,9 +209,9 @@ def rootsOfUnityEquivNthRoots : rootsOfUnity k R ≃ { x // x ∈ nthRoots k (1 rcases x with ⟨x, hx⟩; rw [mem_nthRoots k.pos] at hx simp only [Subtype.coe_mk, ← pow_succ, ← pow_succ', hx, tsub_add_cancel_of_le (show 1 ≤ (k : ℕ) from k.one_le)] - · show (_ : Rˣ) ^ (k : ℕ) = 1 - simp only [Units.ext_iff, hx, Units.val_mk, Units.val_one, Subtype.coe_mk, - Units.val_pow_eq_pow_val] + show (_ : Rˣ) ^ (k : ℕ) = 1 + simp only [Units.ext_iff, hx, Units.val_mk, Units.val_one, Subtype.coe_mk, + Units.val_pow_eq_pow_val] #align roots_of_unity_equiv_nth_roots rootsOfUnityEquivNthRoots variable {k R} @@ -670,8 +670,8 @@ theorem neZero' {n : ℕ+} (hζ : IsPrimitiveRoot ζ n) : NeZero ((n : ℕ) : R) rw [h] at H simp at H refine' hζ.pow_ne_one_of_pos_of_lt hpos _ (frobenius_inj R p this) - · rw [hm.1, hk, pow_succ', mul_assoc, mul_comm p] - exact lt_mul_of_one_lt_right hpos hpri.1.one_lt + rw [hm.1, hk, pow_succ', mul_assoc, mul_comm p] + exact lt_mul_of_one_lt_right hpos hpri.1.one_lt · exact NeZero.of_not_dvd R hp #align is_primitive_root.ne_zero' IsPrimitiveRoot.neZero' diff --git a/Mathlib/RingTheory/RootsOfUnity/Minpoly.lean b/Mathlib/RingTheory/RootsOfUnity/Minpoly.lean index f4f9f93f99a9a..ec91b5f0a4682 100644 --- a/Mathlib/RingTheory/RootsOfUnity/Minpoly.lean +++ b/Mathlib/RingTheory/RootsOfUnity/Minpoly.lean @@ -85,9 +85,9 @@ theorem minpoly_dvd_expand {p : ℕ} (hdiv : ¬p ∣ n) : · simp_all letI : IsIntegrallyClosed ℤ := GCDMonoid.toIsIntegrallyClosed refine' minpoly.isIntegrallyClosed_dvd (h.isIntegral hpos) _ - · rw [aeval_def, coe_expand, ← comp, eval₂_eq_eval_map, map_comp, Polynomial.map_pow, map_X, - eval_comp, eval_pow, eval_X, ← eval₂_eq_eval_map, ← aeval_def] - exact minpoly.aeval _ _ + rw [aeval_def, coe_expand, ← comp, eval₂_eq_eval_map, map_comp, Polynomial.map_pow, map_X, + eval_comp, eval_pow, eval_X, ← eval₂_eq_eval_map, ← aeval_def] + exact minpoly.aeval _ _ #align is_primitive_root.minpoly_dvd_expand IsPrimitiveRoot.minpoly_dvd_expand /-- Let `P` be the minimal polynomial of a root of unity `μ` and `Q` be the minimal polynomial of diff --git a/Mathlib/RingTheory/Trace.lean b/Mathlib/RingTheory/Trace.lean index 259a62dedfc8b..b5da69b79ffc9 100644 --- a/Mathlib/RingTheory/Trace.lean +++ b/Mathlib/RingTheory/Trace.lean @@ -595,9 +595,9 @@ theorem det_traceMatrix_ne_zero' [IsSeparable K L] : det (traceMatrix K pb.basis traceMatrix_eq_embeddingsMatrixReindex_mul_trans K _ _ e, embeddingsMatrixReindex_eq_vandermonde, det_mul, det_transpose] refine mt mul_self_eq_zero.mp ?_ - · simp only [det_vandermonde, Finset.prod_eq_zero_iff, not_exists, sub_eq_zero] - rintro i ⟨_, j, hij, h⟩ - exact (Finset.mem_Ioi.mp hij).ne' (e.injective <| pb.algHom_ext h) + simp only [det_vandermonde, Finset.prod_eq_zero_iff, not_exists, sub_eq_zero] + rintro i ⟨_, j, hij, h⟩ + exact (Finset.mem_Ioi.mp hij).ne' (e.injective <| pb.algHom_ext h) · rw [AlgHom.card, pb.finrank] #align det_trace_matrix_ne_zero' det_traceMatrix_ne_zero' diff --git a/Mathlib/RingTheory/UniqueFactorizationDomain.lean b/Mathlib/RingTheory/UniqueFactorizationDomain.lean index e2e231a6b1c7c..aeda256af1d10 100644 --- a/Mathlib/RingTheory/UniqueFactorizationDomain.lean +++ b/Mathlib/RingTheory/UniqueFactorizationDomain.lean @@ -546,12 +546,12 @@ theorem factors_pow {x : α} (n : ℕ) : match n with | 0 => rw [zero_smul, pow_zero, factors_one, Multiset.rel_zero_right] | n+1 => - · by_cases h0 : x = 0 - · simp [h0, zero_pow n.succ_ne_zero, smul_zero] - · rw [pow_succ', succ_nsmul'] - refine' Multiset.Rel.trans _ (factors_mul h0 (pow_ne_zero n h0)) _ - refine' Multiset.Rel.add _ <| factors_pow n - exact Multiset.rel_refl_of_refl_on fun y _ => Associated.refl _ + by_cases h0 : x = 0 + · simp [h0, zero_pow n.succ_ne_zero, smul_zero] + · rw [pow_succ', succ_nsmul'] + refine' Multiset.Rel.trans _ (factors_mul h0 (pow_ne_zero n h0)) _ + refine' Multiset.Rel.add _ <| factors_pow n + exact Multiset.rel_refl_of_refl_on fun y _ => Associated.refl _ #align unique_factorization_monoid.factors_pow UniqueFactorizationMonoid.factors_pow @[simp] diff --git a/Mathlib/RingTheory/Valuation/ValuationSubring.lean b/Mathlib/RingTheory/Valuation/ValuationSubring.lean index 4afb202d0432f..30c888c68e368 100644 --- a/Mathlib/RingTheory/Valuation/ValuationSubring.lean +++ b/Mathlib/RingTheory/Valuation/ValuationSubring.lean @@ -351,13 +351,13 @@ theorem ofPrime_idealOfLE (R S : ValuationSubring K) (h : R ≤ S) : · intro hx; by_cases hr : x ∈ R; · exact R.le_ofPrime _ hr have : x ≠ 0 := fun h => hr (by rw [h]; exact R.zero_mem) replace hr := (R.mem_or_inv_mem x).resolve_left hr - · -- Porting note: added `⟨⟩` brackets and reordered goals - use 1, ⟨x⁻¹, hr⟩; constructor - · field_simp - · change (⟨x⁻¹, h hr⟩ : S) ∉ nonunits S - rw [mem_nonunits_iff, Classical.not_not] - apply isUnit_of_mul_eq_one _ (⟨x, hx⟩ : S) - ext; field_simp + -- Porting note: added `⟨⟩` brackets and reordered goals + use 1, ⟨x⁻¹, hr⟩; constructor + · field_simp + · change (⟨x⁻¹, h hr⟩ : S) ∉ nonunits S + rw [mem_nonunits_iff, Classical.not_not] + apply isUnit_of_mul_eq_one _ (⟨x, hx⟩ : S) + ext; field_simp #align valuation_subring.of_prime_ideal_of_le ValuationSubring.ofPrime_idealOfLE theorem ofPrime_le_of_le (P Q : Ideal A) [P.IsPrime] [Q.IsPrime] (h : P ≤ Q) : diff --git a/Mathlib/SetTheory/Cardinal/Cofinality.lean b/Mathlib/SetTheory/Cardinal/Cofinality.lean index d7bd634f4df9f..3407578580402 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality.lean @@ -202,15 +202,15 @@ theorem ord_cof_eq (r : α → α → Prop) [IsWellOrder α r] : injection e with e subst b exact irrefl _ h - · intro a - have : { b : S | ¬r b a }.Nonempty := - let ⟨b, bS, ba⟩ := hS a - ⟨⟨b, bS⟩, ba⟩ - let b := (IsWellFounded.wf : WellFounded s).min _ this - have ba : ¬r b a := IsWellFounded.wf.min_mem _ this - refine' ⟨b, ⟨b.2, fun c => not_imp_not.1 fun h => _⟩, ba⟩ - rw [show ∀ b : S, (⟨b, b.2⟩ : S) = b by intro b; cases b; rfl] - exact IsWellFounded.wf.not_lt_min _ this (IsOrderConnected.neg_trans h ba) + intro a + have : { b : S | ¬r b a }.Nonempty := + let ⟨b, bS, ba⟩ := hS a + ⟨⟨b, bS⟩, ba⟩ + let b := (IsWellFounded.wf : WellFounded s).min _ this + have ba : ¬r b a := IsWellFounded.wf.min_mem _ this + refine' ⟨b, ⟨b.2, fun c => not_imp_not.1 fun h => _⟩, ba⟩ + rw [show ∀ b : S, (⟨b, b.2⟩ : S) = b by intro b; cases b; rfl] + exact IsWellFounded.wf.not_lt_min _ this (IsOrderConnected.neg_trans h ba) #align ordinal.ord_cof_eq Ordinal.ord_cof_eq /-! ### Cofinality of suprema and least strict upper bounds -/ diff --git a/Mathlib/SetTheory/Surreal/Dyadic.lean b/Mathlib/SetTheory/Surreal/Dyadic.lean index ddb9c9b3ec89a..1202ffeecfa67 100644 --- a/Mathlib/SetTheory/Surreal/Dyadic.lean +++ b/Mathlib/SetTheory/Surreal/Dyadic.lean @@ -122,37 +122,37 @@ theorem zero_le_powHalf (n : ℕ) : 0 ≤ powHalf n := theorem add_powHalf_succ_self_eq_powHalf (n) : powHalf (n + 1) + powHalf (n + 1) ≈ powHalf n := by induction' n using Nat.strong_induction_on with n hn - · constructor <;> rw [le_iff_forall_lf] <;> constructor - · rintro (⟨⟨⟩⟩ | ⟨⟨⟩⟩) <;> apply lf_of_lt - · calc - 0 + powHalf n.succ ≈ powHalf n.succ := zero_add_equiv _ - _ < powHalf n := powHalf_succ_lt_powHalf n - · calc - powHalf n.succ + 0 ≈ powHalf n.succ := add_zero_equiv _ - _ < powHalf n := powHalf_succ_lt_powHalf n - · cases' n with n - · rintro ⟨⟩ - rintro ⟨⟩ - apply lf_of_moveRight_le - swap - · exact Sum.inl default - calc - powHalf n.succ + powHalf (n.succ + 1) ≤ powHalf n.succ + powHalf n.succ := - add_le_add_left (powHalf_succ_le_powHalf _) _ - _ ≈ powHalf n := hn _ (Nat.lt_succ_self n) - · simp only [powHalf_moveLeft, forall_const] - apply lf_of_lt - calc - 0 ≈ 0 + 0 := Equiv.symm (add_zero_equiv 0) - _ ≤ powHalf n.succ + 0 := add_le_add_right (zero_le_powHalf _) _ - _ < powHalf n.succ + powHalf n.succ := add_lt_add_left (powHalf_pos _) _ - · rintro (⟨⟨⟩⟩ | ⟨⟨⟩⟩) <;> apply lf_of_lt - · calc - powHalf n ≈ powHalf n + 0 := Equiv.symm (add_zero_equiv _) - _ < powHalf n + powHalf n.succ := add_lt_add_left (powHalf_pos _) _ - · calc - powHalf n ≈ 0 + powHalf n := Equiv.symm (zero_add_equiv _) - _ < powHalf n.succ + powHalf n := add_lt_add_right (powHalf_pos _) _ + constructor <;> rw [le_iff_forall_lf] <;> constructor + · rintro (⟨⟨⟩⟩ | ⟨⟨⟩⟩) <;> apply lf_of_lt + · calc + 0 + powHalf n.succ ≈ powHalf n.succ := zero_add_equiv _ + _ < powHalf n := powHalf_succ_lt_powHalf n + · calc + powHalf n.succ + 0 ≈ powHalf n.succ := add_zero_equiv _ + _ < powHalf n := powHalf_succ_lt_powHalf n + · cases' n with n + · rintro ⟨⟩ + rintro ⟨⟩ + apply lf_of_moveRight_le + swap + · exact Sum.inl default + calc + powHalf n.succ + powHalf (n.succ + 1) ≤ powHalf n.succ + powHalf n.succ := + add_le_add_left (powHalf_succ_le_powHalf _) _ + _ ≈ powHalf n := hn _ (Nat.lt_succ_self n) + · simp only [powHalf_moveLeft, forall_const] + apply lf_of_lt + calc + 0 ≈ 0 + 0 := Equiv.symm (add_zero_equiv 0) + _ ≤ powHalf n.succ + 0 := add_le_add_right (zero_le_powHalf _) _ + _ < powHalf n.succ + powHalf n.succ := add_lt_add_left (powHalf_pos _) _ + · rintro (⟨⟨⟩⟩ | ⟨⟨⟩⟩) <;> apply lf_of_lt + · calc + powHalf n ≈ powHalf n + 0 := Equiv.symm (add_zero_equiv _) + _ < powHalf n + powHalf n.succ := add_lt_add_left (powHalf_pos _) _ + · calc + powHalf n ≈ 0 + powHalf n := Equiv.symm (zero_add_equiv _) + _ < powHalf n.succ + powHalf n := add_lt_add_right (powHalf_pos _) _ #align pgame.add_pow_half_succ_self_eq_pow_half SetTheory.PGame.add_powHalf_succ_self_eq_powHalf theorem half_add_half_equiv_one : powHalf 1 + powHalf 1 ≈ 1 := diff --git a/Mathlib/Tactic/NormNum/LegendreSymbol.lean b/Mathlib/Tactic/NormNum/LegendreSymbol.lean index abdfa6265f6ff..75bed46f02915 100644 --- a/Mathlib/Tactic/NormNum/LegendreSymbol.lean +++ b/Mathlib/Tactic/NormNum/LegendreSymbol.lean @@ -75,11 +75,11 @@ theorem jacobiSymNat.one_right (a : ℕ) : jacobiSymNat a 1 = 1 := by theorem jacobiSymNat.zero_left (b : ℕ) (hb : Nat.beq (b / 2) 0 = false) : jacobiSymNat 0 b = 0 := by rw [jacobiSymNat, Nat.cast_zero, jacobiSym.zero_left ?_] - · calc - 1 < 2 * 1 := by decide - _ ≤ 2 * (b / 2) := - Nat.mul_le_mul_left _ (Nat.succ_le.mpr (Nat.pos_of_ne_zero (Nat.ne_of_beq_eq_false hb))) - _ ≤ b := Nat.mul_div_le b 2 + calc + 1 < 2 * 1 := by decide + _ ≤ 2 * (b / 2) := + Nat.mul_le_mul_left _ (Nat.succ_le.mpr (Nat.pos_of_ne_zero (Nat.ne_of_beq_eq_false hb))) + _ ≤ b := Nat.mul_div_le b 2 #align norm_num.jacobi_sym_nat.zero_left_even Mathlib.Meta.NormNum.jacobiSymNat.zero_left #align norm_num.jacobi_sym_nat.zero_left_odd Mathlib.Meta.NormNum.jacobiSymNat.zero_left diff --git a/Mathlib/Topology/Algebra/UniformField.lean b/Mathlib/Topology/Algebra/UniformField.lean index f5aa272976780..ef1bf11cfa0da 100644 --- a/Mathlib/Topology/Algebra/UniformField.lean +++ b/Mathlib/Topology/Algebra/UniformField.lean @@ -85,7 +85,7 @@ theorem continuous_hatInv [CompletableTopField K] {x : hat K} (h : x ≠ 0) : apply CompletableTopField.nice · haveI := denseInducing_coe.comap_nhds_neBot y apply cauchy_nhds.comap - · rw [Completion.comap_coe_eq_uniformity] + rw [Completion.comap_coe_eq_uniformity] · have eq_bot : 𝓝 (0 : hat K) ⊓ 𝓝 y = ⊥ := by by_contra h exact y_ne (eq_of_nhds_neBot <| neBot_iff.mpr h).symm diff --git a/Mathlib/Topology/Connected/PathConnected.lean b/Mathlib/Topology/Connected/PathConnected.lean index e675e827a8744..a73b5983a3939 100644 --- a/Mathlib/Topology/Connected/PathConnected.lean +++ b/Mathlib/Topology/Connected/PathConnected.lean @@ -1063,13 +1063,13 @@ theorem IsPathConnected.exists_path_through_family {n : ℕ} clear hp p induction' n with n hn · use Path.refl (p' 0) - · constructor - · rintro i hi - rw [Nat.le_zero.mp hi] - exact ⟨0, rfl⟩ - · rw [range_subset_iff] - rintro _x - exact hp' 0 le_rfl + constructor + · rintro i hi + rw [Nat.le_zero.mp hi] + exact ⟨0, rfl⟩ + · rw [range_subset_iff] + rintro _x + exact hp' 0 le_rfl · rcases hn fun i hi => hp' i <| Nat.le_succ_of_le hi with ⟨γ₀, hγ₀⟩ rcases h.joinedIn (p' n) (hp' n n.le_succ) (p' <| n + 1) (hp' (n + 1) <| le_rfl) with ⟨γ₁, hγ₁⟩ diff --git a/Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean b/Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean index 2167de9c57d7e..7f51009fb08f0 100644 --- a/Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean +++ b/Mathlib/Topology/ContinuousFunction/StoneWeierstrass.lean @@ -284,7 +284,7 @@ theorem subalgebra_topologicalClosure_eq_top_of_separatesPoints (A : Subalgebra (fun f fm g gm => sup_mem_closed_subalgebra L A.isClosed_topologicalClosure ⟨f, fm⟩ ⟨g, gm⟩) (Subalgebra.SeparatesPoints.strongly (Subalgebra.separatesPoints_monotone A.le_topologicalClosure w)) - · simp [L] + simp [L] #align continuous_map.subalgebra_topological_closure_eq_top_of_separates_points ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPoints /-- An alternative statement of the Stone-Weierstrass theorem. diff --git a/Mathlib/Topology/MetricSpace/Completion.lean b/Mathlib/Topology/MetricSpace/Completion.lean index 5bf034fb649e6..e1075799f0897 100644 --- a/Mathlib/Topology/MetricSpace/Completion.lean +++ b/Mathlib/Topology/MetricSpace/Completion.lean @@ -137,9 +137,9 @@ protected theorem mem_uniformity_dist (s : Set (Completion α × Completion α)) Completion.dist_comm, zero_sub, abs_neg, r] at I exact lt_of_le_of_lt (le_abs_self _) I show t1 ⊆ s - · rintro ⟨a, b⟩ hp - have : dist a b < ε := A a b hp - exact hε this + rintro ⟨a, b⟩ hp + have : dist a b < ε := A a b hp + exact hε this #align uniform_space.completion.mem_uniformity_dist UniformSpace.Completion.mem_uniformity_dist /-- Reformulate `Completion.mem_uniformity_dist` in terms that are suitable for the definition diff --git a/Mathlib/Topology/MetricSpace/HausdorffDistance.lean b/Mathlib/Topology/MetricSpace/HausdorffDistance.lean index 9051564b58808..ba01b88c14432 100644 --- a/Mathlib/Topology/MetricSpace/HausdorffDistance.lean +++ b/Mathlib/Topology/MetricSpace/HausdorffDistance.lean @@ -240,9 +240,9 @@ theorem _root_.IsOpen.exists_iUnion_isClosed {U : Set α} (hU : IsOpen U) : simp only [mem_iUnion, mem_Ici, mem_preimage] exact ⟨n, hn.le⟩ show Monotone F - · intro m n hmn x hx - simp only [F, mem_Ici, mem_preimage] at hx ⊢ - apply le_trans (pow_le_pow_right_of_le_one' a_lt_one.le hmn) hx + intro m n hmn x hx + simp only [F, mem_Ici, mem_preimage] at hx ⊢ + apply le_trans (pow_le_pow_right_of_le_one' a_lt_one.le hmn) hx #align is_open.exists_Union_is_closed IsOpen.exists_iUnion_isClosed theorem _root_.IsCompact.exists_infEdist_eq_edist (hs : IsCompact s) (hne : s.Nonempty) (x : α) : diff --git a/Mathlib/Topology/Sheaves/LocalPredicate.lean b/Mathlib/Topology/Sheaves/LocalPredicate.lean index 07d6dea53895d..d3315d58c97fd 100644 --- a/Mathlib/Topology/Sheaves/LocalPredicate.lean +++ b/Mathlib/Topology/Sheaves/LocalPredicate.lean @@ -287,16 +287,16 @@ theorem stalkToFiber_injective (P : LocalPredicate T) (x : X) -- Then use induction to pick particular representatives of `tU tV : stalk x` obtain ⟨U, ⟨fU, hU⟩, rfl⟩ := jointly_surjective'.{v, v} tU obtain ⟨V, ⟨fV, hV⟩, rfl⟩ := jointly_surjective'.{v, v} tV - · -- Decompose everything into its constituent parts: - dsimp - simp only [stalkToFiber, Types.Colimit.ι_desc_apply'] at h - specialize w (unop U) (unop V) fU hU fV hV h - rcases w with ⟨W, iU, iV, w⟩ - -- and put it back together again in the correct order. - refine' ⟨op W, fun w => fU (iU w : (unop U).1), P.res _ _ hU, _⟩ - rcases W with ⟨W, m⟩ - · exact iU - · exact ⟨colimit_sound iU.op (Subtype.eq rfl), colimit_sound iV.op (Subtype.eq (funext w).symm)⟩ + -- Decompose everything into its constituent parts: + dsimp + simp only [stalkToFiber, Types.Colimit.ι_desc_apply'] at h + specialize w (unop U) (unop V) fU hU fV hV h + rcases w with ⟨W, iU, iV, w⟩ + -- and put it back together again in the correct order. + refine' ⟨op W, fun w => fU (iU w : (unop U).1), P.res _ _ hU, _⟩ + · rcases W with ⟨W, m⟩ + exact iU + · exact ⟨colimit_sound iU.op (Subtype.eq rfl), colimit_sound iV.op (Subtype.eq (funext w).symm)⟩ set_option linter.uppercaseLean3 false in #align Top.stalk_to_fiber_injective TopCat.stalkToFiber_injective diff --git a/Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean b/Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean index b821f008417d2..ffee9c0d31744 100644 --- a/Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean +++ b/Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean @@ -374,9 +374,9 @@ def interUnionPullbackConeLift : s.pt ⟶ F.1.obj (op (U ⊔ V)) := by rcases g with ⟨⟩ <;> dsimp [Pairwise.diagram] <;> simp only [Category.id_comp, s.condition, CategoryTheory.Functor.map_id, Category.comp_id] - · rw [← cancel_mono (F.1.map (eqToHom <| inf_comm U V : U ⊓ V ⟶ _).op), Category.assoc, - Category.assoc, ← F.1.map_comp, ← F.1.map_comp] - exact s.condition.symm + rw [← cancel_mono (F.1.map (eqToHom <| inf_comm U V : U ⊓ V ⟶ _).op), Category.assoc, + Category.assoc, ← F.1.map_comp, ← F.1.map_comp] + exact s.condition.symm set_option linter.uppercaseLean3 false in #align Top.sheaf.inter_union_pullback_cone_lift TopCat.Sheaf.interUnionPullbackConeLift diff --git a/Mathlib/Topology/Sheaves/Sheafify.lean b/Mathlib/Topology/Sheaves/Sheafify.lean index 24d82e564ab9b..3f8c00cb0cde4 100644 --- a/Mathlib/Topology/Sheaves/Sheafify.lean +++ b/Mathlib/Topology/Sheaves/Sheafify.lean @@ -91,10 +91,10 @@ theorem stalkToFiber_surjective (x : X) : Function.Surjective (F.stalkToFiber x) apply TopCat.stalkToFiber_surjective intro t obtain ⟨U, m, s, rfl⟩ := F.germ_exist _ t - · use ⟨U, m⟩ - fconstructor - · exact fun y => F.germ y s - · exact ⟨PrelocalPredicate.sheafifyOf ⟨s, fun _ => rfl⟩, rfl⟩ + use ⟨U, m⟩ + fconstructor + · exact fun y => F.germ y s + · exact ⟨PrelocalPredicate.sheafifyOf ⟨s, fun _ => rfl⟩, rfl⟩ #align Top.presheaf.stalk_to_fiber_surjective TopCat.Presheaf.stalkToFiber_surjective theorem stalkToFiber_injective (x : X) : Function.Injective (F.stalkToFiber x) := by diff --git a/Mathlib/Topology/TietzeExtension.lean b/Mathlib/Topology/TietzeExtension.lean index 9d92cfefea8a1..64392a87ca4bd 100644 --- a/Mathlib/Topology/TietzeExtension.lean +++ b/Mathlib/Topology/TietzeExtension.lean @@ -361,20 +361,20 @@ theorem exists_extension_forall_exists_le_ge_of_closedEmbedding [Nonempty X] (f intro x simp [dg0 (Or.inl <| mem_range_self _), ← hgf] refine' ⟨g + dg, fun y => _, funext hgf⟩ - · have hay : a < (g + dg) y := by - rcases (hg_mem y).1.eq_or_lt with (rfl | hlt) - · refine' (lt_add_iff_pos_right _).2 _ - calc - 0 < c - g y := sub_pos.2 hac - _ = dg y := (dga rfl).symm - · exact hlt.trans_le ((le_add_iff_nonneg_right _).2 <| (dgmem y).1) - rcases ha.exists_between hay with ⟨_, ⟨x, rfl⟩, _, hxy⟩ - refine' ⟨x, hxy.le, _⟩ - rcases le_total c (g y) with hc | hc - · simp [dg0 (Or.inr hc), (hg_mem y).2] - · calc - g y + dg y ≤ c + (c - a) := add_le_add hc (dgmem _).2 - _ = b := by rw [hsub, add_sub_cancel] + have hay : a < (g + dg) y := by + rcases (hg_mem y).1.eq_or_lt with (rfl | hlt) + · refine' (lt_add_iff_pos_right _).2 _ + calc + 0 < c - g y := sub_pos.2 hac + _ = dg y := (dga rfl).symm + · exact hlt.trans_le ((le_add_iff_nonneg_right _).2 <| (dgmem y).1) + rcases ha.exists_between hay with ⟨_, ⟨x, rfl⟩, _, hxy⟩ + refine' ⟨x, hxy.le, _⟩ + rcases le_total c (g y) with hc | hc + · simp [dg0 (Or.inr hc), (hg_mem y).2] + · calc + g y + dg y ≤ c + (c - a) := add_le_add hc (dgmem _).2 + _ = b := by rw [hsub, add_sub_cancel] /- Now we deal with the case `∀ x, f x ≠ b`. The proof is the same as in the first case, with minor modifications that make it hard to deduplicate code. -/ choose xl hxl hgb using hg_mem @@ -394,29 +394,29 @@ theorem exists_extension_forall_exists_le_ge_of_closedEmbedding [Nonempty X] (f intro x simp [dg0 (Or.inl <| mem_range_self _), ← hgf] refine' ⟨g - dg, fun y => _, funext hgf⟩ - · have hyb : (g - dg) y < b := by - rcases (hgb y).eq_or_lt with (rfl | hlt) - · refine' (sub_lt_self_iff _).2 _ - calc - 0 < g y - c := sub_pos.2 hcb - _ = dg y := (dgb rfl).symm - · exact ((sub_le_self_iff _).2 (dgmem _).1).trans_lt hlt - rcases hb.exists_between hyb with ⟨_, ⟨xu, rfl⟩, hyxu, _⟩ - cases' lt_or_le c (g y) with hc hc - · rcases em (a ∈ range f) with (⟨x, rfl⟩ | _) - · refine' ⟨x, xu, _, hyxu.le⟩ + have hyb : (g - dg) y < b := by + rcases (hgb y).eq_or_lt with (rfl | hlt) + · refine' (sub_lt_self_iff _).2 _ + calc + 0 < g y - c := sub_pos.2 hcb + _ = dg y := (dgb rfl).symm + · exact ((sub_le_self_iff _).2 (dgmem _).1).trans_lt hlt + rcases hb.exists_between hyb with ⟨_, ⟨xu, rfl⟩, hyxu, _⟩ + cases' lt_or_le c (g y) with hc hc + · rcases em (a ∈ range f) with (⟨x, rfl⟩ | _) + · refine' ⟨x, xu, _, hyxu.le⟩ + calc + f x = c - (b - c) := by rw [← hsub, sub_sub_cancel] + _ ≤ g y - dg y := sub_le_sub hc.le (dgmem _).2 + · have hay : a < (g - dg) y := by calc - f x = c - (b - c) := by rw [← hsub, sub_sub_cancel] - _ ≤ g y - dg y := sub_le_sub hc.le (dgmem _).2 - · have hay : a < (g - dg) y := by - calc - a = c - (b - c) := by rw [← hsub, sub_sub_cancel] - _ < g y - (b - c) := sub_lt_sub_right hc _ - _ ≤ g y - dg y := sub_le_sub_left (dgmem _).2 _ - rcases ha.exists_between hay with ⟨_, ⟨x, rfl⟩, _, hxy⟩ - exact ⟨x, xu, hxy.le, hyxu.le⟩ - · refine' ⟨xl y, xu, _, hyxu.le⟩ - simp [dg0 (Or.inr hc), hxl] + a = c - (b - c) := by rw [← hsub, sub_sub_cancel] + _ < g y - (b - c) := sub_lt_sub_right hc _ + _ ≤ g y - dg y := sub_le_sub_left (dgmem _).2 _ + rcases ha.exists_between hay with ⟨_, ⟨x, rfl⟩, _, hxy⟩ + exact ⟨x, xu, hxy.le, hyxu.le⟩ + · refine' ⟨xl y, xu, _, hyxu.le⟩ + simp [dg0 (Or.inr hc), hxl] #align bounded_continuous_function.exists_extension_forall_exists_le_ge_of_closed_embedding BoundedContinuousFunction.exists_extension_forall_exists_le_ge_of_closedEmbedding /-- **Tietze extension theorem** for real-valued bounded continuous maps, a version for a closed