From 11b15ff5c728a9c185d7c7c9eb646db823234dc2 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Thu, 23 Apr 2026 23:07:03 +0800 Subject: [PATCH 1/7] kill erw --- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean | 8 ++------ Mathlib/LinearAlgebra/Matrix/Block.lean | 3 +-- Mathlib/LinearAlgebra/TensorProduct/Quotient.lean | 7 +------ .../Integral/Bochner/VitaliCaratheodory.lean | 2 +- Mathlib/MeasureTheory/Integral/Lebesgue/Map.lean | 4 ++-- .../VectorMeasure/Decomposition/RadonNikodym.lean | 4 ++-- Mathlib/RingTheory/Extension/Presentation/Basic.lean | 2 +- 7 files changed, 10 insertions(+), 20 deletions(-) diff --git a/Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean b/Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean index ff5da41877da7e..e21f01884762f4 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean +++ b/Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean @@ -307,15 +307,11 @@ lemma L₀X₂ToP_comp_φ₁ : S.L₀X₂ToP ≫ S.φ₁ = 0 := by set_option backward.isDefEq.respectTransparency false in lemma L₀_g_δ : S.L₀.g ≫ S.δ = 0 := by - rw [← L₀X₂ToP_comp_pullback_snd, assoc] - erw [S.L₀'_exact.g_desc] - rw [L₀X₂ToP_comp_φ₁_assoc, zero_comp] + rw [← L₀X₂ToP_comp_pullback_snd, assoc, S.snd_δ, L₀X₂ToP_comp_φ₁_assoc, zero_comp] set_option backward.isDefEq.respectTransparency false in lemma δ_L₃_f : S.δ ≫ S.L₃.f = 0 := by - rw [← cancel_epi S.L₀'.g] - erw [S.L₀'_exact.g_desc_assoc] - simp [S.v₂₃.comm₁₂, φ₂] + simp [← cancel_epi S.L₀'.g, δ, S.v₂₃.comm₁₂, φ₂] /-- The short complex `L₀.X₂ ⟶ L₀.X₃ ⟶ L₃.X₁`. -/ @[simps] diff --git a/Mathlib/LinearAlgebra/Matrix/Block.lean b/Mathlib/LinearAlgebra/Matrix/Block.lean index b723063aa7e338..acb3aa256054fa 100644 --- a/Mathlib/LinearAlgebra/Matrix/Block.lean +++ b/Mathlib/LinearAlgebra/Matrix/Block.lean @@ -263,8 +263,7 @@ protected theorem BlockTriangular.det [DecidableEq α] [LinearOrder α] (hM : Bl let he : { a // b' a = l } ≃ { a // b a = l } := haveI hc : ∀ i, b i = l → b i ≠ k := fun i hi => ne_of_eq_of_ne hi (ne_of_mem_erase hl) Equiv.subtypeSubtypeEquivSubtype @hc - simp only [toSquareBlock_def] - erw [← Matrix.det_reindex_self he.symm fun i j : { a // b a = l } => M ↑i ↑j] + rw [toSquareBlock_def, ← Matrix.det_reindex_self he.symm] rfl · intro i hi j hj apply hM diff --git a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean index bc98cbfd4fae12..d0595a460fb70d 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean @@ -133,12 +133,7 @@ noncomputable def tensorQuotientEquiv (n : Submodule R N) : (M ⊗[R] N) ⧸ (LinearMap.range (map (LinearMap.id : M →ₗ[R] M) n.subtype)) := congr ((Submodule.quotEquivOfEqBot _ rfl).symm) (LinearEquiv.refl _ _) ≪≫ₗ quotientTensorQuotientEquiv (⊥ : Submodule R M) n ≪≫ₗ - Submodule.Quotient.equiv _ _ (LinearEquiv.refl _ _) (by - simp only [Submodule.map_sup] - erw [Submodule.map_id, Submodule.map_id] - simp only [sup_eq_right] - rw [range_map_eq_span_tmul, range_map_eq_span_tmul] - simp) + Submodule.Quotient.equiv _ _ (LinearEquiv.refl _ _) (by simp [range_map_eq_span_tmul]) @[simp] lemma tensorQuotientEquiv_apply_mk_tmul (n : Submodule R N) (x : M) (y : N) : diff --git a/Mathlib/MeasureTheory/Integral/Bochner/VitaliCaratheodory.lean b/Mathlib/MeasureTheory/Integral/Bochner/VitaliCaratheodory.lean index fe918492197a54..b5e56842f647f8 100644 --- a/Mathlib/MeasureTheory/Integral/Bochner/VitaliCaratheodory.lean +++ b/Mathlib/MeasureTheory/Integral/Bochner/VitaliCaratheodory.lean @@ -367,7 +367,7 @@ theorem exists_upperSemicontinuous_le_lintegral_le (f : α → ℝ≥0) (int_f : ∃ fs : α →ₛ ℝ≥0, (∀ x, fs x ≤ f x) ∧ (∫⁻ x, f x ∂μ) ≤ (∫⁻ x, fs x ∂μ) + ε / 2 := by have := ENNReal.lt_add_right int_f (ENNReal.half_pos ε0).ne' conv_rhs at this => rw [lintegral_eq_nnreal (fun x => (f x : ℝ≥0∞)) μ] - erw [ENNReal.biSup_add] at this <;> [skip; exact ⟨0, fun x => by simp⟩] + rw [ENNReal.biSup_add'] at this <;> [skip; exact ⟨0, fun x => by simp⟩] simp only [lt_iSup_iff] at this rcases this with ⟨fs, fs_le_f, int_fs⟩ refine ⟨fs, fun x => by simpa only [ENNReal.coe_le_coe] using fs_le_f x, ?_⟩ diff --git a/Mathlib/MeasureTheory/Integral/Lebesgue/Map.lean b/Mathlib/MeasureTheory/Integral/Lebesgue/Map.lean index 770b2a1fdbd461..71390c0290ab17 100644 --- a/Mathlib/MeasureTheory/Integral/Lebesgue/Map.lean +++ b/Mathlib/MeasureTheory/Integral/Lebesgue/Map.lean @@ -72,8 +72,8 @@ theorem setLIntegral_map {f : β → ℝ≥0∞} {g : α → β} {s : Set β} theorem lintegral_indicator_const_comp {f : α → β} {s : Set β} (hf : Measurable f) (hs : MeasurableSet s) (c : ℝ≥0∞) : ∫⁻ a, s.indicator (fun _ => c) (f a) ∂μ = c * μ (f ⁻¹' s) := by - erw [lintegral_comp (measurable_const.indicator hs) hf] - rw [lintegral_indicator_const hs, Measure.map_apply hf hs] + rw [← lintegral_map (measurable_const.indicator hs) hf, lintegral_indicator_const hs, + Measure.map_apply hf hs] /-- If `g : α → β` is a measurable embedding and `f : β → ℝ≥0∞` is any function (not necessarily measurable), then `∫⁻ a, f a ∂(map g μ) = ∫⁻ a, f (g a) ∂μ`. Compare with `lintegral_map` which diff --git a/Mathlib/MeasureTheory/VectorMeasure/Decomposition/RadonNikodym.lean b/Mathlib/MeasureTheory/VectorMeasure/Decomposition/RadonNikodym.lean index d9cf55a6de35e9..e000659ce34903 100644 --- a/Mathlib/MeasureTheory/VectorMeasure/Decomposition/RadonNikodym.lean +++ b/Mathlib/MeasureTheory/VectorMeasure/Decomposition/RadonNikodym.lean @@ -34,8 +34,8 @@ theorem withDensityᵥ_rnDeriv_eq (s : SignedMeasure α) (μ : Measure α) [Sigm rw [withDensityᵥ_apply (integrable_rnDeriv _ _) hi, rnDeriv_def, integral_sub, setIntegral_toReal_rnDeriv h.1 i, setIntegral_toReal_rnDeriv h.2 i] · conv_rhs => rw [← s.toSignedMeasure_toJordanDecomposition] - erw [VectorMeasure.sub_apply] - rw [toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi, measureReal_def, + rw [JordanDecomposition.toSignedMeasure, VectorMeasure.sub_apply, + toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi, measureReal_def, measureReal_def] all_goals refine Integrable.integrableOn ?_ diff --git a/Mathlib/RingTheory/Extension/Presentation/Basic.lean b/Mathlib/RingTheory/Extension/Presentation/Basic.lean index b532846bd74134..cb83028d4b3c6d 100644 --- a/Mathlib/RingTheory/Extension/Presentation/Basic.lean +++ b/Mathlib/RingTheory/Extension/Presentation/Basic.lean @@ -257,7 +257,7 @@ private lemma span_range_relation_eq_ker_baseChange : rw [map_zero] at Z simp only [SetLike.mem_coe, RingHom.mem_ker, ← Z, ← hy, TensorProduct.includeRight_apply] - erw [aeval_map_algebraMap T (P.baseChange T).val (P.relation y)] + rw [aeval_map_algebraMap T (P.baseChange T).val (P.relation y)] change _ = TensorProduct.includeRight.toRingHom _ rw [map_aeval, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, TensorProduct.includeRight.comp_algebraMap] From cb18bbc97aae491a819a2ed934e6a52dace6addb Mon Sep 17 00:00:00 2001 From: LehengChen Date: Sat, 25 Apr 2026 06:41:44 +0800 Subject: [PATCH 2/7] Accept erw-elim-v3-0127 task_id: erw-elim-v3-0127 target_path: Mathlib/CategoryTheory/Localization/Construction.lean artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/erw-elim-v3-0127 --- Mathlib/CategoryTheory/Localization/Construction.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Mathlib/CategoryTheory/Localization/Construction.lean b/Mathlib/CategoryTheory/Localization/Construction.lean index 66419db1524e1e..c4722f9c7d0740 100644 --- a/Mathlib/CategoryTheory/Localization/Construction.lean +++ b/Mathlib/CategoryTheory/Localization/Construction.lean @@ -330,9 +330,7 @@ def unitIso : 𝟭 (W.Localization ⥤ D) ≅ functor W D ⋙ inverse W D := (by refine Functor.ext (fun G => ?_) fun G₁ G₂ τ => ?_ · apply uniq - dsimp [Functor] - erw [fac] - rfl + simp [functor, inverse, fac] · apply natTrans_hcomp_injective ext X simp) From a47bc9a921e13869a75d9db9bcdf7f339d92b47c Mon Sep 17 00:00:00 2001 From: LehengChen Date: Sat, 25 Apr 2026 05:47:40 +0800 Subject: [PATCH 3/7] Accept erw-elim-v3-0117 task_id: erw-elim-v3-0117 target_path: Mathlib/CategoryTheory/Limits/Shapes/Images.lean artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/erw-elim-v3-0117 --- Mathlib/CategoryTheory/Limits/Shapes/Images.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Images.lean b/Mathlib/CategoryTheory/Limits/Shapes/Images.lean index 3e2eeaa88d8103..d3d5da1ca5ce78 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Images.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Images.lean @@ -738,9 +738,9 @@ instance (priority := 100) hasImageMapOfIsIso {f g : Arrow C} [HasImage f.hom] [ HasImageMap.mk { map := image.lift ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)) map_ι := by - erw [← cancel_mono (inv sq).right, Category.assoc, ← MonoFactorisation.ofArrowIso_m, - image.lift_fac, Category.assoc, ← Comma.comp_right, IsIso.hom_inv_id, Comma.id_right, - Category.comp_id] } + rw [← cancel_mono (inv sq).right, ← image.as_ι, Category.assoc, + ← MonoFactorisation.ofArrowIso_m, image.lift_fac, Category.assoc, + ← Comma.comp_right, IsIso.hom_inv_id, Comma.id_right, Category.comp_id] } instance HasImageMap.comp {f g h : Arrow C} [HasImage f.hom] [HasImage g.hom] [HasImage h.hom] (sq1 : f ⟶ g) (sq2 : g ⟶ h) [HasImageMap sq1] [HasImageMap sq2] : HasImageMap (sq1 ≫ sq2) := From 004d52af0b5277a1f4079b87590ee6f27e62c322 Mon Sep 17 00:00:00 2001 From: LehengChen Date: Sat, 25 Apr 2026 13:23:52 +0800 Subject: [PATCH 4/7] Accept erw-elim-v3-0280 task_id: erw-elim-v3-0280 target_path: Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/erw-elim-v3-0280 --- .../Sheaves/SheafCondition/PairwiseIntersections.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean b/Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean index eaab0810122e68..17452ef1441df0 100644 --- a/Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean +++ b/Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean @@ -371,7 +371,7 @@ def interUnionPullbackConeLift : s.pt ⟶ F.1.obj (op (U ⊔ V)) := by set_option backward.isDefEq.respectTransparency false in theorem interUnionPullbackConeLift_left : interUnionPullbackConeLift F U V s ≫ F.1.map (homOfLE le_sup_left).op = s.fst := by - erw [Category.assoc] + rw [interUnionPullbackConeLift, Category.assoc] simp_rw [← F.1.map_comp] exact (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 _).some.fac _ <| @@ -380,7 +380,7 @@ theorem interUnionPullbackConeLift_left : set_option backward.isDefEq.respectTransparency false in theorem interUnionPullbackConeLift_right : interUnionPullbackConeLift F U V s ≫ F.1.map (homOfLE le_sup_right).op = s.snd := by - erw [Category.assoc] + rw [interUnionPullbackConeLift, Category.assoc] simp_rw [← F.1.map_comp] exact (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 _).some.fac _ <| @@ -409,10 +409,10 @@ def isLimitPullbackCone : IsLimit (interUnionPullbackCone F U V) := by apply (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 ι).some.hom_ext rintro ((_ | _) | (_ | _)) <;> rw [Category.assoc, Category.assoc] - · erw [← F.1.map_comp] + · rw [Functor.mapCone_π_app, ← F.1.map_comp] convert h₁ apply interUnionPullbackConeLift_left - · erw [← F.1.map_comp] + · rw [Functor.mapCone_π_app, ← F.1.map_comp] convert h₂ apply interUnionPullbackConeLift_right all_goals From f1a38a1b45d3be08afe51e0c583f338ec0286a1c Mon Sep 17 00:00:00 2001 From: LehengChen Date: Sat, 25 Apr 2026 10:41:19 +0800 Subject: [PATCH 5/7] Accept erw-elim-v3-0202 task_id: erw-elim-v3-0202 target_path: Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/erw-elim-v3-0202 --- .../Geometry/RingedSpace/PresheafedSpace/HasColimits.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean b/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean index 8b1a3aadd2054f..e0c59bb85771d6 100644 --- a/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean +++ b/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean @@ -304,7 +304,7 @@ def colimitPresheafObjIsoComponentwiseLimit (F : J ⥤ PresheafedSpace.{_, _, v} simp only [Functor.op_obj, op_inj_iff, Opens.map_coe, SetLike.ext'_iff, Set.preimage_preimage] refine congr_arg (Set.preimage · U.1) (funext fun x => ?_) - erw [← TopCat.comp_app] + simp only [colimitCocone, colimit, ← TopCat.comp_app] congr exact ι_preservesColimitIso_inv (forget C) F (unop X) · intro X Y f @@ -329,7 +329,8 @@ theorem colimitPresheafObjIsoComponentwiseLimit_inv_ι_app (F : J ⥤ Presheafed rw [map_id, comp_id, assoc, assoc, assoc, NatTrans.naturality, ← comp_c_app_assoc, congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc] - erw [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc] + rw [colimitCocone_ι_app_c] + rw [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc] simp set_option backward.isDefEq.respectTransparency false in From ecda1edf5faa5a5e425d206f5bb119155638780b Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Sat, 25 Apr 2026 15:44:00 +0800 Subject: [PATCH 6/7] fix --- Mathlib/CategoryTheory/Limits/Shapes/Images.lean | 6 +++--- .../Geometry/RingedSpace/PresheafedSpace/HasColimits.lean | 6 ++---- 2 files changed, 5 insertions(+), 7 deletions(-) diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Images.lean b/Mathlib/CategoryTheory/Limits/Shapes/Images.lean index d3d5da1ca5ce78..3e2eeaa88d8103 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Images.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Images.lean @@ -738,9 +738,9 @@ instance (priority := 100) hasImageMapOfIsIso {f g : Arrow C} [HasImage f.hom] [ HasImageMap.mk { map := image.lift ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)) map_ι := by - rw [← cancel_mono (inv sq).right, ← image.as_ι, Category.assoc, - ← MonoFactorisation.ofArrowIso_m, image.lift_fac, Category.assoc, - ← Comma.comp_right, IsIso.hom_inv_id, Comma.id_right, Category.comp_id] } + erw [← cancel_mono (inv sq).right, Category.assoc, ← MonoFactorisation.ofArrowIso_m, + image.lift_fac, Category.assoc, ← Comma.comp_right, IsIso.hom_inv_id, Comma.id_right, + Category.comp_id] } instance HasImageMap.comp {f g h : Arrow C} [HasImage f.hom] [HasImage g.hom] [HasImage h.hom] (sq1 : f ⟶ g) (sq2 : g ⟶ h) [HasImageMap sq1] [HasImageMap sq2] : HasImageMap (sq1 ≫ sq2) := diff --git a/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean b/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean index e0c59bb85771d6..c63842208ca42b 100644 --- a/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean +++ b/Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean @@ -327,10 +327,8 @@ theorem colimitPresheafObjIsoComponentwiseLimit_inv_ι_app (F : J ⥤ Presheafed congr_app (Iso.symm_inv _)] dsimp rw [map_id, comp_id, assoc, assoc, assoc, NatTrans.naturality, - ← comp_c_app_assoc, - congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc] - rw [colimitCocone_ι_app_c] - rw [limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc] + ← comp_c_app_assoc, congr_app (colimit.isoColimitCocone_ι_hom _ _), assoc, + colimitCocone_ι_app_c, limitObjIsoLimitCompEvaluation_inv_π_app_assoc, limMap_π_assoc] simp set_option backward.isDefEq.respectTransparency false in From cc1dc28dd3d6910d25f700d192938b1bf7baed06 Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Sat, 25 Apr 2026 19:49:49 +0800 Subject: [PATCH 7/7] kill more erw --- .../Category/ModuleCat/Presheaf/Limits.lean | 12 ++++-------- Mathlib/Algebra/Lie/Classical.lean | 3 ++- Mathlib/AlgebraicTopology/MooreComplex.lean | 3 +-- .../InnerProductSpace/Projection/Basic.lean | 2 +- Mathlib/CategoryTheory/Limits/ColimitLimit.lean | 2 +- .../Limits/Shapes/SequentialProduct.lean | 4 ++-- Mathlib/CategoryTheory/Preadditive/Mat.lean | 2 +- .../Sites/CompatibleSheafification.lean | 17 +++++------------ .../CliffordAlgebra/SpinGroup.lean | 2 +- 9 files changed, 18 insertions(+), 29 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean index a627bb90c15d88..3de0f01899ad66 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean @@ -79,8 +79,7 @@ noncomputable def limitPresheafOfModules : PresheafOfModules R where dsimp simp only [limMap_π, Functor.comp_obj, evaluation_obj, Functor.whiskerLeft_app, restriction_app, assoc] - -- Here we should rewrite using `Functor.assoc` but that gives a "motive is type-incorrect" - erw [preservesLimitIso_hom_π] + simp only [← Functor.assoc, preservesLimitIso_hom_π] rw [← ModuleCat.restrictScalarsId'App_inv_naturality, map_id, ModuleCat.restrictScalarsId'_inv_app] dsimp @@ -92,18 +91,15 @@ noncomputable def limitPresheafOfModules : PresheafOfModules R where intro j simp only [Functor.comp_obj, evaluation_obj, limMap_π, Functor.whiskerLeft_app, restriction_app, map_comp, ModuleCat.restrictScalarsComp'_inv_app, Functor.map_comp, assoc] - -- Here we should rewrite using `Functor.assoc` but that gives a "motive is type-incorrect" - erw [preservesLimitIso_hom_π] + simp only [← Functor.assoc, preservesLimitIso_hom_π] rw [← ModuleCat.restrictScalarsComp'App_inv_naturality] dsimp rw [← Functor.map_comp_assoc, ← Functor.map_comp_assoc, assoc, preservesLimitIso_inv_π] - -- Here we should rewrite using `Functor.assoc` but that gives a "motive is type-incorrect" - erw [limMap_π] + rw [limMap_π] dsimp simp only [Functor.map_comp, assoc, preservesLimitIso_inv_π_assoc] - -- Here we should rewrite using `Functor.assoc` but that gives a "motive is type-incorrect" - erw [limMap_π_assoc] + rw [limMap_π_assoc] dsimp set_option backward.isDefEq.respectTransparency false in diff --git a/Mathlib/Algebra/Lie/Classical.lean b/Mathlib/Algebra/Lie/Classical.lean index c318f18543c6ba..f90a39f51fc2f2 100644 --- a/Mathlib/Algebra/Lie/Classical.lean +++ b/Mathlib/Algebra/Lie/Classical.lean @@ -232,7 +232,8 @@ theorem soIndefiniteEquiv_apply {i : R} (hi : i * i = -1) (A : so' p q R) : (soIndefiniteEquiv p q R hi A : Matrix (p ⊕ q) (p ⊕ q) R) = (Pso p q R i)⁻¹ * (A : Matrix (p ⊕ q) (p ⊕ q) R) * Pso p q R i := by rw [soIndefiniteEquiv, LieEquiv.trans_apply, LieEquiv.ofEq_apply] - erw [skewAdjointMatricesLieSubalgebraEquiv_apply] + simp only [so'] + rw [skewAdjointMatricesLieSubalgebraEquiv_apply] /-- A matrix defining a canonical even-rank symmetric bilinear form. diff --git a/Mathlib/AlgebraicTopology/MooreComplex.lean b/Mathlib/AlgebraicTopology/MooreComplex.lean index 6c9c9dccd7e163..f1efb0157545a6 100644 --- a/Mathlib/AlgebraicTopology/MooreComplex.lean +++ b/Mathlib/AlgebraicTopology/MooreComplex.lean @@ -132,8 +132,7 @@ def map (f : X ⟶ Y) : obj X ⟶ obj Y := rw [Category.assoc, SimplicialObject.δ, ← f.naturality, ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ i (by simp)), Category.assoc] - erw [kernelSubobject_arrow_comp_assoc] - rw [zero_comp, comp_zero])) + rw [← SimplicialObject.δ_def, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero])) fun n => by cases n <;> dsimp [objD, objX] <;> cat_disch diff --git a/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean b/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean index 2a4295c0506c80..4f55678e0725b4 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean @@ -71,7 +71,7 @@ instance HasOrthogonalProjection.map_linearIsometryEquiv [K.HasOrthogonalProject exists_orthogonal v := by rcases HasOrthogonalProjection.exists_orthogonal (K := K) (f.symm v) with ⟨w, hwK, hw⟩ refine ⟨f w, Submodule.mem_map_of_mem hwK, Set.forall_mem_image.2 fun u hu ↦ ?_⟩ - erw [← f.symm.inner_map_map, f.symm_apply_apply, map_sub, f.symm_apply_apply, hw u hu] + simp [← f.symm.inner_map_map, map_sub, hw u hu] instance HasOrthogonalProjection.map_linearIsometryEquiv' [K.HasOrthogonalProjection] {E' : Type*} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') : diff --git a/Mathlib/CategoryTheory/Limits/ColimitLimit.lean b/Mathlib/CategoryTheory/Limits/ColimitLimit.lean index b399182aff4d69..fdf3e279207679 100644 --- a/Mathlib/CategoryTheory/Limits/ColimitLimit.lean +++ b/Mathlib/CategoryTheory/Limits/ColimitLimit.lean @@ -111,6 +111,6 @@ noncomputable def colimitLimitToLimitColimitCone (G : J ⥤ K ⥤ C) [HasLimit G ι_colimitLimitToLimitColimit_π_assoc, curry_obj_obj_obj, Prod.swap_obj, uncurry_obj_obj, ι_colimMap, currying_unitIso_inv_app_app_app, Category.id_comp, limMap_π_assoc, Functor.flip_obj_obj, flipIsoCurrySwapUncurry_hom_app_app] - erw [limitObjIsoLimitCompEvaluation_hom_π_assoc] + simp only [← comp_evaluation G k, limitObjIsoLimitCompEvaluation_hom_π_assoc] end CategoryTheory.Limits diff --git a/Mathlib/CategoryTheory/Limits/Shapes/SequentialProduct.lean b/Mathlib/CategoryTheory/Limits/Shapes/SequentialProduct.lean index 3337b93217dbd3..cce2b6370334c8 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/SequentialProduct.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/SequentialProduct.lean @@ -201,14 +201,14 @@ noncomputable def isLimit : IsLimit (cone f) where rw [cone_π_app_comp_Pi_π_neg f _ _ h] simp only [dite_eq_ite, Functor.ofOpSequence_obj, limit.lift_π_assoc, Fan.mk_pt, Discrete.functor_obj_eq_as, Fan.mk_π_app, Category.assoc] - slice_lhs 2 4 => erw [← functorMap_commSq f h] + slice_lhs 2 4 => simp only [← dite_eq_ite, ← functorMap_commSq f h] simp uniq s m h := by apply Pi.hom_ext intro n simp only [Functor.ofOpSequence_obj, dite_eq_ite, limit.lift_π, Fan.mk_pt, Fan.mk_π_app, ← h ⟨n + 1⟩, Category.assoc] - slice_rhs 2 3 => erw [cone_π_app_comp_Pi_π_pos f (n + 1) _ (by lia)] + slice_rhs 2 3 => simp only [← dite_eq_ite, cone_π_app_comp_Pi_π_pos f (n + 1) n (by lia)] simp section diff --git a/Mathlib/CategoryTheory/Preadditive/Mat.lean b/Mathlib/CategoryTheory/Preadditive/Mat.lean index 66427c64c35345..e4c1a473beddfa 100644 --- a/Mathlib/CategoryTheory/Preadditive/Mat.lean +++ b/Mathlib/CategoryTheory/Preadditive/Mat.lean @@ -195,7 +195,7 @@ instance hasFiniteBiproducts : HasFiniteBiproducts (Mat_ C) where simp_rw [dite_comp, comp_dite] simp only [ite_self, dite_eq_ite, Limits.comp_zero, Limits.zero_comp, eqToHom_trans] - erw [Finset.sum_sigma] + rw [← Finset.univ_sigma_univ, Finset.sum_sigma] dsimp +instances simp only [if_true, Finset.sum_dite_irrel, Finset.mem_univ, Finset.sum_const_zero, Finset.sum_dite_eq'] diff --git a/Mathlib/CategoryTheory/Sites/CompatibleSheafification.lean b/Mathlib/CategoryTheory/Sites/CompatibleSheafification.lean index efad43e98bb0d2..18e80b563e1574 100644 --- a/Mathlib/CategoryTheory/Sites/CompatibleSheafification.lean +++ b/Mathlib/CategoryTheory/Sites/CompatibleSheafification.lean @@ -63,7 +63,6 @@ noncomputable def sheafificationWhiskerLeftIso (P : Cᵒᵖ ⥤ D) refine isoWhiskerRight ?_ _ exact J.plusFunctorWhiskerLeftIso _ -set_option backward.isDefEq.respectTransparency false in @[simp] theorem sheafificationWhiskerLeftIso_hom_app (P : Cᵒᵖ ⥤ D) (F : D ⥤ E) [∀ (F : D ⥤ E) (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] @@ -71,7 +70,7 @@ theorem sheafificationWhiskerLeftIso_hom_app (P : Cᵒᵖ ⥤ D) (F : D ⥤ E) PreservesLimit (W.index P).multicospan F] : (sheafificationWhiskerLeftIso J P).hom.app F = (J.sheafifyCompIso F P).hom := by dsimp [sheafificationWhiskerLeftIso, sheafifyCompIso] - rw [Category.comp_id] + simp only [sheafify, Category.comp_id] @[simp] theorem sheafificationWhiskerLeftIso_inv_app (P : Cᵒᵖ ⥤ D) (F : D ⥤ E) @@ -80,7 +79,7 @@ theorem sheafificationWhiskerLeftIso_inv_app (P : Cᵒᵖ ⥤ D) (F : D ⥤ E) PreservesLimit (W.index P).multicospan F] : (sheafificationWhiskerLeftIso J P).inv.app F = (J.sheafifyCompIso F P).inv := by dsimp [sheafificationWhiskerLeftIso, sheafifyCompIso] - erw [Category.id_comp] + simp only [sheafify, Category.id_comp] /-- The isomorphism between the sheafification of `P` composed with `F` and the sheafification of `P ⋙ F`, functorially in `P`. -/ @@ -93,32 +92,26 @@ noncomputable def sheafificationWhiskerRightIso : refine (associator _ _ _).symm ≪≫ ?_ exact isoWhiskerRight (J.plusFunctorWhiskerRightIso _) (J.plusFunctor E) -set_option backward.isDefEq.respectTransparency false in @[simp] theorem sheafificationWhiskerRightIso_hom_app : (J.sheafificationWhiskerRightIso F).hom.app P = (J.sheafifyCompIso F P).hom := by dsimp [sheafificationWhiskerRightIso, sheafifyCompIso] - simp only [Category.id_comp, Category.comp_id] - erw [Category.id_comp] + simp only [sheafify, Category.id_comp, Category.comp_id] -set_option backward.isDefEq.respectTransparency false in @[simp] theorem sheafificationWhiskerRightIso_inv_app : (J.sheafificationWhiskerRightIso F).inv.app P = (J.sheafifyCompIso F P).inv := by dsimp [sheafificationWhiskerRightIso, sheafifyCompIso] - simp only [Category.comp_id] - erw [Category.id_comp] + simp only [sheafify, Category.id_comp, Category.comp_id] -set_option backward.isDefEq.respectTransparency false in @[simp, reassoc] theorem whiskerRight_toSheafify_sheafifyCompIso_hom : whiskerRight (J.toSheafify _) _ ≫ (J.sheafifyCompIso F P).hom = J.toSheafify _ := by dsimp [sheafifyCompIso] - erw [whiskerRight_comp, Category.assoc] + simp only [toSheafify, sheafify, whiskerRight_comp, Category.assoc] slice_lhs 2 3 => rw [plusCompIso_whiskerRight] rw [Category.assoc, ← J.plusMap_comp, whiskerRight_toPlus_comp_plusCompIso_hom, ← Category.assoc, whiskerRight_toPlus_comp_plusCompIso_hom] - rfl @[simp, reassoc] theorem toSheafify_comp_sheafifyCompIso_inv : diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean index 7a89455eb57e99..9917233aedbacd 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean @@ -136,7 +136,7 @@ theorem conjAct_smul_range_ι {x : (CliffordAlgebra Q)ˣ} (hx : x ∈ lipschitzG refine Eq.trans_le ?_ this simp only [map_inv, smul_inv_smul] intro x hx - erw [Submodule.map_le_iff_le_comap] + rw [Submodule.pointwise_smul_def, Submodule.map_le_iff_le_comap] rintro _ ⟨m, rfl⟩ exact conjAct_smul_ι_mem_range_ι hx _