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/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/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/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/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 _ 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