diff --git a/Archive/Imo/Imo1988Q6.lean b/Archive/Imo/Imo1988Q6.lean index 33af2cf96003e..89f7d19b5bc77 100644 --- a/Archive/Imo/Imo1988Q6.lean +++ b/Archive/Imo/Imo1988Q6.lean @@ -207,7 +207,7 @@ theorem imo1988_q6 {a b : ℕ} (h : a * b + 1 ∣ a ^ 2 + b ^ 2) : hk (fun x => k * x) (fun x => x * x - k) fun _ _ => False <;> clear hk a b · -- We will now show that the fibers of the solution set are described by a quadratic equation. - intro x y; dsimp only + intro x y rw [← Int.coe_nat_inj', ← sub_eq_zero] apply eq_iff_eq_cancel_right.2 simp; ring @@ -265,7 +265,7 @@ example {a b : ℕ} (h : a * b ∣ a ^ 2 + b ^ 2 + 1) : 3 * a * b = a ^ 2 + b ^ hk (fun x => k * x) (fun x => x * x + 1) fun x _ => x ≤ 1 <;> clear hk a b · -- We will now show that the fibers of the solution set are described by a quadratic equation. - intro x y; dsimp only + intro x y rw [← Int.coe_nat_inj', ← sub_eq_zero] apply eq_iff_eq_cancel_right.2 simp; ring diff --git a/Archive/Sensitivity.lean b/Archive/Sensitivity.lean index 5856a8f5c95b7..d672ca99eb326 100644 --- a/Archive/Sensitivity.lean +++ b/Archive/Sensitivity.lean @@ -399,7 +399,6 @@ theorem exists_eigenvalue (H : Set (Q m.succ)) (hH : Card H ≥ 2 ^ m + 1) : let W := Span (e '' H) let img := range (g m) suffices 0 < dim (W ⊓ img) by - simp only [exists_prop] exact_mod_cast exists_mem_ne_zero_of_rank_pos this have dim_le : dim (W ⊔ img) ≤ 2 ^ (m + 1) := by convert ← rank_submodule_le (W ⊔ img) diff --git a/Mathlib/Algebra/Associated.lean b/Mathlib/Algebra/Associated.lean index d80cda105e037..09c4c8e331970 100644 --- a/Mathlib/Algebra/Associated.lean +++ b/Mathlib/Algebra/Associated.lean @@ -145,9 +145,7 @@ theorem prime_pow_succ_dvd_mul {α : Type*} [CancelCommMonoidWithZero α] {p x y rw [or_iff_not_imp_right] intro hy induction' i with i ih generalizing x - · simp only [zero_add, pow_one] at * - rw [pow_one] - rw [pow_one] at hxy + · rw [pow_one] at hxy ⊢ exact (h.dvd_or_dvd hxy).resolve_right hy rw [pow_succ] at hxy ⊢ obtain ⟨x', rfl⟩ := (h.dvd_or_dvd (dvd_of_mul_right_dvd hxy)).resolve_right hy diff --git a/Mathlib/Algebra/BigOperators/Basic.lean b/Mathlib/Algebra/BigOperators/Basic.lean index 3b62e193e178e..450da9daceb74 100644 --- a/Mathlib/Algebra/BigOperators/Basic.lean +++ b/Mathlib/Algebra/BigOperators/Basic.lean @@ -1003,7 +1003,7 @@ theorem prod_ite_of_false {p : α → Prop} {hp : DecidablePred p} (f g : α → ∏ x in s, (if p x then f x else g x) = ∏ x in s, g x := by rw [prod_ite, filter_false_of_mem, filter_true_of_mem] · simp only [prod_empty, one_mul] - all_goals intros; simp; apply h; assumption + all_goals intros; apply h; assumption #align finset.prod_ite_of_false Finset.prod_ite_of_false #align finset.sum_ite_of_false Finset.sum_ite_of_false diff --git a/Mathlib/Algebra/BigOperators/Ring.lean b/Mathlib/Algebra/BigOperators/Ring.lean index 931c0bd611ee4..65186bfe8cd49 100644 --- a/Mathlib/Algebra/BigOperators/Ring.lean +++ b/Mathlib/Algebra/BigOperators/Ring.lean @@ -151,8 +151,7 @@ theorem prod_add [DecidableEq α] (f g : α → β) (s : Finset α) : (by simp) (by simp)) (fun t _ a _ => a ∈ t) (by simp [Classical.em]) - (by simp_rw [mem_filter, Function.funext_iff, eq_iff_iff, mem_singleton, mem_pi, - mem_insert, iff_true, iff_false]; tauto) + (by simp_rw [mem_filter, Function.funext_iff, eq_iff_iff, mem_pi, mem_insert]; tauto) (by simp_rw [ext_iff, @mem_filter _ _ (id _), mem_powerset]; tauto) #align finset.prod_add Finset.prod_add diff --git a/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean b/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean index 97f90101fa781..23987d20df11c 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean @@ -124,7 +124,7 @@ theorem left_unitality (X : Type u) : change q x' = Finsupp.mapDomain (λ_ X).hom (finsuppTensorFinsupp' R (𝟙_ (Type u)) X (Finsupp.single PUnit.unit 1 ⊗ₜ[R] Finsupp.single x 1)) x' simp_rw [finsuppTensorFinsupp'_single_tmul_single, - ModuleCat.MonoidalCategory.leftUnitor_hom_apply, Finsupp.smul_single', mul_one, + ModuleCat.MonoidalCategory.leftUnitor_hom_apply, mul_one, Finsupp.mapDomain_single, CategoryTheory.leftUnitor_hom_apply, one_smul] #align Module.free.left_unitality ModuleCat.Free.left_unitality @@ -145,7 +145,7 @@ theorem right_unitality (X : Type u) : change q x' = Finsupp.mapDomain (ρ_ X).hom (finsuppTensorFinsupp' R X (𝟙_ (Type u)) (Finsupp.single x 1 ⊗ₜ[R] Finsupp.single PUnit.unit 1)) x' simp_rw [finsuppTensorFinsupp'_single_tmul_single, - ModuleCat.MonoidalCategory.rightUnitor_hom_apply, Finsupp.smul_single', mul_one, + ModuleCat.MonoidalCategory.rightUnitor_hom_apply, mul_one, Finsupp.mapDomain_single, CategoryTheory.rightUnitor_hom_apply, one_smul] #align Module.free.right_unitality ModuleCat.Free.right_unitality diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean index f2e0501c5aafa..0e36f05e12ae3 100644 --- a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean +++ b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean @@ -544,7 +544,6 @@ def HomEquiv.fromExtendScalars {X Y} (g : X ⟶ (restrictScalars f).obj Y) : map_smul' := fun (r : R) (s : S) => ?_} · ext dsimp - simp only [LinearMap.coe_mk, LinearMap.add_apply] rw [← add_smul] · ext x apply mul_smul (f r) s (g x) diff --git a/Mathlib/Algebra/CharP/MixedCharZero.lean b/Mathlib/Algebra/CharP/MixedCharZero.lean index b9ce1746b5323..ce50f18412cf3 100644 --- a/Mathlib/Algebra/CharP/MixedCharZero.lean +++ b/Mathlib/Algebra/CharP/MixedCharZero.lean @@ -230,7 +230,7 @@ noncomputable def algebraRat (h : ∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ intro a b field_simp trans (↑((a * b).num * a.den * b.den) : R) - · simp_rw [Int.cast_mul, Int.cast_ofNat, Rat.coe_pnatDen] + · simp_rw [Int.cast_mul, Int.cast_ofNat] ring rw [Rat.mul_num_den' a b] simp @@ -238,7 +238,7 @@ noncomputable def algebraRat (h : ∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ intro a b field_simp trans (↑((a + b).num * a.den * b.den) : R) - · simp_rw [Int.cast_mul, Int.cast_ofNat, Rat.coe_pnatDen] + · simp_rw [Int.cast_mul, Int.cast_ofNat] ring rw [Rat.add_num_den' a b] simp } diff --git a/Mathlib/Algebra/GeomSum.lean b/Mathlib/Algebra/GeomSum.lean index c8cfc0fb8878e..fe41c03ad05d9 100644 --- a/Mathlib/Algebra/GeomSum.lean +++ b/Mathlib/Algebra/GeomSum.lean @@ -86,7 +86,6 @@ theorem op_geom_sum (x : α) (n : ℕ) : op (∑ i in range n, x ^ i) = ∑ i in @[simp] theorem op_geom_sum₂ (x y : α) (n : ℕ) : ∑ i in range n, op y ^ (n - 1 - i) * op x ^ i = ∑ i in range n, op y ^ i * op x ^ (n - 1 - i):= by - simp only [op_sum, op_mul, op_pow] rw [← sum_range_reflect] refine' sum_congr rfl fun j j_in => _ rw [mem_range, Nat.lt_iff_add_one_le] at j_in @@ -319,7 +318,6 @@ protected theorem Commute.geom_sum₂_Ico_mul [Ring α] {x y : α} (h : Commute have : (∑ k in Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k) = ∑ k in Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k) := by refine' sum_congr rfl fun k _ => _ - simp only [ge_iff_le, tsub_le_iff_right] have hp := Commute.pow_pow (Commute.op h.symm) (n - 1 - k) k simpa [Commute, SemiconjBy] using hp simp only [this] diff --git a/Mathlib/Algebra/GroupPower/Basic.lean b/Mathlib/Algebra/GroupPower/Basic.lean index c95f87017a77d..6de5e6c9a665e 100644 --- a/Mathlib/Algebra/GroupPower/Basic.lean +++ b/Mathlib/Algebra/GroupPower/Basic.lean @@ -176,7 +176,6 @@ theorem pow_eq_pow_mod {M : Type*} [Monoid M] {x : M} (m : ℕ) {n : ℕ} (h : x x ^ m = x ^ (m % n) := by have t : x ^ m = x ^ (n * (m / n) + m % n) := congr_arg (fun a => x ^ a) ((Nat.add_comm _ _).trans (Nat.mod_add_div _ _)).symm - dsimp at t rw [t, pow_add, pow_mul, h, one_pow, one_mul] #align pow_eq_pow_mod pow_eq_pow_mod #align nsmul_eq_mod_nsmul nsmul_eq_mod_nsmul diff --git a/Mathlib/Algebra/Homology/Homotopy.lean b/Mathlib/Algebra/Homology/Homotopy.lean index 5c7c1c40b1203..ac54a9a3487e8 100644 --- a/Mathlib/Algebra/Homology/Homotopy.lean +++ b/Mathlib/Algebra/Homology/Homotopy.lean @@ -349,7 +349,6 @@ def nullHomotopy (hom : ∀ i j, C.X i ⟶ D.X j) (zero : ∀ i j, ¬c.Rel j i def nullHomotopy' (h : ∀ i j, c.Rel j i → (C.X i ⟶ D.X j)) : Homotopy (nullHomotopicMap' h) 0 := by apply nullHomotopy fun i j => dite (c.Rel j i) (h i j) fun _ => 0 intro i j hij - dsimp rw [dite_eq_right_iff] intro hij' exfalso @@ -375,7 +374,6 @@ theorem nullHomotopicMap'_f {k₂ k₁ k₀ : ι} (r₂₁ : c.Rel k₂ k₁) (r (nullHomotopicMap' h).f k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁ := by simp only [nullHomotopicMap'] rw [nullHomotopicMap_f r₂₁ r₁₀] - dsimp split_ifs rfl #align homotopy.null_homotopic_map'_f Homotopy.nullHomotopicMap'_f @@ -395,7 +393,6 @@ theorem nullHomotopicMap'_f_of_not_rel_left {k₁ k₀ : ι} (r₁₀ : c.Rel k (nullHomotopicMap' h).f k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀ := by simp only [nullHomotopicMap'] rw [nullHomotopicMap_f_of_not_rel_left r₁₀ hk₀] - dsimp split_ifs rfl #align homotopy.null_homotopic_map'_f_of_not_rel_left Homotopy.nullHomotopicMap'_f_of_not_rel_left @@ -415,7 +412,6 @@ theorem nullHomotopicMap'_f_of_not_rel_right {k₁ k₀ : ι} (r₁₀ : c.Rel k (nullHomotopicMap' h).f k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ := by simp only [nullHomotopicMap'] rw [nullHomotopicMap_f_of_not_rel_right r₁₀ hk₁] - dsimp split_ifs rfl #align homotopy.null_homotopic_map'_f_of_not_rel_right Homotopy.nullHomotopicMap'_f_of_not_rel_right diff --git a/Mathlib/Algebra/Module/Injective.lean b/Mathlib/Algebra/Module/Injective.lean index 844acd060b6ff..2dfe07b839715 100644 --- a/Mathlib/Algebra/Module/Injective.lean +++ b/Mathlib/Algebra/Module/Injective.lean @@ -419,7 +419,6 @@ def extensionOfMaxAdjoin (h : Module.Baer R Q) (y : N) : ExtensionOf i f where congr } is_extension m := by dsimp - simp only [LinearPMap.mk_apply, LinearMap.coe_mk] rw [(extensionOfMax i f).is_extension, ExtensionOfMaxAdjoin.extensionToFun_wd i f h _ ⟨i m, _⟩ 0 _, map_zero, add_zero] simp diff --git a/Mathlib/Algebra/Module/Torsion.lean b/Mathlib/Algebra/Module/Torsion.lean index f631dbe0e4837..0d526764c7034 100644 --- a/Mathlib/Algebra/Module/Torsion.lean +++ b/Mathlib/Algebra/Module/Torsion.lean @@ -426,8 +426,7 @@ theorem iSup_torsionBySet_ideal_eq_torsionBySet_iInf [DecidableEq ι] : · have := coe_mem (μ i) simp only [mem_iInf] at this exact Ideal.mul_mem_left _ _ (this j hj ij) - · simp_rw [coe_mk] - rw [← Finset.sum_smul, hμ, one_smul] + · rw [← Finset.sum_smul, hμ, one_smul] #align submodule.supr_torsion_by_ideal_eq_torsion_by_infi Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf -- Porting note: iSup_torsionBySet_ideal_eq_torsionBySet_iInf now requires DecidableEq ι diff --git a/Mathlib/Algebra/Order/CompleteField.lean b/Mathlib/Algebra/Order/CompleteField.lean index ff6445956870d..e65446a6a0c45 100644 --- a/Mathlib/Algebra/Order/CompleteField.lean +++ b/Mathlib/Algebra/Order/CompleteField.lean @@ -261,7 +261,6 @@ theorem le_inducedMap_mul_self_of_mem_cutMap (ha : 0 < a) (b : β) (hb : b ∈ c trans (q' : β) ^ 2 exact_mod_cast hqq'.le rw [pow_two] at hqa ⊢ - push_cast at hqa exact mul_self_le_mul_self (by exact_mod_cast hq'.le) (le_csSup (cutMap_bddAbove β a) <| coe_mem_cutMap_iff.2 <| lt_of_mul_self_lt_mul_self ha.le hqa) diff --git a/Mathlib/Algebra/QuaternionBasis.lean b/Mathlib/Algebra/QuaternionBasis.lean index f76d154cf91c2..31a83a936872e 100644 --- a/Mathlib/Algebra/QuaternionBasis.lean +++ b/Mathlib/Algebra/QuaternionBasis.lean @@ -125,9 +125,7 @@ theorem lift_add (x y : ℍ[R,c₁,c₂]) : q.lift (x + y) = q.lift x + q.lift y theorem lift_mul (x y : ℍ[R,c₁,c₂]) : q.lift (x * y) = q.lift x * q.lift y := by simp only [lift, Algebra.algebraMap_eq_smul_one] - simp only [add_mul] - simp_rw [add_mul, mul_add, smul_mul_assoc, mul_smul_comm, one_mul, mul_one, ← Algebra.smul_def, - smul_add, smul_smul] + simp_rw [add_mul, mul_add, smul_mul_assoc, mul_smul_comm, one_mul, mul_one, smul_smul] simp only [i_mul_i, j_mul_j, i_mul_j, j_mul_i, i_mul_k, k_mul_i, k_mul_j, j_mul_k, k_mul_k] simp only [smul_smul, smul_neg, sub_eq_add_neg, add_smul, ← add_assoc, mul_neg, neg_smul] simp only [mul_right_comm _ _ (c₁ * c₂), mul_comm _ (c₁ * c₂)] diff --git a/Mathlib/AlgebraicGeometry/AffineScheme.lean b/Mathlib/AlgebraicGeometry/AffineScheme.lean index f794766330724..941355433d09b 100644 --- a/Mathlib/AlgebraicGeometry/AffineScheme.lean +++ b/Mathlib/AlgebraicGeometry/AffineScheme.lean @@ -220,7 +220,7 @@ def IsAffineOpen.fromSpec {X : Scheme} {U : Opens X} (hU : IsAffineOpen U) : instance IsAffineOpen.isOpenImmersion_fromSpec {X : Scheme} {U : Opens X} (hU : IsAffineOpen U) : IsOpenImmersion hU.fromSpec := by - delta IsAffineOpen.fromSpec; dsimp; simp only [Scheme.comp_val] + delta IsAffineOpen.fromSpec; dsimp -- Porting note : this was automatic repeat apply (config := { allowSynthFailures := true }) PresheafedSpace.IsOpenImmersion.comp #align algebraic_geometry.is_affine_open.is_open_immersion_from_Spec AlgebraicGeometry.IsAffineOpen.isOpenImmersion_fromSpec diff --git a/Mathlib/AlgebraicGeometry/Gluing.lean b/Mathlib/AlgebraicGeometry/Gluing.lean index 267b30270e387..7111257d225ca 100644 --- a/Mathlib/AlgebraicGeometry/Gluing.lean +++ b/Mathlib/AlgebraicGeometry/Gluing.lean @@ -378,7 +378,6 @@ theorem fromGlued_injective : Function.Injective 𝒰.fromGlued.1.base := by rw [𝒰.gluedCover.ι_eq_iff] right use e.hom ⟨⟨x, y⟩, h⟩ - simp_rw [← comp_apply] constructor -- Porting note: in the two subproofs below, added the `change` lines · change (e.hom ≫ _) ⟨(x, y), h⟩ = x diff --git a/Mathlib/AlgebraicGeometry/LocallyRingedSpace.lean b/Mathlib/AlgebraicGeometry/LocallyRingedSpace.lean index bbf34a66726eb..4367ae2db3a85 100644 --- a/Mathlib/AlgebraicGeometry/LocallyRingedSpace.lean +++ b/Mathlib/AlgebraicGeometry/LocallyRingedSpace.lean @@ -236,7 +236,6 @@ def restrict {U : TopCat} (X : LocallyRingedSpace) {f : U ⟶ X.toTopCat} (h : O LocallyRingedSpace where localRing := by intro x - dsimp at * -- We show that the stalk of the restriction is isomorphic to the original stalk, apply @RingEquiv.localRing _ _ _ (X.localRing (f x)) exact (X.restrictStalkIso h x).symm.commRingCatIsoToRingEquiv diff --git a/Mathlib/AlgebraicGeometry/PresheafedSpace/HasColimits.lean b/Mathlib/AlgebraicGeometry/PresheafedSpace/HasColimits.lean index 595e5b2addb53..914371331cf3b 100644 --- a/Mathlib/AlgebraicGeometry/PresheafedSpace/HasColimits.lean +++ b/Mathlib/AlgebraicGeometry/PresheafedSpace/HasColimits.lean @@ -156,7 +156,6 @@ def pushforwardDiagramToColimit (F : J ⥤ PresheafedSpace.{_, _, v} C) : Opens.map_comp_obj, Pushforward.comp_inv_app, pushforwardEq_hom_app, eqToHom_op, id_eq, eqToHom_map, id_comp, assoc, eqToHom_trans] dsimp - simp only [eqToHom_trans, id_comp] congr 1 -- The key fact is `(F.map f).c.congr`, -- which allows us in rewrite in the argument of `(F.map f).c.app`. diff --git a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean index 6105f74d7dabc..7f43e8d3c3f0a 100644 --- a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean +++ b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean @@ -471,7 +471,7 @@ theorem carrier.smul_mem (c x : A) (hx : x ∈ carrier f_deg q) : c • x ∈ ca refine' DirectSum.Decomposition.inductionOn 𝒜 _ _ _ · rw [zero_smul]; exact carrier.zero_mem f_deg hm _ · rintro n ⟨a, ha⟩ i - simp_rw [Subtype.coe_mk, proj_apply, smul_eq_mul, coe_decompose_mul_of_left_mem 𝒜 i ha] + simp_rw [proj_apply, smul_eq_mul, coe_decompose_mul_of_left_mem 𝒜 i ha] -- Porting note: having trouble with Mul instance let product : A⁰_ f := Mul.mul (Quotient.mk'' ⟨_, ⟨a ^ m, pow_mem_graded m ha⟩, ⟨_, ?_⟩, ⟨n, rfl⟩⟩ : A⁰_ f) @@ -481,8 +481,8 @@ theorem carrier.smul_mem (c x : A) (hx : x ∈ carrier f_deg q) : c • x ∈ ca · dsimp erw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk'', HomogeneousLocalization.mul_val, HomogeneousLocalization.val_mk'', - HomogeneousLocalization.val_mk'', Subtype.coe_mk] - simp_rw [mul_pow, Subtype.coe_mk]; rw [Localization.mk_mul] + HomogeneousLocalization.val_mk''] + simp_rw [mul_pow]; rw [Localization.mk_mul] congr; erw [← pow_add, Nat.add_sub_of_le h] · rw [(_ : m • n = _)]; mem_tac; simp only [smul_eq_mul, mul_comm] · rw [(_ : m • (i - n) = _)]; mem_tac; simp only [smul_eq_mul, mul_comm] @@ -543,7 +543,7 @@ theorem carrier.asIdeal.prime : (carrier.asIdeal f_deg hm q).IsPrime := rw [← and_forall_ne nx, and_iff_left, ← and_forall_ne ny, and_iff_left] · apply q.2.mem_or_mem; convert hxy (nx + ny) using 1 dsimp - simp_rw [proj_apply, decompose_of_mem_same 𝒜 hnx, decompose_of_mem_same 𝒜 hny, + simp_rw [decompose_of_mem_same 𝒜 hnx, decompose_of_mem_same 𝒜 hny, decompose_of_mem_same 𝒜 (SetLike.GradedMonoid.toGradedMul.mul_mem hnx hny), mul_pow, pow_add] simp only [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk'', @@ -552,7 +552,7 @@ theorem carrier.asIdeal.prime : (carrier.asIdeal f_deg hm q).IsPrime := all_goals intro n hn; convert q.1.zero_mem using 1 rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk'', - HomogeneousLocalization.zero_val]; simp_rw [proj_apply, Subtype.coe_mk] + HomogeneousLocalization.zero_val]; simp_rw [proj_apply] convert mk_zero (S := Submonoid.powers f) _ rw [decompose_of_mem_ne 𝒜 _ hn.symm, zero_pow hm] · first | exact hnx | exact hny diff --git a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean index 9349fc372809f..8f4240ecd8b3f 100644 --- a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean +++ b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean @@ -371,7 +371,6 @@ theorem zeroLocus_vanishingIdeal_eq_closure (t : Set (ProjectiveSpectrum 𝒜)) theorem vanishingIdeal_closure (t : Set (ProjectiveSpectrum 𝒜)) : vanishingIdeal (closure t) = vanishingIdeal t := by have := (gc_ideal 𝒜).u_l_u_eq_u t - dsimp only at this ext1 erw [zeroLocus_vanishingIdeal_eq_closure 𝒜 t] at this exact this diff --git a/Mathlib/AlgebraicTopology/CechNerve.lean b/Mathlib/AlgebraicTopology/CechNerve.lean index f0924fae68709..8545d54209844 100644 --- a/Mathlib/AlgebraicTopology/CechNerve.lean +++ b/Mathlib/AlgebraicTopology/CechNerve.lean @@ -151,7 +151,6 @@ def cechNerveEquiv (X : SimplicialObject.Augmented C) (F : Arrow C) : invFun := equivalenceRightToLeft _ _ left_inv := by intro A - dsimp ext · dsimp erw [WidePullback.lift_π] @@ -167,7 +166,6 @@ def cechNerveEquiv (X : SimplicialObject.Augmented C) (F : Arrow C) : · rfl right_inv := by intro A - dsimp ext x : 2 · refine' WidePullback.hom_ext _ _ _ (fun j => _) _ · dsimp @@ -309,7 +307,6 @@ def cechConerveEquiv (F : Arrow C) (X : CosimplicialObject.Augmented C) : invFun := equivalenceRightToLeft _ _ left_inv := by intro A - dsimp ext x : 2 · rfl · refine' WidePushout.hom_ext _ _ _ (fun j => _) _ diff --git a/Mathlib/AlgebraicTopology/ExtraDegeneracy.lean b/Mathlib/AlgebraicTopology/ExtraDegeneracy.lean index de232ef8a3f9e..ef3f477b8fce6 100644 --- a/Mathlib/AlgebraicTopology/ExtraDegeneracy.lean +++ b/Mathlib/AlgebraicTopology/ExtraDegeneracy.lean @@ -335,7 +335,6 @@ noncomputable def extraDegeneracy : SimplicialObject.Augmented.ExtraDegeneracy f subst hk erw [Fin.succ_succAbove_succ, ExtraDegeneracy.s_comp_π_succ, ExtraDegeneracy.s_comp_π_succ] - dsimp simp only [WidePullback.lift_π] · simp only [assoc, WidePullback.lift_base] erw [ExtraDegeneracy.s_comp_base, ExtraDegeneracy.s_comp_base] @@ -354,7 +353,6 @@ noncomputable def extraDegeneracy : SimplicialObject.Augmented.ExtraDegeneracy f subst hk erw [Fin.succ_predAbove_succ, ExtraDegeneracy.s_comp_π_succ, ExtraDegeneracy.s_comp_π_succ] - dsimp simp only [WidePullback.lift_π] · simp only [assoc, WidePullback.lift_base] erw [ExtraDegeneracy.s_comp_base, ExtraDegeneracy.s_comp_base] diff --git a/Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean b/Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean index d2f3fa94f1477..6afc4ab4c9e32 100644 --- a/Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean +++ b/Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean @@ -264,8 +264,7 @@ theorem trans_assoc_reparam {x₀ x₁ x₂ x₃ : X} (p : Path x₀ x₁) (q : linarith · exfalso linarith - · simp only [h₁, if_false, dif_neg (show ¬False from id)] - congr + · congr ring #align path.homotopy.trans_assoc_reparam Path.Homotopy.trans_assoc_reparam diff --git a/Mathlib/AlgebraicTopology/FundamentalGroupoid/Product.lean b/Mathlib/AlgebraicTopology/FundamentalGroupoid/Product.lean index 74b7b6379704b..f3d83ec1bf215 100644 --- a/Mathlib/AlgebraicTopology/FundamentalGroupoid/Product.lean +++ b/Mathlib/AlgebraicTopology/FundamentalGroupoid/Product.lean @@ -173,7 +173,6 @@ def prodToProdTop : πₓ A × πₓ B ⥤ πₓ (TopCat.of (A × B)) where map_id := by rintro ⟨x₀, x₁⟩ simp only [CategoryTheory.prod_id, FundamentalGroupoid.id_eq_path_refl] - dsimp rfl map_comp {x y z} f g := match x, y, z, f, g with diff --git a/Mathlib/AlgebraicTopology/SplitSimplicialObject.lean b/Mathlib/AlgebraicTopology/SplitSimplicialObject.lean index 0dd4200680eed..52939154bd404 100644 --- a/Mathlib/AlgebraicTopology/SplitSimplicialObject.lean +++ b/Mathlib/AlgebraicTopology/SplitSimplicialObject.lean @@ -97,7 +97,6 @@ instance : Fintype (IndexSet Δ) := simp only [unop_op, Sigma.mk.inj_iff, Fin.mk.injEq] at h₁ have h₂ : Δ₁ = Δ₂ := by ext1 - simp at h₁ simpa only [Fin.mk_eq_mk] using h₁.1 subst h₂ refine' ext _ _ rfl _ diff --git a/Mathlib/Analysis/Analytic/Composition.lean b/Mathlib/Analysis/Analytic/Composition.lean index ed9da17f5812f..a4665617df85c 100644 --- a/Mathlib/Analysis/Analytic/Composition.lean +++ b/Mathlib/Analysis/Analytic/Composition.lean @@ -972,7 +972,6 @@ theorem sigma_pi_composition_eq_iff ofFn fun i : Fin (Composition.length a') => (b' i).blocks.sum at this simpa [Composition.blocks_sum, Composition.ofFn_blocksFun] using this induction h - simp only [true_and_iff, eq_self_iff_true, heq_iff_eq] ext1 · rfl · simp only [heq_eq_eq, ofFn_inj] at H ⊢ @@ -1170,8 +1169,7 @@ def sigmaEquivSigmaPi (n : ℕ) : rw [get_of_eq (splitWrtComposition_join _ _ _)] · simp only [get_ofFn] rfl - · simp only [map_ofFn] - congr + · congr · simp only [map_ofFn] rfl #align composition.sigma_equiv_sigma_pi Composition.sigmaEquivSigmaPi diff --git a/Mathlib/Analysis/Analytic/Inverse.lean b/Mathlib/Analysis/Analytic/Inverse.lean index c3974f76adc1a..bdd6be7b4d0ef 100644 --- a/Mathlib/Analysis/Analytic/Inverse.lean +++ b/Mathlib/Analysis/Analytic/Inverse.lean @@ -434,7 +434,6 @@ theorem radius_right_inv_pos_of_radius_pos_aux1 (n : ℕ) (p : ℕ → ℝ) (hp MultilinearMap.map_sum_finset (MultilinearMap.mkPiAlgebra ℝ (Fin j) ℝ) fun _ (m : ℕ) => r * (a ^ m * p m)] simp only [MultilinearMap.mkPiAlgebra_apply] - dsimp simp [prod_const, ← mul_sum, mul_pow] #align formal_multilinear_series.radius_right_inv_pos_of_radius_pos_aux1 FormalMultilinearSeries.radius_right_inv_pos_of_radius_pos_aux1 diff --git a/Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean b/Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean index 3a76efa0bc3e0..938b8e6ea7857 100644 --- a/Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean +++ b/Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean @@ -237,7 +237,6 @@ theorem u_exists : · have I1 : x ∉ support f := by rwa [f_support] have I2 : -x ∉ support f := by rw [f_support] - simp only at hx simpa using hx simp only [mem_support, Classical.not_not] at I1 I2 simp only [I1, I2, add_zero, zero_div] @@ -459,7 +458,6 @@ theorem y_pos_of_mem_ball {D : ℝ} {x : E} (Dpos : 0 < D) (D_lt_one : D < 1) apply closedBall_subset_closedBall' _ (ball_subset_closedBall hy) rw [← one_smul ℝ x, dist_eq_norm, hz, ← sub_smul, one_smul, norm_smul, ID] simp only [B.ne', div_le_iff B, field_simps] - simp only [mem_ball_zero_iff] at hx nlinarith only [hx, D_lt_one] apply lt_of_lt_of_le _ (measure_mono C) apply measure_ball_pos diff --git a/Mathlib/Analysis/Calculus/LHopital.lean b/Mathlib/Analysis/Calculus/LHopital.lean index 6084306d73d50..5f5aa29bfe0bc 100644 --- a/Mathlib/Analysis/Calculus/LHopital.lean +++ b/Mathlib/Analysis/Calculus/LHopital.lean @@ -80,7 +80,6 @@ theorem lhopital_zero_right_on_Ioo (hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x have cmp : ∀ x ∈ Ioo a b, a < c x ∧ c x < x := fun x hx => (hc x hx).1 rw [← nhdsWithin_Ioo_eq_nhdsWithin_Ioi hab] apply tendsto_nhdsWithin_congr this - simp only apply hdiv.comp refine' tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ (tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds diff --git a/Mathlib/Analysis/Convex/Between.lean b/Mathlib/Analysis/Convex/Between.lean index 92453eee513c5..00e26e73b4711 100644 --- a/Mathlib/Analysis/Convex/Between.lean +++ b/Mathlib/Analysis/Convex/Between.lean @@ -530,7 +530,6 @@ theorem Sbtw.affineCombination_of_mem_affineSpan_pair [NoZeroDivisors R] [NoZero (s.affineCombination R p w₂) := by rw [affineCombination_mem_affineSpan_pair ha hw hw₁ hw₂] at h rcases h with ⟨r, hr⟩ - dsimp only at hr 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] @@ -630,7 +629,6 @@ theorem sbtw_of_sbtw_of_sbtw_of_mem_affineSpan_pair [NoZeroSMulDivisors R V] have h₂s := sign_eq_of_affineCombination_mem_affineSpan_single_lineMap t.Independent hw (Finset.mem_univ _) (Finset.mem_univ _) (Finset.mem_univ _) h₁₂.symm h₂₃ h₁₃ hr₂0 hr₂1 h₂' - dsimp only at h₁s h₂s rw [← Finset.univ.affineCombination_affineCombinationSingleWeights R t.points (Finset.mem_univ i₁), ← Finset.univ.affineCombination_affineCombinationLineMapWeights t.points (Finset.mem_univ _) diff --git a/Mathlib/Analysis/Convex/Side.lean b/Mathlib/Analysis/Convex/Side.lean index 0e498e678b216..646076298811e 100644 --- a/Mathlib/Analysis/Convex/Side.lean +++ b/Mathlib/Analysis/Convex/Side.lean @@ -765,7 +765,7 @@ theorem sOppSide_lineMap_right {s : AffineSubspace R P} {x y : P} (hx : x ∈ s) theorem setOf_wSameSide_eq_image2 {s : AffineSubspace R P} {x p : P} (hx : x ∉ s) (hp : p ∈ s) : { y | s.WSameSide x y } = Set.image2 (fun (t : R) q => t • (x -ᵥ p) +ᵥ q) (Set.Ici 0) s := by ext y - simp_rw [Set.mem_setOf, Set.mem_image2, Set.mem_Ici, mem_coe] + simp_rw [Set.mem_setOf, Set.mem_image2, Set.mem_Ici] constructor · rw [wSameSide_iff_exists_left hp, or_iff_right hx] rintro ⟨p₂, hp₂, h | h | ⟨r₁, r₂, hr₁, hr₂, h⟩⟩ @@ -784,7 +784,7 @@ theorem setOf_wSameSide_eq_image2 {s : AffineSubspace R P} {x p : P} (hx : x ∉ theorem setOf_sSameSide_eq_image2 {s : AffineSubspace R P} {x p : P} (hx : x ∉ s) (hp : p ∈ s) : { y | s.SSameSide x y } = Set.image2 (fun (t : R) q => t • (x -ᵥ p) +ᵥ q) (Set.Ioi 0) s := by ext y - simp_rw [Set.mem_setOf, Set.mem_image2, Set.mem_Ioi, mem_coe] + simp_rw [Set.mem_setOf, Set.mem_image2, Set.mem_Ioi] constructor · rw [sSameSide_iff_exists_left hp] rintro ⟨-, hy, p₂, hp₂, h | h | ⟨r₁, r₂, hr₁, hr₂, h⟩⟩ @@ -802,7 +802,7 @@ theorem setOf_sSameSide_eq_image2 {s : AffineSubspace R P} {x p : P} (hx : x ∉ theorem setOf_wOppSide_eq_image2 {s : AffineSubspace R P} {x p : P} (hx : x ∉ s) (hp : p ∈ s) : { y | s.WOppSide x y } = Set.image2 (fun (t : R) q => t • (x -ᵥ p) +ᵥ q) (Set.Iic 0) s := by ext y - simp_rw [Set.mem_setOf, Set.mem_image2, Set.mem_Iic, mem_coe] + simp_rw [Set.mem_setOf, Set.mem_image2, Set.mem_Iic] constructor · rw [wOppSide_iff_exists_left hp, or_iff_right hx] rintro ⟨p₂, hp₂, h | h | ⟨r₁, r₂, hr₁, hr₂, h⟩⟩ @@ -821,7 +821,7 @@ theorem setOf_wOppSide_eq_image2 {s : AffineSubspace R P} {x p : P} (hx : x ∉ theorem setOf_sOppSide_eq_image2 {s : AffineSubspace R P} {x p : P} (hx : x ∉ s) (hp : p ∈ s) : { y | s.SOppSide x y } = Set.image2 (fun (t : R) q => t • (x -ᵥ p) +ᵥ q) (Set.Iio 0) s := by ext y - simp_rw [Set.mem_setOf, Set.mem_image2, Set.mem_Iio, mem_coe] + simp_rw [Set.mem_setOf, Set.mem_image2, Set.mem_Iio] constructor · rw [sOppSide_iff_exists_left hp] rintro ⟨-, hy, p₂, hp₂, h | h | ⟨r₁, r₂, hr₁, hr₂, h⟩⟩ diff --git a/Mathlib/Analysis/Distribution/SchwartzSpace.lean b/Mathlib/Analysis/Distribution/SchwartzSpace.lean index 76966c9771875..c5828fe999a0c 100644 --- a/Mathlib/Analysis/Distribution/SchwartzSpace.lean +++ b/Mathlib/Analysis/Distribution/SchwartzSpace.lean @@ -629,7 +629,6 @@ theorem _root_.Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform_aux {f · simp only [Finset.le_sup'_iff, le_max_iff] right exact ⟨N, hN, rfl.le⟩ - simp_rw [Real.rpow_nat_cast] refine' pow_le_pow (by simp only [le_add_iff_nonneg_right, norm_nonneg]) _ exact Finset.le_sup hN #align function.has_temperate_growth.norm_iterated_fderiv_le_uniform_aux Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform_aux diff --git a/Mathlib/Analysis/Fourier/PoissonSummation.lean b/Mathlib/Analysis/Fourier/PoissonSummation.lean index 467fe64ff188e..aab09219a031b 100644 --- a/Mathlib/Analysis/Fourier/PoissonSummation.lean +++ b/Mathlib/Analysis/Fourier/PoissonSummation.lean @@ -92,7 +92,7 @@ theorem Real.fourierCoeff_tsum_comp_add {f : C(ℝ, ℂ)} suffices Integrable (e * f) from this.hasSum_intervalIntegral_comp_add_int.tsum_eq apply integrable_of_summable_norm_Icc convert hf ⟨Icc 0 1, isCompact_Icc⟩ using 1 - simp_rw [ContinuousMap.comp_apply, mul_comp] at eadd ⊢ + simp_rw [mul_comp] at eadd ⊢ simp_rw [eadd] exact funext fun n => neK ⟨Icc 0 1, isCompact_Icc⟩ _ -- Minor tidying to finish diff --git a/Mathlib/Analysis/InnerProductSpace/OfNorm.lean b/Mathlib/Analysis/InnerProductSpace/OfNorm.lean index c07adb4e1e9f4..b454e58cbd10c 100644 --- a/Mathlib/Analysis/InnerProductSpace/OfNorm.lean +++ b/Mathlib/Analysis/InnerProductSpace/OfNorm.lean @@ -219,14 +219,14 @@ private theorem add_left_aux7 (y z : E) : 2 * (‖(I : 𝕜) • y + z‖ * ‖(I : 𝕜) • y + z‖ + ‖z‖ * ‖z‖) - ‖(I : 𝕜) • y‖ * ‖(I : 𝕜) • y‖ := by apply eq_sub_of_add_eq have h₀ := parallelogram_identity ((I : 𝕜) • y + z) z - convert h₀ using 4 <;> · try simp only [two_smul, smul_add]; abel + convert h₀ using 4 <;> · (try simp only [two_smul, smul_add]); abel private theorem add_left_aux8 (y z : E) : ‖(I : 𝕜) • y - 2 • z‖ * ‖(I : 𝕜) • y - 2 • z‖ = 2 * (‖(I : 𝕜) • y - z‖ * ‖(I : 𝕜) • y - z‖ + ‖z‖ * ‖z‖) - ‖(I : 𝕜) • y‖ * ‖(I : 𝕜) • y‖ := by apply eq_sub_of_add_eq' have h₀ := parallelogram_identity ((I : 𝕜) • y - z) z - convert h₀ using 4 <;> · try simp only [two_smul, smul_add]; abel + convert h₀ using 4 <;> · (try simp only [two_smul, smul_add]); abel theorem add_left (x y z : E) : inner_ 𝕜 (x + y) z = inner_ 𝕜 x z + inner_ 𝕜 y z := by simp only [inner_, ← mul_add] diff --git a/Mathlib/Analysis/InnerProductSpace/Projection.lean b/Mathlib/Analysis/InnerProductSpace/Projection.lean index e1336692a8457..39c29e513d3a8 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection.lean @@ -1332,7 +1332,7 @@ theorem OrthogonalFamily.projection_directSum_coeAddHom [DecidableEq ι] {V : ι · rw [orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, DFinsupp.single_eq_of_ne hij.symm] exact hV.isOrtho hij.symm x.prop - · simp_rw [map_add, DFinsupp.add_apply] + · simp_rw [map_add] exact congr_arg₂ (· + ·) hx hy #align orthogonal_family.projection_direct_sum_coe_add_hom OrthogonalFamily.projection_directSum_coeAddHom diff --git a/Mathlib/Analysis/Matrix.lean b/Mathlib/Analysis/Matrix.lean index b1cb7f7ca1aa6..b06c9d6a41ac2 100644 --- a/Mathlib/Analysis/Matrix.lean +++ b/Mathlib/Analysis/Matrix.lean @@ -116,9 +116,8 @@ theorem norm_map_eq (A : Matrix m n α) (f : α → β) (hf : ∀ a, ‖f a‖ = #align matrix.norm_map_eq Matrix.norm_map_eq @[simp] -theorem nnnorm_transpose (A : Matrix m n α) : ‖Aᵀ‖₊ = ‖A‖₊ := by - simp_rw [Pi.nnnorm_def] - exact Finset.sup_comm _ _ _ +theorem nnnorm_transpose (A : Matrix m n α) : ‖Aᵀ‖₊ = ‖A‖₊ := + Finset.sup_comm _ _ _ #align matrix.nnnorm_transpose Matrix.nnnorm_transpose @[simp] diff --git a/Mathlib/Analysis/NormedSpace/Exponential.lean b/Mathlib/Analysis/NormedSpace/Exponential.lean index b4d9eca711564..2a7ac26ed6b6a 100644 --- a/Mathlib/Analysis/NormedSpace/Exponential.lean +++ b/Mathlib/Analysis/NormedSpace/Exponential.lean @@ -312,7 +312,7 @@ theorem map_exp_of_mem_ball {F} [RingHomClass F 𝔸 𝔹] (f : F) (hf : Continu rw [exp_eq_tsum, exp_eq_tsum] refine' ((expSeries_summable_of_mem_ball' _ hx).hasSum.map f hf).tsum_eq.symm.trans _ dsimp only [Function.comp] - simp_rw [one_div, map_inv_nat_cast_smul f 𝕂 𝕂, map_pow] + simp_rw [map_inv_nat_cast_smul f 𝕂 𝕂, map_pow] #align map_exp_of_mem_ball map_exp_of_mem_ball end CompleteAlgebra diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm.lean index 78986cad68e03..67f03d179db58 100644 --- a/Mathlib/Analysis/NormedSpace/OperatorNorm.lean +++ b/Mathlib/Analysis/NormedSpace/OperatorNorm.lean @@ -399,8 +399,8 @@ instance toSeminormedAddCommGroup : SeminormedAddCommGroup (E →SL[σ₁₂] F) theorem nnnorm_def (f : E →SL[σ₁₂] F) : ‖f‖₊ = sInf { c | ∀ x, ‖f x‖₊ ≤ c * ‖x‖₊ } := by ext rw [NNReal.coe_sInf, coe_nnnorm, norm_def, NNReal.coe_image] - simp_rw [← NNReal.coe_le_coe, NNReal.coe_mul, coe_nnnorm, mem_setOf_eq, Subtype.coe_mk, - exists_prop, NNReal.coe_mk, exists_prop] + simp_rw [← NNReal.coe_le_coe, NNReal.coe_mul, coe_nnnorm, mem_setOf_eq, NNReal.coe_mk, + exists_prop] #align continuous_linear_map.nnnorm_def ContinuousLinearMap.nnnorm_def /-- If one controls the norm of every `A x`, then one controls the norm of `A`. -/ diff --git a/Mathlib/Analysis/NormedSpace/PiLp.lean b/Mathlib/Analysis/NormedSpace/PiLp.lean index bb5ae9281658e..1f3f81f2fb4ad 100644 --- a/Mathlib/Analysis/NormedSpace/PiLp.lean +++ b/Mathlib/Analysis/NormedSpace/PiLp.lean @@ -597,8 +597,8 @@ theorem norm_sq_eq_of_L2 (β : ι → Type*) [∀ i, SeminormedAddCommGroup (β theorem dist_eq_of_L2 {β : ι → Type*} [∀ i, SeminormedAddCommGroup (β i)] (x y : PiLp 2 β) : dist x y = (∑ i, dist (x i) (y i) ^ 2).sqrt := by - simp_rw [dist_eq_norm, norm_eq_of_L2, Pi.sub_apply] - rfl -- Porting note: `Pi.sub_apply` doesn't work + simp_rw [dist_eq_norm, norm_eq_of_L2] + rfl #align pi_Lp.dist_eq_of_L2 PiLp.dist_eq_of_L2 theorem nndist_eq_of_L2 {β : ι → Type*} [∀ i, SeminormedAddCommGroup (β i)] (x y : PiLp 2 β) : @@ -700,10 +700,9 @@ def _root_.LinearIsometryEquiv.piLpCongrLeft (e : ι ≃ ι') : -- Porting note: this avoids spurious `x` and `y` arguments clear x y rcases p.dichotomy with (rfl | h) - · simp_rw [norm_eq_ciSup, LinearEquiv.piCongrLeft'_apply 𝕜 (fun _ : ι => E) e x' _] + · simp_rw [norm_eq_ciSup] exact e.symm.iSup_congr fun _ => rfl · simp only [norm_eq_sum (zero_lt_one.trans_le h)] - simp_rw [LinearEquiv.piCongrLeft'_apply 𝕜 (fun _ : ι => E) e x' _] congr 1 exact Fintype.sum_equiv e.symm _ _ fun _ => rfl #align linear_isometry_equiv.pi_Lp_congr_left LinearIsometryEquiv.piLpCongrLeft diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean index 50890e45beaff..698b52d8fafbb 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean @@ -300,8 +300,7 @@ theorem arg_of_im_neg {z : ℂ} (hz : z.im < 0) : arg z = -Real.arccos (z.re / a theorem arg_conj (x : ℂ) : arg (conj x) = if arg x = π then π else -arg x := by simp_rw [arg_eq_pi_iff, arg, neg_im, conj_im, conj_re, abs_conj, neg_div, neg_neg, - Real.arcsin_neg, apply_ite Neg.neg, neg_add, neg_sub, neg_neg, ← sub_eq_add_neg, sub_neg_eq_add, - add_comm π] + Real.arcsin_neg] rcases lt_trichotomy x.re 0 with (hr | hr | hr) <;> rcases lt_trichotomy x.im 0 with (hi | hi | hi) · simp [hr, hr.not_le, hi.le, hi.ne, not_le.2 hi, add_comm] diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Log.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Log.lean index aae4a82f31d57..69f5cd6dd87fd 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/Log.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/Log.lean @@ -121,7 +121,7 @@ theorem log_inv_eq_ite (x : ℂ) : log x⁻¹ = if x.arg = π then -conj (log x) · simp [hx] rw [inv_def, log_mul_ofReal, Real.log_inv, ofReal_neg, ← sub_eq_neg_add, log_conj_eq_ite] · simp_rw [log, map_add, map_mul, conj_ofReal, conj_I, normSq_eq_abs, Real.log_pow, - Nat.cast_two, ofReal_mul, ofReal_bit0, ofReal_one, neg_add, mul_neg, two_mul, neg_neg] + Nat.cast_two, ofReal_mul, neg_add, mul_neg, neg_neg] norm_num; rw [two_mul] -- Porting note: added to simplify `↑2` split_ifs · rw [add_sub_right_comm, sub_add_cancel'] diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean index bf7a8eff94db9..8a771ad00cf5c 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean @@ -224,12 +224,11 @@ theorem partialGamma_add_one {s : ℂ} (hs : 0 < s.re) {X : ℝ} (hX : 0 ≤ X) (Gamma_integrand_deriv_integrable_B hs hX), intervalIntegral.integral_neg, neg_add, neg_neg] at int_eval rw [eq_sub_of_add_eq int_eval, sub_neg_eq_add, neg_sub, add_comm, add_sub] - simp only [sub_left_inj, add_left_inj] have : (fun x => (-x).exp * (s * x ^ (s - 1)) : ℝ → ℂ) = (fun x => s * (-x).exp * x ^ (s - 1) : ℝ → ℂ) := by ext1; ring rw [this] have t := @integral_const_mul 0 X volume _ _ s fun x : ℝ => (-x).exp * x ^ (s - 1) - dsimp at t; rw [← t, ofReal_zero, zero_cpow] + rw [← t, ofReal_zero, zero_cpow] · rw [MulZeroClass.mul_zero, add_zero]; congr 2; ext1; ring · contrapose! hs; rw [hs, zero_re] #align complex.partial_Gamma_add_one Complex.partialGamma_add_one diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean index 320359cff17a8..25e9dc7f9a30b 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean @@ -190,7 +190,6 @@ theorem betaIntegral_recurrence {u v : ℂ} (hu : 0 < re u) (hv : 0 < re v) : ring have h_int := ((betaIntegral_convergent hu hv').const_mul u).sub ((betaIntegral_convergent hu' hv).const_mul v) - dsimp only at h_int rw [add_sub_cancel, add_sub_cancel] at h_int have int_ev := intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le zero_le_one hc hder h_int have hF0 : F 0 = 0 := by diff --git a/Mathlib/Analysis/SpecialFunctions/Gaussian.lean b/Mathlib/Analysis/SpecialFunctions/Gaussian.lean index 732ccc913ce90..c7e94b2d77c81 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gaussian.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gaussian.lean @@ -544,7 +544,7 @@ theorem _root_.fourier_transform_gaussian_pi (hb : 0 < b.re) : convert _root_.fourier_transform_gaussian h1 (-2 * π * t) using 1 · congr 1 with x : 1 congr 2 - all_goals push_cast; ring + any_goals push_cast; ring · conv_lhs => rw [mul_comm] congr 2 · field_simp [ofReal_ne_zero.mpr pi_ne_zero]; ring diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean index e00b490099797..bc3c0f0cfc140 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean @@ -32,7 +32,7 @@ theorem cos_eq_zero_iff {θ : ℂ} : cos θ = 0 ↔ ∃ k : ℤ, θ = (2 * k + 1 have h : (exp (θ * I) + exp (-θ * I)) / 2 = 0 ↔ exp (2 * θ * I) = -1 := by rw [@div_eq_iff _ _ (exp (θ * I) + exp (-θ * I)) 2 0 two_ne_zero, MulZeroClass.zero_mul, add_eq_zero_iff_eq_neg, neg_eq_neg_one_mul, ← div_eq_iff (exp_ne_zero _), ← exp_sub] - field_simp only; congr 3; ring_nf + congr 3; ring_nf rw [cos, h, ← exp_pi_mul_I, exp_eq_exp_iff_exists_int, mul_right_comm] refine' exists_congr fun x => _ refine' (iff_of_eq <| congr_arg _ _).trans (mul_right_inj' <| mul_ne_zero two_ne_zero I_ne_zero) diff --git a/Mathlib/CategoryTheory/Abelian/LeftDerived.lean b/Mathlib/CategoryTheory/Abelian/LeftDerived.lean index 59e3cb2ec6b2f..6ba9646fbadb8 100644 --- a/Mathlib/CategoryTheory/Abelian/LeftDerived.lean +++ b/Mathlib/CategoryTheory/Abelian/LeftDerived.lean @@ -102,8 +102,6 @@ theorem leftDerivedZeroToSelfApp_comp_inv [EnoughProjectives C] [PreservesFinite rw [Category.assoc, Category.assoc, Category.assoc] convert Category.comp_id (leftDerivedObjIso F 0 P).hom rw [← Category.assoc, ← Category.assoc, Iso.comp_inv_eq] - -- Porting note: working around 'motive is not type correct' - simp only [Category.id_comp] -- Porting note: broken ext apply homology.hom_from_ext simp only [← Category.assoc] diff --git a/Mathlib/CategoryTheory/CofilteredSystem.lean b/Mathlib/CategoryTheory/CofilteredSystem.lean index 1def9bd3daced..b7479641f1790 100644 --- a/Mathlib/CategoryTheory/CofilteredSystem.lean +++ b/Mathlib/CategoryTheory/CofilteredSystem.lean @@ -246,7 +246,7 @@ theorem IsMittagLeffler.toPreimages (h : F.IsMittagLeffler) : (F.toPreimages s). rw [mem_preimage, ← map_comp_apply, h₄, ← Category.assoc, map_comp_apply, h₃, ← map_comp_apply] apply mem_iInter.1 hx - · simp_rw [toPreimages_map, MapsTo.val_restrict_apply, Subtype.coe_mk] + · simp_rw [toPreimages_map, MapsTo.val_restrict_apply] rw [← Category.assoc, map_comp_apply, h₃, map_comp_apply] #align category_theory.functor.is_mittag_leffler.to_preimages CategoryTheory.Functor.IsMittagLeffler.toPreimages diff --git a/Mathlib/CategoryTheory/DifferentialObject.lean b/Mathlib/CategoryTheory/DifferentialObject.lean index 5e655b1bc7fc8..440bd01778d6e 100644 --- a/Mathlib/CategoryTheory/DifferentialObject.lean +++ b/Mathlib/CategoryTheory/DifferentialObject.lean @@ -137,8 +137,8 @@ instance hasZeroMorphisms : HasZeroMorphisms (DifferentialObject S C) where def isoApp {X Y : DifferentialObject S C} (f : X ≅ Y) : X.obj ≅ Y.obj where hom := f.hom.f inv := f.inv.f - hom_inv_id := by dsimp; rw [← comp_f, Iso.hom_inv_id, id_f] - inv_hom_id := by dsimp; rw [← comp_f, Iso.inv_hom_id, id_f] + hom_inv_id := by rw [← comp_f, Iso.hom_inv_id, id_f] + inv_hom_id := by rw [← comp_f, Iso.inv_hom_id, id_f] #align category_theory.differential_object.iso_app CategoryTheory.DifferentialObject.isoApp @[simp] @@ -162,7 +162,6 @@ def mkIso {X Y : DifferentialObject S C} (f : X.obj ≅ Y.obj) (hf : X.d ≫ f.h X ≅ Y where hom := ⟨f.hom, hf⟩ inv := ⟨f.inv, by - dsimp rw [← Functor.mapIso_inv, Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp, Functor.mapIso_hom, hf]⟩ hom_inv_id := by ext1; dsimp; exact f.hom_inv_id diff --git a/Mathlib/CategoryTheory/IsConnected.lean b/Mathlib/CategoryTheory/IsConnected.lean index 92f5f9c812989..30cfa82be7052 100644 --- a/Mathlib/CategoryTheory/IsConnected.lean +++ b/Mathlib/CategoryTheory/IsConnected.lean @@ -184,7 +184,6 @@ theorem IsConnected.of_induct [Nonempty J] {j₀ : J} have w := h { j | F j = F j₀ } rfl (fun {j₁} {j₂} f => by change F j₁ = F j₀ ↔ F j₂ = F j₀ simp [a f];) - dsimp at w intro j j' rw [w j, w j'] #align category_theory.is_connected.of_induct CategoryTheory.IsConnected.of_induct diff --git a/Mathlib/CategoryTheory/Limits/Cones.lean b/Mathlib/CategoryTheory/Limits/Cones.lean index 89b76c38d326e..2336d0efb66a3 100644 --- a/Mathlib/CategoryTheory/Limits/Cones.lean +++ b/Mathlib/CategoryTheory/Limits/Cones.lean @@ -441,7 +441,7 @@ instance functorialityFull [Full G] [Faithful G] : Full (functoriality F G) wher instance functorialityFaithful [Faithful G] : Faithful (Cones.functoriality F G) where map_injective {c} {c'} f g e := by apply ConeMorphism.ext f g - let f := ConeMorphism.mk.inj e; dsimp [functoriality] + let f := ConeMorphism.mk.inj e apply G.map_injective f #align category_theory.limits.cones.functoriality_faithful CategoryTheory.Limits.Cones.functorialityFaithful diff --git a/Mathlib/CategoryTheory/Limits/Final.lean b/Mathlib/CategoryTheory/Limits/Final.lean index 9f4afb0a07227..db7b2c8ccbb2f 100644 --- a/Mathlib/CategoryTheory/Limits/Final.lean +++ b/Mathlib/CategoryTheory/Limits/Final.lean @@ -424,7 +424,6 @@ theorem cofinal_of_colimit_comp_coyoneda_iso_pUnit exact ⟨StructuredArrow.mk y⟩ apply zigzag_isConnected rintro ⟨⟨⟨⟩⟩, X₁, f₁⟩ ⟨⟨⟨⟩⟩, X₂, f₂⟩ - dsimp at * let y₁ := colimit.ι (F ⋙ coyoneda.obj (op d)) X₁ f₁ let y₂ := colimit.ι (F ⋙ coyoneda.obj (op d)) X₂ f₂ have e : y₁ = y₂ := by diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean index f998f0aa2745a..327d6861096d5 100644 --- a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean +++ b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean @@ -69,7 +69,6 @@ instance (priority := 100) preservesZeroMorphisms_of_isLeftAdjoint (F : C ⥤ D) PreservesZeroMorphisms F where map_zero X Y := by let adj := Adjunction.ofLeftAdjoint F - dsimp calc F.map (0 : X ⟶ Y) = F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y) := ?_ _ = F.map 0 ≫ F.map ((rightAdjoint F).map (0 : F.obj X ⟶ _)) ≫ adj.counit.app (F.obj Y) := ?_ diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Images.lean b/Mathlib/CategoryTheory/Limits/Shapes/Images.lean index 9d1a1b36c035d..9ab47764eda15 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Images.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Images.lean @@ -110,7 +110,6 @@ theorem ext {F F' : MonoFactorisation f} (hI : F.I = F'.I) cases' F with _ Fm _ _ Ffac; cases' F' with _ Fm' _ _ Ffac' cases' hI simp at hm - dsimp at Ffac Ffac' congr · apply (cancel_mono Fm).1 rw [Ffac, hm, Ffac'] diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean b/Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean index 3bfdc277992f1..51b865a3857eb 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean @@ -638,10 +638,10 @@ noncomputable def ofSigmaCofork (c : Cofork I.fstSigmaMap I.sndSigmaMap) : Multi | WalkingMultispan.left a => (Sigma.ι I.left a : _) ≫ I.fstSigmaMap ≫ c.π | WalkingMultispan.right b => (Sigma.ι I.right b : _) ≫ c.π naturality := by - rintro (_ | _) (_ | _) (_ | _ | _) <;> dsimp + rintro (_ | _) (_ | _) (_ | _ | _) · simp · simp - · dsimp; rw [c.condition]; simp + · simp [c.condition] · simp } #align category_theory.limits.multicofork.of_sigma_cofork CategoryTheory.Limits.Multicofork.ofSigmaCofork diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean b/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean index f4b12a1c650fc..0719f61e130bf 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean @@ -518,7 +518,6 @@ every morphism out of it is a monomorphism. -/ theorem InitialMonoClass.of_isInitial {I : C} (hI : IsInitial I) (h : ∀ X, Mono (hI.to X)) : InitialMonoClass C where isInitial_mono_from {I'} X hI' := by - dsimp rw [hI'.hom_ext (hI'.to X) ((hI'.uniqueUpToIso hI).hom ≫ hI.to X)] apply mono_comp #align category_theory.limits.initial_mono_class.of_is_initial CategoryTheory.Limits.InitialMonoClass.of_isInitial diff --git a/Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean b/Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean index 4fbc467cdc9cd..450770693988f 100644 --- a/Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean +++ b/Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean @@ -71,9 +71,8 @@ def limitConeIsLimit (F : J ⥤ Mon_ C) : IsLimit (limitCone F) where { hom := limit.lift (F ⋙ Mon_.forget C) ((Mon_.forget C).mapCone s) mul_hom := by dsimp - ext; simp; dsimp - slice_rhs 1 2 => - rw [← MonoidalCategory.tensor_comp, limit.lift_π] } + ext; simp + slice_rhs 1 2 => rw [← MonoidalCategory.tensor_comp, limit.lift_π] } fac s h := by ext; simp uniq s m w := by ext1 diff --git a/Mathlib/CategoryTheory/Pi/Basic.lean b/Mathlib/CategoryTheory/Pi/Basic.lean index f3b9c80f79956..e5a77ced14518 100644 --- a/Mathlib/CategoryTheory/Pi/Basic.lean +++ b/Mathlib/CategoryTheory/Pi/Basic.lean @@ -172,11 +172,8 @@ variable {C} pair of corresponding components. -/ @[simps] def isoApp {X Y : ∀ i, C i} (f : X ≅ Y) (i : I) : X i ≅ Y i := - ⟨f.hom i, f.inv i, by - dsimp - rw [← comp_apply, Iso.hom_inv_id, id_apply], by - dsimp - rw [← comp_apply, Iso.inv_hom_id, id_apply]⟩ + ⟨f.hom i, f.inv i, + by rw [← comp_apply, Iso.hom_inv_id, id_apply], by rw [← comp_apply, Iso.inv_hom_id, id_apply]⟩ #align category_theory.pi.iso_app CategoryTheory.Pi.isoApp @[simp] diff --git a/Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean b/Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean index 4aa21d0e645d8..63441d9970a99 100644 --- a/Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean +++ b/Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean @@ -100,7 +100,6 @@ noncomputable def matrixDecomposition (o : HomOrthogonal s) {α β : Type} [Fint right_inv z := by ext i ⟨j, w⟩ ⟨k, ⟨⟩⟩ simp only [eqToHom_refl, biproduct.matrix_components, Category.id_comp] - simp only [Set.mem_preimage, Set.mem_singleton_iff] split_ifs with h · simp · exfalso diff --git a/Mathlib/CategoryTheory/Preadditive/Mat.lean b/Mathlib/CategoryTheory/Preadditive/Mat.lean index ba1051530a64f..9a77d14ea5c8f 100644 --- a/Mathlib/CategoryTheory/Preadditive/Mat.lean +++ b/Mathlib/CategoryTheory/Preadditive/Mat.lean @@ -387,7 +387,6 @@ lemma additiveObjIsoBiproduct_hom_π (F : Mat_ C ⥤ D) [Functor.Additive F] (M F.map (M.isoBiproductEmbedding.hom ≫ biproduct.π _ i) := by dsimp [additiveObjIsoBiproduct] rw [biproduct.lift_π, Category.assoc] - dsimp [Functor.mapBiproduct] erw [biproduct.lift_π, ← F.map_comp] simp diff --git a/Mathlib/CategoryTheory/Shift/Basic.lean b/Mathlib/CategoryTheory/Shift/Basic.lean index cb103ad902033..ee271249d1311 100644 --- a/Mathlib/CategoryTheory/Shift/Basic.lean +++ b/Mathlib/CategoryTheory/Shift/Basic.lean @@ -73,7 +73,7 @@ structure ShiftMkCore where /-- compatibility with the associativity -/ assoc_hom_app : ∀ (m₁ m₂ m₃ : A) (X : C), (add (m₁ + m₂) m₃).hom.app X ≫ (F m₃).map ((add m₁ m₂).hom.app X) = - eqToHom (by dsimp; rw [add_assoc]) ≫ (add m₁ (m₂ + m₃)).hom.app X ≫ + eqToHom (by rw [add_assoc]) ≫ (add m₁ (m₂ + m₃)).hom.app X ≫ (add m₂ m₃).hom.app ((F m₁).obj X) := by aesop_cat /-- compatibility with the left addition with 0 -/ zero_add_hom_app : ∀ (n : A) (X : C), (add 0 n).hom.app X = @@ -93,7 +93,7 @@ attribute [reassoc] assoc_hom_app lemma assoc_inv_app (h : ShiftMkCore C A) (m₁ m₂ m₃ : A) (X : C) : (h.F m₃).map ((h.add m₁ m₂).inv.app X) ≫ (h.add (m₁ + m₂) m₃).inv.app X = (h.add m₂ m₃).inv.app ((h.F m₁).obj X) ≫ (h.add m₁ (m₂ + m₃)).inv.app X ≫ - eqToHom (by dsimp; rw [add_assoc]) := by + eqToHom (by rw [add_assoc]) := by rw [← cancel_mono ((h.add (m₁ + m₂) m₃).hom.app X ≫ (h.F m₃).map ((h.add m₁ m₂).hom.app X)), Category.assoc, Category.assoc, Category.assoc, Iso.inv_hom_id_app_assoc, ← Functor.map_comp, Iso.inv_hom_id_app, Functor.map_id, h.assoc_hom_app, eqToHom_trans_assoc, eqToHom_refl, diff --git a/Mathlib/CategoryTheory/Sites/Canonical.lean b/Mathlib/CategoryTheory/Sites/Canonical.lean index 86165ecd14684..cab20f66d040c 100644 --- a/Mathlib/CategoryTheory/Sites/Canonical.lean +++ b/Mathlib/CategoryTheory/Sites/Canonical.lean @@ -134,7 +134,6 @@ theorem isSheafFor_trans (P : Cᵒᵖ ⥤ Type v) (R S : Sieve X) apply Presieve.isSheafFor_subsieve_aux P this apply isSheafFor_bind _ _ _ hR hS · intro Y f hf Z g - dsimp rw [← pullback_comp] apply (hS (R.downward_closed hf _)).isSeparatedFor · intro Y f hf diff --git a/Mathlib/CategoryTheory/Sites/LeftExact.lean b/Mathlib/CategoryTheory/Sites/LeftExact.lean index 94697086ee4f2..7e3df8e2fa48d 100644 --- a/Mathlib/CategoryTheory/Sites/LeftExact.lean +++ b/Mathlib/CategoryTheory/Sites/LeftExact.lean @@ -168,7 +168,7 @@ theorem liftToPlusObjLimitObj_fac {K : Type max v u} [SmallCategory K] [FinCateg rw [limit.lift_π] dsimp rw [ι_colimitLimitIso_limit_π_assoc] - simp_rw [← NatTrans.comp_app, ← Category.assoc, ← NatTrans.comp_app] + simp_rw [← Category.assoc, ← NatTrans.comp_app] rw [limit.lift_π, Category.assoc] congr 1 rw [← Iso.comp_inv_eq] diff --git a/Mathlib/CategoryTheory/Sites/Plus.lean b/Mathlib/CategoryTheory/Sites/Plus.lean index e089700358f9b..4dcf4be32d7a1 100644 --- a/Mathlib/CategoryTheory/Sites/Plus.lean +++ b/Mathlib/CategoryTheory/Sites/Plus.lean @@ -278,7 +278,6 @@ theorem isIso_toPlus_of_isSheaf (hP : Presheaf.IsSheaf J P) : IsIso (J.toPlus P) suffices : ∀ X, IsIso ((J.toPlus P).app X) · apply NatIso.isIso_of_isIso_app intro X - dsimp suffices : IsIso (colimit.ι (J.diagram P X.unop) (op ⊤)) · apply IsIso.comp_isIso suffices : ∀ (S T : (J.Cover X.unop)ᵒᵖ) (f : S ⟶ T), IsIso ((J.diagram P X.unop).map f) diff --git a/Mathlib/CategoryTheory/Sites/Sheaf.lean b/Mathlib/CategoryTheory/Sites/Sheaf.lean index dad0467df405a..a3c35e2a64a83 100644 --- a/Mathlib/CategoryTheory/Sites/Sheaf.lean +++ b/Mathlib/CategoryTheory/Sites/Sheaf.lean @@ -615,12 +615,11 @@ def isSheafForIsSheafFor' (P : Cᵒᵖ ⥤ A) (s : A ⥤ Type max v₁ u₁) · refine' limit.hom_ext (fun j => _) dsimp [Equalizer.Presieve.firstMap, firstMap] simp only [limit.lift_π, map_lift_piComparison, assoc, Fan.mk_π_app, Functor.map_comp] - dsimp [Equalizer.Presieve.firstMap, firstMap] - erw [piComparison_comp_π_assoc] + rw [piComparison_comp_π_assoc] · refine' limit.hom_ext (fun j => _) dsimp [Equalizer.Presieve.secondMap, secondMap] simp only [limit.lift_π, map_lift_piComparison, assoc, Fan.mk_π_app, Functor.map_comp] - erw [piComparison_comp_π_assoc] + rw [piComparison_comp_π_assoc] · dsimp simp · refine' Fork.ext (Iso.refl _) _ diff --git a/Mathlib/Combinatorics/Additive/Behrend.lean b/Mathlib/Combinatorics/Additive/Behrend.lean index ad41b9cd0f82a..4bf8c1bd7495f 100644 --- a/Mathlib/Combinatorics/Additive/Behrend.lean +++ b/Mathlib/Combinatorics/Additive/Behrend.lean @@ -465,7 +465,6 @@ theorem bound (hN : 4096 ≤ N) : (N : ℝ) ^ (1 / nValue N : ℝ) / exp 1 < dVa rw [cast_pos] exact hN.trans_lt' (by norm_num1) refine' le_trans _ this - simp only [cast_one] rw [← div_le_iff'] · exact log_two_gt_d9.le.trans' (by norm_num1) · norm_num1 diff --git a/Mathlib/Combinatorics/Configuration.lean b/Mathlib/Combinatorics/Configuration.lean index a2f496019d4d6..34ff37de56738 100644 --- a/Mathlib/Combinatorics/Configuration.lean +++ b/Mathlib/Combinatorics/Configuration.lean @@ -149,7 +149,7 @@ theorem Nondegenerate.exists_injective_of_card_le [Nondegenerate P L] [Fintype P have hs₂ : (s.biUnion t)ᶜ.card ≤ 1 := by -- At most one line through two points of `s` refine' Finset.card_le_one_iff.mpr @fun p₁ p₂ hp₁ hp₂ => _ - simp_rw [Finset.mem_compl, Finset.mem_biUnion, exists_prop, not_exists, not_and, + simp_rw [Finset.mem_compl, Finset.mem_biUnion, not_exists, not_and, Set.mem_toFinset, Set.mem_setOf_eq, Classical.not_not] at hp₁ hp₂ obtain ⟨l₁, l₂, hl₁, hl₂, hl₃⟩ := Finset.one_lt_card_iff.mp (Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hs₀, hs₁⟩) diff --git a/Mathlib/Combinatorics/Hall/Finite.lean b/Mathlib/Combinatorics/Hall/Finite.lean index 6bf149aae00a6..6a3afeeec7bfb 100644 --- a/Mathlib/Combinatorics/Hall/Finite.lean +++ b/Mathlib/Combinatorics/Hall/Finite.lean @@ -210,7 +210,7 @@ theorem hall_hard_inductive_step_B {n : ℕ} (hn : Fintype.card ι = n + 1) · refine' hf'.dite _ hf'' (@fun x x' => im_disj x x' _ _) · intro x simp only [of_eq_true] - split_ifs with h <;> simp + split_ifs with h · exact hsf' ⟨x, h⟩ · exact sdiff_subset _ _ (hsf'' ⟨x, h⟩) set_option linter.uppercaseLean3 false in diff --git a/Mathlib/Combinatorics/Quiver/Cast.lean b/Mathlib/Combinatorics/Quiver/Cast.lean index c4da00bdf69f6..dac1648d64d79 100644 --- a/Mathlib/Combinatorics/Quiver/Cast.lean +++ b/Mathlib/Combinatorics/Quiver/Cast.lean @@ -147,8 +147,9 @@ theorem hom_cast_eq_of_cons_eq_cons {u v v' w : U} {p : Path u v} {p' : Path u v theorem eq_nil_of_length_zero {u v : U} (p : Path u v) (hzero : p.length = 0) : p.cast (eq_of_length_zero p hzero) rfl = Path.nil := by - cases p <;> simp only [Nat.succ_ne_zero, length_cons] at hzero - rfl + cases p + · rfl + · simp only [Nat.succ_ne_zero, length_cons] at hzero #align quiver.eq_nil_of_length_zero Quiver.eq_nil_of_length_zero end Quiver diff --git a/Mathlib/Combinatorics/SetFamily/Compression/UV.lean b/Mathlib/Combinatorics/SetFamily/Compression/UV.lean index d2cfb386c0d28..b87145e412540 100644 --- a/Mathlib/Combinatorics/SetFamily/Compression/UV.lean +++ b/Mathlib/Combinatorics/SetFamily/Compression/UV.lean @@ -208,7 +208,6 @@ theorem card_compression (u v : α) (s : Finset α) : (𝓒 u v s).card = s.card · rw [disjoint_iff_inter_eq_empty] exact filter_inter_filter_neg_eq _ _ _ intro a ha b hb hab - dsimp at hab rw [mem_coe, mem_filter, Function.comp_apply] at ha hb rw [compress] at ha hab split_ifs at ha hab with has diff --git a/Mathlib/Computability/DFA.lean b/Mathlib/Computability/DFA.lean index 45c8b101859a7..142a0e5ab6d48 100644 --- a/Mathlib/Computability/DFA.lean +++ b/Mathlib/Computability/DFA.lean @@ -110,7 +110,6 @@ theorem evalFrom_split [Fintype σ] {x : List α} {s t : σ} (hlen : Fintype.car wlog hle : (n : ℕ) ≤ m · exact this _ hlen hx _ _ hneq.symm heq.symm (le_of_not_le hle) have hm : (m : ℕ) ≤ Fintype.card σ := Fin.is_le m - dsimp at heq refine' ⟨M.evalFrom s ((x.take m).take n), (x.take m).take n, (x.take m).drop n, x.drop m, _, _, _, by rfl, _⟩ diff --git a/Mathlib/Computability/Halting.lean b/Mathlib/Computability/Halting.lean index e14b2bc1ac51a..f08c76313733e 100644 --- a/Mathlib/Computability/Halting.lean +++ b/Mathlib/Computability/Halting.lean @@ -377,7 +377,6 @@ theorem rfindOpt {n} {f : Vector ℕ (n + 1) → ℕ} (hf : @Partrec' (n + 1) f) exists_congr fun a => (and_congr (iff_of_eq _) Iff.rfl).trans (and_congr_right fun h => _) · congr funext n - simp only [Part.some_inj, PFun.coe_val] cases f (n ::ᵥ v) <;> simp [Nat.succ_le_succ]; rfl · have := Nat.rfind_spec h simp only [Part.coe_some, Part.mem_some_iff] at this diff --git a/Mathlib/Computability/RegularExpressions.lean b/Mathlib/Computability/RegularExpressions.lean index ede9d2ac36b69..243b243d255bd 100644 --- a/Mathlib/Computability/RegularExpressions.lean +++ b/Mathlib/Computability/RegularExpressions.lean @@ -320,7 +320,7 @@ theorem star_rmatch_iff (P : RegularExpression α) : simp only [ne_eq, not_false_iff, true_and, rmatch] exact ht case tail ht' => exact helem t' ht' - · rintro ⟨S, hsum, helem⟩; dsimp + · rintro ⟨S, hsum, helem⟩ cases' x with a x · rfl · rw [rmatch, deriv, mul_rmatch_iff] diff --git a/Mathlib/Computability/TuringMachine.lean b/Mathlib/Computability/TuringMachine.lean index 8f9e98b441677..30890dff70be2 100644 --- a/Mathlib/Computability/TuringMachine.lean +++ b/Mathlib/Computability/TuringMachine.lean @@ -2560,7 +2560,6 @@ theorem tr_respects_aux₂ {k : K} {q : Stmt₂₁} {v : σ} {S : ∀ k, List ( dsimp only; simp; cases o <;> simp only [stWrite, stVar, trStAct, TM1.stepAux] case push f => have := Tape.write_move_right_n fun a : Γ' ↦ (a.1, update a.2 k (some (f v))) - dsimp only at this refine' ⟨_, fun k' ↦ _, by -- Porting note: `rw [...]` to `erw [...]; rfl`. @@ -2725,7 +2724,6 @@ theorem tr_respects : Respects (TM2.step M) (TM1.step (tr M)) TrCfg := by theorem trCfg_init (k) (L : List (Γ k)) : TrCfg (TM2.init k L) (TM1.init (trInit k L) : Cfg₂₁) := by rw [(_ : TM1.init _ = _)] · refine' ⟨ListBlank.mk (L.reverse.map fun a ↦ update default k (some a)), fun k' ↦ _⟩ - simp only [TM2.Cfg.stk, TM2.init] refine' ListBlank.ext fun i ↦ _ rw [ListBlank.map_mk, ListBlank.nth_mk, List.getI_eq_iget_get?, List.map_map] have : ((proj k').f ∘ fun a => update (β := fun k => Option (Γ k)) default k (some a)) diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean index 5adbc53883116..6ac6b0ce66598 100644 --- a/Mathlib/Data/Fin/Basic.lean +++ b/Mathlib/Data/Fin/Basic.lean @@ -1689,7 +1689,6 @@ theorem castPred_one : castPred (1 : Fin (n + 2)) = 1 := by theorem predAbove_zero {i : Fin (n + 2)} (hi : i ≠ 0) : predAbove 0 i = i.pred hi := by dsimp [predAbove] rw [dif_pos] - simp only [castSucc_zero] exact pos_iff_ne_zero.mpr hi #align fin.pred_above_zero Fin.predAbove_zero diff --git a/Mathlib/Data/Fin/VecNotation.lean b/Mathlib/Data/Fin/VecNotation.lean index 71fabfcba777d..33154f6b9f496 100644 --- a/Mathlib/Data/Fin/VecNotation.lean +++ b/Mathlib/Data/Fin/VecNotation.lean @@ -326,7 +326,6 @@ theorem vecAlt0_vecAppend (v : Fin n → α) : vecAlt0 rfl (vecAppend rfl v v) = simp_rw [Function.comp, bit0, vecAlt0, vecAppend_eq_ite] split_ifs with h <;> congr · rw [Fin.val_mk] at h - simp only [Fin.ext_iff, Fin.val_add, Fin.val_mk] exact (Nat.mod_eq_of_lt h).symm · rw [Fin.val_mk, not_lt] at h simp only [Fin.ext_iff, Fin.val_add, Fin.val_mk, Nat.mod_eq_sub_mod h] @@ -344,9 +343,8 @@ theorem vecAlt1_vecAppend (v : Fin (n + 1) → α) : vecAlt1 rfl (vecAppend rfl simp only [Nat.zero_eq, zero_add, Nat.lt_one_iff] at hi; subst i; rfl | succ n => split_ifs with h <;> simp_rw [bit1, bit0] <;> congr - · simp only [Fin.ext_iff, Fin.val_add, Fin.val_mk] - rw [Fin.val_mk] at h - erw [Nat.mod_eq_of_lt (Nat.lt_of_succ_lt h)] + · rw [Fin.val_mk] at h + rw [Nat.mod_eq_of_lt (Nat.lt_of_succ_lt h)] erw [Nat.mod_eq_of_lt h] · rw [Fin.val_mk, not_lt] at h simp only [Fin.ext_iff, Fin.val_add, Fin.val_mk, Nat.mod_add_mod, Fin.val_one, diff --git a/Mathlib/Data/List/OfFn.lean b/Mathlib/Data/List/OfFn.lean index ed2a607e14962..5cb4f31b57c4a 100644 --- a/Mathlib/Data/List/OfFn.lean +++ b/Mathlib/Data/List/OfFn.lean @@ -186,7 +186,6 @@ theorem ofFn_get : ∀ l : List α, (ofFn (get l)) = l | a :: l => by rw [ofFn_succ] congr - simp only [Fin.val_succ] exact ofFn_get l set_option linter.deprecated false in diff --git a/Mathlib/Data/List/Pairwise.lean b/Mathlib/Data/List/Pairwise.lean index df7275326a434..e825d1a939e89 100644 --- a/Mathlib/Data/List/Pairwise.lean +++ b/Mathlib/Data/List/Pairwise.lean @@ -432,7 +432,7 @@ theorem forall_mem_pwFilter (neg_trans : ∀ {x y z}, R x z → R x y ∨ R y z) ⟨by induction' l with x l IH; · exact fun _ _ h => (not_mem_nil _ h).elim simp only [forall_mem_cons] - by_cases h : ∀ y ∈ pwFilter R l, R x y <;> dsimp at h + by_cases h : ∀ y ∈ pwFilter R l, R x y · simp only [pwFilter_cons_of_pos h, forall_mem_cons, and_imp] exact fun r H => ⟨r, IH H⟩ · rw [pwFilter_cons_of_neg h] diff --git a/Mathlib/Data/List/Perm.lean b/Mathlib/Data/List/Perm.lean index 820353bff3ea2..a4dc836e18bea 100644 --- a/Mathlib/Data/List/Perm.lean +++ b/Mathlib/Data/List/Perm.lean @@ -239,11 +239,9 @@ theorem Perm.filterMap (f : α → Option β) {l₁ l₂ : List α} (p : l₁ ~ induction p with | nil => simp | cons x _p IH => - simp only [filterMap] cases h : f x <;> simp [h, filterMap, IH, Perm.cons] | swap x y l₂ => - simp only [filterMap] cases hx : f x <;> cases hy : f y <;> simp [hx, hy, filterMap, swap] @@ -1295,8 +1293,7 @@ theorem perm_permutations'Aux_comm (a b : α) (l : List α) : theorem Perm.permutations' {s t : List α} (p : s ~ t) : permutations' s ~ permutations' t := by induction' p with a s t _ IH a b l s t u _ _ IH₁ IH₂; · simp - · simp only [permutations'] - exact IH.bind_right _ + · exact IH.bind_right _ · dsimp [permutations'] rw [bind_assoc, bind_assoc] apply Perm.bind_left diff --git a/Mathlib/Data/List/Sublists.lean b/Mathlib/Data/List/Sublists.lean index e8442e5f2e8b7..c20a0d329a103 100644 --- a/Mathlib/Data/List/Sublists.lean +++ b/Mathlib/Data/List/Sublists.lean @@ -60,7 +60,6 @@ theorem sublists'Aux_eq_array_foldl (a : α) : ∀ (r₁ r₂ : List (List α)), theorem sublists'_eq_sublists'Aux (l : List α) : sublists' l = l.foldr (fun a r => sublists'Aux a r r) [[]] := by simp only [sublists', sublists'Aux_eq_array_foldl] - dsimp only rw [← List.foldr_hom Array.toList] · rfl · intros _ _; congr <;> simp diff --git a/Mathlib/Data/Nat/Choose/Multinomial.lean b/Mathlib/Data/Nat/Choose/Multinomial.lean index b340eaeb772d7..e36fa5b43e1c2 100644 --- a/Mathlib/Data/Nat/Choose/Multinomial.lean +++ b/Mathlib/Data/Nat/Choose/Multinomial.lean @@ -129,7 +129,6 @@ theorem binomial_succ_succ [DecidableEq α] (h : a ≠ b) : h, Ne.def, ite_true, ite_false] rw [if_neg h.symm] rw [add_succ, choose_succ_succ, succ_add_eq_succ_add] - simp only ring #align nat.binomial_succ_succ Nat.binomial_succ_succ diff --git a/Mathlib/Data/Nat/Squarefree.lean b/Mathlib/Data/Nat/Squarefree.lean index 69cbc3d401db2..a87bdd040cb6c 100644 --- a/Mathlib/Data/Nat/Squarefree.lean +++ b/Mathlib/Data/Nat/Squarefree.lean @@ -279,7 +279,6 @@ theorem divisors_filter_squarefree {n : ℕ} (h0 : n ≠ 0) : rw [Finset.mem_powerset, ← Finset.val_le_iff, Multiset.toFinset_val] at hs have hs0 : s.val.prod ≠ 0 := by rw [Ne.def, Multiset.prod_eq_zero_iff] - simp only [exists_prop, id.def, exists_eq_right] intro con apply not_irreducible_zero diff --git a/Mathlib/Data/PFun.lean b/Mathlib/Data/PFun.lean index 065b807d7bbb1..4bd2825be72e6 100644 --- a/Mathlib/Data/PFun.lean +++ b/Mathlib/Data/PFun.lean @@ -270,8 +270,8 @@ theorem mem_fix_iff {f : α →. Sum β α} {a : α} {b : β} : rw [WellFounded.fixFEq] at h₂ simp at h₂ cases' h₂ with h₂ h₃ - split at h₃ <;> simp at h₃ - next e => subst b; refine' Or.inl ⟨h₂, e⟩ + split at h₃ + next e => simp at h₃; subst b; refine' Or.inl ⟨h₂, e⟩ next e => exact Or.inr ⟨_, ⟨_, e⟩, Part.mem_assert _ h₃⟩, fun h => by simp [fix] diff --git a/Mathlib/Data/PFunctor/Multivariate/W.lean b/Mathlib/Data/PFunctor/Multivariate/W.lean index 96546cfd09ae1..443b329e048b4 100644 --- a/Mathlib/Data/PFunctor/Multivariate/W.lean +++ b/Mathlib/Data/PFunctor/Multivariate/W.lean @@ -219,7 +219,7 @@ theorem w_ind {α : TypeVec n} {C : P.W α → Prop} (∀ i, C (f i)) → C (P.wMk a f' f)) : ∀ x, C x := by intro x; cases' x with a f - apply @wp_ind n P α fun a f => C ⟨a, f⟩; dsimp + apply @wp_ind n P α fun a f => C ⟨a, f⟩ intro a f f' ih' dsimp [wMk] at ih let ih'' := ih a (P.wPathDestLeft f') fun i => ⟨f i, P.wPathDestRight f' i⟩ diff --git a/Mathlib/Data/PNat/Factors.lean b/Mathlib/Data/PNat/Factors.lean index 6954589a0b2c2..c36cb520eec71 100644 --- a/Mathlib/Data/PNat/Factors.lean +++ b/Mathlib/Data/PNat/Factors.lean @@ -213,7 +213,6 @@ theorem prod_ofPNatList (l : List ℕ+) (h) : (ofPNatList l h).prod = l.prod := /-- The product map gives a homomorphism from the additive monoid of multisets to the multiplicative monoid ℕ+. -/ theorem prod_zero : (0 : PrimeMultiset).prod = 1 := by - dsimp [Prod] exact Multiset.prod_zero #align prime_multiset.prod_zero PrimeMultiset.prod_zero diff --git a/Mathlib/Data/PNat/Prime.lean b/Mathlib/Data/PNat/Prime.lean index a0ab1dd035b05..ad9cc5364822d 100644 --- a/Mathlib/Data/PNat/Prime.lean +++ b/Mathlib/Data/PNat/Prime.lean @@ -296,7 +296,7 @@ theorem gcd_eq_left {m n : ℕ+} : m ∣ n → m.gcd n = m := by #align pnat.gcd_eq_left PNat.gcd_eq_left theorem Coprime.pow {m n : ℕ+} (k l : ℕ) (h : m.Coprime n) : (m ^ k).coprime (n ^ l) := by - rw [← coprime_coe] at *; simp only [pow_coe]; apply Nat.coprime.pow; apply h + rw [← coprime_coe] at *; apply Nat.coprime.pow; apply h #align pnat.coprime.pow PNat.Coprime.pow end Coprime diff --git a/Mathlib/Data/Polynomial/Degree/Lemmas.lean b/Mathlib/Data/Polynomial/Degree/Lemmas.lean index 198e580cd3198..7ae724bf9d8eb 100644 --- a/Mathlib/Data/Polynomial/Degree/Lemmas.lean +++ b/Mathlib/Data/Polynomial/Degree/Lemmas.lean @@ -232,8 +232,7 @@ theorem natDegree_sum_eq_of_disjoint (f : S → R[X]) (s : Finset S) have hs : s.Nonempty := ⟨x, hx⟩ refine' natDegree_eq_of_degree_eq_some _ rw [degree_sum_eq_of_disjoint] - · dsimp - rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, + · rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, Nat.cast_withBot, Finset.coe_sup' hs, ← Finset.sup'_eq_sup hs] refine' le_antisymm _ _ diff --git a/Mathlib/Data/Polynomial/UnitTrinomial.lean b/Mathlib/Data/Polynomial/UnitTrinomial.lean index 36f812e241b69..5df1e4a7ae08b 100644 --- a/Mathlib/Data/Polynomial/UnitTrinomial.lean +++ b/Mathlib/Data/Polynomial/UnitTrinomial.lean @@ -225,7 +225,7 @@ theorem irreducible_aux1 {k m n : ℕ} (hkm : k < m) (hmn : m < n) (u v w : Unit have key : n - m + k < n := by rwa [← lt_tsub_iff_right, tsub_lt_tsub_iff_left_of_le hmn.le] rw [hp, trinomial_mirror hkm hmn u.ne_zero w.ne_zero] simp_rw [trinomial_def, C_mul_X_pow_eq_monomial, add_mul, mul_add, monomial_mul_monomial, - toFinsupp_add, toFinsupp_monomial, Finsupp.filter_add] + toFinsupp_add, toFinsupp_monomial] -- Porting note: added next line (less powerful `simp`). rw [Finsupp.filter_add, Finsupp.filter_add, Finsupp.filter_add, Finsupp.filter_add, Finsupp.filter_add, Finsupp.filter_add, Finsupp.filter_add, Finsupp.filter_add] diff --git a/Mathlib/Data/QPF/Multivariate/Basic.lean b/Mathlib/Data/QPF/Multivariate/Basic.lean index 530e4c0f17cad..b7ea12ad971d4 100644 --- a/Mathlib/Data/QPF/Multivariate/Basic.lean +++ b/Mathlib/Data/QPF/Multivariate/Basic.lean @@ -133,7 +133,7 @@ theorem liftP_iff {α : TypeVec n} (p : ∀ ⦃i⦄, α i → Prop) (x : F α) : · rw [← hy, ← abs_repr y, h, ← abs_map]; rfl intro i j apply (f i j).property - rintro ⟨a, f, h₀, h₁⟩; dsimp at * + rintro ⟨a, f, h₀, h₁⟩ use abs ⟨a, fun i j => ⟨f i j, h₁ i j⟩⟩ rw [← abs_map, h₀]; rfl #align mvqpf.liftp_iff MvQPF.liftP_iff diff --git a/Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean b/Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean index 0f81c9bd5e7da..781048609589e 100644 --- a/Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean +++ b/Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean @@ -144,7 +144,6 @@ def Cofix.dest {α : TypeVec n} : Cofix F α → F (α.append1 (Cofix F α)) := intro x y h exact ⟨r, pr, h⟩ rw [← Quot.factor_mk_eq _ _ this] - dsimp conv => lhs rw [appendFun_comp_id, comp_map, ← abs_map, pr rxy, abs_map, ← comp_map, @@ -415,7 +414,6 @@ theorem liftR_map_last [lawful: LawfulMvFunctor F] apply ih simp only [lastFun_from_append1_drop_last, lastFun_toSubtype, lastFun_appendFun, lastFun_subtypeVal, comp.left_id, lastFun_comp, lastFun_prod] - dsimp ext1 rfl liftR_map _ _ _ _ (toSubtype _ ⊚ fromAppend1DropLast ⊚ c ⊚ b) hh diff --git a/Mathlib/Data/QPF/Univariate/Basic.lean b/Mathlib/Data/QPF/Univariate/Basic.lean index 444a30436dade..065a04c4fa94d 100644 --- a/Mathlib/Data/QPF/Univariate/Basic.lean +++ b/Mathlib/Data/QPF/Univariate/Basic.lean @@ -413,7 +413,6 @@ def Cofix.dest : Cofix F → F (Cofix F) := intro x y h exact ⟨r, pr, h⟩ rw [← Quot.factor_mk_eq _ _ this] - dsimp conv => lhs rw [comp_map, ← abs_map, pr rxy, abs_map, ← comp_map]) diff --git a/Mathlib/Data/Rat/Star.lean b/Mathlib/Data/Rat/Star.lean index 8f61ad3f7892e..5d6e0dfa75300 100644 --- a/Mathlib/Data/Rat/Star.lean +++ b/Mathlib/Data/Rat/Star.lean @@ -46,7 +46,6 @@ instance : StarOrderedRing ℚ := simp only [Function.const_apply, Finset.sum_const, Finset.card_range, nsmul_eq_mul] rw [← Int.cast_ofNat, Int.ofNat_mul, Int.coe_natAbs, abs_of_nonneg (num_nonneg_iff_zero_le.mpr hx), Int.cast_mul, Int.cast_ofNat] - simp only [Int.cast_mul, Int.cast_ofNat] rw [← mul_assoc, mul_assoc (x.num : ℚ), mul_one_div_cancel (Nat.cast_ne_zero.mpr x.pos.ne'), mul_one, mul_one_div, Rat.num_div_den] end Rat diff --git a/Mathlib/Data/Seq/Parallel.lean b/Mathlib/Data/Seq/Parallel.lean index 60e48e0bd1a2a..a003e07ea207b 100644 --- a/Mathlib/Data/Seq/Parallel.lean +++ b/Mathlib/Data/Seq/Parallel.lean @@ -307,7 +307,7 @@ theorem map_parallel (f : α → β) (S) : map f (parallel S) = parallel (S.map simp [parallel.aux1] rw [this] cases' parallel.aux2 l with a l' <;> simp - induction' S using WSeq.recOn with c S S <;> simp <;> simp [parallel.aux1] <;> + induction' S using WSeq.recOn with c S S <;> simp <;> exact ⟨_, _, rfl, rfl⟩ #align computation.map_parallel Computation.map_parallel diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean index b79f60ed4c9d4..9b9cade0f229d 100644 --- a/Mathlib/Data/Seq/Seq.lean +++ b/Mathlib/Data/Seq/Seq.lean @@ -342,7 +342,6 @@ def corec (f : β → Option (α × β)) (b : β) : Seq α := by theorem corec_eq (f : β → Option (α × β)) (b : β) : destruct (corec f b) = omap (corec f) (f b) := by dsimp [corec, destruct, nth] - dsimp -- porting note: next two lines were `change`...`with`... have h: Stream'.corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).1 := rfl rw [h] diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean index 9ae49a544d397..30d2c53c19cb4 100644 --- a/Mathlib/Data/Set/Card.lean +++ b/Mathlib/Data/Set/Card.lean @@ -794,7 +794,6 @@ theorem surj_on_of_inj_on_of_ncard_le {t : Set β} (f : ∀ a ∈ s, β) (hf : apply hinj _ _ hx hy hxy have hft := ht.fintype have hft' := Fintype.ofInjective f' finj - simp_rw [ncard_eq_toFinset_card] at hst set f'' : ∀ a, a ∈ s.toFinset → β := fun a h ↦ f a (by simpa using h) convert @Finset.surj_on_of_inj_on_of_card_le _ _ _ t.toFinset f'' _ _ _ _ (by simpa) · simp @@ -818,7 +817,6 @@ theorem inj_on_of_surj_on_of_ncard_le {t : Set β} (f : ∀ a ∈ s, β) (hf : exact ⟨_, ha, rfl⟩ haveI := hs.fintype haveI := Fintype.ofSurjective _ hsurj - simp_rw [ncard_eq_toFinset_card] at hst set f'' : ∀ a, a ∈ s.toFinset → β := fun a h ↦ f a (by simpa using h) exact @Finset.inj_on_of_surj_on_of_card_le _ _ _ t.toFinset f'' diff --git a/Mathlib/Data/Stream/Init.lean b/Mathlib/Data/Stream/Init.lean index b7d2a4d32c9cc..ca774e8916fb8 100644 --- a/Mathlib/Data/Stream/Init.lean +++ b/Mathlib/Data/Stream/Init.lean @@ -362,7 +362,6 @@ theorem map_iterate (f : α → α) (a : α) : iterate f (f a) = map f (iterate induction' n with n' ih · rfl · unfold map iterate nth - dsimp rw [map, nth] at ih rw [iterate] exact congrArg f ih diff --git a/Mathlib/FieldTheory/PolynomialGaloisGroup.lean b/Mathlib/FieldTheory/PolynomialGaloisGroup.lean index c8d7d90047a06..221626e506cfc 100644 --- a/Mathlib/FieldTheory/PolynomialGaloisGroup.lean +++ b/Mathlib/FieldTheory/PolynomialGaloisGroup.lean @@ -457,7 +457,7 @@ theorem card_complex_roots_eq_card_real_add_card_not_gal_inv (p : ℚ[X]) : intro z; rw [Set.mem_toFinset, mem_rootSet_of_ne hp] have hb : ∀ z : ℂ, z ∈ b ↔ aeval z p = 0 ∧ z.im = 0 := by intro z - simp_rw [Finset.mem_image, exists_prop, Set.mem_toFinset, mem_rootSet_of_ne hp] + simp_rw [Finset.mem_image, Set.mem_toFinset, mem_rootSet_of_ne hp] constructor · rintro ⟨w, hw, rfl⟩ exact ⟨by rw [aeval_algHom_apply, hw, AlgHom.map_zero], rfl⟩ @@ -472,7 +472,7 @@ theorem card_complex_roots_eq_card_real_add_card_not_gal_inv (p : ℚ[X]) : exact Complex.conj_eq_iff_im have hc : ∀ z : ℂ, z ∈ c ↔ aeval z p = 0 ∧ z.im ≠ 0 := by intro z - simp_rw [Finset.mem_image, exists_prop] + simp_rw [Finset.mem_image] constructor · rintro ⟨w, hw, rfl⟩ exact ⟨(mem_rootSet.mp w.2).2, mt (hc0 w).mpr (Equiv.Perm.mem_support.mp hw)⟩ diff --git a/Mathlib/Geometry/Euclidean/Circumcenter.lean b/Mathlib/Geometry/Euclidean/Circumcenter.lean index 2574a402d7752..7ba8c6dafdd8e 100644 --- a/Mathlib/Geometry/Euclidean/Circumcenter.lean +++ b/Mathlib/Geometry/Euclidean/Circumcenter.lean @@ -203,12 +203,12 @@ theorem _root_.AffineIndependent.existsUnique_dist_eq {ι : Type*} [hne : Nonemp use ⟨p i, 0⟩ simp only [Set.range_unique, AffineSubspace.mem_affineSpan_singleton] constructor - · simp_rw [hi default, Set.singleton_subset_iff, Sphere.mem_coe, mem_sphere, dist_self] + · simp_rw [hi default, Set.singleton_subset_iff] exact ⟨⟨⟩, by simp only [Metric.sphere_zero, Set.mem_singleton_iff]⟩ · rintro ⟨cc, cr⟩ simp only rintro ⟨rfl, hdist⟩ - simp [Set.singleton_subset_iff, Sphere.mem_coe, mem_sphere, dist_self] at hdist + simp [Set.singleton_subset_iff] at hdist rw [hi default, hdist] · have i := hne.some let ι2 := { x // x ≠ i } diff --git a/Mathlib/Geometry/Manifold/Instances/Real.lean b/Mathlib/Geometry/Manifold/Instances/Real.lean index d14a5f29c72a1..609f3188ef8bb 100644 --- a/Mathlib/Geometry/Manifold/Instances/Real.lean +++ b/Mathlib/Geometry/Manifold/Instances/Real.lean @@ -174,7 +174,7 @@ def IccLeftChart (x y : ℝ) [h : Fact (x < y)] : map_source' := by simp only [imp_self, sub_lt_sub_iff_right, mem_setOf_eq, forall_true_iff] map_target' := by simp only [min_lt_iff, mem_setOf_eq]; intro z hz; left - dsimp at hz; linarith + linarith left_inv' := by rintro ⟨z, hz⟩ h'z simp only [mem_setOf_eq, mem_Icc] at hz h'z @@ -223,7 +223,7 @@ def IccRightChart (x y : ℝ) [h : Fact (x < y)] : map_source' := by simp only [imp_self, mem_setOf_eq, sub_lt_sub_iff_left, forall_true_iff] map_target' := by simp only [lt_max_iff, mem_setOf_eq]; intro z hz; left - dsimp at hz; linarith + linarith left_inv' := by rintro ⟨z, hz⟩ h'z simp only [mem_setOf_eq, mem_Icc] at hz h'z diff --git a/Mathlib/GroupTheory/SchurZassenhaus.lean b/Mathlib/GroupTheory/SchurZassenhaus.lean index 10d03936bcf54..cb373081dc6bc 100644 --- a/Mathlib/GroupTheory/SchurZassenhaus.lean +++ b/Mathlib/GroupTheory/SchurZassenhaus.lean @@ -90,7 +90,7 @@ theorem smul_diff' (h : H) : letI := H.fintypeQuotientOfFiniteIndex rw [diff, diff, index_eq_card, ←Finset.card_univ, ←Finset.prod_const, ←Finset.prod_mul_distrib] refine' Finset.prod_congr rfl fun q _ => _ - simp_rw [Subtype.ext_iff, MonoidHom.id_apply, coe_mul, coe_mk, mul_assoc, mul_right_inj] + simp_rw [Subtype.ext_iff, MonoidHom.id_apply, coe_mul, mul_assoc, mul_right_inj] rw [smul_apply_eq_smul_apply_inv_smul, smul_eq_mul_unop, unop_op, mul_left_inj, ←Subtype.ext_iff, Equiv.apply_eq_iff_eq, inv_smul_eq_iff] exact self_eq_mul_right.mpr ((QuotientGroup.eq_one_iff _).mpr h.2) diff --git a/Mathlib/GroupTheory/Transfer.lean b/Mathlib/GroupTheory/Transfer.lean index 1f529a1250e2f..376081fd0cc9b 100644 --- a/Mathlib/GroupTheory/Transfer.lean +++ b/Mathlib/GroupTheory/Transfer.lean @@ -60,7 +60,7 @@ theorem diff_mul_diff : diff ϕ R S * diff ϕ S T = diff ϕ R T := (prod_congr rfl fun q _ => (ϕ.map_mul _ _).symm.trans (congr_arg ϕ - (by simp_rw [Subtype.ext_iff, coe_mul, coe_mk, mul_assoc, mul_inv_cancel_left]))) + (by simp_rw [Subtype.ext_iff, coe_mul, mul_assoc, mul_inv_cancel_left]))) #align subgroup.left_transversals.diff_mul_diff Subgroup.leftTransversals.diff_mul_diff #align add_subgroup.left_transversals.diff_add_diff AddSubgroup.leftTransversals.diff_add_diff @@ -83,7 +83,7 @@ theorem smul_diff_smul (g : G) : diff ϕ (g • S) (g • T) = diff ϕ S T := (fun _ _ => congr_arg ϕ (by - simp_rw [coe_mk, smul_apply_eq_smul_apply_inv_smul, smul_eq_mul, mul_inv_rev, mul_assoc, + simp_rw [smul_apply_eq_smul_apply_inv_smul, smul_eq_mul, mul_inv_rev, mul_assoc, inv_mul_cancel_left])) (fun q _ => g • q) (fun _ _ => mem_univ _) (fun q _ => smul_inv_smul g q) fun q _ => inv_smul_smul g q diff --git a/Mathlib/Init/Data/Nat/Lemmas.lean b/Mathlib/Init/Data/Nat/Lemmas.lean index 92a6b32d55518..b91f950c66540 100644 --- a/Mathlib/Init/Data/Nat/Lemmas.lean +++ b/Mathlib/Init/Data/Nat/Lemmas.lean @@ -819,9 +819,7 @@ lemma repr_length (n e : Nat) : 0 < e → n < 10 ^ e → (Nat.repr n).length <= | succ n => by_cases hterm : n.succ / 10 = 0 case pos => simp only [hterm, Nat.toDigitsCore]; assumption - case neg => - simp only [hterm] - exact to_digits_core_length 10 (by decide) (Nat.succ n + 1) (Nat.succ n) e he e0 + case neg => exact to_digits_core_length 10 (by decide) (Nat.succ n + 1) (Nat.succ n) e he e0 end Find diff --git a/Mathlib/LinearAlgebra/AffineSpace/Independent.lean b/Mathlib/LinearAlgebra/AffineSpace/Independent.lean index 0ef4b257f34aa..cf0410409315d 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/Independent.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/Independent.lean @@ -737,7 +737,6 @@ theorem sign_eq_of_affineCombination_mem_affineSpan_pair {p : ι → P} (h : Aff SignType.sign (w i) = SignType.sign (w j) := by rw [affineCombination_mem_affineSpan_pair h hw hw₁ hw₂] at hs rcases hs with ⟨r, hr⟩ - dsimp only at hr rw [hr i hi, hr j hj, hi0, hj0, add_zero, add_zero, sub_zero, sub_zero, sign_mul, sign_mul, hij] #align sign_eq_of_affine_combination_mem_affine_span_pair sign_eq_of_affineCombination_mem_affineSpan_pair diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean index 68f3ec6e0e33f..3558f2b162920 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean @@ -241,7 +241,6 @@ theorem even_induction {P : ∀ x, x ∈ evenOdd Q 0 → Prop} (zero_add (0 : ZMod 2) ▸ SetLike.mul_mem_graded (ι_mul_ι_mem_evenOdd_zero Q m₁ m₂) hx)) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0) : P x hx := by refine' evenOdd_induction Q 0 (fun rx => _) (@hadd) hιι_mul x hx - simp_rw [ZMod.val_zero, pow_zero] rintro ⟨r, rfl⟩ exact hr r #align clifford_algebra.even_induction CliffordAlgebra.even_induction diff --git a/Mathlib/LinearAlgebra/DirectSum/Finsupp.lean b/Mathlib/LinearAlgebra/DirectSum/Finsupp.lean index bba18b6d573a4..618f1f4108eac 100644 --- a/Mathlib/LinearAlgebra/DirectSum/Finsupp.lean +++ b/Mathlib/LinearAlgebra/DirectSum/Finsupp.lean @@ -65,13 +65,11 @@ theorem finsuppTensorFinsupp_apply (R M N ι κ : Sort _) [CommRing R] [AddCommG simp [tmul_add, hg₁, hg₂] · intro k' n simp only [finsuppTensorFinsupp_single] - simp only [Finsupp.single_apply] -- split_ifs; finish can close the goal from here by_cases h1 : (i', k') = (i, k) · simp only [Prod.mk.inj_iff] at h1 simp [h1] - · simp only [h1, if_false] - simp only [Prod.mk.inj_iff, not_and_or] at h1 + · simp only [Prod.mk.inj_iff, not_and_or] at h1 cases' h1 with h1 h1 <;> simp [h1] #align finsupp_tensor_finsupp_apply finsuppTensorFinsupp_apply diff --git a/Mathlib/LinearAlgebra/Dual.lean b/Mathlib/LinearAlgebra/Dual.lean index f90a2c1873657..d3e08937e1e2b 100644 --- a/Mathlib/LinearAlgebra/Dual.lean +++ b/Mathlib/LinearAlgebra/Dual.lean @@ -737,7 +737,6 @@ variable [DecidableEq ι] (h : DualBases e ε) theorem dual_lc (l : ι →₀ R) (i : ι) : ε i (DualBases.lc e l) = l i := by erw [LinearMap.map_sum] - simp_rw [map_smul] -- Porting note: cannot get at • -- simp only [h.eval, map_smul, smul_eq_mul] rw [Finset.sum_eq_single i] diff --git a/Mathlib/LinearAlgebra/Lagrange.lean b/Mathlib/LinearAlgebra/Lagrange.lean index 3909f5a8337ea..05553a88ddfa2 100644 --- a/Mathlib/LinearAlgebra/Lagrange.lean +++ b/Mathlib/LinearAlgebra/Lagrange.lean @@ -514,7 +514,7 @@ theorem eval_nodal_not_at_node (hx : ∀ i ∈ s, x ≠ v i) : eval x (nodal s v theorem nodal_eq_mul_nodal_erase [DecidableEq ι] (hi : i ∈ s) : nodal s v = (X - C (v i)) * nodal (s.erase i) v := by - simp_rw [nodal, mul_prod_erase _ _ hi, Finset.mul_prod_erase _ (fun x => X - C (v x)) hi] + simp_rw [nodal, Finset.mul_prod_erase _ (fun x => X - C (v x)) hi] #align lagrange.nodal_eq_mul_nodal_erase Lagrange.nodal_eq_mul_nodal_erase theorem X_sub_C_dvd_nodal (v : ι → F) (hi : i ∈ s) : X - C (v i) ∣ nodal s v := diff --git a/Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean b/Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean index 84dbed4634156..1bdedc9f6742c 100644 --- a/Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean +++ b/Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean @@ -163,7 +163,7 @@ theorem exists_mulVec_eq_zero_iff' {A : Type*} (K : Type*) [DecidableEq n] [Comm ((algebraMap A K).mapMatrix M).mulVec (algebraMap _ K b • v) i := ?_ _ = 0 := ?_ _ = algebraMap A K 0 := (RingHom.map_zero _).symm - · simp_rw [RingHom.map_mulVec, mulVec, dotProduct, Function.comp_apply, hf, Subtype.coe_mk, + · simp_rw [RingHom.map_mulVec, mulVec, dotProduct, Function.comp_apply, hf, RingHom.mapMatrix_apply, Pi.smul_apply, smul_eq_mul, Algebra.smul_def] · rw [mulVec_smul, mul_eq, Pi.smul_apply, Pi.zero_apply, smul_zero] #align matrix.exists_mul_vec_eq_zero_iff' Matrix.exists_mulVec_eq_zero_iff' diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean b/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean index 84eaa4690c291..ad1367a755eb1 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean @@ -168,7 +168,6 @@ theorem anisotropic_of_pi [Fintype ι] {R} [OrderedRing R] [∀ i, Module R (M theorem nonneg_pi_iff [Fintype ι] {R} [OrderedRing R] [∀ i, Module R (Mᵢ i)] {Q : ∀ i, QuadraticForm R (Mᵢ i)} : (∀ x, 0 ≤ pi Q x) ↔ ∀ i x, 0 ≤ Q i x := by simp_rw [pi, sum_apply, comp_apply, LinearMap.proj_apply] - dsimp only constructor -- TODO: does this generalize to a useful lemma independent of `QuadraticForm`? · intro h i x diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean b/Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean index 930da9db99284..0680af1130b20 100644 --- a/Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean +++ b/Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean @@ -156,7 +156,6 @@ theorem toDirectSum_tensorPower_tprod {n} (x : Fin n → M) : toDirectSum (tprod R M n x) = DirectSum.of _ n (PiTensorProduct.tprod R x) := by rw [tprod_apply, AlgHom.map_list_prod, List.map_ofFn] simp_rw [Function.comp, toDirectSum_ι] - dsimp only rw [DirectSum.list_prod_ofFn_of_eq_dProd] apply DirectSum.of_eq_of_gradedMonoid_eq rw [GradedMonoid.mk_list_dProd] diff --git a/Mathlib/LinearAlgebra/TensorPower.lean b/Mathlib/LinearAlgebra/TensorPower.lean index ab4d2229be0bd..a3dca84d41e27 100644 --- a/Mathlib/LinearAlgebra/TensorPower.lean +++ b/Mathlib/LinearAlgebra/TensorPower.lean @@ -169,8 +169,7 @@ variable {R} theorem one_mul {n} (a : (⨂[R]^n) M) : cast R M (zero_add n) (ₜ1 ₜ* a) = a := by rw [gMul_def, gOne_def] induction' a using PiTensorProduct.induction_on with r a x y hx hy - · dsimp only at a - rw [TensorProduct.tmul_smul, LinearEquiv.map_smul, LinearEquiv.map_smul, ← gMul_def, + · rw [TensorProduct.tmul_smul, LinearEquiv.map_smul, LinearEquiv.map_smul, ← gMul_def, tprod_mul_tprod, cast_tprod] congr 2 with i rw [Fin.elim0'_append] @@ -182,8 +181,7 @@ theorem one_mul {n} (a : (⨂[R]^n) M) : cast R M (zero_add n) (ₜ1 ₜ* a) = a theorem mul_one {n} (a : (⨂[R]^n) M) : cast R M (add_zero _) (a ₜ* ₜ1) = a := by rw [gMul_def, gOne_def] induction' a using PiTensorProduct.induction_on with r a x y hx hy - · dsimp only at a - rw [← TensorProduct.smul_tmul', LinearEquiv.map_smul, LinearEquiv.map_smul, ← gMul_def, + · rw [← TensorProduct.smul_tmul', LinearEquiv.map_smul, LinearEquiv.map_smul, ← gMul_def, tprod_mul_tprod R a _, cast_tprod] congr 2 with i rw [Fin.append_elim0'] diff --git a/Mathlib/Logic/Equiv/Embedding.lean b/Mathlib/Logic/Equiv/Embedding.lean index 14eccb6046825..351c7a8e7866c 100644 --- a/Mathlib/Logic/Equiv/Embedding.lean +++ b/Mathlib/Logic/Equiv/Embedding.lean @@ -37,11 +37,9 @@ def sumEmbeddingEquivProdEmbeddingDisjoint {α β γ : Type*} : rintro (a₁ | b₁) (a₂ | b₂) f_eq <;> simp only [Equiv.coe_fn_symm_mk, Sum.elim_inl, Sum.elim_inr] at f_eq · rw [f.injective f_eq] - · simp! only at f_eq - exfalso + · exfalso refine disj.le_bot ⟨⟨a₁, f_eq⟩, ⟨b₂, by simp [f_eq]⟩⟩ - · simp! only at f_eq - exfalso + · exfalso exact disj.le_bot ⟨⟨a₂, rfl⟩, ⟨b₁, f_eq⟩⟩ · rw [g.injective f_eq]⟩ left_inv f := by diff --git a/Mathlib/MeasureTheory/Constructions/Pi.lean b/Mathlib/MeasureTheory/Constructions/Pi.lean index 6a3dc552d678a..9618025b8281b 100644 --- a/Mathlib/MeasureTheory/Constructions/Pi.lean +++ b/Mathlib/MeasureTheory/Constructions/Pi.lean @@ -317,7 +317,6 @@ theorem pi_pi_aux [∀ i, SigmaFinite (μ i)] (s : ∀ i, Set (α i)) (hs : ∀ · rw [Measure.pi, toMeasure_apply _ _ (MeasurableSet.pi countable_univ fun i _ => hs i)] apply OuterMeasure.pi_pi_le · haveI : Encodable ι := Fintype.toEncodable ι - rw [← pi'_pi μ s] simp_rw [← pi'_pi μ s, Measure.pi, toMeasure_apply _ _ (MeasurableSet.pi countable_univ fun i _ => hs i)] suffices (pi' μ).toOuterMeasure ≤ OuterMeasure.pi fun i => (μ i).toOuterMeasure by exact this _ diff --git a/Mathlib/MeasureTheory/Decomposition/Lebesgue.lean b/Mathlib/MeasureTheory/Decomposition/Lebesgue.lean index faab629000866..566c66a8c4a97 100644 --- a/Mathlib/MeasureTheory/Decomposition/Lebesgue.lean +++ b/Mathlib/MeasureTheory/Decomposition/Lebesgue.lean @@ -442,7 +442,7 @@ theorem exists_positive_of_not_mutuallySingular (μ ν : Measure α) [IsFiniteMe -- since `μ` and `ν` are not mutually singular, `μ A = 0` implies `ν Aᶜ > 0` rw [MutuallySingular] at h; push_neg at h have := h _ hAmeas hμ - simp_rw [hA₁, compl_iInter, compl_compl] at this + simp_rw [compl_iInter, compl_compl] at this -- as `Aᶜ = ⋃ n, f n`, `ν Aᶜ > 0` implies there exists some `n` such that `ν (f n) > 0` obtain ⟨n, hn⟩ := exists_measure_pos_of_not_measure_iUnion_null this -- thus, choosing `f n` as the set `E` suffices diff --git a/Mathlib/MeasureTheory/Decomposition/UnsignedHahn.lean b/Mathlib/MeasureTheory/Decomposition/UnsignedHahn.lean index 4c5f8273e7ac8..a9407d075ef04 100644 --- a/Mathlib/MeasureTheory/Decomposition/UnsignedHahn.lean +++ b/Mathlib/MeasureTheory/Decomposition/UnsignedHahn.lean @@ -93,7 +93,7 @@ theorem hahn_decomposition [IsFiniteMeasure μ] [IsFiniteMeasure ν] : exact MeasurableSet.biInter (to_countable _) fun i _ => he₁ _ have f_subset_f : ∀ {a b c d}, a ≤ b → c ≤ d → f a d ⊆ f b c := by intro a b c d hab hcd - simp_rw [Finset.inf_eq_iInf, Finset.inf_eq_iInf] + simp_rw [Finset.inf_eq_iInf] exact biInter_subset_biInter_left (Finset.Ico_subset_Ico hab <| Nat.succ_le_succ hcd) have f_succ : ∀ n m, n ≤ m → f n (m + 1) = f n m ∩ e (m + 1) := by intro n m hnm diff --git a/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean b/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean index b05f907229a01..ab3b390a49088 100644 --- a/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean +++ b/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean @@ -270,7 +270,8 @@ theorem ae_nonneg_of_forall_set_integral_nonneg_of_stronglyMeasurable (hfm : Str by_contra h refine' (lt_self_iff_false (∫ x in s, f x ∂μ)).mp (h_int_gt.trans_lt _) refine' (mul_neg_iff.mpr (Or.inr ⟨hb_neg, _⟩)).trans_le _ - swap; · simp_rw [Measure.restrict_restrict hs]; exact hf_zero s hs mus + swap + · exact hf_zero s hs mus refine' ENNReal.toReal_nonneg.lt_of_ne fun h_eq => h _ cases' (ENNReal.toReal_eq_zero_iff _).mp h_eq.symm with hμs_eq_zero hμs_eq_top · exact hμs_eq_zero diff --git a/Mathlib/MeasureTheory/Function/LpSpace.lean b/Mathlib/MeasureTheory/Function/LpSpace.lean index a1b0bbcefe187..b96350926946c 100644 --- a/Mathlib/MeasureTheory/Function/LpSpace.lean +++ b/Mathlib/MeasureTheory/Function/LpSpace.lean @@ -1451,7 +1451,7 @@ private theorem snorm'_sum_norm_sub_le_tsum_of_cauchy_snorm' {f : ℕ → α → fun n => funext fun x => by simp rw [hgf_norm_diff] refine' (snorm'_sum_le (fun i _ => ((hf (i + 1)).sub (hf i)).norm) hp1).trans _ - simp_rw [← Pi.sub_apply, snorm'_norm] + simp_rw [snorm'_norm] refine' (Finset.sum_le_sum _).trans (sum_le_tsum _ (fun m _ => zero_le _) ENNReal.summable) exact fun m _ => (h_cau m (m + 1) m (Nat.le_succ m) (le_refl m)).le diff --git a/Mathlib/MeasureTheory/Integral/Average.lean b/Mathlib/MeasureTheory/Integral/Average.lean index 5db561dbe4c60..d7f54c0b37c44 100644 --- a/Mathlib/MeasureTheory/Integral/Average.lean +++ b/Mathlib/MeasureTheory/Integral/Average.lean @@ -782,7 +782,6 @@ theorem tendsto_integral_smul_of_tendsto_average_norm_sub simp only [integral_undef hi, lt_self_iff_false, not_false_eq_true] have I : ∀ᶠ i in l, ∫ y, g i y • (f y - c) ∂μ + (∫ y, g i y ∂μ) • c = ∫ y, g i y • f y ∂μ := by filter_upwards [f_int, g_int, g_supp, g_bound] with i hif hig hisupp hibound - dsimp rw [← integral_smul_const, ← integral_add] · simp only [smul_sub, sub_add_cancel] · simp_rw [smul_sub] diff --git a/Mathlib/MeasureTheory/Integral/Bochner.lean b/Mathlib/MeasureTheory/Integral/Bochner.lean index 52ec48b4bdb59..f3be4813c50b3 100644 --- a/Mathlib/MeasureTheory/Integral/Bochner.lean +++ b/Mathlib/MeasureTheory/Integral/Bochner.lean @@ -1263,7 +1263,7 @@ theorem integral_nonpos {f : α → ℝ} (hf : f ≤ 0) : ∫ a, f a ∂μ ≤ 0 theorem integral_eq_zero_iff_of_nonneg_ae {f : α → ℝ} (hf : 0 ≤ᵐ[μ] f) (hfi : Integrable f μ) : ∫ x, f x ∂μ = 0 ↔ f =ᵐ[μ] 0 := by simp_rw [integral_eq_lintegral_of_nonneg_ae hf hfi.1, ENNReal.toReal_eq_zero_iff, - ← ENNReal.not_lt_top, ← hasFiniteIntegral_iff_ofReal hf, hfi.2, not_true, or_false_iff] + ← ENNReal.not_lt_top, ← hasFiniteIntegral_iff_ofReal hf, hfi.2, or_false_iff] -- Porting note: split into parts, to make `rw` and `simp` work rw [lintegral_eq_zero_iff'] · rw [← hf.le_iff_eq, Filter.EventuallyEq, Filter.EventuallyLE] @@ -1538,7 +1538,7 @@ theorem integral_tsum {ι} [Countable ι] {f : ι → α → G} (hf : ∀ i, AES · intro n filter_upwards with x rfl - · simp_rw [← coe_nnnorm, ← NNReal.coe_tsum] + · simp_rw [← NNReal.coe_tsum] rw [aestronglyMeasurable_iff_aemeasurable] apply AEMeasurable.coe_nnreal_real apply AEMeasurable.nnreal_tsum diff --git a/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean b/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean index 24c0754304b80..16d5c33a386ed 100644 --- a/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean +++ b/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean @@ -283,7 +283,7 @@ theorem measure_integral_sub_linear_isLittleO_of_tendsto_ae' [IsMeasurablyGenera refine ((A.trans_le fun t ↦ ?_).sub (B.trans_le fun t ↦ ?_)).congr_left fun t ↦ ?_ · cases le_total (u t) (v t) <;> simp [*] · cases le_total (u t) (v t) <;> simp [*] - · simp_rw [intervalIntegral, sub_smul] + · simp_rw [intervalIntegral] abel #align interval_integral.measure_integral_sub_linear_is_o_of_tendsto_ae' intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae' @@ -431,7 +431,7 @@ theorem measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae (tendsto_const_pure.mono_right FTCFilter.pure_le) hub filter_upwards [A, A', B, B'] with _ ua_va a_ua ub_vb b_ub rw [← integral_interval_sub_interval_comm'] - · dsimp only; abel + · abel exacts [ub_vb, ua_va, b_ub.symm.trans <| hab.symm.trans a_ua] #align interval_integral.measure_integral_sub_integral_sub_linear_is_o_of_tendsto_ae intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae @@ -1216,7 +1216,7 @@ theorem integral_eq_sub_of_hasDerivAt_of_tendsto (hab : a < b) {fa fb} set F : ℝ → E := update (update f a fa) b fb have Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x := by refine' fun x hx => (hderiv x hx).congr_of_eventuallyEq _ - filter_upwards [Ioo_mem_nhds hx.1 hx.2] with _ hy; simp only + filter_upwards [Ioo_mem_nhds hx.1 hx.2] with _ hy rw [update_noteq hy.2.ne, update_noteq hy.1.ne'] have hcont : ContinuousOn F (Icc a b) := by rw [continuousOn_update_iff, continuousOn_update_iff, Icc_diff_right, Ico_diff_left] diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral.lean index c5bdb6b565214..695a9112542db 100644 --- a/Mathlib/MeasureTheory/Integral/IntervalIntegral.lean +++ b/Mathlib/MeasureTheory/Integral/IntervalIntegral.lean @@ -1195,7 +1195,7 @@ theorem continuousOn_primitive [NoAtoms μ] (h_int : IntegrableOn f (Icc a b) μ by_cases h : a ≤ b · have : ∀ x ∈ Icc a b, ∫ t in Ioc a x, f t ∂μ = ∫ t in a..x, f t ∂μ := by intro x x_in - simp_rw [← uIoc_of_le h, integral_of_le x_in.1] + simp_rw [integral_of_le x_in.1] rw [continuousOn_congr this] intro x₀ _ refine' continuousWithinAt_primitive (measure_singleton x₀) _ diff --git a/Mathlib/MeasureTheory/Integral/Lebesgue.lean b/Mathlib/MeasureTheory/Integral/Lebesgue.lean index 3ed5914f5a144..4a0276fa22569 100644 --- a/Mathlib/MeasureTheory/Integral/Lebesgue.lean +++ b/Mathlib/MeasureTheory/Integral/Lebesgue.lean @@ -767,7 +767,6 @@ theorem set_lintegral_eq_const {f : α → ℝ≥0∞} (hf : Measurable f) (r : ∫⁻ x in { x | f x = r }, f x ∂μ = r * μ { x | f x = r } := by have : ∀ᵐ x ∂μ, x ∈ { x | f x = r } → f x = r := ae_of_all μ fun _ hx => hx rw [set_lintegral_congr_fun _ this] - dsimp rw [lintegral_const, Measure.restrict_apply MeasurableSet.univ, Set.univ_inter] exact hf (measurableSet_singleton r) #align measure_theory.set_lintegral_eq_const MeasureTheory.set_lintegral_eq_const diff --git a/Mathlib/MeasureTheory/Integral/SetToL1.lean b/Mathlib/MeasureTheory/Integral/SetToL1.lean index c94e4ab2e4d08..014c8b3cfc41f 100644 --- a/Mathlib/MeasureTheory/Integral/SetToL1.lean +++ b/Mathlib/MeasureTheory/Integral/SetToL1.lean @@ -659,7 +659,6 @@ theorem norm_eq_sum_mul (f : α →₁ₛ[μ] G) : ‖f‖ = ∑ x in (toSimpleFunc f).range, (μ (toSimpleFunc f ⁻¹' {x})).toReal * ‖x‖ := by rw [norm_toSimpleFunc, snorm_one_eq_lintegral_nnnorm] have h_eq := SimpleFunc.map_apply (fun x => (‖x‖₊ : ℝ≥0∞)) (toSimpleFunc f) - dsimp only at h_eq simp_rw [← h_eq] rw [SimpleFunc.lintegral_eq_lintegral, SimpleFunc.map_lintegral, ENNReal.toReal_sum] · congr diff --git a/Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean b/Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean index 709ac9d07e4db..351e8b3ca8688 100644 --- a/Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean +++ b/Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean @@ -149,7 +149,6 @@ theorem SimpleFunc.exists_le_lowerSemicontinuous_lintegral_ge (f : α →ₛ ℝ rw [lintegral_add_left f₁.measurable.coe_nnreal_ennreal, lintegral_add_left g₁cont.measurable.coe_nnreal_ennreal] convert add_le_add g₁int g₂int using 1 - simp only conv_lhs => rw [← ENNReal.add_halves ε] abel #align measure_theory.simple_func.exists_le_lower_semicontinuous_lintegral_ge MeasureTheory.SimpleFunc.exists_le_lowerSemicontinuous_lintegral_ge @@ -378,7 +377,6 @@ theorem SimpleFunc.exists_upperSemicontinuous_le_lintegral_le (f : α →ₛ ℝ rw [lintegral_add_left f₁.measurable.coe_nnreal_ennreal, lintegral_add_left g₁cont.measurable.coe_nnreal_ennreal] convert add_le_add g₁int g₂int using 1 - simp only conv_lhs => rw [← ENNReal.add_halves ε] abel #align measure_theory.simple_func.exists_upper_semicontinuous_le_lintegral_le MeasureTheory.SimpleFunc.exists_upperSemicontinuous_le_lintegral_le diff --git a/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean b/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean index dc9316199d202..2f16bf93cfc00 100644 --- a/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean +++ b/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean @@ -520,7 +520,6 @@ theorem tendsto_zero_testAgainstNN_of_tendsto_zero_mass {γ : Type*} {F : Filter simp_rw [show ∀ i, dist ((μs i).testAgainstNN f) 0 = (μs i).testAgainstNN f by simp only [dist_nndist, NNReal.nndist_zero_eq_val', eq_self_iff_true, imp_true_iff]] refine' squeeze_zero (fun i => NNReal.coe_nonneg _) obs _ - simp_rw [NNReal.coe_mul] have lim_pair : Tendsto (fun i => (⟨nndist f 0, (μs i).mass⟩ : ℝ × ℝ)) F (𝓝 ⟨nndist f 0, 0⟩) := by refine' (Prod.tendsto_iff _ _).mpr ⟨tendsto_const_nhds, _⟩ exact (NNReal.continuous_coe.tendsto 0).comp mass_lim diff --git a/Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean b/Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean index 9388eb3373a2a..149253193975e 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean @@ -77,8 +77,7 @@ theorem parallelepiped_comp_equiv (v : ι → E) (e : ι' ≃ ι) : congr 1 with x have := fun z : ι' → ℝ => e.symm.sum_comp fun i => z i • v (e i) simp_rw [Equiv.apply_symm_apply] at this - simp_rw [Function.comp_apply, ge_iff_le, zero_le_one, not_true, gt_iff_lt, mem_image, mem_Icc, - Equiv.piCongrLeft'_apply, this] + simp_rw [Function.comp_apply, mem_image, mem_Icc, Equiv.piCongrLeft'_apply, this] #align parallelepiped_comp_equiv parallelepiped_comp_equiv -- The parallelepiped associated to an orthonormal basis of `ℝ` is either `[0, 1]` or `[-1, 0]`. @@ -107,7 +106,7 @@ theorem parallelepiped_orthonormalBasis_one_dim (b : OrthonormalBasis ι ℝ ℝ simp only [Finset.univ_unique, Fin.default_eq_zero, smul_eq_mul, mul_one, Finset.sum_singleton, ← image_comp, Function.comp_apply, image_id', ge_iff_le, zero_le_one, not_true, gt_iff_lt] · right - simp_rw [H, parallelepiped, Algebra.id.smul_eq_mul, mul_one, A] + simp_rw [H, parallelepiped, Algebra.id.smul_eq_mul, A] simp only [Finset.univ_unique, Fin.default_eq_zero, mul_neg, mul_one, Finset.sum_neg_distrib, Finset.sum_singleton, ← image_comp, Function.comp, image_neg, preimage_neg_Icc, neg_zero] #align parallelepiped_orthonormal_basis_one_dim parallelepiped_orthonormalBasis_one_dim diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean b/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean index 4afedea996426..d8ddeb6e2a596 100644 --- a/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean +++ b/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean @@ -161,7 +161,7 @@ theorem measure_eq_iInf (s : Set α) : μ s = ⨅ (t) (_ : s ⊆ t) (_ : Measura `nonempty_measurable_superset`. -/ theorem measure_eq_iInf' (μ : Measure α) (s : Set α) : μ s = ⨅ t : { t // s ⊆ t ∧ MeasurableSet t }, μ t := by - simp_rw [iInf_subtype, iInf_and, Subtype.coe_mk, ← measure_eq_iInf] + simp_rw [iInf_subtype, iInf_and, ← measure_eq_iInf] #align measure_theory.measure_eq_infi' MeasureTheory.measure_eq_iInf' theorem measure_eq_inducedOuterMeasure : diff --git a/Mathlib/MeasureTheory/PiSystem.lean b/Mathlib/MeasureTheory/PiSystem.lean index d56d99e054e25..0598ddc4637f2 100644 --- a/Mathlib/MeasureTheory/PiSystem.lean +++ b/Mathlib/MeasureTheory/PiSystem.lean @@ -312,8 +312,6 @@ theorem mem_generatePiSystem_iUnion_elim {α β} {g : β → Set (Set α)} (h_pi and_true_iff, true_and_iff] at h1 ⊢ all_goals exact h1 intro b h_b - -- Porting note: `simp only` required for a beta reduction - simp only [] split_ifs with hbs hbt hbt · refine' h_pi b (f_s b) (h_s b hbs) (f_t' b) (h_t' b hbt) (Set.Nonempty.mono _ h_nonempty) exact Set.inter_subset_inter (Set.biInter_subset_of_mem hbs) (Set.biInter_subset_of_mem hbt) diff --git a/Mathlib/ModelTheory/Semantics.lean b/Mathlib/ModelTheory/Semantics.lean index 14a09841bb0a8..f36653ddda5cd 100644 --- a/Mathlib/ModelTheory/Semantics.lean +++ b/Mathlib/ModelTheory/Semantics.lean @@ -332,7 +332,7 @@ theorem realize_foldr_sup (l : List (L.BoundedFormula α n)) (v : α → M) (xs (l.foldr (· ⊔ ·) ⊥).Realize v xs ↔ ∃ φ ∈ l, BoundedFormula.Realize φ v xs := by induction' l with φ l ih · simp - · simp_rw [List.foldr_cons, realize_sup, ih, exists_prop, List.mem_cons, or_and_right, exists_or, + · simp_rw [List.foldr_cons, realize_sup, ih, List.mem_cons, or_and_right, exists_or, exists_eq_left] #align first_order.language.bounded_formula.realize_foldr_sup FirstOrder.Language.BoundedFormula.realize_foldr_sup diff --git a/Mathlib/NumberTheory/ADEInequality.lean b/Mathlib/NumberTheory/ADEInequality.lean index 577b8b277b3b2..f2ec0a7f8b61c 100644 --- a/Mathlib/NumberTheory/ADEInequality.lean +++ b/Mathlib/NumberTheory/ADEInequality.lean @@ -198,7 +198,6 @@ theorem lt_four {q r : ℕ+} (hqr : q ≤ r) (H : 1 < sumInv {2, q, r}) : q < 4 contrapose! H rw [sumInv_pqr] have h4r := H.trans hqr - simp at H have hq: (q : ℚ)⁻¹ ≤ 4⁻¹ := by rw [inv_le_inv _ h4] assumption_mod_cast @@ -216,7 +215,6 @@ theorem lt_six {r : ℕ+} (H : 1 < sumInv {2, 3, r}) : r < 6 := by have h6 : (0 : ℚ) < 6 := by norm_num contrapose! H rw [sumInv_pqr] - simp at H have hr: (r : ℚ)⁻¹ ≤ 6⁻¹ := by rw [inv_le_inv _ h6] assumption_mod_cast diff --git a/Mathlib/NumberTheory/ArithmeticFunction.lean b/Mathlib/NumberTheory/ArithmeticFunction.lean index 22f5d3e23f11c..ce80477c055f8 100644 --- a/Mathlib/NumberTheory/ArithmeticFunction.lean +++ b/Mathlib/NumberTheory/ArithmeticFunction.lean @@ -1027,8 +1027,6 @@ theorem isMultiplicative_moebius : IsMultiplicative μ := by 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] - simp only [Nat.isUnit_iff, ZeroHom.toFun_eq_coe, IsUnit.mul_iff, mul_ite, ite_mul, - zero_mul, mul_zero] rw [pow_add, ite_mul_zero_left, ite_mul_zero_right] split_ifs <;> -- porting note: added simp -- porting note: added @@ -1042,7 +1040,7 @@ theorem moebius_mul_coe_zeta : (μ * ζ : ArithmeticFunction ℤ) = 1 := by refine' recOnPosPrimePosCoprime _ _ _ _ n · intro p n hp hn rw [coe_mul_zeta_apply, sum_divisors_prime_pow hp, sum_range_succ'] - simp_rw [Function.Embedding.coeFn_mk, pow_zero, moebius_apply_one, + simp_rw [pow_zero, moebius_apply_one, moebius_apply_prime_pow hp (Nat.succ_ne_zero _), Nat.succ_inj', sum_ite_eq', mem_range, if_pos hn, add_left_neg] rw [one_apply_ne] diff --git a/Mathlib/NumberTheory/Bernoulli.lean b/Mathlib/NumberTheory/Bernoulli.lean index c0acaa37d0bdd..2d3ff7c91a9e5 100644 --- a/Mathlib/NumberTheory/Bernoulli.lean +++ b/Mathlib/NumberTheory/Bernoulli.lean @@ -235,7 +235,7 @@ theorem sum_bernoulli (n : ℕ) : mul_one, choose_zero_right, cast_zero, if_false, zero_add, succ_succ_ne_one] ring have f := sum_bernoulli' n.succ.succ - simp_rw [sum_range_succ', bernoulli'_one, choose_one_right, cast_succ, ← eq_sub_iff_add_eq] at f + simp_rw [sum_range_succ', cast_succ, ← eq_sub_iff_add_eq] at f -- porting note: was `convert f` refine' Eq.trans _ (Eq.trans f _) · congr @@ -297,7 +297,6 @@ theorem bernoulliPowerSeries_mul_exp_sub_one : bernoulliPowerSeries A * (exp A - field_simp [mul_ne_zero hj (hfact x.2), hfact x.1, mul_comm _ (bernoulli x.1), mul_assoc, Nat.factorial_ne_zero, hj] -- porting note: was `cc`, which was not yet ported - simp only left ring #align bernoulli_power_series_mul_exp_sub_one bernoulliPowerSeries_mul_exp_sub_one @@ -323,7 +322,6 @@ theorem sum_range_pow (n p : ℕ) : simp only [coeff_mul, coeff_mk, cast_mul, sum_antidiagonal_eq_sum_range_succ f] apply sum_congr rfl intros m h - simp only [Finset.mem_range] simp only [exp_pow_eq_rescale_exp, rescale, one_div, coeff_mk, RingHom.coe_mk, coeff_exp, RingHom.id_apply, cast_mul, algebraMap_rat_rat] -- manipulate factorials and binomial coefficients diff --git a/Mathlib/NumberTheory/ClassNumber/AdmissibleCardPowDegree.lean b/Mathlib/NumberTheory/ClassNumber/AdmissibleCardPowDegree.lean index bb8c8c1ce9d78..fb4198dfd2800 100644 --- a/Mathlib/NumberTheory/ClassNumber/AdmissibleCardPowDegree.lean +++ b/Mathlib/NumberTheory/ClassNumber/AdmissibleCardPowDegree.lean @@ -118,13 +118,11 @@ theorem exists_approx_polynomial {b : Fq[X]} (hb : b ≠ 0) {ε : ℝ} (hε : 0 · obtain ⟨i₀, i₁, i_ne, mod_eq⟩ := exists_eq_polynomial le_rfl b le_b (fun i => A i % b) fun i => EuclideanDomain.mod_lt (A i) hb refine' ⟨i₀, i₁, i_ne, _⟩ - simp only at mod_eq rwa [mod_eq, sub_self, map_zero, Int.cast_zero] -- Otherwise, it suffices to choose two elements whose difference is of small enough degree. rw [not_le] at le_b obtain ⟨i₀, i₁, i_ne, deg_lt⟩ := exists_approx_polynomial_aux le_rfl b (fun i => A i % b) fun i => EuclideanDomain.mod_lt (A i) hb - simp only at deg_lt use i₀, i₁, i_ne -- Again, if the remainders are equal we are done. by_cases h : A i₁ % b = A i₀ % b diff --git a/Mathlib/NumberTheory/NumberField/Embeddings.lean b/Mathlib/NumberTheory/NumberField/Embeddings.lean index 0249ae893d76b..2f9ad15b3b305 100644 --- a/Mathlib/NumberTheory/NumberField/Embeddings.lean +++ b/Mathlib/NumberTheory/NumberField/Embeddings.lean @@ -449,8 +449,7 @@ theorem prod_eq_abs_norm (x : K) : intro _ _ hφ rw [← (Finset.mem_filter.mp hφ).2] rfl - simp_rw [Finset.prod_congr rfl (this _), Finset.mem_univ, forall_true_left, Finset.prod_const, - card_filter_mk_eq] + simp_rw [Finset.prod_congr rfl (this _), Finset.prod_const, card_filter_mk_eq] · rw [eq_ratCast, Rat.cast_abs, ← Complex.abs_ofReal, Complex.ofReal_rat_cast] #align number_field.infinite_place.prod_eq_abs_norm NumberField.InfinitePlace.prod_eq_abs_norm diff --git a/Mathlib/NumberTheory/Padics/PadicIntegers.lean b/Mathlib/NumberTheory/Padics/PadicIntegers.lean index 5ec828264f7e7..8bcf6a7768dab 100644 --- a/Mathlib/NumberTheory/Padics/PadicIntegers.lean +++ b/Mathlib/NumberTheory/Padics/PadicIntegers.lean @@ -685,7 +685,7 @@ instance isFractionRing : IsFractionRing ℤ_[p] ℚ_[p] where simp only [map_pow, map_natCast, algebraMap_apply, PadicInt.coe_pow, PadicInt.coe_nat_cast, Subtype.coe_mk, Nat.cast_pow] eq_iff_exists' := by - simp_rw [algebraMap_apply, algebraMap_apply, Subtype.coe_inj] + simp_rw [algebraMap_apply, Subtype.coe_inj] refine ⟨fun h => ⟨1, by rw [h]⟩, ?_⟩ rintro ⟨⟨c, hc⟩, h⟩ exact (mul_eq_mul_left_iff.mp h).resolve_right (mem_nonZeroDivisors_iff_ne_zero.mp hc) diff --git a/Mathlib/NumberTheory/Padics/RingHoms.lean b/Mathlib/NumberTheory/Padics/RingHoms.lean index f4e19d6bb3ad5..d8b7fb8b8e902 100644 --- a/Mathlib/NumberTheory/Padics/RingHoms.lean +++ b/Mathlib/NumberTheory/Padics/RingHoms.lean @@ -341,7 +341,6 @@ theorem dvd_appr_sub_appr (x : ℤ_[p]) (m n : ℕ) (h : m ≤ n) : p ^ m ∣ x. dsimp [appr] split_ifs with h · exact ih - dsimp rw [add_comm, add_tsub_assoc_of_le (appr_mono _ (Nat.le_add_right m k))] apply dvd_add _ ih apply dvd_mul_of_dvd_left diff --git a/Mathlib/NumberTheory/ZetaFunction.lean b/Mathlib/NumberTheory/ZetaFunction.lean index 2ca042684c22d..c0fb1e72eb4da 100644 --- a/Mathlib/NumberTheory/ZetaFunction.lean +++ b/Mathlib/NumberTheory/ZetaFunction.lean @@ -247,7 +247,7 @@ theorem isBigO_zero_zetaKernel₂ : IsBigO (𝓝[>] 0) zetaKernel₂ fun t => ex have h4 := h3.mul (isBigO_refl (fun t : ℝ => 1 / (sqrt t : ℂ)) (𝓝[>] 0)).norm_right refine h4.congr' ?_ ?_ · refine eventually_of_mem self_mem_nhdsWithin fun x hx => ?_ - simp_rw [← mul_assoc] + dsimp rw [mul_comm, ← mul_assoc, one_div_mul_cancel, one_mul] exact ofReal_ne_zero.mpr ((sqrt_ne_zero <| le_of_lt hx).mpr (ne_of_gt hx)) · refine eventually_of_mem self_mem_nhdsWithin fun x _ => ?_ diff --git a/Mathlib/NumberTheory/ZetaValues.lean b/Mathlib/NumberTheory/ZetaValues.lean index 32d9c3815c073..95a8b51258a57 100644 --- a/Mathlib/NumberTheory/ZetaValues.lean +++ b/Mathlib/NumberTheory/ZetaValues.lean @@ -86,7 +86,6 @@ theorem integral_bernoulliFun_eq_zero {k : ℕ} (hk : k ≠ 0) : ∫ x : ℝ in (0)..1, bernoulliFun k x = 0 := by rw [integral_eq_sub_of_hasDerivAt (fun x _ => antideriv_bernoulliFun k x) ((Polynomial.continuous _).intervalIntegrable _ _)] - dsimp only rw [bernoulliFun_eval_one] split_ifs with h · exfalso; exact hk (Nat.succ_inj'.mp h) diff --git a/Mathlib/Order/RelIso/Basic.lean b/Mathlib/Order/RelIso/Basic.lean index aaa8f0761f975..270a000634009 100644 --- a/Mathlib/Order/RelIso/Basic.lean +++ b/Mathlib/Order/RelIso/Basic.lean @@ -452,7 +452,6 @@ theorem acc_lift₂_iff [Setoid α] {r : α → α → Prop} · exact RelHomClass.acc (Quotient.mkRelHom H) a · intro ac induction' ac with _ _ IH - dsimp at IH refine' ⟨_, fun q h => _⟩ obtain ⟨a', rfl⟩ := q.exists_rep exact IH a' h diff --git a/Mathlib/Order/WellFoundedSet.lean b/Mathlib/Order/WellFoundedSet.lean index 6f95db4c74f99..b530751c9d01a 100644 --- a/Mathlib/Order/WellFoundedSet.lean +++ b/Mathlib/Order/WellFoundedSet.lean @@ -782,8 +782,7 @@ theorem partiallyWellOrderedOn_sublistForall₂ (r : α → α → Prop) [IsRefl have hnil : ∀ n, f n ≠ List.nil := fun n con => hf1.2 n n.succ n.lt_succ_self (con.symm ▸ List.SublistForall₂.nil) have : ∀ n, (f n).headI ∈ s - · simp only [Set.range_subset_iff, Function.comp_apply] - exact fun n => hf1.1 n _ (List.head!_mem_self (hnil n)) + · exact fun n => hf1.1 n _ (List.head!_mem_self (hnil n)) obtain ⟨g, hg⟩ := h.exists_monotone_subseq (fun n => (f n).headI) this have hf' := hf2 (g 0) (fun n => if n < g 0 then f n else List.tail (f (g (n - g 0)))) diff --git a/Mathlib/Probability/Kernel/CondCdf.lean b/Mathlib/Probability/Kernel/CondCdf.lean index 4be287948013e..d0fb5fbeaffc2 100644 --- a/Mathlib/Probability/Kernel/CondCdf.lean +++ b/Mathlib/Probability/Kernel/CondCdf.lean @@ -139,7 +139,7 @@ theorem lintegral_iInf_directed_of_measurable {mα : MeasurableSpace α} [Counta cases nonempty_encodable β cases isEmpty_or_nonempty β · -- Porting note: the next `simp only` doesn't do anything, so added a workaround below. - simp only [WithTop.iInf_empty, lintegral_const] + -- simp only [WithTop.iInf_empty, lintegral_const] conv => lhs congr @@ -901,13 +901,12 @@ theorem set_lintegral_condCdf (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] (x (measurable_condCdf ρ q).ennreal_ofReal] rotate_left · intro b - simp_rw [h_coe] rw [set_lintegral_condCdf_rat ρ _ hs] exact measure_ne_top ρ _ · refine' Monotone.directed_ge fun i j hij a => ENNReal.ofReal_le_ofReal ((condCdf ρ a).mono _) rw [h_coe, h_coe] exact_mod_cast hij - simp_rw [h_coe, set_lintegral_condCdf_rat ρ _ hs] + simp_rw [set_lintegral_condCdf_rat ρ _ hs] rw [← measure_iInter_eq_iInf] · rw [← prod_iInter] congr with y diff --git a/Mathlib/Probability/Kernel/MeasurableIntegral.lean b/Mathlib/Probability/Kernel/MeasurableIntegral.lean index 2885603707c83..52213a5c2fb76 100644 --- a/Mathlib/Probability/Kernel/MeasurableIntegral.lean +++ b/Mathlib/Probability/Kernel/MeasurableIntegral.lean @@ -133,8 +133,9 @@ variable [IsSFiniteKernel κ] [IsSFiniteKernel η] /-- Auxiliary lemma for `Measurable.lintegral_kernel_prod_right`. -/ theorem kernel.measurable_lintegral_indicator_const {t : Set (α × β)} (ht : MeasurableSet t) (c : ℝ≥0∞) : Measurable fun a => ∫⁻ b, t.indicator (Function.const (α × β) c) (a, b) ∂κ a := by - simp_rw [lintegral_indicator_const_comp measurable_prod_mk_left ht _] - -- Porting note: `simp_rw` doesn't take, added the `conv` below + -- Porting note: was originally by + -- `simp_rw [lintegral_indicator_const_comp measurable_prod_mk_left ht _]` + -- but this has no effect, so added the `conv` below conv => congr ext diff --git a/Mathlib/Probability/Martingale/BorelCantelli.lean b/Mathlib/Probability/Martingale/BorelCantelli.lean index c7f77bf03f1a4..360faf71b2f4b 100644 --- a/Mathlib/Probability/Martingale/BorelCantelli.lean +++ b/Mathlib/Probability/Martingale/BorelCantelli.lean @@ -162,7 +162,6 @@ theorem Submartingale.exists_tendsto_of_abs_bddAbove_aux [IsFiniteMeasure μ] have heq : ∀ n, stoppedValue f (leastGE f i n) ω = f n ω := by intro n rw [leastGE]; unfold hitting; rw [stoppedValue] - simp only rw [if_neg] simp only [Set.mem_Icc, Set.mem_union, Set.mem_Ici] push_neg @@ -191,7 +190,7 @@ theorem Submartingale.bddAbove_iff_exists_tendsto [IsFiniteMeasure μ] (hf : Sub have hgbdd : ∀ᵐ ω ∂μ, ∀ i : ℕ, |g (i + 1) ω - g i ω| ≤ ↑R := by simpa only [sub_sub_sub_cancel_right] filter_upwards [hg.bddAbove_iff_exists_tendsto_aux hg0 hgbdd] with ω hω - convert hω using 1 <;> simp_rw [eq_iff_iff] + convert hω using 1 · refine' ⟨fun h => _, fun h => _⟩ <;> obtain ⟨b, hb⟩ := h <;> refine' ⟨b + |f 0 ω|, fun y hy => _⟩ <;> obtain ⟨n, rfl⟩ := hy · simp_rw [sub_eq_add_neg] diff --git a/Mathlib/Probability/ProbabilityMassFunction/Uniform.lean b/Mathlib/Probability/ProbabilityMassFunction/Uniform.lean index 3263933c08838..db86b215fbfb6 100644 --- a/Mathlib/Probability/ProbabilityMassFunction/Uniform.lean +++ b/Mathlib/Probability/ProbabilityMassFunction/Uniform.lean @@ -83,7 +83,7 @@ theorem toOuterMeasure_uniformOfFinset_apply : (uniformOfFinset s hs).toOuterMeasure t = ∑' x, if x ∈ t then uniformOfFinset s hs x else 0 := toOuterMeasure_apply (uniformOfFinset s hs) t _ = ∑' x, if x ∈ s ∧ x ∈ t then (s.card : ℝ≥0∞)⁻¹ else 0 := - (tsum_congr fun x => by simp_rw [uniformOfFinset_apply, and_comm, ← ite_and, and_comm]) + (tsum_congr fun x => by simp_rw [uniformOfFinset_apply, ← ite_and, and_comm]) _ = ∑ x in s.filter (· ∈ t), if x ∈ s ∧ x ∈ t then (s.card : ℝ≥0∞)⁻¹ else 0 := (tsum_eq_sum fun x hx => if_neg fun h => hx (Finset.mem_filter.2 h)) _ = ∑ _x in s.filter (· ∈ t), (s.card : ℝ≥0∞)⁻¹ := diff --git a/Mathlib/Probability/Process/Filtration.lean b/Mathlib/Probability/Process/Filtration.lean index 848d79afb5dae..d56f65c1c3d6a 100644 --- a/Mathlib/Probability/Process/Filtration.lean +++ b/Mathlib/Probability/Process/Filtration.lean @@ -67,7 +67,7 @@ protected theorem le (f : Filtration ι m) (i : ι) : f i ≤ m := @[ext] protected theorem ext {f g : Filtration ι m} (h : (f : ι → MeasurableSpace Ω) = g) : f = g := by - cases f; cases g; simp only; congr + cases f; cases g; congr #align measure_theory.filtration.ext MeasureTheory.Filtration.ext variable (ι) diff --git a/Mathlib/Probability/Variance.lean b/Mathlib/Probability/Variance.lean index fc844954965a7..4634dff20022d 100644 --- a/Mathlib/Probability/Variance.lean +++ b/Mathlib/Probability/Variance.lean @@ -246,7 +246,6 @@ theorem evariance_def' [@IsProbabilityMeasure Ω _ ℙ] {X : Ω → ℝ} (hX : A by_cases hℒ : Memℒp X 2 · rw [← hℒ.ofReal_variance_eq, variance_def' hℒ, ENNReal.ofReal_sub _ (sq_nonneg _)] congr - simp_rw [← ENNReal.coe_pow] rw [lintegral_coe_eq_integral] · congr 2 with ω simp only [Pi.pow_apply, NNReal.coe_pow, coe_nnnorm, Real.norm_eq_abs, Even.pow_abs even_two] diff --git a/Mathlib/RepresentationTheory/Basic.lean b/Mathlib/RepresentationTheory/Basic.lean index 2a62c3c74a268..f1fb8da23505f 100644 --- a/Mathlib/RepresentationTheory/Basic.lean +++ b/Mathlib/RepresentationTheory/Basic.lean @@ -413,11 +413,11 @@ def linHom : Representation k G (V →ₗ[k] W) where map_one' := LinearMap.ext fun x => by dsimp -- Porting note: now needed - simp_rw [coe_mk, inv_one, map_one, one_apply, one_eq_id, comp_id, id_comp] + simp_rw [inv_one, map_one, one_eq_id, comp_id, id_comp] map_mul' g h := LinearMap.ext fun x => by dsimp -- Porting note: now needed - simp_rw [coe_mul, coe_mk, Function.comp_apply, mul_inv_rev, map_mul, mul_eq_comp, comp_assoc] + simp_rw [mul_inv_rev, map_mul, mul_eq_comp, comp_assoc] #align representation.lin_hom Representation.linHom @[simp] diff --git a/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean b/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean index 9a7e757a17c13..73e9daaab4a9f 100644 --- a/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean +++ b/Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean @@ -425,7 +425,6 @@ def cechNerveTerminalFromIso : NatIso.ofComponents (fun n => limit.isoLimitCone (Action.ofMulActionLimitCone _ _)) fun f => by refine' IsLimit.hom_ext (Action.ofMulActionLimitCone.{u, 0} G fun _ => G).2 fun j => _ dsimp only [cechNerveTerminalFrom, Pi.lift] - dsimp rw [Category.assoc, limit.isoLimitCone_hom_π, limit.lift_π, Category.assoc] exact (limit.isoLimitCone_hom_π _ _).symm #align classifying_space_universal_cover.cech_nerve_terminal_from_iso classifyingSpaceUniversalCover.cechNerveTerminalFromIso diff --git a/Mathlib/RingTheory/Coprime/Lemmas.lean b/Mathlib/RingTheory/Coprime/Lemmas.lean index e5d0e06df71d0..0d5d8626f028b 100644 --- a/Mathlib/RingTheory/Coprime/Lemmas.lean +++ b/Mathlib/RingTheory/Coprime/Lemmas.lean @@ -158,9 +158,8 @@ theorem exists_sum_eq_one_iff_pairwise_coprime [DecidableEq I] (h : t.Nonempty) use fun i ↦ if i = a then u else v * μ i have hμ' : (∑ i in t, v * ((μ i * ∏ j in t \ {i}, s j) * s a)) = v * s a := by rw [← mul_sum, ← sum_mul, hμ, one_mul] - rw [sum_cons, cons_eq_insert, sdiff_singleton_eq_erase, erase_insert hat] - dsimp - rw [if_pos rfl, ← huv, ← hμ', sum_congr rfl] + rw [sum_cons, cons_eq_insert, sdiff_singleton_eq_erase, erase_insert hat, if_pos rfl, + ← huv, ← hμ', sum_congr rfl] intro x hx rw [mul_assoc, if_neg fun ha : x = a ↦ hat (ha.casesOn hx)] rw [mul_assoc] diff --git a/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean b/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean index fc305fab9a05d..8f2fb5f8bcfeb 100644 --- a/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean +++ b/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean @@ -445,13 +445,13 @@ instance : Algebra R (v.adicCompletionIntegers K) where ext --Porting note: added instance letI : Valued K ℤₘ₀ := adicValued v - simp_rw [RingHom.map_mul, Subring.coe_mul, Subtype.coe_mk, UniformSpace.Completion.coe_mul] + simp_rw [RingHom.map_mul, Subring.coe_mul, UniformSpace.Completion.coe_mul] map_zero' := by simp only [map_zero]; rfl map_add' x y := by ext --Porting note: added instance letI : Valued K ℤₘ₀ := adicValued v - simp_rw [RingHom.map_add, Subring.coe_add, Subtype.coe_mk, UniformSpace.Completion.coe_add] + simp_rw [RingHom.map_add, Subring.coe_add, UniformSpace.Completion.coe_add] commutes' r x := by -- Porting note: added `dsimp` line dsimp diff --git a/Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean b/Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean index 57c078c3d0c2a..002764af8ecda 100644 --- a/Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean +++ b/Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean @@ -214,7 +214,6 @@ theorem zero : (0 : K_hat R K).IsFiniteAdele := by have h_zero : (Valued.v (0 : v.adicCompletion K) : WithZero (Multiplicative ℤ)) = 0 := Valued.v.map_zero' rw [h_zero]; exact zero_le_one' _ - simp_rw [Pi.zero_apply, h_empty] -- Porting note: was `exact`, but `OfNat` got in the way. convert finite_empty #align dedekind_domain.prod_adic_completions.is_finite_adele.zero DedekindDomain.ProdAdicCompletions.IsFiniteAdele.zero @@ -262,7 +261,6 @@ theorem one : (1 : K_hat R K).IsFiniteAdele := by ext v; rw [mem_empty_iff_false, iff_false_iff]; intro hv rw [mem_setOf] at hv; apply hv; rw [mem_adicCompletionIntegers] exact le_of_eq Valued.v.map_one' - simp_rw [Pi.one_apply, h_empty] -- Porting note: was `exact`, but `OfNat` got in the way. convert finite_empty #align dedekind_domain.prod_adic_completions.is_finite_adele.one DedekindDomain.ProdAdicCompletions.IsFiniteAdele.one diff --git a/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean b/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean index ed930920fc980..08330c9a3773d 100644 --- a/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean +++ b/Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean @@ -347,7 +347,6 @@ instance : SMul α (HomogeneousLocalization 𝒜 x) where @[simp] theorem smul_val (y : HomogeneousLocalization 𝒜 x) (n : α) : (n • y).val = n • y.val := by induction y using Quotient.inductionOn - simp only [Quotient.liftOn₂'_mk, Quotient.liftOn'_mk] change Localization.mk _ _ = n • Localization.mk _ _ dsimp only rw [Localization.smul_mk] @@ -408,7 +407,6 @@ theorem one_val : (1 : HomogeneousLocalization 𝒜 x).val = 1 := theorem add_val (y1 y2 : HomogeneousLocalization 𝒜 x) : (y1 + y2).val = y1.val + y2.val := by induction y1 using Quotient.inductionOn induction y2 using Quotient.inductionOn - simp only [Quotient.liftOn₂'_mk, Quotient.liftOn'_mk] change Localization.mk _ _ = Localization.mk _ _ + Localization.mk _ _ dsimp only rw [Localization.add_mk] @@ -419,7 +417,6 @@ theorem add_val (y1 y2 : HomogeneousLocalization 𝒜 x) : (y1 + y2).val = y1.va theorem mul_val (y1 y2 : HomogeneousLocalization 𝒜 x) : (y1 * y2).val = y1.val * y2.val := by induction y1 using Quotient.inductionOn induction y2 using Quotient.inductionOn - simp only [Quotient.liftOn₂'_mk, Quotient.liftOn'_mk] change Localization.mk _ _ = Localization.mk _ _ * Localization.mk _ _ dsimp only rw [Localization.mk_mul] @@ -429,7 +426,6 @@ theorem mul_val (y1 y2 : HomogeneousLocalization 𝒜 x) : (y1 * y2).val = y1.va @[simp] theorem neg_val (y : HomogeneousLocalization 𝒜 x) : (-y).val = -y.val := by induction y using Quotient.inductionOn - simp only [Quotient.liftOn₂'_mk, Quotient.liftOn'_mk] change Localization.mk _ _ = -Localization.mk _ _ dsimp only rw [Localization.neg_mk] @@ -444,7 +440,6 @@ theorem sub_val (y1 y2 : HomogeneousLocalization 𝒜 x) : (y1 - y2).val = y1.va @[simp] theorem pow_val (y : HomogeneousLocalization 𝒜 x) (n : ℕ) : (y ^ n).val = y.val ^ n := by induction y using Quotient.inductionOn - simp only [Quotient.liftOn₂'_mk, Quotient.liftOn'_mk] change Localization.mk _ _ = Localization.mk _ _ ^ n rw [Localization.mk_pow] dsimp only @@ -525,7 +520,6 @@ theorem eq_num_div_den (f : HomogeneousLocalization 𝒜 x) : have := Quotient.out_eq' f apply_fun HomogeneousLocalization.val at this rw [← this] - simp only [Quotient.liftOn'_mk''] rfl #align homogeneous_localization.eq_num_div_denom HomogeneousLocalization.eq_num_div_den diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean index c31a8ca32fcce..45b42315e17eb 100644 --- a/Mathlib/RingTheory/Ideal/Operations.lean +++ b/Mathlib/RingTheory/Ideal/Operations.lean @@ -1134,7 +1134,6 @@ theorem subset_union_prime' {R : Type u} [CommRing R] {s : Finset ι} {f : ι exact h specialize ih hp' hn' h' refine' ih.imp id (Or.imp id (Exists.imp fun k => _)) - simp only [exists_prop] exact And.imp (fun hk => Finset.insert_subset_insert i (Finset.subset_insert j u) hk) id by_cases Ha : f a ≤ f i · have h' : (I : Set R) ⊆ f i ∪ f b ∪ ⋃ j ∈ (↑t : Set ι), f j := by diff --git a/Mathlib/RingTheory/MvPolynomial/Symmetric.lean b/Mathlib/RingTheory/MvPolynomial/Symmetric.lean index e1bd16d23ee74..5af86fead33a2 100644 --- a/Mathlib/RingTheory/MvPolynomial/Symmetric.lean +++ b/Mathlib/RingTheory/MvPolynomial/Symmetric.lean @@ -238,7 +238,6 @@ theorem support_esymm'' (n : ℕ) [DecidableEq σ] [Nontrivial R] : have hs := biUnion_congr (of_eq_true (eq_self s)) (hsingle s) have ht := biUnion_congr (of_eq_true (eq_self t)) (hsingle t) rw [hs, ht] at this - simp only [Finsupp.support_single_ne_zero _ one_ne_zero] at this · simp only [biUnion_singleton_eq_self] at this exact absurd this hst.symm all_goals intro x y; simp [Finsupp.support_single_disjoint] diff --git a/Mathlib/RingTheory/Norm.lean b/Mathlib/RingTheory/Norm.lean index 0d5680f6f67f0..12daca3406924 100644 --- a/Mathlib/RingTheory/Norm.lean +++ b/Mathlib/RingTheory/Norm.lean @@ -285,7 +285,7 @@ theorem prod_embeddings_eq_finrank_pow [Algebra L F] [IsScalarTower K L F] [IsAl ← Finset.univ_sigma_univ, Finset.prod_sigma, ← Finset.prod_pow] refine Finset.prod_congr rfl fun σ _ => ?_ · letI : Algebra L E := σ.toRingHom.toAlgebra - simp_rw [Finset.prod_const, Finset.card_univ] + simp_rw [Finset.prod_const] congr exact AlgHom.card L F E · intro σ diff --git a/Mathlib/RingTheory/OreLocalization/Basic.lean b/Mathlib/RingTheory/OreLocalization/Basic.lean index 510433b6d51e6..78cee56c17c6f 100644 --- a/Mathlib/RingTheory/OreLocalization/Basic.lean +++ b/Mathlib/RingTheory/OreLocalization/Basic.lean @@ -736,7 +736,8 @@ theorem right_distrib (x y z : R[S⁻¹]) : (x + y) * z = x * z + y * z := by rw [OreLocalization.expand' r₁ s₁ sa] rw [OreLocalization.expand r₂ s₂ ra (by rw [← ha]; apply SetLike.coe_mem)] rw [← Subtype.coe_eq_of_eq_mk ha] - repeat' rw [oreDiv_mul_oreDiv]; simp only [add_mul, add_oreDiv] + repeat rw [oreDiv_mul_oreDiv] + simp only [add_mul, add_oreDiv] #align ore_localization.right_distrib OreLocalization.right_distrib instance instSemiringOreLocalization : Semiring R[S⁻¹] := diff --git a/Mathlib/RingTheory/Polynomial/Basic.lean b/Mathlib/RingTheory/Polynomial/Basic.lean index c00d5c57a83fb..198a85d6a076f 100644 --- a/Mathlib/RingTheory/Polynomial/Basic.lean +++ b/Mathlib/RingTheory/Polynomial/Basic.lean @@ -221,7 +221,7 @@ theorem geom_sum_X_comp_X_add_one_eq_sum (n : ℕ) : Nat.cast_zero, Finset.mem_range, not_lt, eq_self_iff_true, if_true, imp_true_iff] induction' n with n ih generalizing i · dsimp; simp only [zero_comp, coeff_zero, Nat.cast_zero] - · dsimp; simp only [geom_sum_succ', ih, add_comp, X_pow_comp, coeff_add, Nat.choose_succ_succ, + · simp only [geom_sum_succ', ih, add_comp, X_pow_comp, coeff_add, Nat.choose_succ_succ, Nat.cast_add, coeff_X_add_one_pow] set_option linter.uppercaseLean3 false in #align polynomial.geom_sum_X_comp_X_add_one_eq_sum Polynomial.geom_sum_X_comp_X_add_one_eq_sum diff --git a/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean b/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean index 9c0f94fe5b7de..13505da3e5de3 100644 --- a/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean +++ b/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean @@ -74,7 +74,6 @@ theorem cyclotomic_pos {n : ℕ} (hn : 2 < n) {R} [LinearOrderedCommRing R] (x : induction' n using Nat.strong_induction_on with n ih have hn' : 0 < n := pos_of_gt hn have hn'' : 1 < n := one_lt_two.trans hn - dsimp at ih have := prod_cyclotomic_eq_geom_sum hn' R apply_fun eval x at this rw [← cons_self_properDivisors hn'.ne', Finset.erase_cons_of_ne _ hn''.ne', Finset.prod_cons, diff --git a/Mathlib/RingTheory/Polynomial/Pochhammer.lean b/Mathlib/RingTheory/Polynomial/Pochhammer.lean index f5fefe3fd2011..b3aa53ee26342 100644 --- a/Mathlib/RingTheory/Polynomial/Pochhammer.lean +++ b/Mathlib/RingTheory/Polynomial/Pochhammer.lean @@ -119,7 +119,6 @@ theorem pochhammer_succ_comp_X_add_one (n : ℕ) : pochhammer ℕ (n + 1) + (n + 1) * (pochhammer ℕ n).comp (X + 1) by simpa [map_comp] using congr_arg (Polynomial.map (Nat.castRingHom S)) this nth_rw 2 [pochhammer_succ_left] - simp only rw [← add_mul, pochhammer_succ_right ℕ n, mul_comp, mul_comm, add_comp, X_comp, nat_cast_comp, add_comm, ← add_assoc] ring diff --git a/Mathlib/RingTheory/PowerBasis.lean b/Mathlib/RingTheory/PowerBasis.lean index 33cffd1e49ec0..e39f6abc0327b 100644 --- a/Mathlib/RingTheory/PowerBasis.lean +++ b/Mathlib/RingTheory/PowerBasis.lean @@ -175,7 +175,6 @@ theorem dim_le_natDegree_of_root (pb : PowerBasis A S) {p : A[X]} (ne_zero : p refine' Fintype.sum_eq_zero _ fun i => _ simp_rw [aeval_eq_sum_range' hlt, Finset.sum_range, ← pb.basis_eq_pow] at root have := Fintype.linearIndependent_iff.1 pb.basis.linearIndependent _ root - dsimp only at this rw [this, monomial_zero_right] #align power_basis.dim_le_nat_degree_of_root PowerBasis.dim_le_natDegree_of_root diff --git a/Mathlib/RingTheory/RootsOfUnity/Minpoly.lean b/Mathlib/RingTheory/RootsOfUnity/Minpoly.lean index c0b3ba34cc0e2..23b5d58850ee1 100644 --- a/Mathlib/RingTheory/RootsOfUnity/Minpoly.lean +++ b/Mathlib/RingTheory/RootsOfUnity/Minpoly.lean @@ -61,7 +61,6 @@ set_option linter.uppercaseLean3 false in theorem separable_minpoly_mod {p : ℕ} [Fact p.Prime] (hdiv : ¬p ∣ n) : Separable (map (Int.castRingHom (ZMod p)) (minpoly ℤ μ)) := by have hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1 := by - simp [Polynomial.map_pow, map_X, Polynomial.map_one, Polynomial.map_sub] convert RingHom.map_dvd (mapRingHom (Int.castRingHom (ZMod p))) (minpoly_dvd_x_pow_sub_one h) simp only [map_sub, map_pow, coe_mapRingHom, map_X, map_one] diff --git a/Mathlib/RingTheory/Valuation/ValuationSubring.lean b/Mathlib/RingTheory/Valuation/ValuationSubring.lean index ba1d283296f9c..c72ec65bd8197 100644 --- a/Mathlib/RingTheory/Valuation/ValuationSubring.lean +++ b/Mathlib/RingTheory/Valuation/ValuationSubring.lean @@ -615,7 +615,7 @@ theorem image_maximalIdeal : ((↑) : A → K) '' LocalRing.maximalIdeal A = A.n ext a simp only [Set.mem_image, SetLike.mem_coe, mem_nonunits_iff_exists_mem_maximalIdeal] erw [Subtype.exists] - simp_rw [Subtype.coe_mk, exists_and_right, exists_eq_right] + simp_rw [exists_and_right, exists_eq_right] -- Porting note: added simp #align valuation_subring.image_maximal_ideal ValuationSubring.image_maximalIdeal diff --git a/Mathlib/RingTheory/WittVector/MulCoeff.lean b/Mathlib/RingTheory/WittVector/MulCoeff.lean index ade1028116c98..2cd1b5e4cbcaf 100644 --- a/Mathlib/RingTheory/WittVector/MulCoeff.lean +++ b/Mathlib/RingTheory/WittVector/MulCoeff.lean @@ -281,7 +281,6 @@ theorem nth_mul_coeff' (n : ℕ) : intro x y dsimp [peval] rw [← hf₀] - simp only [Function.uncurry_apply_pair] congr ext a cases' a with a ha diff --git a/Mathlib/SetTheory/Game/Basic.lean b/Mathlib/SetTheory/Game/Basic.lean index 0f85fa84aa86d..0f2df47e91aef 100644 --- a/Mathlib/SetTheory/Game/Basic.lean +++ b/Mathlib/SetTheory/Game/Basic.lean @@ -220,7 +220,6 @@ theorem quot_sub (a b : PGame) : ⟦a - b⟧ = (⟦a⟧ : Game) - ⟦b⟧ := theorem quot_eq_of_mk'_quot_eq {x y : PGame} (L : x.LeftMoves ≃ y.LeftMoves) (R : x.RightMoves ≃ y.RightMoves) (hl : ∀ i, (⟦x.moveLeft i⟧ : Game) = ⟦y.moveLeft (L i)⟧) (hr : ∀ j, (⟦x.moveRight j⟧ : Game) = ⟦y.moveRight (R j)⟧) : (⟦x⟧ : Game) = ⟦y⟧ := by - simp_rw [Quotient.eq'] at hl hr exact Quot.sound (equiv_of_mk_equiv L R (fun _ => Game.PGame.equiv_iff_game_eq.2 (hl _)) (fun _ => Game.PGame.equiv_iff_game_eq.2 (hr _))) #align pgame.quot_eq_of_mk_quot_eq PGame.quot_eq_of_mk'_quot_eq diff --git a/Mathlib/SetTheory/Ordinal/Notation.lean b/Mathlib/SetTheory/Ordinal/Notation.lean index a91f50781e885..070b506c7ec29 100644 --- a/Mathlib/SetTheory/Ordinal/Notation.lean +++ b/Mathlib/SetTheory/Ordinal/Notation.lean @@ -464,8 +464,8 @@ theorem add_nfBelow {b} : ∀ {o₁ o₂}, NFBelow o₁ b → NFBelow o₂ b → have h' := add_nfBelow (h₁.snd.mono <| le_of_lt h₁.lt) h₂ simp [oadd_add]; revert h'; cases' a + o with e' n' a' <;> intro h' · exact NFBelow.oadd h₁.fst NFBelow.zero h₁.lt - simp [add]; have : ((e.cmp e').Compares e e') := @cmp_compares _ _ h₁.fst h'.fst - cases h: cmp e e' <;> simp [add] <;> dsimp [addAux] <;> simp [h] + have : ((e.cmp e').Compares e e') := @cmp_compares _ _ h₁.fst h'.fst + cases h: cmp e e' <;> dsimp [addAux] <;> simp [h] · exact h' · simp [h] at this subst e' @@ -835,7 +835,7 @@ instance nf_opow (o₁ o₂) [NF o₁] [NF o₂] : NF (o₁ ^ o₂) := by infer_instance · simp [(· ^ ·),Pow.pow,pow, opow, opowAux2, e₁, e₂, split_eq_scale_split' e₂] have := na.fst - cases' k with k <;> simp <;> skip <;> dsimp + cases' k with k <;> simp · infer_instance · cases k <;> cases m <;> infer_instance #align onote.NF_opow ONote.nf_opow diff --git a/Mathlib/SetTheory/Surreal/Dyadic.lean b/Mathlib/SetTheory/Surreal/Dyadic.lean index 47fbaaf7c3b03..9057dd768ba1e 100644 --- a/Mathlib/SetTheory/Surreal/Dyadic.lean +++ b/Mathlib/SetTheory/Surreal/Dyadic.lean @@ -242,7 +242,7 @@ def dyadicMap : Localization.Away (2 : ℤ) →+ Surreal where have h₂ : 1 < (2 : ℤ).natAbs := one_lt_two have hpow₂ := Submonoid.log_pow_int_eq_self h₂ simp_rw [Submonoid.pow_apply] at hpow₂ - simp_rw [Localization.add_mk, Localization.liftOn_mk, Subtype.coe_mk, + simp_rw [Localization.add_mk, Localization.liftOn_mk, Submonoid.log_mul (Int.pow_right_injective h₂), hpow₂] calc (2 ^ b' * c + 2 ^ d' * a) • powHalf (b' + d') = diff --git a/Mathlib/Tactic/ToAdditive.lean b/Mathlib/Tactic/ToAdditive.lean index c407413a57f5f..4294c944ab02b 100644 --- a/Mathlib/Tactic/ToAdditive.lean +++ b/Mathlib/Tactic/ToAdditive.lean @@ -96,7 +96,7 @@ Id.run do if (s.get i₁).isUpper then if let some strs := endCapitalNames.find? (s.extract 0 i₁) then if let some (pref, newS) := strs.findSome? - fun x ↦ (s.extract i₁ s.endPos).dropPrefix? x |>.map (x, ·.toString) then + fun x : String ↦ (s.extract i₁ s.endPos).dropPrefix? x |>.map (x, ·.toString) then return splitCase newS 0 <| (s.extract 0 i₁ ++ pref)::r if !(s.get i₀).isUpper then return splitCase (s.extract i₁ s.endPos) 0 <| (s.extract 0 i₁)::r diff --git a/Mathlib/Topology/Algebra/Semigroup.lean b/Mathlib/Topology/Algebra/Semigroup.lean index 1a52fd213e753..3edff530b6e16 100644 --- a/Mathlib/Topology/Algebra/Semigroup.lean +++ b/Mathlib/Topology/Algebra/Semigroup.lean @@ -67,8 +67,7 @@ theorem exists_idempotent_of_compact_t2_of_continuous_mul_left {M} [Nonempty M] convert @IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed _ _ _ hcnemp.coe_sort ((↑) : c → Set M) ?_ ?_ ?_ ?_ - · simp only [Subtype.range_coe_subtype, Set.setOf_mem_eq] - exact Set.sInter_eq_iInter + · exact Set.sInter_eq_iInter · refine' DirectedOn.directed_val (IsChain.directedOn hc.symm) exacts [fun i => (hcs i.prop).2.1, fun i => (hcs i.prop).1.isCompact, fun i => (hcs i.prop).1] · rw [Set.mem_sInter] diff --git a/Mathlib/Topology/Algebra/Valuation.lean b/Mathlib/Topology/Algebra/Valuation.lean index 72ef0058df3cc..2c9a7b18b6255 100644 --- a/Mathlib/Topology/Algebra/Valuation.lean +++ b/Mathlib/Topology/Algebra/Valuation.lean @@ -56,8 +56,7 @@ theorem subgroups_basis : RingSubgroupsBasis fun γ : Γ₀ˣ => (v.ltAddSubgrou change v (x * y) < _ rw [Valuation.map_mul, Hx, MulZeroClass.zero_mul] exact Units.zero_lt γ - · simp only [image_subset_iff, setOf_subset_setOf, preimage_setOf_eq, Valuation.map_mul] - use γx⁻¹ * γ + · use γx⁻¹ * γ rintro y (vy_lt : v y < ↑(γx⁻¹ * γ)) change (v (x * y) : Γ₀) < γ rw [Valuation.map_mul, Hx, mul_comm] diff --git a/Mathlib/Topology/Algebra/ValuedField.lean b/Mathlib/Topology/Algebra/ValuedField.lean index cdb9a2fcbea86..60018dfa547f5 100644 --- a/Mathlib/Topology/Algebra/ValuedField.lean +++ b/Mathlib/Topology/Algebra/ValuedField.lean @@ -311,7 +311,6 @@ noncomputable def extensionValuation : Valuation (hat K) Γ₀ where (isClosed_le (cont.comp continuous_add) <| cont.comp continuous_fst).union (isClosed_le (cont.comp continuous_add) <| cont.comp continuous_snd) · intro x y - dsimp norm_cast rw [← le_max_iff] exact v.map_add x y diff --git a/Mathlib/Topology/Category/TopCat/Limits/Products.lean b/Mathlib/Topology/Category/TopCat/Limits/Products.lean index bba1b4f380107..49c6249845f29 100644 --- a/Mathlib/Topology/Category/TopCat/Limits/Products.lean +++ b/Mathlib/Topology/Category/TopCat/Limits/Products.lean @@ -325,8 +325,6 @@ theorem binaryCofan_isColimit_iff {X Y : TopCat} (c : BinaryCofan X Y) : (binaryCofanIsColimit X Y)).symm.openEmbedding.comp openEmbedding_inl, (homeoOfIso <| h.coconePointUniqueUpToIso (binaryCofanIsColimit X Y)).symm.openEmbedding.comp openEmbedding_inr, _⟩ - simp only [Functor.map_comp] - erw [Set.range_comp, ← eq_compl_iff_isCompl, coe_comp, coe_comp, Set.range_comp _ Sum.inr, ← Set.image_compl_eq (homeoOfIso <| h.coconePointUniqueUpToIso (binaryCofanIsColimit X Y)).symm.bijective, Set.compl_range_inr, Set.image_comp] diff --git a/Mathlib/Topology/ContinuousFunction/Ideals.lean b/Mathlib/Topology/ContinuousFunction/Ideals.lean index a1736c198eb9f..431f1ed34d0ac 100644 --- a/Mathlib/Topology/ContinuousFunction/Ideals.lean +++ b/Mathlib/Topology/ContinuousFunction/Ideals.lean @@ -108,7 +108,7 @@ theorem mem_idealOfSet {s : Set X} {f : C(X, R)} : #align continuous_map.mem_ideal_of_set ContinuousMap.mem_idealOfSet theorem not_mem_idealOfSet {s : Set X} {f : C(X, R)} : f ∉ idealOfSet R s ↔ ∃ x ∈ sᶜ, f x ≠ 0 := by - simp_rw [mem_idealOfSet, exists_prop]; push_neg; rfl + simp_rw [mem_idealOfSet]; push_neg; rfl #align continuous_map.not_mem_ideal_of_set ContinuousMap.not_mem_idealOfSet /-- Given an ideal `I` of `C(X, R)`, construct the set of points for which every function in the @@ -124,7 +124,7 @@ theorem not_mem_setOfIdeal {I : Ideal C(X, R)} {x : X} : theorem mem_setOfIdeal {I : Ideal C(X, R)} {x : X} : x ∈ setOfIdeal I ↔ ∃ f ∈ I, (f : C(X, R)) x ≠ 0 := by - simp_rw [setOfIdeal, Set.mem_compl_iff, Set.mem_setOf, exists_prop]; push_neg; rfl + simp_rw [setOfIdeal, Set.mem_compl_iff, Set.mem_setOf]; push_neg; rfl #align continuous_map.mem_set_of_ideal ContinuousMap.mem_setOfIdeal theorem setOfIdeal_open [T2Space R] (I : Ideal C(X, R)) : IsOpen (setOfIdeal I) := by diff --git a/Mathlib/Topology/Gluing.lean b/Mathlib/Topology/Gluing.lean index bdbf56074403a..694923143d2dd 100644 --- a/Mathlib/Topology/Gluing.lean +++ b/Mathlib/Topology/Gluing.lean @@ -168,7 +168,6 @@ theorem eqvGen_of_π_eq 𝖣.diagram.fstSigmaMap 𝖣.diagram.sndSigmaMap) x y := by delta GlueData.π Multicoequalizer.sigmaπ at h - simp_rw [comp_app] at h -- Porting note: inlined `inferInstance` instead of leaving as a side goal. replace h := (TopCat.mono_iff_injective (Multicoequalizer.isoCoequalizer 𝖣.diagram).inv).mp inferInstance h diff --git a/Mathlib/Topology/Instances/AddCircle.lean b/Mathlib/Topology/Instances/AddCircle.lean index 0dc0d5e016f7a..d10558eef48b0 100644 --- a/Mathlib/Topology/Instances/AddCircle.lean +++ b/Mathlib/Topology/Instances/AddCircle.lean @@ -459,7 +459,7 @@ def setAddOrderOfEquiv {n : ℕ} (hn : 0 < n) : Equiv.ofBijective (fun m => ⟨↑((m : 𝕜) / n * p), addOrderOf_div_of_gcd_eq_one hn m.prop.2⟩) (by refine' ⟨fun m₁ m₂ h => Subtype.ext _, fun u => _⟩ - · simp_rw [Subtype.ext_iff, Subtype.coe_mk] at h + · simp_rw [Subtype.ext_iff] at h rw [← sub_eq_zero, ← coe_sub, ← sub_mul, ← sub_div, ← Int.cast_ofNat m₁, ← Int.cast_ofNat m₂, ← Int.cast_sub, coe_eq_zero_iff] at h obtain ⟨m, hm⟩ := h diff --git a/Mathlib/Topology/List.lean b/Mathlib/Topology/List.lean index 586d9da436df9..1e734d9d3ec95 100644 --- a/Mathlib/Topology/List.lean +++ b/Mathlib/Topology/List.lean @@ -90,7 +90,7 @@ theorem tendsto_cons_iff {β : Type*} {f : List α → β} {b : Filter β} {a : simp only [nhds_cons, Filter.prod_eq, (Filter.map_def _ _).symm, (Filter.seq_eq_filter_seq _ _).symm] simp [-Filter.map_def, (· ∘ ·), functor_norm] - rw [this, Filter.tendsto_map'_iff]; dsimp; rfl + rw [this, Filter.tendsto_map'_iff]; rfl #align list.tendsto_cons_iff List.tendsto_cons_iff theorem continuous_cons : Continuous fun x : α × List α => (x.1::x.2 : List α) := diff --git a/Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean b/Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean index 6d2678b6eca17..8fafb2fec95bd 100644 --- a/Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean +++ b/Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean @@ -128,8 +128,7 @@ of all opens contained in some `U i`. instance : Functor.Final (pairwiseToOpensLeCover U) := ⟨fun V => isConnected_of_zigzag fun A B => by - rcases A with ⟨⟨⟨⟩⟩, ⟨i⟩ | ⟨i, j⟩, a⟩ <;> rcases B with ⟨⟨⟨⟩⟩, ⟨i'⟩ | ⟨i', j'⟩, b⟩ <;> - dsimp at * + rcases A with ⟨⟨⟨⟩⟩, ⟨i⟩ | ⟨i, j⟩, a⟩ <;> rcases B with ⟨⟨⟨⟩⟩, ⟨i'⟩ | ⟨i', j'⟩, b⟩ · refine' ⟨[{ left := ⟨⟨⟩⟩ right := pair i i' diff --git a/Mathlib/Topology/Spectral/Hom.lean b/Mathlib/Topology/Spectral/Hom.lean index 8e5fa8bdf03d1..3c1466d21f02c 100644 --- a/Mathlib/Topology/Spectral/Hom.lean +++ b/Mathlib/Topology/Spectral/Hom.lean @@ -191,7 +191,7 @@ theorem coe_comp_continuousMap (f : SpectralMap β γ) (g : SpectralMap α β) : -- porting note: removed `simp` from this and added lemma above to address `simpNF` lint theorem coe_comp_continuousMap' (f : SpectralMap β γ) (g : SpectralMap α β) : (f.comp g : ContinuousMap α γ) = (f : ContinuousMap β γ).comp g := by - simp only [@coe_comp]; rfl + rfl #align spectral_map.coe_comp_continuous_map SpectralMap.coe_comp_continuousMap' @[simp] diff --git a/test/Simps.lean b/test/Simps.lean index 3688fbbaefbbc..ae17e6f543e05 100644 --- a/test/Simps.lean +++ b/test/Simps.lean @@ -804,8 +804,7 @@ example {x : Set ℕ} (h : Set.univ = x) : Nat.SetPlus1.s = x := by def Nat.SetPlus2 : SetPlus ℕ := ⟨Set.univ, 1, trivial⟩ example {x : Set ℕ} (h : Set.univ = x) : Nat.SetPlus2.s = x := by - dsimp only [Nat.SetPlus2_s] - -- successIfFail { rw [h] } -- todo + fail_if_success { rw [h] } exact h @[simps (config := {rhsMd := .default})] @@ -942,13 +941,12 @@ example (h : false) (x y : { x : Fin (Nat.add 3 0) // 1 + 1 = 2 }) : myTypeDef.A guard_target = { _x : Fin 3 // True } = Unit /- note: calling only one of `simp` or `dsimp` does not produce the current target as the following tests show. -/ - -- successIfFail { guard_hyp x : { x : Fin 3 // true } } + fail_if_success { guard_hyp x : { _x : Fin 3 // true } } dsimp at x - -- successIfFail { guard_hyp x : { x : Fin 3 // true } } + fail_if_success { guard_hyp x : { _x : Fin 3 // true } } simp at y - -- successIfFail { guard_hyp y : { x : Fin 3 // true } } + fail_if_success { guard_hyp y : { _x : Fin 3 // true } } simp at x - dsimp at y guard_hyp x : { _x : Fin 3 // True } guard_hyp y : { _x : Fin 3 // True } contradiction diff --git a/test/says.lean b/test/says.lean index c0a51f254dd74..f60d86c39c29b 100644 --- a/test/says.lean +++ b/test/says.lean @@ -40,7 +40,7 @@ example : true := by -- Check that `says` does not reverify the right-hand-side. set_option says.no_verify_in_CI true in example (x y : List α) : (x ++ y).length = x.length + y.length := by - simp? says simp only [] + simp? says skip simp -- Check that with `says.verify` `says` will reverify that the left-hand-side constructs diff --git a/test/solve_by_elim/basic.lean b/test/solve_by_elim/basic.lean index 552feef7edb4a..3dd74e58d775c 100644 --- a/test/solve_by_elim/basic.lean +++ b/test/solve_by_elim/basic.lean @@ -113,7 +113,6 @@ example : 6 = 6 ∧ [7] = [7] := by -- Test that `solve_by_elim*`, which works on multiple goals, -- successfully uses the relevant local hypotheses for each goal. example (f g : ℕ → Prop) : (∃ k : ℕ, f k) ∨ (∃ k : ℕ, g k) ↔ ∃ k : ℕ, f k ∨ g k := by - dsimp at * fconstructor rintro (⟨n, fn⟩ | ⟨n, gn⟩) pick_goal 3