From e194c75699f5107c3020dd83bb1dc00cf62f62aa Mon Sep 17 00:00:00 2001 From: negiizhao Date: Wed, 15 Nov 2023 21:24:58 +0000 Subject: [PATCH] perf(FunLike.Basic): beta reduce `CoeFun.coe` (#7905) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This eliminates `(fun a ↦ β) α` in the type when applying a `FunLike`. Co-authored-by: Matthew Ballard Co-authored-by: Eric Wieser --- Archive/Sensitivity.lean | 1 - Mathlib/Algebra/Algebra/RestrictScalars.lean | 4 ++-- Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean | 8 ++++---- Mathlib/Algebra/DirectLimit.lean | 5 +---- Mathlib/Algebra/Group/Hom/Defs.lean | 2 +- Mathlib/Algebra/Homology/ModuleCat.lean | 3 +-- Mathlib/Algebra/Module/Torsion.lean | 2 +- Mathlib/Algebra/Order/Monoid/ToMulBot.lean | 2 +- Mathlib/Algebra/Polynomial/BigOperators.lean | 5 +++-- Mathlib/Algebra/Quaternion.lean | 2 +- Mathlib/Algebra/Ring/BooleanRing.lean | 2 +- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean | 4 ++-- Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean | 2 +- Mathlib/AlgebraicGeometry/Scheme.lean | 2 +- Mathlib/AlgebraicGeometry/Spec.lean | 4 ++-- Mathlib/AlgebraicGeometry/StructureSheaf.lean | 2 +- Mathlib/Analysis/Calculus/AffineMap.lean | 1 - Mathlib/Analysis/Convex/Between.lean | 1 - Mathlib/Analysis/Fourier/AddCircle.lean | 1 - Mathlib/Analysis/Fourier/FourierTransform.lean | 4 +--- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean | 1 - Mathlib/CategoryTheory/Limits/Opposites.lean | 4 ++-- Mathlib/CategoryTheory/SingleObj.lean | 2 +- Mathlib/Data/Finset/Image.lean | 2 +- Mathlib/Data/Finsupp/Basic.lean | 2 +- Mathlib/Data/Finsupp/Defs.lean | 2 +- Mathlib/Data/Finsupp/Pointwise.lean | 2 +- Mathlib/Data/FunLike/Basic.lean | 3 ++- Mathlib/Data/IsROrC/Basic.lean | 4 ++-- Mathlib/Data/MvPolynomial/Basic.lean | 2 +- Mathlib/Data/Nat/Factorization/Basic.lean | 2 +- Mathlib/Data/Polynomial/RingDivision.lean | 2 +- Mathlib/Data/ZMod/Basic.lean | 2 +- Mathlib/FieldTheory/Fixed.lean | 1 - Mathlib/FieldTheory/IntermediateField.lean | 4 +--- Mathlib/FieldTheory/Laurent.lean | 3 +-- Mathlib/FieldTheory/Minpoly/Basic.lean | 8 +++----- Mathlib/FieldTheory/RatFunc.lean | 4 +--- .../RingedSpace/LocallyRingedSpace/HasColimits.lean | 2 +- Mathlib/Geometry/RingedSpace/Stalks.lean | 2 +- Mathlib/GroupTheory/FreeGroup/Basic.lean | 2 +- Mathlib/GroupTheory/Perm/Cycle/Basic.lean | 2 -- Mathlib/GroupTheory/SpecificGroups/Alternating.lean | 3 +-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean | 4 ++-- Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean | 2 +- Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean | 3 +-- Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean | 2 +- Mathlib/LinearAlgebra/StdBasis.lean | 1 - Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean | 4 ++-- Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean | 6 +++--- Mathlib/Logic/Equiv/Set.lean | 2 +- Mathlib/Logic/Equiv/TransferInstance.lean | 5 +---- Mathlib/MeasureTheory/Function/UniformIntegrable.lean | 4 ++-- Mathlib/MeasureTheory/Integral/SetToL1.lean | 8 -------- Mathlib/NumberTheory/ArithmeticFunction.lean | 4 +--- Mathlib/NumberTheory/ClassNumber/Finite.lean | 10 +--------- Mathlib/NumberTheory/FunctionField.lean | 2 +- Mathlib/NumberTheory/NumberField/Units.lean | 7 ++++--- Mathlib/Order/WithBot.lean | 4 +--- Mathlib/Probability/ProbabilityMassFunction/Monad.lean | 2 +- Mathlib/RingTheory/AdjoinRoot.lean | 2 +- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean | 4 ++-- Mathlib/RingTheory/EisensteinCriterion.lean | 4 +--- Mathlib/RingTheory/FractionalIdeal.lean | 2 +- Mathlib/RingTheory/HahnSeries.lean | 2 +- Mathlib/RingTheory/IsTensorProduct.lean | 4 +--- Mathlib/RingTheory/LaurentSeries.lean | 2 +- Mathlib/RingTheory/Localization/Basic.lean | 4 ++-- Mathlib/RingTheory/Localization/FractionRing.lean | 2 +- Mathlib/RingTheory/Localization/Integral.lean | 8 +++----- Mathlib/RingTheory/Perfection.lean | 10 +++++----- Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean | 2 +- Mathlib/RingTheory/RingHom/Surjective.lean | 2 +- Mathlib/RingTheory/RootsOfUnity/Basic.lean | 1 - Mathlib/RingTheory/Trace.lean | 4 +--- Mathlib/RingTheory/WittVector/Frobenius.lean | 5 ++--- .../RingTheory/WittVector/FrobeniusFractionField.lean | 2 +- Mathlib/RingTheory/WittVector/Identities.lean | 2 -- Mathlib/RingTheory/WittVector/MulCoeff.lean | 4 ++-- Mathlib/RingTheory/WittVector/StructurePolynomial.lean | 1 - Mathlib/SetTheory/Ordinal/Basic.lean | 4 ++-- Mathlib/Topology/Category/Profinite/Nobeling.lean | 2 +- Mathlib/Topology/Category/TopCat/Limits/Products.lean | 2 +- Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean | 2 +- Mathlib/Topology/Gluing.lean | 1 - Mathlib/Topology/Sheaves/Stalks.lean | 3 +-- test/FunLike.lean | 6 ++++++ 87 files changed, 111 insertions(+), 164 deletions(-) create mode 100644 test/FunLike.lean diff --git a/Archive/Sensitivity.lean b/Archive/Sensitivity.lean index 930668edaeaec..92320d5089a0e 100644 --- a/Archive/Sensitivity.lean +++ b/Archive/Sensitivity.lean @@ -455,7 +455,6 @@ theorem huang_degree_theorem (H : Set (Q m.succ)) (hH : Card H ≥ 2 ^ m + 1) : |(coeffs y).sum fun (i : Q m.succ) (a : ℝ) => a • (ε q ∘ f m.succ ∘ fun i : Q m.succ => e i) i| := by erw [(f m.succ).map_finsupp_total, (ε q).map_finsupp_total, Finsupp.total_apply] - rfl _ ≤ ∑ p in (coeffs y).support, |coeffs y p * (ε q <| f m.succ <| e p)| := (norm_sum_le _ fun p => coeffs y p * _) _ = ∑ p in (coeffs y).support, |coeffs y p| * ite (p ∈ q.adjacent) 1 0 := by diff --git a/Mathlib/Algebra/Algebra/RestrictScalars.lean b/Mathlib/Algebra/Algebra/RestrictScalars.lean index 319b36613aed2..0716caba53603 100644 --- a/Mathlib/Algebra/Algebra/RestrictScalars.lean +++ b/Mathlib/Algebra/Algebra/RestrictScalars.lean @@ -217,8 +217,8 @@ theorem RestrictScalars.ringEquiv_map_smul (r : R) (x : RestrictScalars R S A) : instance RestrictScalars.algebra : Algebra R (RestrictScalars R S A) := { (algebraMap S A).comp (algebraMap R S) with smul := (· • ·) - commutes' := fun _ _ ↦ Algebra.commutes' _ _ - smul_def' := fun _ _ ↦ Algebra.smul_def' _ _ } + commutes' := fun _ _ ↦ Algebra.commutes' (A := A) _ _ + smul_def' := fun _ _ ↦ Algebra.smul_def' (A := A) _ _ } @[simp] theorem RestrictScalars.ringEquiv_algebraMap (r : R) : diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean index a02aa37dea621..ef9cff13dd432 100644 --- a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean +++ b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean @@ -333,8 +333,8 @@ instance mulAction : MulAction S <| (restrictScalars f).obj ⟨S⟩ →ₗ[R] M instance distribMulAction : DistribMulAction S <| (restrictScalars f).obj ⟨S⟩ →ₗ[R] M := { CoextendScalars.mulAction f _ with - smul_add := fun s g h => LinearMap.ext fun t : S => by simp - smul_zero := fun s => LinearMap.ext fun t : S => by simp } + smul_add := fun s g h => LinearMap.ext fun _ : S => by simp + smul_zero := fun s => LinearMap.ext fun _ : S => by simp } #align category_theory.Module.coextend_scalars.distrib_mul_action ModuleCat.CoextendScalars.distribMulAction /-- `S` acts on Hom(S, M) by `s • g = x ↦ g (x • s)`, this action defines an `S`-module structure on @@ -586,8 +586,7 @@ def HomEquiv.toRestrictScalars {X Y} (g : (extendScalars f).obj X ⟶ Y) : letI : Module R S := Module.compHom S f letI : Module R Y := Module.compHom Y f dsimp - rw [RestrictScalars.smul_def, ← LinearMap.map_smul] - erw [tmul_smul] + erw [RestrictScalars.smul_def, ← LinearMap.map_smul, tmul_smul] congr #align category_theory.Module.extend_restrict_scalars_adj.hom_equiv.to_restrict_scalars ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars @@ -658,6 +657,7 @@ def homEquiv {X Y} : change S at x dsimp erw [← LinearMap.map_smul, ExtendScalars.smul_tmul, mul_one x] + rfl · rw [map_add, map_add, ih1, ih2] right_inv g := by letI m1 : Module R S := Module.compHom S f; letI m2 : Module R Y := Module.compHom Y f diff --git a/Mathlib/Algebra/DirectLimit.lean b/Mathlib/Algebra/DirectLimit.lean index 6e62ea3518c24..9e3d45e2c64a8 100644 --- a/Mathlib/Algebra/DirectLimit.lean +++ b/Mathlib/Algebra/DirectLimit.lean @@ -501,7 +501,6 @@ theorem of.zero_exact_aux2 {x : FreeCommRing (Σi, G i)} {s t} (hxs : IsSupporte dsimp only -- porting note: Lean 3 could get away with far fewer hints for inputs in the line below have := DirectedSystem.map_map (fun i j h => f' i j h) (hj p hps) hjk - dsimp only at this rw [this] · rintro x y ihx ihy rw [(restriction _).map_add, (FreeCommRing.lift _).map_add, (f' j k hjk).map_add, ihx, ihy, @@ -529,7 +528,6 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : FreeCom restriction_of, dif_pos, lift_of, lift_of] dsimp only have := DirectedSystem.map_map (fun i j h => f' i j h) hij (le_refl j : j ≤ j) - dsimp only at this rw [this] exact sub_self _ exacts [Or.inr rfl, Or.inl rfl] @@ -539,8 +537,7 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : FreeCom -- porting note: the Lean3 proof contained `rw [restriction_of]`, but this -- lemma does not seem to work here · rw [RingHom.map_sub, RingHom.map_sub] - erw [lift_of, dif_pos rfl, RingHom.map_one, RingHom.map_one, lift_of, - RingHom.map_one, sub_self] + erw [lift_of, dif_pos rfl, RingHom.map_one, lift_of, RingHom.map_one, sub_self] · refine' ⟨i, {⟨i, x + y⟩, ⟨i, x⟩, ⟨i, y⟩}, _, isSupported_sub (isSupported_of.2 <| Or.inl rfl) diff --git a/Mathlib/Algebra/Group/Hom/Defs.lean b/Mathlib/Algebra/Group/Hom/Defs.lean index ead6d79ac594c..f8a707bc23a78 100644 --- a/Mathlib/Algebra/Group/Hom/Defs.lean +++ b/Mathlib/Algebra/Group/Hom/Defs.lean @@ -443,7 +443,7 @@ theorem map_pow [Monoid G] [Monoid H] [MonoidHomClass F G H] (f : F) (a : G) : theorem map_zpow' [DivInvMonoid G] [DivInvMonoid H] [MonoidHomClass F G H] (f : F) (hf : ∀ x : G, f x⁻¹ = (f x)⁻¹) (a : G) : ∀ n : ℤ, f (a ^ n) = f a ^ n | (n : ℕ) => by rw [zpow_ofNat, map_pow, zpow_ofNat] - | Int.negSucc n => by rw [zpow_negSucc, hf, map_pow, ← zpow_negSucc, ← zpow_negSucc] + | Int.negSucc n => by rw [zpow_negSucc, hf, map_pow, ← zpow_negSucc] #align map_zpow' map_zpow' #align map_zsmul' map_zsmul' diff --git a/Mathlib/Algebra/Homology/ModuleCat.lean b/Mathlib/Algebra/Homology/ModuleCat.lean index 535724074f5e6..57f3a47153e6a 100644 --- a/Mathlib/Algebra/Homology/ModuleCat.lean +++ b/Mathlib/Algebra/Homology/ModuleCat.lean @@ -120,9 +120,8 @@ example (f g : C ⟶ D) (h : Homotopy f g) (i : ι) : erw [LinearMap.add_apply] rw [LinearMap.add_apply, prevD_eq_toPrev_dTo, dNext_eq_dFrom_fromNext] -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [comp_apply, comp_apply, comp_apply] + erw [comp_apply, comp_apply] erw [x.2, map_zero] - dsimp abel end ModuleCat diff --git a/Mathlib/Algebra/Module/Torsion.lean b/Mathlib/Algebra/Module/Torsion.lean index 3432afba97cfe..d9222cfde4e50 100644 --- a/Mathlib/Algebra/Module/Torsion.lean +++ b/Mathlib/Algebra/Module/Torsion.lean @@ -375,7 +375,7 @@ variable (R M) theorem torsion_gc : @GaloisConnection (Submodule R M) (Ideal R)ᵒᵈ _ _ annihilator fun I => - torsionBySet R M <| OrderDual.ofDual I := + torsionBySet R M ↑(OrderDual.ofDual I) := fun _ _ => ⟨fun h x hx => (mem_torsionBySet_iff _ _).mpr fun ⟨_, ha⟩ => mem_annihilator.mp (h ha) x hx, fun h a ha => mem_annihilator.mpr fun _ hx => (mem_torsionBySet_iff _ _).mp (h hx) ⟨a, ha⟩⟩ diff --git a/Mathlib/Algebra/Order/Monoid/ToMulBot.lean b/Mathlib/Algebra/Order/Monoid/ToMulBot.lean index 93958eb969df3..ef10b84da2190 100644 --- a/Mathlib/Algebra/Order/Monoid/ToMulBot.lean +++ b/Mathlib/Algebra/Order/Monoid/ToMulBot.lean @@ -36,7 +36,7 @@ theorem toMulBot_zero : toMulBot (0 : WithZero (Multiplicative α)) = Multiplica @[simp] theorem toMulBot_coe (x : Multiplicative α) : - toMulBot ↑x = Multiplicative.ofAdd (Multiplicative.toAdd x : WithBot α) := + toMulBot ↑x = Multiplicative.ofAdd (↑(Multiplicative.toAdd x) : WithBot α) := rfl #align with_zero.to_mul_bot_coe WithZero.toMulBot_coe diff --git a/Mathlib/Algebra/Polynomial/BigOperators.lean b/Mathlib/Algebra/Polynomial/BigOperators.lean index 08d773e83609f..253fa061b07c3 100644 --- a/Mathlib/Algebra/Polynomial/BigOperators.lean +++ b/Mathlib/Algebra/Polynomial/BigOperators.lean @@ -267,9 +267,10 @@ theorem multiset_prod_X_sub_C_coeff_card_pred (t : Multiset R) (ht : 0 < Multise nontriviality R convert multiset_prod_X_sub_C_nextCoeff (by assumption) rw [nextCoeff]; split_ifs with h - · rw [natDegree_multiset_prod_of_monic] at h <;> simp only [Multiset.mem_map] at * + · rw [natDegree_multiset_prod_of_monic] at h swap - · rintro _ ⟨_, _, rfl⟩ + · simp only [Multiset.mem_map] + rintro _ ⟨_, _, rfl⟩ apply monic_X_sub_C simp_rw [Multiset.sum_eq_zero_iff, Multiset.mem_map] at h contrapose! h diff --git a/Mathlib/Algebra/Quaternion.lean b/Mathlib/Algebra/Quaternion.lean index daa8a18366909..eee60e3e10169 100644 --- a/Mathlib/Algebra/Quaternion.lean +++ b/Mathlib/Algebra/Quaternion.lean @@ -1267,7 +1267,7 @@ theorem im_sq : a.im ^ 2 = -normSq a.im := by simp_rw [sq, ← star_mul_self, im_star, neg_mul, neg_neg] #align quaternion.im_sq Quaternion.im_sq -theorem coe_normSq_add : (normSq (a + b) : ℍ[R]) = normSq a + a * star b + b * star a + normSq b := +theorem coe_normSq_add : normSq (a + b) = normSq a + a * star b + b * star a + normSq b := by simp only [star_add, ← self_mul_star, mul_add, add_mul, add_assoc, add_left_comm] #align quaternion.coe_norm_sq_add Quaternion.coe_normSq_add diff --git a/Mathlib/Algebra/Ring/BooleanRing.lean b/Mathlib/Algebra/Ring/BooleanRing.lean index a512af109e2dd..bf44a5c95fc12 100644 --- a/Mathlib/Algebra/Ring/BooleanRing.lean +++ b/Mathlib/Algebra/Ring/BooleanRing.lean @@ -342,7 +342,7 @@ theorem toBoolAlg_add_add_mul (a b : α) : toBoolAlg (a + b + a * b) = toBoolAlg @[simp] theorem toBoolAlg_add (a b : α) : toBoolAlg (a + b) = toBoolAlg a ∆ toBoolAlg b := - (ofBoolAlg_symmDiff _ _).symm + (ofBoolAlg_symmDiff a b).symm #align to_boolalg_add toBoolAlg_add /-- Turn a ring homomorphism from Boolean rings `α` to `β` into a bounded lattice homomorphism diff --git a/Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean b/Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean index f1bdee1037b7d..6f3e24b709846 100644 --- a/Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean +++ b/Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean @@ -304,10 +304,10 @@ def identityToΓSpec : 𝟭 LocallyRingedSpace.{u} ⟶ Γ.rightOp ⋙ Spec.toLoc -- The next six lines were `rw [ContinuousMap.coe_mk, ContinuousMap.coe_mk]` before -- leanprover/lean4#2644 have : (ContinuousMap.mk (toΓSpecFun Y) (toΓSpec_continuous _)) (f.val.base x) - = toΓSpecFun Y (f.val.base x) := by erw [ContinuousMap.coe_mk]; rfl + = toΓSpecFun Y (f.val.base x) := by rw [ContinuousMap.coe_mk] erw [this] have : (ContinuousMap.mk (toΓSpecFun X) (toΓSpec_continuous _)) x - = toΓSpecFun X x := by erw [ContinuousMap.coe_mk] + = toΓSpecFun X x := by rw [ContinuousMap.coe_mk] erw [this] dsimp [toΓSpecFun] -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 diff --git a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean b/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean index 2b5075ed6adc2..3b932ca68adfc 100644 --- a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean +++ b/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean @@ -485,7 +485,7 @@ theorem vanishingIdeal_strict_anti_mono_iff {s t : Set (PrimeSpectrum R)} (hs : /-- The antitone order embedding of closed subsets of `Spec R` into ideals of `R`. -/ def closedsEmbedding (R : Type*) [CommRing R] : (TopologicalSpace.Closeds <| PrimeSpectrum R)ᵒᵈ ↪o Ideal R := - OrderEmbedding.ofMapLEIff (fun s => vanishingIdeal <| OrderDual.ofDual s) fun s _ => + OrderEmbedding.ofMapLEIff (fun s => vanishingIdeal ↑(OrderDual.ofDual s)) fun s _ => (vanishingIdeal_anti_mono_iff s.2).symm #align prime_spectrum.closeds_embedding PrimeSpectrum.closedsEmbedding diff --git a/Mathlib/AlgebraicGeometry/Scheme.lean b/Mathlib/AlgebraicGeometry/Scheme.lean index 0ef5e9f03138f..47d718eb557f2 100644 --- a/Mathlib/AlgebraicGeometry/Scheme.lean +++ b/Mathlib/AlgebraicGeometry/Scheme.lean @@ -342,7 +342,7 @@ lemma basicOpen_restrict (i : V ⟶ U) (f : X.presheaf.obj (op U)) : theorem preimage_basicOpen {X Y : Scheme} (f : X ⟶ Y) {U : Opens Y.carrier} (r : Y.presheaf.obj <| op U) : (Opens.map f.1.base).obj (Y.basicOpen r) = - @Scheme.basicOpen X ((Opens.map f.1.base).obj U) (f.1.c.app _ r) := + @Scheme.basicOpen X ((Opens.map f.1.base).obj U) (f.1.c.app (op U) r) := LocallyRingedSpace.preimage_basicOpen f r #align algebraic_geometry.Scheme.preimage_basic_open AlgebraicGeometry.Scheme.preimage_basicOpen diff --git a/Mathlib/AlgebraicGeometry/Spec.lean b/Mathlib/AlgebraicGeometry/Spec.lean index 6fc6adc4eb10c..7bc32cebef6a3 100644 --- a/Mathlib/AlgebraicGeometry/Spec.lean +++ b/Mathlib/AlgebraicGeometry/Spec.lean @@ -262,9 +262,9 @@ def Spec.locallyRingedSpaceMap {R S : CommRingCat} (f : R ⟶ S) : replace ha := (stalkIso S p).hom.isUnit_map ha rw [← comp_apply, show localizationToStalk S p = (stalkIso S p).inv from rfl, Iso.inv_hom_id, id_apply] at ha - -- Porting note : `R` had to be made explicit + -- Porting note : `f` had to be made explicit replace ha := IsLocalRingHom.map_nonunit - (R := Localization.AtPrime (PrimeSpectrum.comap f p).asIdeal) _ ha + (f := (Localization.localRingHom (PrimeSpectrum.comap f p).asIdeal p.asIdeal f _)) _ ha convert RingHom.isUnit_map (stalkIso R (PrimeSpectrum.comap f p)).inv ha erw [← comp_apply, show stalkToFiberRingHom R _ = (stalkIso _ _).hom from rfl, Iso.hom_inv_id, id_apply] diff --git a/Mathlib/AlgebraicGeometry/StructureSheaf.lean b/Mathlib/AlgebraicGeometry/StructureSheaf.lean index 1bd1cc7cbc6ff..9008f330c6e69 100644 --- a/Mathlib/AlgebraicGeometry/StructureSheaf.lean +++ b/Mathlib/AlgebraicGeometry/StructureSheaf.lean @@ -483,7 +483,7 @@ def localizationToStalk (x : PrimeSpectrum.Top R) : @[simp] theorem localizationToStalk_of (x : PrimeSpectrum.Top R) (f : R) : localizationToStalk R x (algebraMap _ (Localization _) f) = toStalk R x f := - IsLocalization.lift_eq _ f + IsLocalization.lift_eq (S := Localization x.asIdeal.primeCompl) _ f #align algebraic_geometry.structure_sheaf.localization_to_stalk_of AlgebraicGeometry.StructureSheaf.localizationToStalk_of @[simp] diff --git a/Mathlib/Analysis/Calculus/AffineMap.lean b/Mathlib/Analysis/Calculus/AffineMap.lean index 1f5a99580c503..8aeb4c073a7a7 100644 --- a/Mathlib/Analysis/Calculus/AffineMap.lean +++ b/Mathlib/Analysis/Calculus/AffineMap.lean @@ -32,7 +32,6 @@ variable [NormedAddCommGroup W] [NormedSpace 𝕜 W] theorem contDiff {n : ℕ∞} (f : V →A[𝕜] W) : ContDiff 𝕜 n f := by rw [f.decomp] apply f.contLinear.contDiff.add - simp only exact contDiff_const #align continuous_affine_map.cont_diff ContinuousAffineMap.contDiff diff --git a/Mathlib/Analysis/Convex/Between.lean b/Mathlib/Analysis/Convex/Between.lean index f270d72ef9f47..0d580c813e0d9 100644 --- a/Mathlib/Analysis/Convex/Between.lean +++ b/Mathlib/Analysis/Convex/Between.lean @@ -538,7 +538,6 @@ theorem Sbtw.affineCombination_of_mem_affineSpan_pair [NoZeroDivisors R] [NoZero rw [hr i his, sbtw_mul_sub_add_iff] at hs change ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i at hr rw [s.affineCombination_congr hr fun _ _ => rfl] - dsimp only rw [← s.weightedVSub_vadd_affineCombination, s.weightedVSub_const_smul, ← s.affineCombination_vsub, ← lineMap_apply, sbtw_lineMap_iff, and_iff_left hs.2, ← @vsub_ne_zero V, s.affineCombination_vsub] diff --git a/Mathlib/Analysis/Fourier/AddCircle.lean b/Mathlib/Analysis/Fourier/AddCircle.lean index dca9a506db54e..871f57d1dbe6f 100644 --- a/Mathlib/Analysis/Fourier/AddCircle.lean +++ b/Mathlib/Analysis/Fourier/AddCircle.lean @@ -570,7 +570,6 @@ theorem fourierCoeffOn_of_hasDerivAt {a b : ℝ} (hab : a < b) {f f' : ℝ → conv => pattern (occs := 1 2 3) fourier _ _ * _ <;> (rw [mul_comm]) rw [integral_mul_deriv_eq_deriv_mul hf (fun x _ => has_antideriv_at_fourier_neg hT hn x) hf' (((map_continuous (fourier (-n))).comp (AddCircle.continuous_mk' _)).intervalIntegrable _ _)] - dsimp only have : ∀ u v w : ℂ, u * ((b - a : ℝ) / v * w) = (b - a : ℝ) / v * (u * w) := by intros; ring conv in intervalIntegral _ _ _ _ => congr; ext; rw [this] rw [(by ring : ((b - a : ℝ) : ℂ) / (-2 * π * I * n) = ((b - a : ℝ) : ℂ) * (1 / (-2 * π * I * n)))] diff --git a/Mathlib/Analysis/Fourier/FourierTransform.lean b/Mathlib/Analysis/Fourier/FourierTransform.lean index 6e4081af54f08..e4e88fe2276a6 100644 --- a/Mathlib/Analysis/Fourier/FourierTransform.lean +++ b/Mathlib/Analysis/Fourier/FourierTransform.lean @@ -104,9 +104,7 @@ theorem fourierIntegral_comp_add_right [MeasurableAdd V] (e : Multiplicative ext1 w dsimp only [fourierIntegral, Function.comp_apply] conv in L _ => rw [← add_sub_cancel v v₀] - rw [integral_add_right_eq_self fun v : V => e[-L (v - v₀) w] • f v] - dsimp only - rw [← integral_smul] + rw [integral_add_right_eq_self fun v : V => e[-L (v - v₀) w] • f v, ← integral_smul] congr 1 with v rw [← smul_assoc, smul_eq_mul, ← Submonoid.coe_mul, ← e.map_mul, ← ofAdd_add, ← LinearMap.neg_apply, ← sub_eq_add_neg, ← LinearMap.sub_apply, LinearMap.map_sub, neg_sub] diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean index 7765861455b10..3aa499402cf54 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean @@ -141,7 +141,6 @@ theorem arg_mem_Ioc (z : ℂ) : arg z ∈ Set.Ioc (-π) π := by rcases existsUnique_add_zsmul_mem_Ioc Real.two_pi_pos (arg z) (-π) with ⟨N, hN, -⟩ rw [two_mul, neg_add_cancel_left, ← two_mul, zsmul_eq_mul] at hN rw [← abs_mul_cos_add_sin_mul_I z, ← cos_add_int_mul_two_pi _ N, ← sin_add_int_mul_two_pi _ N] - simp only [← ofReal_one, ← ofReal_bit0, ← ofReal_mul, ← ofReal_add, ofReal_int_cast] have := arg_mul_cos_add_sin_mul_I (abs.pos hz) hN push_cast at this rwa [this] diff --git a/Mathlib/CategoryTheory/Limits/Opposites.lean b/Mathlib/CategoryTheory/Limits/Opposites.lean index c97249fc88558..b147588969f4c 100644 --- a/Mathlib/CategoryTheory/Limits/Opposites.lean +++ b/Mathlib/CategoryTheory/Limits/Opposites.lean @@ -790,14 +790,14 @@ noncomputable def pullbackIsoUnopPushout {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) theorem pullbackIsoUnopPushout_inv_fst {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasPushout f.op g.op] : (pullbackIsoUnopPushout f g).inv ≫ pullback.fst = (pushout.inl : _ ⟶ pushout f.op g.op).unop := - (IsLimit.conePointUniqueUpToIso_inv_comp _ _ _).trans (by simp) + (IsLimit.conePointUniqueUpToIso_inv_comp _ _ _).trans (by simp [unop_id (X := { unop := X })]) #align category_theory.limits.pullback_iso_unop_pushout_inv_fst CategoryTheory.Limits.pullbackIsoUnopPushout_inv_fst @[reassoc (attr := simp)] theorem pullbackIsoUnopPushout_inv_snd {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasPushout f.op g.op] : (pullbackIsoUnopPushout f g).inv ≫ pullback.snd = (pushout.inr : _ ⟶ pushout f.op g.op).unop := - (IsLimit.conePointUniqueUpToIso_inv_comp _ _ _).trans (by simp) + (IsLimit.conePointUniqueUpToIso_inv_comp _ _ _).trans (by simp [unop_id (X := { unop := Y })]) #align category_theory.limits.pullback_iso_unop_pushout_inv_snd CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd @[reassoc (attr := simp)] diff --git a/Mathlib/CategoryTheory/SingleObj.lean b/Mathlib/CategoryTheory/SingleObj.lean index 60e1a059fe675..3ac73b2f21571 100644 --- a/Mathlib/CategoryTheory/SingleObj.lean +++ b/Mathlib/CategoryTheory/SingleObj.lean @@ -231,7 +231,7 @@ set_option linter.uppercaseLean3 false in #align Mon.to_Cat_full MonCat.toCatFull instance toCat_faithful : Faithful toCat where - map_injective h := by simpa [toCat] using h + map_injective h := by rwa [toCat, (SingleObj.mapHom _ _).apply_eq_iff_eq] at h set_option linter.uppercaseLean3 false in #align Mon.to_Cat_faithful MonCat.toCat_faithful diff --git a/Mathlib/Data/Finset/Image.lean b/Mathlib/Data/Finset/Image.lean index d55dae3d7938e..f24b7f0010bb6 100644 --- a/Mathlib/Data/Finset/Image.lean +++ b/Mathlib/Data/Finset/Image.lean @@ -66,7 +66,7 @@ variable {f : α ↪ β} {s : Finset α} @[simp] theorem mem_map {b : β} : b ∈ s.map f ↔ ∃ a ∈ s, f a = b := - mem_map.trans <| by simp only [exists_prop]; rfl + Multiset.mem_map #align finset.mem_map Finset.mem_map --Porting note: Higher priority to apply before `mem_map`. diff --git a/Mathlib/Data/Finsupp/Basic.lean b/Mathlib/Data/Finsupp/Basic.lean index f26d195b77fa5..769e146b76731 100644 --- a/Mathlib/Data/Finsupp/Basic.lean +++ b/Mathlib/Data/Finsupp/Basic.lean @@ -1401,7 +1401,7 @@ section variable [Zero M] [MonoidWithZero R] [MulActionWithZero R M] -@[simp] +@[simp, nolint simpNF] -- `simpNF` incorrectly complains the LHS doesn't simplify. theorem single_smul (a b : α) (f : α → M) (r : R) : single a r b • f a = single a (r • f b) b := by by_cases h : a = b <;> simp [h] #align finsupp.single_smul Finsupp.single_smul diff --git a/Mathlib/Data/Finsupp/Defs.lean b/Mathlib/Data/Finsupp/Defs.lean index c74c0f22384f9..f2d0ebf8d5a48 100644 --- a/Mathlib/Data/Finsupp/Defs.lean +++ b/Mathlib/Data/Finsupp/Defs.lean @@ -774,7 +774,7 @@ theorem mapRange_apply {f : M → N} {hf : f 0 = 0} {g : α →₀ M} {a : α} : @[simp] theorem mapRange_zero {f : M → N} {hf : f 0 = 0} : mapRange f hf (0 : α →₀ M) = 0 := - ext fun a => by simp only [hf, zero_apply, mapRange_apply] + ext fun _ => by simp only [hf, zero_apply, mapRange_apply] #align finsupp.map_range_zero Finsupp.mapRange_zero @[simp] diff --git a/Mathlib/Data/Finsupp/Pointwise.lean b/Mathlib/Data/Finsupp/Pointwise.lean index 07370e428575e..0e5fa531a6821 100644 --- a/Mathlib/Data/Finsupp/Pointwise.lean +++ b/Mathlib/Data/Finsupp/Pointwise.lean @@ -108,7 +108,7 @@ instance pointwiseScalar [Semiring β] : SMul (α → β) (α →₀ β) where #align finsupp.pointwise_scalar Finsupp.pointwiseScalar @[simp] -theorem coe_pointwise_smul [Semiring β] (f : α → β) (g : α →₀ β) : FunLike.coe (f • g) = f • g := +theorem coe_pointwise_smul [Semiring β] (f : α → β) (g : α →₀ β) : ⇑(f • g) = f • ⇑g := rfl #align finsupp.coe_pointwise_smul Finsupp.coe_pointwise_smul diff --git a/Mathlib/Data/FunLike/Basic.lean b/Mathlib/Data/FunLike/Basic.lean index 731158da2d819..1b518f9aa6905 100644 --- a/Mathlib/Data/FunLike/Basic.lean +++ b/Mathlib/Data/FunLike/Basic.lean @@ -146,7 +146,8 @@ namespace FunLike variable {F α β} [i : FunLike F α β] -instance (priority := 100) hasCoeToFun : CoeFun F fun _ ↦ ∀ a : α, β a where coe := FunLike.coe +instance (priority := 100) hasCoeToFun : CoeFun F (fun _ ↦ ∀ a : α, β a) where + coe := @FunLike.coe _ _ β _ -- need to make explicit to beta reduce for non-dependent functions #eval Lean.Elab.Command.liftTermElabM do Std.Tactic.Coe.registerCoercion ``FunLike.coe diff --git a/Mathlib/Data/IsROrC/Basic.lean b/Mathlib/Data/IsROrC/Basic.lean index 73e4221c937a5..1a1c188d8cd9d 100644 --- a/Mathlib/Data/IsROrC/Basic.lean +++ b/Mathlib/Data/IsROrC/Basic.lean @@ -830,11 +830,11 @@ noncomputable instance Real.isROrC : IsROrC ℝ where mul_re_ax z w := by simp only [sub_zero, mul_zero, AddMonoidHom.zero_apply, AddMonoidHom.id_apply] mul_im_ax z w := by simp only [add_zero, zero_mul, mul_zero, AddMonoidHom.zero_apply] conj_re_ax z := by simp only [starRingEnd_apply, star_id_of_comm] - conj_im_ax z := by simp only [neg_zero, AddMonoidHom.zero_apply] + conj_im_ax _ := by simp only [neg_zero, AddMonoidHom.zero_apply] conj_I_ax := by simp only [RingHom.map_zero, neg_zero] norm_sq_eq_def_ax z := by simp only [sq, Real.norm_eq_abs, ← abs_mul, abs_mul_self z, add_zero, mul_zero, AddMonoidHom.zero_apply, AddMonoidHom.id_apply] - mul_im_I_ax z := by simp only [mul_zero, AddMonoidHom.zero_apply] + mul_im_I_ax _ := by simp only [mul_zero, AddMonoidHom.zero_apply] le_iff_re_im := (and_iff_left rfl).symm #align real.is_R_or_C Real.isROrC diff --git a/Mathlib/Data/MvPolynomial/Basic.lean b/Mathlib/Data/MvPolynomial/Basic.lean index 34dfa8268d988..784a7c62f4d87 100644 --- a/Mathlib/Data/MvPolynomial/Basic.lean +++ b/Mathlib/Data/MvPolynomial/Basic.lean @@ -1702,7 +1702,7 @@ theorem eval₂_mem {f : R →+* S} {p : MvPolynomial σ R} {s : subS} · subst h rw [MvPolynomial.not_mem_support_iff.1 ha, map_zero] exact zero_mem _ - · rwa [if_neg h, zero_add] at this + · rwa [zero_add] at this #align mv_polynomial.eval₂_mem MvPolynomial.eval₂_mem theorem eval_mem {p : MvPolynomial σ S} {s : subS} (hs : ∀ i ∈ p.support, p.coeff i ∈ s) {v : σ → S} diff --git a/Mathlib/Data/Nat/Factorization/Basic.lean b/Mathlib/Data/Nat/Factorization/Basic.lean index 895b6a80f36b0..3f785a85f4e20 100644 --- a/Mathlib/Data/Nat/Factorization/Basic.lean +++ b/Mathlib/Data/Nat/Factorization/Basic.lean @@ -429,7 +429,7 @@ theorem factorization_prime_le_iff_dvd {d n : ℕ} (hd : d ≠ 0) (hn : n ≠ 0) (∀ p : ℕ, p.Prime → d.factorization p ≤ n.factorization p) ↔ d ∣ n := by rw [← factorization_le_iff_dvd hd hn] refine' ⟨fun h p => (em p.Prime).elim (h p) fun hp => _, fun h p _ => h p⟩ - simp_rw [factorization_eq_zero_of_non_prime _ hp, le_refl] + simp_rw [factorization_eq_zero_of_non_prime _ hp] #align nat.factorization_prime_le_iff_dvd Nat.factorization_prime_le_iff_dvd theorem pow_succ_factorization_not_dvd {n p : ℕ} (hn : n ≠ 0) (hp : p.Prime) : diff --git a/Mathlib/Data/Polynomial/RingDivision.lean b/Mathlib/Data/Polynomial/RingDivision.lean index 3511a78bc1d7d..6d21fe59d68db 100644 --- a/Mathlib/Data/Polynomial/RingDivision.lean +++ b/Mathlib/Data/Polynomial/RingDivision.lean @@ -1328,7 +1328,7 @@ theorem card_roots_le_map [IsDomain A] [IsDomain B] {p : A[X]} {f : A →+* B} ( theorem card_roots_le_map_of_injective [IsDomain A] [IsDomain B] {p : A[X]} {f : A →+* B} (hf : Function.Injective f) : Multiset.card p.roots ≤ Multiset.card (p.map f).roots := by by_cases hp0 : p = 0 - · simp only [hp0, roots_zero, Polynomial.map_zero, Multiset.card_zero]; rfl + · simp only [hp0, roots_zero, Polynomial.map_zero, Multiset.card_zero] exact card_roots_le_map ((Polynomial.map_ne_zero_iff hf).mpr hp0) #align polynomial.card_roots_le_map_of_injective Polynomial.card_roots_le_map_of_injective diff --git a/Mathlib/Data/ZMod/Basic.lean b/Mathlib/Data/ZMod/Basic.lean index 215cba43bda29..5de6d7b454cd7 100644 --- a/Mathlib/Data/ZMod/Basic.lean +++ b/Mathlib/Data/ZMod/Basic.lean @@ -794,7 +794,7 @@ def chineseRemainder {m n : ℕ} (h : m.Coprime n) : ZMod (m * n) ≃+* ZMod m let to_fun : ZMod (m * n) → ZMod m × ZMod n := ZMod.castHom (show m.lcm n ∣ m * n by simp [Nat.lcm_dvd_iff]) (ZMod m × ZMod n) let inv_fun : ZMod m × ZMod n → ZMod (m * n) := fun x => - if m * n = 0 then if m = 1 then RingHom.snd _ _ x else RingHom.fst _ _ x + if m * n = 0 then if m = 1 then RingHom.snd _ (ZMod n) x else RingHom.fst (ZMod m) _ x else Nat.chineseRemainder h x.1.val x.2.val have inv : Function.LeftInverse inv_fun to_fun ∧ Function.RightInverse inv_fun to_fun := if hmn0 : m * n = 0 then by diff --git a/Mathlib/FieldTheory/Fixed.lean b/Mathlib/FieldTheory/Fixed.lean index fc0accdeaa811..35bac55da3d87 100644 --- a/Mathlib/FieldTheory/Fixed.lean +++ b/Mathlib/FieldTheory/Fixed.lean @@ -163,7 +163,6 @@ theorem linearIndependent_smul_of_linearIndependent {s : Finset F} : ∑ x in s, (fun y => l y • MulAction.toFun G F y) x g' rw [← smul_sum, ← sum_apply _ _ fun y => l y • toFun G F y, ← sum_apply _ _ fun y => l y • toFun G F y] - dsimp only rw [hla, toFun_apply, toFun_apply, smul_smul, mul_inv_cancel_left] #align fixed_points.linear_independent_smul_of_linear_independent FixedPoints.linearIndependent_smul_of_linearIndependent diff --git a/Mathlib/FieldTheory/IntermediateField.lean b/Mathlib/FieldTheory/IntermediateField.lean index 2ef4ac58bd1f5..f3666e6fdb58b 100644 --- a/Mathlib/FieldTheory/IntermediateField.lean +++ b/Mathlib/FieldTheory/IntermediateField.lean @@ -533,9 +533,7 @@ theorem coe_isIntegral_iff {R : Type*} [CommRing R] [Algebra R K] [Algebra R L] refine' ⟨P, hPmo, (injective_iff_map_eq_zero _).1 (algebraMap (↥S) L).injective _ _⟩ letI : IsScalarTower R S L := IsScalarTower.of_algebraMap_eq (congr_fun rfl) rw [eval₂_eq_eval_map, ← eval₂_at_apply, eval₂_eq_eval_map, Polynomial.map_map, ← - --Porting note: very strange that I have to `rw` twice with `eval₂_eq_eval_map`. - -- The first `rw` does nothing - IsScalarTower.algebraMap_eq, ← eval₂_eq_eval_map, ← eval₂_eq_eval_map] + IsScalarTower.algebraMap_eq, ← eval₂_eq_eval_map] exact hProot · obtain ⟨P, hPmo, hProot⟩ := h refine' ⟨P, hPmo, _⟩ diff --git a/Mathlib/FieldTheory/Laurent.lean b/Mathlib/FieldTheory/Laurent.lean index e9deebc07fdba..3b7b8aae4fda2 100644 --- a/Mathlib/FieldTheory/Laurent.lean +++ b/Mathlib/FieldTheory/Laurent.lean @@ -72,8 +72,7 @@ theorem laurentAux_div : @[simp] theorem laurentAux_algebraMap : laurentAux r (algebraMap _ _ p) = algebraMap _ _ (taylor r p) := by - rw [← mk_one, ← mk_one, mk_eq_div, laurentAux_div, mk_eq_div, taylor_one, map_one, map_one, - map_one] + rw [← mk_one, ← mk_one, mk_eq_div, laurentAux_div, mk_eq_div, taylor_one, map_one, map_one] #align ratfunc.laurent_aux_algebra_map RatFunc.laurentAux_algebraMap /-- The Laurent expansion of rational functions about a value. -/ diff --git a/Mathlib/FieldTheory/Minpoly/Basic.lean b/Mathlib/FieldTheory/Minpoly/Basic.lean index bd9ada0cd2d5a..01b36011e67c6 100644 --- a/Mathlib/FieldTheory/Minpoly/Basic.lean +++ b/Mathlib/FieldTheory/Minpoly/Basic.lean @@ -86,11 +86,9 @@ variable (A x) @[simp] theorem aeval : aeval x (minpoly A x) = 0 := by delta minpoly - split_ifs with hx -- Porting note: `split_ifs` doesn't remove the `if`s - · rw [dif_pos hx] - exact (degree_lt_wf.min_mem _ hx).2 - · rw [dif_neg hx] - exact aeval_zero _ + split_ifs with hx + · exact (degree_lt_wf.min_mem _ hx).2 + · exact aeval_zero _ #align minpoly.aeval minpoly.aeval /-- A minimal polynomial is not `1`. -/ diff --git a/Mathlib/FieldTheory/RatFunc.lean b/Mathlib/FieldTheory/RatFunc.lean index 2acaf122ac270..1eb700ef9ec05 100644 --- a/Mathlib/FieldTheory/RatFunc.lean +++ b/Mathlib/FieldTheory/RatFunc.lean @@ -863,7 +863,6 @@ theorem map_apply_div {R F : Type*} [CommRing R] [IsDomain R] [MonoidWithZeroHom · have : (0 : RatFunc K) = algebraMap K[X] _ 0 / algebraMap K[X] _ 1 := by simp rw [map_zero, map_zero, map_zero, div_zero, div_zero, this, map_apply_div_ne_zero, map_one, map_one, div_one, map_zero, map_zero] - simp only [map_zero, map_one, div_one] -- porting note: this `simp` was not needed exact one_ne_zero exact map_apply_div_ne_zero _ _ _ _ hq #align ratfunc.map_apply_div RatFunc.map_apply_div @@ -1226,7 +1225,6 @@ theorem num_div_denom (x : RatFunc K) : algebraMap _ _ (num x) / algebraMap _ _ induction' x using RatFunc.induction_on with p q hq -- porting note: had to hint the type of this `have` have q_div_ne_zero : q / gcd p q ≠ 0 := right_div_gcd_ne_zero hq - dsimp only rw [num_div p q, denom_div p hq, RingHom.map_mul, RingHom.map_mul, mul_div_mul_left, div_eq_div_iff, ← RingHom.map_mul, ← RingHom.map_mul, mul_comm _ q, ← EuclideanDomain.mul_div_assoc, ← EuclideanDomain.mul_div_assoc, mul_comm] @@ -1286,7 +1284,7 @@ theorem num_denom_mul (x y : RatFunc K) : #align ratfunc.num_denom_mul RatFunc.num_denom_mul theorem num_dvd {x : RatFunc K} {p : K[X]} (hp : p ≠ 0) : - num x ∣ p ↔ ∃ (q : K[X]) (hq : q ≠ 0), x = algebraMap _ _ p / algebraMap _ _ q := by + num x ∣ p ↔ ∃ (q : K[X]) (_ : q ≠ 0), x = algebraMap _ _ p / algebraMap _ _ q := by constructor · rintro ⟨q, rfl⟩ obtain ⟨_hx, hq⟩ := mul_ne_zero_iff.mp hp diff --git a/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean b/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean index 014c08b899f38..40c18aea1f299 100644 --- a/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean +++ b/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean @@ -250,7 +250,7 @@ instance coequalizer_π_stalk_isLocalRingHom (x : Y) : NatTrans.naturality, comp_apply, TopCat.Presheaf.pushforwardObj_map, ← isUnit_map_iff (Y.presheaf.map (eqToHom hV').op)] -- Porting note : change `rw` to `erw` - erw [← comp_apply, ← comp_apply, Category.assoc, ← Y.presheaf.map_comp] + erw [← comp_apply, ← comp_apply, ← Y.presheaf.map_comp] convert @RingedSpace.isUnit_res_basicOpen Y.toRingedSpace (unop _) (((coequalizer.π f.val g.val).c.app (op U)) s) #align algebraic_geometry.LocallyRingedSpace.has_coequalizer.coequalizer_π_stalk_is_local_ring_hom AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_stalk_isLocalRingHom diff --git a/Mathlib/Geometry/RingedSpace/Stalks.lean b/Mathlib/Geometry/RingedSpace/Stalks.lean index ab79ab90bb4dd..8391a80cc40fa 100644 --- a/Mathlib/Geometry/RingedSpace/Stalks.lean +++ b/Mathlib/Geometry/RingedSpace/Stalks.lean @@ -225,7 +225,7 @@ def stalkIso {X Y : PresheafedSpace.{_, _, v} C} (α : X ≅ Y) (x : X) : set_option linter.uppercaseLean3 false in #align algebraic_geometry.PresheafedSpace.stalk_map.stalk_iso AlgebraicGeometry.PresheafedSpace.stalkMap.stalkIso -@[simp, reassoc, elementwise] +@[reassoc, elementwise, simp, nolint simpNF] -- see std4#365 for the simpNF issue theorem stalkSpecializes_stalkMap {X Y : PresheafedSpace.{_, _, v} C} (f : X ⟶ Y) {x y : X} (h : x ⤳ y) : Y.presheaf.stalkSpecializes (f.base.map_specializes h) ≫ stalkMap f x = diff --git a/Mathlib/GroupTheory/FreeGroup/Basic.lean b/Mathlib/GroupTheory/FreeGroup/Basic.lean index 9079d76cb116b..4f7a0e4332bd8 100644 --- a/Mathlib/GroupTheory/FreeGroup/Basic.lean +++ b/Mathlib/GroupTheory/FreeGroup/Basic.lean @@ -945,7 +945,7 @@ theorem sum_mk : sum (mk L) = List.sum (L.map fun x => cond x.2 x.1 (-x.1)) := @[simp] theorem sum.of {x : α} : sum (of x) = x := - prod.of + @prod.of _ (_) _ #align free_group.sum.of FreeGroup.sum.of -- note: there are no bundled homs with different notation in the domain and codomain, so we copy diff --git a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean index 95618e5c447b8..053d3d20e7706 100644 --- a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean +++ b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean @@ -533,7 +533,6 @@ theorem IsCycle.sign {f : Perm α} (hf : IsCycle f) : sign f = -(-1) ^ f.support have h : swap x (f x) * f = 1 := by simp only [mul_def, one_def] rw [hf.eq_swap_of_apply_apply_eq_self hx.1 h1, swap_apply_left, swap_swap] - dsimp only rw [sign_mul, sign_swap hx.1.symm, h, sign_one, hf.eq_swap_of_apply_apply_eq_self hx.1 h1, card_support_swap hx.1.symm] rfl @@ -543,7 +542,6 @@ theorem IsCycle.sign {f : Perm α} (hf : IsCycle f) : sign f = -(-1) ^ f.support card_insert_of_not_mem (not_mem_erase _ _), sdiff_singleton_eq_erase] have : card (support (swap x (f x) * f)) < card (support f) := card_support_swap_mul hx.1 - dsimp only rw [sign_mul, sign_swap hx.1.symm, (hf.swap_mul hx.1 h1).sign, ← h] simp only [mul_neg, neg_mul, one_mul, neg_neg, pow_add, pow_one, mul_one] termination_by _ => f.support.card diff --git a/Mathlib/GroupTheory/SpecificGroups/Alternating.lean b/Mathlib/GroupTheory/SpecificGroups/Alternating.lean index 3dcf4048c87ee..4c8d57c2689ea 100644 --- a/Mathlib/GroupTheory/SpecificGroups/Alternating.lean +++ b/Mathlib/GroupTheory/SpecificGroups/Alternating.lean @@ -280,7 +280,7 @@ theorem isConj_swap_mul_swap_of_cycleType_two {g : Perm (Fin 5)} (ha : g ∈ alt rw [← Multiset.eq_replicate_card] at h2 rw [← sum_cycleType, h2, Multiset.sum_replicate, smul_eq_mul] at h have h : Multiset.card g.cycleType ≤ 3 := - le_of_mul_le_mul_right (le_trans h (by simp only [card_fin]; ring_nf)) (by simp) + le_of_mul_le_mul_right (le_trans h (by simp only [card_fin])) (by simp) rw [mem_alternatingGroup, sign_of_cycleType, h2] at ha norm_num at ha rw [pow_add, pow_mul, Int.units_pow_two, one_mul, Units.ext_iff, Units.val_one, @@ -347,7 +347,6 @@ instance isSimpleGroup_five : IsSimpleGroup (alternatingGroup (Fin 5)) := have con := mem_alternatingGroup.1 gA contrapose! con rw [sign_of_cycleType, cycleType_of_card_le_mem_cycleType_add_two (by decide) ng] - dsimp only decide · -- If `n = 5`, then `g` is itself a 5-cycle, conjugate to `finRotate 5`. refine' (isConj_iff_cycleType_eq.2 _).normalClosure_eq_top_of normalClosure_finRotate_five diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean index 5ce702ad50ec2..329500322280a 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean @@ -143,12 +143,12 @@ theorem contractRight_mul_ι (a : M) (b : CliffordAlgebra Q) : theorem contractLeft_algebraMap_mul (r : R) (b : CliffordAlgebra Q) : d⌋(algebraMap _ _ r * b) = algebraMap _ _ r * (d⌋b) := by - rw [← Algebra.smul_def, map_smul, Algebra.smul_def, Algebra.smul_def] + rw [← Algebra.smul_def, map_smul, Algebra.smul_def] #align clifford_algebra.contract_left_algebra_map_mul CliffordAlgebra.contractLeft_algebraMap_mul theorem contractLeft_mul_algebraMap (a : CliffordAlgebra Q) (r : R) : d⌋(a * algebraMap _ _ r) = d⌋a * algebraMap _ _ r := by - rw [← Algebra.commutes, contractLeft_algebraMap_mul, Algebra.commutes, Algebra.commutes] + rw [← Algebra.commutes, contractLeft_algebraMap_mul, Algebra.commutes] #align clifford_algebra.contract_left_mul_algebra_map CliffordAlgebra.contractLeft_mul_algebraMap theorem contractRight_algebraMap_mul (r : R) (b : CliffordAlgebra Q) : diff --git a/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean index 224094e5a2c73..e315b8a079716 100644 --- a/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean +++ b/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean @@ -138,7 +138,7 @@ theorem induction {C : ExteriorAlgebra R M → Prop} /-- The left-inverse of `algebraMap`. -/ def algebraMapInv : ExteriorAlgebra R M →ₐ[R] R := - ExteriorAlgebra.lift R ⟨(0 : M →ₗ[R] R), fun m => by simp⟩ + ExteriorAlgebra.lift R ⟨(0 : M →ₗ[R] R), fun _ => by simp⟩ #align exterior_algebra.algebra_map_inv ExteriorAlgebra.algebraMapInv variable (M) diff --git a/Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean b/Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean index 1c5c9ad67ffa1..76204f904d8c0 100644 --- a/Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean +++ b/Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean @@ -35,10 +35,9 @@ protected def GradedAlgebra.ι : (ι R).codRestrict _ fun m => by simpa only [pow_one] using LinearMap.mem_range_self _ m #align exterior_algebra.graded_algebra.ι ExteriorAlgebra.GradedAlgebra.ι --- porting note: replaced coercion to sort with an explicit subtype notation theorem GradedAlgebra.ι_apply (m : M) : GradedAlgebra.ι R M m = - DirectSum.of (fun i => {x // x ∈ (LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ i)}) 1 + DirectSum.of (fun i : ℕ => LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M) ^ i) 1 ⟨ι R m, by simpa only [pow_one] using LinearMap.mem_range_self _ m⟩ := rfl #align exterior_algebra.graded_algebra.ι_apply ExteriorAlgebra.GradedAlgebra.ι_apply diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 50606d04b806b..4534063e6217c 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -74,7 +74,7 @@ theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ theorem polarBilin_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : polarBilin (Q₁.tmul Q₂) = ⅟(2 : A) • (polarBilin Q₁).tmul (polarBilin Q₂) := by - simp_rw [←two_nsmul_associated A, ←two_nsmul_associated R, BilinForm.tmul, map_smul, tmul_smul, + simp_rw [←two_nsmul_associated A, ←two_nsmul_associated R, BilinForm.tmul, tmul_smul, ←smul_tmul', map_nsmul, associated_tmul] rw [smul_comm (_ : A) (_ : ℕ), ← smul_assoc, two_smul _ (_ : A), invOf_two_add_invOf_two, one_smul] diff --git a/Mathlib/LinearAlgebra/StdBasis.lean b/Mathlib/LinearAlgebra/StdBasis.lean index 3455b2aa4bda1..d0c9c0364d155 100644 --- a/Mathlib/LinearAlgebra/StdBasis.lean +++ b/Mathlib/LinearAlgebra/StdBasis.lean @@ -182,7 +182,6 @@ theorem linearIndependent_stdBasis [Ring R] [∀ i, AddCommGroup (Ms i)] [∀ i, exact (hs j).map' _ (ker_stdBasis _ _ _) apply linearIndependent_iUnion_finite hs' · intro j J _ hiJ - simp only have h₀ : ∀ j, span R (range fun i : ιs j => stdBasis R Ms j (v j i)) ≤ LinearMap.range (stdBasis R Ms j) := by diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean index 456b4fa5f2b4f..c36e99a700892 100644 --- a/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean +++ b/Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean @@ -107,10 +107,10 @@ variable {M} irreducible_def ι : M →ₗ[R] TensorAlgebra R M := { toFun := fun m => RingQuot.mkAlgHom R _ (FreeAlgebra.ι R m) map_add' := fun x y => by - rw [← AlgHom.map_add] + rw [← (RingQuot.mkAlgHom R (Rel R M)).map_add] exact RingQuot.mkAlgHom_rel R Rel.add map_smul' := fun r x => by - rw [← AlgHom.map_smul] + rw [← (RingQuot.mkAlgHom R (Rel R M)).map_smul] exact RingQuot.mkAlgHom_rel R Rel.smul } #align tensor_algebra.ι TensorAlgebra.ι diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean b/Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean index e7a9a418340cf..7cb1fcbf8a33e 100644 --- a/Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean +++ b/Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean @@ -117,7 +117,7 @@ theorem ofDirectSum_toDirectSum (x : TensorAlgebra R M) : AlgHom.congr_fun ofDirectSum_comp_toDirectSum x #align tensor_algebra.of_direct_sum_to_direct_sum TensorAlgebra.ofDirectSum_toDirectSum -@[simp] +@[simp, nolint simpNF] -- see std4#365 for the simpNF issue theorem mk_reindex_cast {n m : ℕ} (h : n = m) (x : (⨂[R]^n) M) : GradedMonoid.mk (A := fun i => (⨂[R]^i) M) m (PiTensorProduct.reindex R M (Equiv.cast <| congr_arg Fin h) x) = @@ -128,8 +128,8 @@ theorem mk_reindex_cast {n m : ℕ} (h : n = m) (x : (⨂[R]^n) M) : @[simp] theorem mk_reindex_fin_cast {n m : ℕ} (h : n = m) (x : (⨂[R]^n) M) : GradedMonoid.mk (A := fun i => (⨂[R]^i) M) m - (PiTensorProduct.reindex R M (Fin.castIso h).toEquiv x) = GradedMonoid.mk n x := - by rw [Fin.castIso_to_equiv, mk_reindex_cast h] + (PiTensorProduct.reindex R M (Fin.castIso h).toEquiv x) = GradedMonoid.mk n x := by + rw [Fin.castIso_to_equiv, mk_reindex_cast h] #align tensor_algebra.mk_reindex_fin_cast TensorAlgebra.mk_reindex_fin_cast /-- The product of tensor products made of a single vector is the same as a single product of diff --git a/Mathlib/Logic/Equiv/Set.lean b/Mathlib/Logic/Equiv/Set.lean index e866f50c4868e..ad4d0840336b3 100644 --- a/Mathlib/Logic/Equiv/Set.lean +++ b/Mathlib/Logic/Equiv/Set.lean @@ -486,7 +486,7 @@ protected noncomputable def image {α β} (f : α → β) (s : Set α) (H : Inje #align equiv.set.image Equiv.Set.image #align equiv.set.image_apply Equiv.Set.image_apply -@[simp] +@[simp, nolint simpNF] -- see std4#365 for the simpNF issue protected theorem image_symm_apply {α β} (f : α → β) (s : Set α) (H : Injective f) (x : α) (h : x ∈ s) : (Set.image f s H).symm ⟨f x, ⟨x, ⟨h, rfl⟩⟩⟩ = ⟨x, h⟩ := by apply (Set.image f s H).injective diff --git a/Mathlib/Logic/Equiv/TransferInstance.lean b/Mathlib/Logic/Equiv/TransferInstance.lean index 1b2dec28269d7..e91bb9083f1a4 100644 --- a/Mathlib/Logic/Equiv/TransferInstance.lean +++ b/Mathlib/Logic/Equiv/TransferInstance.lean @@ -554,10 +554,7 @@ protected def algebra (e : α ≃ β) [Semiring β] : · exact ((ringEquiv e).symm : β →+* α).comp (algebraMap R β) · intro r x simp only [Function.comp_apply, RingHom.coe_comp] - have p := ringEquiv_symm_apply e - dsimp at p - erw [p] - clear p + erw [ringEquiv_symm_apply e] apply (ringEquiv e).injective simp only [(ringEquiv e).map_mul] simp [Algebra.commutes] diff --git a/Mathlib/MeasureTheory/Function/UniformIntegrable.lean b/Mathlib/MeasureTheory/Function/UniformIntegrable.lean index 4dde1d4c5c1f5..9c824b3cb486a 100644 --- a/Mathlib/MeasureTheory/Function/UniformIntegrable.lean +++ b/Mathlib/MeasureTheory/Function/UniformIntegrable.lean @@ -451,12 +451,12 @@ theorem unifIntegrable_finite [Finite ι] (hp_one : 1 ≤ p) (hp_top : p ≠ ∞ (hf : ∀ i, Memℒp (f i) p μ) : UnifIntegrable f p μ := by obtain ⟨n, hn⟩ := Finite.exists_equiv_fin ι intro ε hε - set g : Fin n → α → β := f ∘ hn.some.symm with hgeq + let g : Fin n → α → β := f ∘ hn.some.symm have hg : ∀ i, Memℒp (g i) p μ := fun _ => hf _ obtain ⟨δ, hδpos, hδ⟩ := unifIntegrable_fin μ hp_one hp_top hg hε refine' ⟨δ, hδpos, fun i s hs hμs => _⟩ specialize hδ (hn.some i) s hs hμs - simp_rw [hgeq, Function.comp_apply, Equiv.symm_apply_apply] at hδ + simp_rw [Function.comp_apply, Equiv.symm_apply_apply] at hδ assumption #align measure_theory.unif_integrable_finite MeasureTheory.unifIntegrable_finite diff --git a/Mathlib/MeasureTheory/Integral/SetToL1.lean b/Mathlib/MeasureTheory/Integral/SetToL1.lean index c0f1ab15d520b..573afc7088656 100644 --- a/Mathlib/MeasureTheory/Integral/SetToL1.lean +++ b/Mathlib/MeasureTheory/Integral/SetToL1.lean @@ -1081,8 +1081,6 @@ theorem setToL1_add_left (hT : DominatedFinMeasAdditive μ T C) rw [this, ContinuousLinearMap.add_apply] refine' ContinuousLinearMap.extend_unique (setToL1SCLM α E μ (hT.add hT')) _ _ _ _ _ ext1 f - simp only [ContinuousLinearMap.add_comp, ContinuousLinearMap.coe_comp', Function.comp_apply, - ContinuousLinearMap.add_apply] suffices setToL1 hT f + setToL1 hT' f = setToL1SCLM α E μ (hT.add hT') f by rw [← this]; rfl rw [setToL1_eq_setToL1SCLM, setToL1_eq_setToL1SCLM, setToL1SCLM_add_left hT hT'] @@ -1095,8 +1093,6 @@ theorem setToL1_add_left' (hT : DominatedFinMeasAdditive μ T C) suffices setToL1 hT'' = setToL1 hT + setToL1 hT' by rw [this, ContinuousLinearMap.add_apply] refine' ContinuousLinearMap.extend_unique (setToL1SCLM α E μ hT'') _ _ _ _ _ ext1 f - simp only [ContinuousLinearMap.add_comp, ContinuousLinearMap.coe_comp', Function.comp_apply, - ContinuousLinearMap.add_apply] suffices setToL1 hT f + setToL1 hT' f = setToL1SCLM α E μ hT'' f by rw [← this]; congr rw [setToL1_eq_setToL1SCLM, setToL1_eq_setToL1SCLM, setToL1SCLM_add_left' hT hT' hT'' h_add] @@ -1107,8 +1103,6 @@ theorem setToL1_smul_left (hT : DominatedFinMeasAdditive μ T C) (c : ℝ) (f : suffices setToL1 (hT.smul c) = c • setToL1 hT by rw [this, ContinuousLinearMap.smul_apply] refine' ContinuousLinearMap.extend_unique (setToL1SCLM α E μ (hT.smul c)) _ _ _ _ _ ext1 f - simp only [ContinuousLinearMap.coe_comp', Function.comp_apply, ContinuousLinearMap.smul_comp, - Pi.smul_apply, ContinuousLinearMap.coe_smul'] suffices c • setToL1 hT f = setToL1SCLM α E μ (hT.smul c) f by rw [← this]; congr rw [setToL1_eq_setToL1SCLM, setToL1SCLM_smul_left c hT] #align measure_theory.L1.set_to_L1_smul_left MeasureTheory.L1.setToL1_smul_left @@ -1120,8 +1114,6 @@ theorem setToL1_smul_left' (hT : DominatedFinMeasAdditive μ T C) suffices setToL1 hT' = c • setToL1 hT by rw [this, ContinuousLinearMap.smul_apply] refine' ContinuousLinearMap.extend_unique (setToL1SCLM α E μ hT') _ _ _ _ _ ext1 f - simp only [ContinuousLinearMap.coe_comp', Function.comp_apply, ContinuousLinearMap.smul_comp, - Pi.smul_apply, ContinuousLinearMap.coe_smul'] suffices c • setToL1 hT f = setToL1SCLM α E μ hT' f by rw [← this]; congr rw [setToL1_eq_setToL1SCLM, setToL1SCLM_smul_left' c hT hT' h_smul] #align measure_theory.L1.set_to_L1_smul_left' MeasureTheory.L1.setToL1_smul_left' diff --git a/Mathlib/NumberTheory/ArithmeticFunction.lean b/Mathlib/NumberTheory/ArithmeticFunction.lean index bcc39278b8eb7..e753555a175cd 100644 --- a/Mathlib/NumberTheory/ArithmeticFunction.lean +++ b/Mathlib/NumberTheory/ArithmeticFunction.lean @@ -1048,9 +1048,7 @@ theorem isMultiplicative_moebius : IsMultiplicative μ := by dsimp only [coe_mk, ZeroHom.toFun_eq_coe, Eq.ndrec, ZeroHom.coe_mk] simp only [IsUnit.mul_iff, Nat.isUnit_iff, squarefree_mul hnm, ite_and, mul_ite, ite_mul, zero_mul, mul_zero] - rw [cardFactors_mul hn hm] -- porting note: `simp` does not seem to use this lemma. - simp only [moebius, ZeroHom.coe_mk, squarefree_mul hnm, ite_and, cardFactors_mul hn hm] - rw [pow_add, ite_mul_zero_left, ite_mul_zero_right] + rw [cardFactors_mul hn hm, pow_add, ite_mul_zero_left, ite_mul_zero_right] split_ifs <;> -- porting note: added simp -- porting note: added #align nat.arithmetic_function.is_multiplicative_moebius Nat.ArithmeticFunction.isMultiplicative_moebius diff --git a/Mathlib/NumberTheory/ClassNumber/Finite.lean b/Mathlib/NumberTheory/ClassNumber/Finite.lean index abae019871eaf..9d565d1bead91 100644 --- a/Mathlib/NumberTheory/ClassNumber/Finite.lean +++ b/Mathlib/NumberTheory/ClassNumber/Finite.lean @@ -91,15 +91,7 @@ theorem norm_le (a : S) {y : ℤ} (hy : ∀ k, abv (bS.repr a k) ≤ y) : rw [Algebra.norm_apply, ← LinearMap.det_toMatrix bS] simp only [Algebra.norm_apply, AlgHom.map_sum, AlgHom.map_smul, map_sum, map_smul, Algebra.toMatrix_lmul_eq, normBound, smul_mul_assoc, ← mul_pow] - --Porting note: rest of proof was - -- convert Matrix.det_sum_smul_le Finset.univ _ hy using 3 - -- · rw [Finset.card_univ, smul_mul_assoc, mul_comm] - -- · intro i j k - -- apply Finset.le_max' - -- exact finset.mem_image.mpr ⟨⟨i, j, k⟩, Finset.mem_univ _, rfl⟩ - rw [← LinearMap.det_toMatrix bS] - convert Matrix.det_sum_smul_le (n := ι) Finset.univ _ hy using 3 - · simp; rfl + convert Matrix.det_sum_smul_le Finset.univ _ hy using 3 · rw [Finset.card_univ, smul_mul_assoc, mul_comm] · intro i j k apply Finset.le_max' diff --git a/Mathlib/NumberTheory/FunctionField.lean b/Mathlib/NumberTheory/FunctionField.lean index 59cc6a91c85cb..4d00f9ae67ca2 100644 --- a/Mathlib/NumberTheory/FunctionField.lean +++ b/Mathlib/NumberTheory/FunctionField.lean @@ -154,7 +154,7 @@ variable [DecidableEq (RatFunc Fq)] Explicitly, if `f/g ∈ Fq(t)` is a nonzero quotient of polynomials, its valuation at infinity is `Multiplicative.ofAdd(degree(f) - degree(g))`. -/ def inftyValuationDef (r : RatFunc Fq) : ℤₘ₀ := - if r = 0 then 0 else Multiplicative.ofAdd r.intDegree + if r = 0 then 0 else ↑(Multiplicative.ofAdd r.intDegree) #align function_field.infty_valuation_def FunctionField.inftyValuationDef theorem InftyValuation.map_zero' : inftyValuationDef Fq 0 = 0 := diff --git a/Mathlib/NumberTheory/NumberField/Units.lean b/Mathlib/NumberTheory/NumberField/Units.lean index c5cdf20b092b8..13c5bc1c48b18 100644 --- a/Mathlib/NumberTheory/NumberField/Units.lean +++ b/Mathlib/NumberTheory/NumberField/Units.lean @@ -199,7 +199,7 @@ variable (K) /-- The logarithmic embedding of the units (seen as an `Additive` group). -/ def logEmbedding : Additive ((𝓞 K)ˣ) →+ ({w : InfinitePlace K // w ≠ w₀} → ℝ) := -{ toFun := fun x w => mult w.val * Real.log (w.val (Additive.toMul x)) +{ toFun := fun x w => mult w.val * Real.log (w.val ↑(Additive.toMul x)) map_zero' := by simp; rfl map_add' := fun _ _ => by simp [Real.log_mul, mul_add]; rfl } @@ -555,7 +555,8 @@ def basisModTorsion : Basis (Fin (rank K)) ℤ (Additive ((𝓞 K)ˣ ⧸ (torsio /-- A fundamental system of units of `K`. The units of `fundSystem` are arbitrary lifts of the units in `basisModTorsion`. -/ def fundSystem : Fin (rank K) → (𝓞 K)ˣ := - fun i => Quotient.out' (Additive.toMul (basisModTorsion K i)) + -- `:)` prevents the `⧸` decaying to a quotient by `leftRel` when we unfold this later + fun i => Quotient.out' (Additive.toMul (basisModTorsion K i) :) /-- The exponents that appear in the unique decomposition of a unit as the product of a root of unity and powers of the units of the fundamental system `fundSystem` (see @@ -580,7 +581,7 @@ theorem exist_unique_eq_mul_prod (x : (𝓞 K)ˣ) : ∃! (ζ : torsion K) (e : F have h_tors : ζ ∈ torsion K := by rw [← QuotientGroup.eq_one_iff, QuotientGroup.mk_mul, QuotientGroup.mk_inv, ← ofMul_eq_zero, ofMul_mul, ofMul_inv, QuotientGroup.mk_prod, ofMul_prod] - simp_rw [QuotientGroup.mk_zpow, ofMul_zpow, fundSystem, QuotientGroup.out_eq', ofMul_toMul] + simp_rw [QuotientGroup.mk_zpow, ofMul_zpow, fundSystem, QuotientGroup.out_eq'] rw [add_eq_zero_iff_eq_neg, neg_neg] exact ((basisModTorsion K).sum_repr (Additive.ofMul ↑x)).symm refine ⟨⟨ζ, h_tors⟩, ?_, ?_⟩ diff --git a/Mathlib/Order/WithBot.lean b/Mathlib/Order/WithBot.lean index 7dc5ec72c1f30..5fb7b47f03359 100644 --- a/Mathlib/Order/WithBot.lean +++ b/Mathlib/Order/WithBot.lean @@ -893,7 +893,7 @@ protected theorem _root_.IsMin.withTop (h : IsMin a) : IsMin (a : WithTop α) := -- defeq to is_max_to_dual_iff.mp (is_max.with_bot _), but that breaks API boundary intro _ hb rw [← toDual_le_toDual_iff] at hb - simpa [toDual_le_iff] using (IsMax.withBot h : IsMax (toDual a : WithBot αᵒᵈ)) hb + simpa [toDual_le_iff] using h.toDual.withBot hb #align is_min.with_top IsMin.withTop theorem untop_le_iff {a : WithTop α} {b : α} (h : a ≠ ⊤) : @@ -1318,7 +1318,6 @@ instance instWellFoundedGT [LT α] [WellFoundedGT α] : WellFoundedGT (WithTop revert this generalize ha : WithBot.toDual a = b intro ac - dsimp at ac induction' ac with _ H IH generalizing a subst ha exact ⟨_, fun a' h => IH (WithTop.toDual a') (toDual_lt_toDual.mpr h) _ rfl⟩⟩ @@ -1331,7 +1330,6 @@ instance _root_.WithBot.instWellFoundedGT [LT α] [WellFoundedGT α] : WellFound revert this generalize ha : WithBot.toDual a = b intro ac - dsimp at ac induction' ac with _ H IH generalizing a subst ha exact ⟨_, fun a' h => IH (WithBot.toDual a') (toDual_lt_toDual.mpr h) _ rfl⟩⟩ diff --git a/Mathlib/Probability/ProbabilityMassFunction/Monad.lean b/Mathlib/Probability/ProbabilityMassFunction/Monad.lean index 593d2c84ef4d0..a42b515ebd589 100644 --- a/Mathlib/Probability/ProbabilityMassFunction/Monad.lean +++ b/Mathlib/Probability/ProbabilityMassFunction/Monad.lean @@ -130,7 +130,7 @@ theorem mem_support_bind_iff (b : β) : @[simp] theorem pure_bind (a : α) (f : α → PMF β) : (pure a).bind f = f a := by have : ∀ b a', ite (a' = a) (f a' b) 0 = ite (a' = a) (f a b) 0 := fun b a' => by - split_ifs with h <;> simp; subst h; simp + split_ifs with h <;> simp [h] ext b simp [this] #align pmf.pure_bind PMF.pure_bind diff --git a/Mathlib/RingTheory/AdjoinRoot.lean b/Mathlib/RingTheory/AdjoinRoot.lean index 53583c7ce909d..c81be0d8ad019 100644 --- a/Mathlib/RingTheory/AdjoinRoot.lean +++ b/Mathlib/RingTheory/AdjoinRoot.lean @@ -895,7 +895,7 @@ noncomputable def quotientEquivQuotientMinpolyMap (pb : PowerBasis R S) (I : Ide rw [← Ideal.Quotient.mk_algebraMap, Ideal.quotientEquiv_apply, RingHom.toFun_eq_coe, Ideal.quotientMap_mk, AlgEquiv.toRingEquiv_eq_coe, RingEquiv.coe_toRingHom, AlgEquiv.coe_ringEquiv, AlgEquiv.commutes, - Quotient.mk_algebraMap]; rfl)).trans (AdjoinRoot.quotEquivQuotMap _ _) + Quotient.mk_algebraMap])).trans (AdjoinRoot.quotEquivQuotMap _ _) #align power_basis.quotient_equiv_quotient_minpoly_map PowerBasis.quotientEquivQuotientMinpolyMap -- This lemma should have the simp tag but this causes a lint issue. diff --git a/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean b/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean index cf8881473e997..90a45a8b4ece3 100644 --- a/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean +++ b/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean @@ -78,8 +78,8 @@ multiplicative valuation. -/ def intValuationDef (r : R) : ℤₘ₀ := if r = 0 then 0 else - Multiplicative.ofAdd - (-(Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r} : Ideal R)).factors : ℤ) + ↑(Multiplicative.ofAdd + (-(Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r} : Ideal R)).factors : ℤ)) #align is_dedekind_domain.height_one_spectrum.int_valuation_def IsDedekindDomain.HeightOneSpectrum.intValuationDef theorem intValuationDef_if_pos {r : R} (hr : r = 0) : v.intValuationDef r = 0 := diff --git a/Mathlib/RingTheory/EisensteinCriterion.lean b/Mathlib/RingTheory/EisensteinCriterion.lean index f22d5ea64e99f..08244107ff76e 100644 --- a/Mathlib/RingTheory/EisensteinCriterion.lean +++ b/Mathlib/RingTheory/EisensteinCriterion.lean @@ -65,9 +65,7 @@ set_option linter.uppercaseLean3 false in theorem eval_zero_mem_ideal_of_eq_mul_X_pow {n : ℕ} {P : Ideal R} {q : R[X]} {c : Polynomial (R ⧸ P)} (hq : map (mk P) q = c * X ^ n) (hn0 : 0 < n) : eval 0 q ∈ P := by rw [← coeff_zero_eq_eval_zero, ← eq_zero_iff_mem, ← coeff_map, hq, - --Porting note: why is this lemma required twice? - coeff_zero_eq_eval_zero, coeff_zero_eq_eval_zero, - eval_mul, eval_pow, eval_X, zero_pow hn0, mul_zero] + coeff_zero_eq_eval_zero, eval_mul, eval_pow, eval_X, zero_pow hn0, mul_zero] set_option linter.uppercaseLean3 false in #align polynomial.eisenstein_criterion_aux.eval_zero_mem_ideal_of_eq_mul_X_pow Polynomial.EisensteinCriterionAux.eval_zero_mem_ideal_of_eq_mul_X_pow diff --git a/Mathlib/RingTheory/FractionalIdeal.lean b/Mathlib/RingTheory/FractionalIdeal.lean index f98a36a1de77a..21a9b567ba34b 100644 --- a/Mathlib/RingTheory/FractionalIdeal.lean +++ b/Mathlib/RingTheory/FractionalIdeal.lean @@ -916,7 +916,7 @@ theorem canonicalEquiv_symm : (canonicalEquiv S P P').symm = canonicalEquiv S P' #align fractional_ideal.canonical_equiv_symm FractionalIdeal.canonicalEquiv_symm theorem canonicalEquiv_flip (I) : canonicalEquiv S P P' (canonicalEquiv S P' P I) = I := by - rw [← canonicalEquiv_symm, RingEquiv.apply_symm_apply] + rw [← canonicalEquiv_symm]; erw [RingEquiv.apply_symm_apply] #align fractional_ideal.canonical_equiv_flip FractionalIdeal.canonicalEquiv_flip @[simp] diff --git a/Mathlib/RingTheory/HahnSeries.lean b/Mathlib/RingTheory/HahnSeries.lean index fd28c6861300d..a2d004d0fc3b6 100644 --- a/Mathlib/RingTheory/HahnSeries.lean +++ b/Mathlib/RingTheory/HahnSeries.lean @@ -1202,7 +1202,7 @@ theorem ofPowerSeries_X_pow {R} [CommSemiring R] (n : ℕ) : induction' n with n ih · simp rfl - · rw [pow_succ, pow_succ, ih, ofPowerSeries_X, mul_comm, single_mul_single, one_mul, + · rw [pow_succ, ih, ofPowerSeries_X, mul_comm, single_mul_single, one_mul, Nat.cast_succ, add_comm] #align hahn_series.of_power_series_X_pow HahnSeries.ofPowerSeries_X_pow diff --git a/Mathlib/RingTheory/IsTensorProduct.lean b/Mathlib/RingTheory/IsTensorProduct.lean index 8b49ca77dd733..3bd9937b0086d 100644 --- a/Mathlib/RingTheory/IsTensorProduct.lean +++ b/Mathlib/RingTheory/IsTensorProduct.lean @@ -179,9 +179,7 @@ noncomputable nonrec def IsBaseChange.lift (g : M →ₗ[R] Q) : N →ₗ[S] Q : · rw [smul_zero, map_zero, smul_zero] · intro s m change h.lift F (r • s • f m) = r • h.lift F (s • f m) - rw [← mul_smul, hF, hF] - rw [mul_smul] -- Porting note: this line does nothing - apply mul_smul + rw [← mul_smul, hF, hF, mul_smul] · intro x₁ x₂ e₁ e₂ rw [map_add, smul_add, map_add, smul_add, e₁, e₂] } #align is_base_change.lift IsBaseChange.lift diff --git a/Mathlib/RingTheory/LaurentSeries.lean b/Mathlib/RingTheory/LaurentSeries.lean index 5ec72e9de9fe3..d12f35c5e8cce 100644 --- a/Mathlib/RingTheory/LaurentSeries.lean +++ b/Mathlib/RingTheory/LaurentSeries.lean @@ -135,7 +135,7 @@ instance of_powerSeries_localization [CommRing R] : rfl · simp only [single_mul_single, mul_one, add_left_neg] rfl - · simp + · dsimp; rw [ofPowerSeries_X_pow] surj' := by intro z by_cases h : 0 ≤ z.order diff --git a/Mathlib/RingTheory/Localization/Basic.lean b/Mathlib/RingTheory/Localization/Basic.lean index e49fa369a992e..c0bcbf4794651 100644 --- a/Mathlib/RingTheory/Localization/Basic.lean +++ b/Mathlib/RingTheory/Localization/Basic.lean @@ -459,7 +459,7 @@ theorem mk'_add (x₁ x₂ : R) (y₁ y₂ : M) : (by rw [mul_comm (_ + _), mul_add, mul_mk'_eq_mk'_of_mul, mk'_add_eq_iff_add_mul_eq_mul, mul_comm (_ * _), ← mul_assoc, add_comm, ← map_mul, mul_mk'_eq_mk'_of_mul, - add_comm _ (mk' _ _ _), mk'_add_eq_iff_add_mul_eq_mul] + mk'_add_eq_iff_add_mul_eq_mul] simp only [map_add, Submonoid.coe_mul, map_mul] ring) #align is_localization.mk'_add IsLocalization.mk'_add @@ -1339,7 +1339,7 @@ theorem IsLocalization.map_units_map_submonoid (y : M) : IsUnit (algebraMap R S exact IsLocalization.map_units Sₘ ⟨algebraMap R S y, Algebra.mem_algebraMapSubmonoid_of_mem y⟩ #align is_localization.map_units_map_submonoid IsLocalization.map_units_map_submonoid -@[simp] +-- can't be simp, as `S` only appears on the RHS theorem IsLocalization.algebraMap_mk' (x : R) (y : M) : algebraMap Rₘ Sₘ (IsLocalization.mk' Rₘ x y) = IsLocalization.mk' Sₘ (algebraMap R S x) diff --git a/Mathlib/RingTheory/Localization/FractionRing.lean b/Mathlib/RingTheory/Localization/FractionRing.lean index fee315b83875a..5467692e69cb3 100644 --- a/Mathlib/RingTheory/Localization/FractionRing.lean +++ b/Mathlib/RingTheory/Localization/FractionRing.lean @@ -163,7 +163,7 @@ theorem mk'_eq_div {r} (s : nonZeroDivisors A) : mk' K r s = algebraMap A K r / #align is_fraction_ring.mk'_eq_div IsFractionRing.mk'_eq_div theorem div_surjective (z : K) : - ∃ (x y : A) (hy : y ∈ nonZeroDivisors A), algebraMap _ _ x / algebraMap _ _ y = z := + ∃ (x y : A) (_ : y ∈ nonZeroDivisors A), algebraMap _ _ x / algebraMap _ _ y = z := let ⟨x, ⟨y, hy⟩, h⟩ := mk'_surjective (nonZeroDivisors A) z ⟨x, y, hy, by rwa [mk'_eq_div] at h⟩ #align is_fraction_ring.div_surjective IsFractionRing.div_surjective diff --git a/Mathlib/RingTheory/Localization/Integral.lean b/Mathlib/RingTheory/Localization/Integral.lean index 1d03bae662d7a..df78c130910b5 100644 --- a/Mathlib/RingTheory/Localization/Integral.lean +++ b/Mathlib/RingTheory/Localization/Integral.lean @@ -83,14 +83,12 @@ theorem integerNormalization_spec (p : S[X]) : use Classical.choose (exist_integer_multiples_of_finset M (p.support.image p.coeff)) intro i rw [integerNormalization_coeff, coeffIntegerNormalization] - split_ifs with hi -- Porting note: didn't remove the ifs - · rw [dif_pos hi] - exact + split_ifs with hi + · exact Classical.choose_spec (Classical.choose_spec (exist_integer_multiples_of_finset M (p.support.image p.coeff)) (p.coeff i) (Finset.mem_image.mpr ⟨i, hi, rfl⟩)) - · rw [dif_neg hi] - rw [RingHom.map_zero, not_mem_support_iff.mp hi, smul_zero] + · rw [RingHom.map_zero, not_mem_support_iff.mp hi, smul_zero] -- Porting note: was `convert (smul_zero _).symm, ...` #align is_localization.integer_normalization_spec IsLocalization.integerNormalization_spec diff --git a/Mathlib/RingTheory/Perfection.lean b/Mathlib/RingTheory/Perfection.lean index f60d40e3ecdd6..fb8eadc0e8acc 100644 --- a/Mathlib/RingTheory/Perfection.lean +++ b/Mathlib/RingTheory/Perfection.lean @@ -428,7 +428,7 @@ theorem preVal_mul {x y : ModP K v O hv p} (hxy0 : x * y ≠ 0) : have hy0 : y ≠ 0 := mt (by rintro rfl; rw [mul_zero]) hxy0 obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective y - rw [← RingHom.map_mul] at hxy0 ⊢ + rw [← map_mul (Ideal.Quotient.mk (Ideal.span {↑p})) r s] at hxy0 ⊢ rw [preVal_mk hx0, preVal_mk hy0, preVal_mk hxy0, RingHom.map_mul, v.map_mul] #align mod_p.pre_val_mul ModP.preVal_mul @@ -442,7 +442,7 @@ theorem preVal_add (x y : ModP K v O hv p) : · rw [hxy0, preVal_zero]; exact zero_le _ obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective y - rw [← RingHom.map_add] at hxy0 ⊢ + rw [← map_add (Ideal.Quotient.mk (Ideal.span {↑p})) r s] at hxy0 ⊢ rw [preVal_mk hx0, preVal_mk hy0, preVal_mk hxy0, RingHom.map_add]; exact v.map_add _ _ #align mod_p.pre_val_add ModP.preVal_add @@ -479,8 +479,8 @@ theorem mul_ne_zero_of_pow_p_ne_zero {x y : ModP K v O hv p} (hx : x ^ p ≠ 0) obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective y have h1p : (0 : ℝ) < 1 / p := one_div_pos.2 (Nat.cast_pos.2 hp.1.pos) - rw [← RingHom.map_mul]; rw [← RingHom.map_pow] at hx hy - rw [← v_p_lt_val hv] at hx hy ⊢ + erw [← RingHom.map_mul]; erw [← RingHom.map_pow] at hx hy + erw [← v_p_lt_val hv] at hx hy ⊢ rw [RingHom.map_pow, v.map_pow, ← rpow_lt_rpow_iff h1p, ← rpow_nat_cast, ← rpow_mul, mul_one_div_cancel (Nat.cast_ne_zero.2 hp.1.ne_zero : (p : ℝ) ≠ 0), rpow_one] at hx hy rw [RingHom.map_mul, v.map_mul]; refine' lt_of_le_of_lt _ (mul_lt_mul₀ hx hy) @@ -540,7 +540,7 @@ theorem valAux_eq {f : PreTilt K v O hv p} {n : ℕ} (hfn : coeff _ _ n f ≠ 0) obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le (Nat.find_min' h hfn) induction' k with k ih · rfl - obtain ⟨x, hx⟩ := Ideal.Quotient.mk_surjective (coeff _ _ (Nat.find h + k + 1) f) + obtain ⟨x, hx⟩ := Ideal.Quotient.mk_surjective (coeff (ModP K v O hv p) p (Nat.find h + k + 1) f) have h1 : (Ideal.Quotient.mk _ x : ModP K v O hv p) ≠ 0 := hx.symm ▸ hfn have h2 : (Ideal.Quotient.mk _ (x ^ p) : ModP K v O hv p) ≠ 0 := by erw [RingHom.map_pow, hx, ← RingHom.map_pow, coeff_pow_p] diff --git a/Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean b/Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean index a2f5b6b2441d4..f6b4eaa205b7c 100644 --- a/Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean +++ b/Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean @@ -80,7 +80,7 @@ theorem cyclotomic_expand_eq_cyclotomic {p n : ℕ} (hp : Nat.Prime p) (hdiv : p · simp haveI := NeZero.of_pos hzero suffices expand ℤ p (cyclotomic n ℤ) = cyclotomic (n * p) ℤ by - rw [← map_cyclotomic_int, ← map_expand, this, map_cyclotomic_int, map_cyclotomic] + rw [← map_cyclotomic_int, ← map_expand, this, map_cyclotomic_int] refine' eq_of_monic_of_dvd_of_natDegree_le (cyclotomic.monic _ _) ((cyclotomic.monic n ℤ).expand hp.pos) _ _ · have hpos := Nat.mul_pos hzero hp.pos diff --git a/Mathlib/RingTheory/RingHom/Surjective.lean b/Mathlib/RingTheory/RingHom/Surjective.lean index b92a432ad4121..527a0a7e3255f 100644 --- a/Mathlib/RingTheory/RingHom/Surjective.lean +++ b/Mathlib/RingTheory/RingHom/Surjective.lean @@ -60,7 +60,7 @@ theorem surjective_ofLocalizationSpan : OfLocalizationSpan surjective := by fapply Subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem _ l.support (fun x : s => f x) fun x : s => f (l x) - · dsimp only; simp_rw [← _root_.map_mul, ← map_sum, ← f.map_one]; exact f.congr_arg hl + · simp_rw [← _root_.map_mul, ← map_sum, ← f.map_one]; exact f.congr_arg hl · exact fun _ => Set.mem_range_self _ · exact fun _ => Set.mem_range_self _ · intro r diff --git a/Mathlib/RingTheory/RootsOfUnity/Basic.lean b/Mathlib/RingTheory/RootsOfUnity/Basic.lean index acb94aabd54f5..ff5f7d134c8f2 100644 --- a/Mathlib/RingTheory/RootsOfUnity/Basic.lean +++ b/Mathlib/RingTheory/RootsOfUnity/Basic.lean @@ -993,7 +993,6 @@ theorem autToPow_spec (f : S ≃ₐ[R] S) : μ ^ (hμ.autToPow R f : ZMod n).val rw [IsPrimitiveRoot.coe_autToPow_apply] generalize_proofs h have := h.choose_spec - dsimp only [AlgEquiv.toAlgHom_eq_coe, AlgEquiv.coe_algHom] at this refine' (_ : ((hμ.toRootsOfUnity : Sˣ) : S) ^ _ = _).trans this.symm rw [← rootsOfUnity.coe_pow, ← rootsOfUnity.coe_pow] congr 2 diff --git a/Mathlib/RingTheory/Trace.lean b/Mathlib/RingTheory/Trace.lean index 1db78e3e0f0db..138215d0363a6 100644 --- a/Mathlib/RingTheory/Trace.lean +++ b/Mathlib/RingTheory/Trace.lean @@ -302,9 +302,7 @@ theorem trace_eq_sum_roots [FiniteDimensional K L] {x : L} algebraMap K F (Algebra.trace K L x) = finrank K⟮x⟯ L • ((minpoly K x).aroots F).sum := by rw [trace_eq_trace_adjoin K x, Algebra.smul_def, RingHom.map_mul, ← Algebra.smul_def, - IntermediateField.AdjoinSimple.trace_gen_eq_sum_roots _ hF] --- Porting note: last `simp` was `IsScalarTower.algebraMap_smul` inside the `rw`. - simp only [eq_natCast, map_natCast, nsmul_eq_mul] + IntermediateField.AdjoinSimple.trace_gen_eq_sum_roots _ hF, IsScalarTower.algebraMap_smul] #align trace_eq_sum_roots trace_eq_sum_roots end EqSumRoots diff --git a/Mathlib/RingTheory/WittVector/Frobenius.lean b/Mathlib/RingTheory/WittVector/Frobenius.lean index 486c31a0fbe40..3c6fbd43a22b6 100644 --- a/Mathlib/RingTheory/WittVector/Frobenius.lean +++ b/Mathlib/RingTheory/WittVector/Frobenius.lean @@ -156,7 +156,7 @@ theorem map_frobeniusPoly (n : ℕ) : add_mul, mul_right_comm, mul_right_comm (C ((p : ℚ) ^ (n + 1))), ← C_mul, ← C_mul, pow_succ, mul_assoc (p : ℚ) ((p : ℚ) ^ n), h1, mul_one, C_1, one_mul, add_comm _ (X n ^ p), add_assoc, ← add_sub, add_right_inj, frobeniusPolyAux_eq, RingHom.map_sub, map_X, mul_sub, sub_eq_add_neg, - add_comm _ (C (p : ℚ) * X (n + 1)), ← add_sub, show (Int.castRingHom ℚ) ↑p = (p : ℚ) from rfl, + add_comm _ (C (p : ℚ) * X (n + 1)), ← add_sub, add_right_inj, neg_eq_iff_eq_neg, neg_sub, eq_comm] simp only [map_sum, mul_sum, sum_mul, ← sum_sub_distrib] apply sum_congr rfl @@ -172,8 +172,7 @@ theorem map_frobeniusPoly (n : ℕ) : rw [mem_range] at hj rw [RingHom.map_mul, RingHom.map_mul, RingHom.map_pow, RingHom.map_pow, RingHom.map_pow, RingHom.map_pow, RingHom.map_pow, map_C, map_X, mul_pow] - rw [mul_comm (C (p : ℚ) ^ i), mul_comm _ ((X i ^ p) ^ _), - show (Int.castRingHom ℚ) ↑p = (p : ℚ) from rfl, mul_comm (C (p : ℚ) ^ (j + 1)), + rw [mul_comm (C (p : ℚ) ^ i), mul_comm _ ((X i ^ p) ^ _), mul_comm (C (p : ℚ) ^ (j + 1)), mul_comm (C (p : ℚ))] simp only [mul_assoc] apply congr_arg diff --git a/Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean b/Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean index 93033ed914fb2..4db9064b31166 100644 --- a/Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean +++ b/Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean @@ -272,7 +272,7 @@ theorem exists_frobenius_solution_fractionRing_aux (m n : ℕ) (r' q' : 𝕎 k) #align witt_vector.exists_frobenius_solution_fraction_ring_aux WittVector.exists_frobenius_solution_fractionRing_aux theorem exists_frobenius_solution_fractionRing {a : FractionRing (𝕎 k)} (ha : a ≠ 0) : - ∃ (b : FractionRing (𝕎 k)) (hb : b ≠ 0) (m : ℤ), + ∃ (b : FractionRing (𝕎 k)) (_ : b ≠ 0) (m : ℤ), φ b * a = (p : FractionRing (𝕎 k)) ^ m * b := by revert ha refine' Localization.induction_on a _ diff --git a/Mathlib/RingTheory/WittVector/Identities.lean b/Mathlib/RingTheory/WittVector/Identities.lean index f6f10ce89d41e..f9647d26e0046 100644 --- a/Mathlib/RingTheory/WittVector/Identities.lean +++ b/Mathlib/RingTheory/WittVector/Identities.lean @@ -40,7 +40,6 @@ noncomputable section -- Porting note: `ghost_calc` failure: `simp only []` and the manual instances had to be added. /-- The composition of Frobenius and Verschiebung is multiplication by `p`. -/ theorem frobenius_verschiebung (x : 𝕎 R) : frobenius (verschiebung x) = x * p := by - simp only [] have : IsPoly p fun {R} [CommRing R] x ↦ frobenius (verschiebung x) := IsPoly.comp (hg := frobenius_isPoly p) (hf := verschiebung_isPoly) have : IsPoly p fun {R} [CommRing R] x ↦ x * p := mulN_isPoly p p @@ -106,7 +105,6 @@ variable {p R} /-- The “projection formula” for Frobenius and Verschiebung. -/ theorem verschiebung_mul_frobenius (x y : 𝕎 R) : verschiebung (x * frobenius y) = verschiebung x * y := by - simp only [] have : IsPoly₂ p fun {R} [Rcr : CommRing R] x y ↦ verschiebung (x * frobenius y) := IsPoly.comp₂ (hg := verschiebung_isPoly) (hf := IsPoly₂.comp (hh := mulIsPoly₂) (hf := idIsPolyI' p) (hg := frobenius_isPoly p)) diff --git a/Mathlib/RingTheory/WittVector/MulCoeff.lean b/Mathlib/RingTheory/WittVector/MulCoeff.lean index ab6e5b6171a79..9300e40ee7489 100644 --- a/Mathlib/RingTheory/WittVector/MulCoeff.lean +++ b/Mathlib/RingTheory/WittVector/MulCoeff.lean @@ -153,7 +153,7 @@ theorem mul_polyOfInterest_aux3 (n : ℕ) : wittPolyProd p (n + 1) = (p : 𝕄) ^ (n + 1) * X (1, n + 1) * rename (Prod.mk (0 : Fin 2)) (wittPolynomial p ℤ (n + 1)) + remainder p n := by -- a useful auxiliary fact - have mvpz : (p : 𝕄) ^ (n + 1) = MvPolynomial.C ((p : ℤ) ^ (n + 1)) := by simp only; norm_cast + have mvpz : (p : 𝕄) ^ (n + 1) = MvPolynomial.C ((p : ℤ) ^ (n + 1)) := by norm_cast -- Porting note: the original proof applies `sum_range_succ` through a non-`conv` rewrite, -- but this does not work in Lean 4; the whole proof also times out very badly. The proof has been -- nearly totally rewritten here and now finishes quite fast. @@ -211,7 +211,7 @@ theorem polyOfInterest_vars_eq (n : ℕ) : (polyOfInterest p n).vars = ((p : 𝕄) ^ (n + 1) * (wittMul p (n + 1) + (p : 𝕄) ^ (n + 1) * X (0, n + 1) * X (1, n + 1) - X (0, n + 1) * rename (Prod.mk (1 : Fin 2)) (wittPolynomial p ℤ (n + 1)) - X (1, n + 1) * rename (Prod.mk (0 : Fin 2)) (wittPolynomial p ℤ (n + 1)))).vars := by - have : (p : 𝕄) ^ (n + 1) = C ((p : ℤ) ^ (n + 1)) := by simp only; norm_cast + have : (p : 𝕄) ^ (n + 1) = C ((p : ℤ) ^ (n + 1)) := by norm_cast rw [polyOfInterest, this, vars_C_mul] apply pow_ne_zero exact_mod_cast hp.out.ne_zero diff --git a/Mathlib/RingTheory/WittVector/StructurePolynomial.lean b/Mathlib/RingTheory/WittVector/StructurePolynomial.lean index 6ee1ade278846..cee7b2b2a2c88 100644 --- a/Mathlib/RingTheory/WittVector/StructurePolynomial.lean +++ b/Mathlib/RingTheory/WittVector/StructurePolynomial.lean @@ -257,7 +257,6 @@ theorem C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum (Φ : MvPolynomial idx have : p ^ (n + 1) = p ^ k * p ^ (n - k + 1) := by rw [← pow_add, ← add_assoc]; congr 2; rw [add_comm, ← tsub_eq_iff_eq_add_of_le hk] rw [this] - simp only -- Porting note: without this, the next `rw` doesn't do anything rw [Nat.cast_mul, Nat.cast_pow, Nat.cast_pow] apply mul_dvd_mul_left ((p : MvPolynomial (idx × ℕ) ℤ) ^ k) rw [show p ^ (n + 1 - k) = p * p ^ (n - k) by rw [← pow_succ, ← tsub_add_eq_add_tsub hk]] diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean index c7b105ac6ada0..6cc16b2266bd9 100644 --- a/Mathlib/SetTheory/Ordinal/Basic.lean +++ b/Mathlib/SetTheory/Ordinal/Basic.lean @@ -302,10 +302,10 @@ theorem type_preimage {α β : Type u} (r : α → α → Prop) [IsWellOrder α (RelIso.preimage f r).ordinal_type_eq #align ordinal.type_preimage Ordinal.type_preimage -@[simp] +@[simp, nolint simpNF] -- `simpNF` incorrectly complains the LHS doesn't simplify. theorem type_preimage_aux {α β : Type u} (r : α → α → Prop) [IsWellOrder α r] (f : β ≃ α) : @type _ (fun x y => r (f x) (f y)) (inferInstanceAs (IsWellOrder β (↑f ⁻¹'o r))) = type r := by - convert (RelIso.preimage f r).ordinal_type_eq + convert (RelIso.preimage f r).ordinal_type_eq @[elab_as_elim] theorem inductionOn {C : Ordinal → Prop} (o : Ordinal) diff --git a/Mathlib/Topology/Category/Profinite/Nobeling.lean b/Mathlib/Topology/Category/Profinite/Nobeling.lean index c81b2a088a71b..982314c312b73 100644 --- a/Mathlib/Topology/Category/Profinite/Nobeling.lean +++ b/Mathlib/Topology/Category/Profinite/Nobeling.lean @@ -1558,7 +1558,7 @@ theorem Products.max_eq_eval (l : Products I) (hl : l.val ≠ []) (∀ i, i ∈ l.Tail.val → (x.val i = true)) = (∀ i, i ∈ l.Tail.val → (SwapTrue o x.val i = true)) · apply forall_congr; intro i; apply forall_congr; intro hi; rw [hi' i hi] simp only [H] - split_ifs with h₁ h₂ h₃ <;> dsimp [e] + split_ifs with h₁ h₂ h₃ <;> try (dsimp [e]) · rw [if_pos (swapTrue_eq_true _ _), if_neg] · rfl · simp [mem_C'_eq_false C ho x x.prop, Bool.coe_false] diff --git a/Mathlib/Topology/Category/TopCat/Limits/Products.lean b/Mathlib/Topology/Category/TopCat/Limits/Products.lean index 3e8e0e76b4604..07e716929dc6f 100644 --- a/Mathlib/Topology/Category/TopCat/Limits/Products.lean +++ b/Mathlib/Topology/Category/TopCat/Limits/Products.lean @@ -132,7 +132,7 @@ theorem sigmaIsoSigma_hom_ι_apply {ι : Type v} (α : ι → TopCatMax.{v, u}) @[simp] theorem sigmaIsoSigma_inv_apply {ι : Type v} (α : ι → TopCatMax.{v, u}) (i : ι) (x : α i) : (sigmaIsoSigma α).inv ⟨i, x⟩ = (Sigma.ι α i : _) x := by - rw [← sigmaIsoSigma_hom_ι_apply, ← comp_app, ←comp_app, Category.assoc, Iso.hom_inv_id, + rw [← sigmaIsoSigma_hom_ι_apply, ← comp_app, ←comp_app, Iso.hom_inv_id, Category.comp_id] #align Top.sigma_iso_sigma_inv_apply TopCat.sigmaIsoSigma_inv_apply diff --git a/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean b/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean index abf537df39ab7..8ce5d253e3d9f 100644 --- a/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean +++ b/Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean @@ -170,7 +170,7 @@ theorem range_pullback_to_prod {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) : use (pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, h⟩ apply Concrete.limit_ext rintro ⟨⟨⟩⟩ <;> - rw [←comp_apply, prod.comp_lift, ←comp_apply, limit.lift_π] <;> + rw [←comp_apply, ←comp_apply, limit.lift_π] <;> -- This used to be `simp` before leanprover/lean4#2644 aesop_cat #align Top.range_pullback_to_prod TopCat.range_pullback_to_prod diff --git a/Mathlib/Topology/Gluing.lean b/Mathlib/Topology/Gluing.lean index aa8a38dd698a4..a970c8ea77e8c 100644 --- a/Mathlib/Topology/Gluing.lean +++ b/Mathlib/Topology/Gluing.lean @@ -208,7 +208,6 @@ theorem ι_eq_iff_rel (i j : D.J) (x : D.U i) (y : D.U j) : rw [← show _ = Sigma.mk j y from ConcreteCategory.congr_hom (sigmaIsoSigma.{_, u} D.U).inv_hom_id _] change InvImage D.Rel (sigmaIsoSigma.{_, u} D.U).hom _ _ - simp only [TopCat.sigmaIsoSigma_inv_apply] rw [← (InvImage.equivalence _ _ D.rel_equiv).eqvGen_iff] refine' EqvGen.mono _ (D.eqvGen_of_π_eq h : _) rintro _ _ ⟨x⟩ diff --git a/Mathlib/Topology/Sheaves/Stalks.lean b/Mathlib/Topology/Sheaves/Stalks.lean index 5763e6cf11629..7a514af1e6de1 100644 --- a/Mathlib/Topology/Sheaves/Stalks.lean +++ b/Mathlib/Topology/Sheaves/Stalks.lean @@ -195,7 +195,6 @@ theorem comp (ℱ : X.Presheaf C) (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : change (_ : colimit _ ⟶ _) = (_ : colimit _ ⟶ _) ext U rcases U with ⟨⟨_, _⟩, _⟩ - simp only [colimit.ι_map_assoc, colimit.ι_pre_assoc, whiskerRight_app, Category.assoc] simp [stalkFunctor, stalkPushforward] set_option linter.uppercaseLean3 false in #align Top.presheaf.stalk_pushforward.comp TopCat.Presheaf.stalkPushforward.comp @@ -364,7 +363,7 @@ theorem stalkSpecializes_stalkFunctor_map {F G : X.Presheaf C} (f : F ⟶ G) {x set_option linter.uppercaseLean3 false in #align Top.presheaf.stalk_specializes_stalk_functor_map TopCat.Presheaf.stalkSpecializes_stalkFunctor_map -@[simp, reassoc, elementwise] +@[reassoc, elementwise, simp, nolint simpNF] -- see std4#365 for the simpNF issue theorem stalkSpecializes_stalkPushforward (f : X ⟶ Y) (F : X.Presheaf C) {x y : X} (h : x ⤳ y) : (f _* F).stalkSpecializes (f.map_specializes h) ≫ F.stalkPushforward _ f x = F.stalkPushforward _ f y ≫ F.stalkSpecializes h := by diff --git a/test/FunLike.lean b/test/FunLike.lean new file mode 100644 index 0000000000000..b05f66ef4465a --- /dev/null +++ b/test/FunLike.lean @@ -0,0 +1,6 @@ +import Mathlib.Data.FunLike.Basic + +variable {F α β : Sort*} [i : FunLike F α fun _ ↦ β] (f : F) (a : α) + +/-- info: ↑f a : β -/ +#guard_msgs in #check f a