From 201b6d10627217ccee43877c426740ff7961084d Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 19 Aug 2024 11:09:50 +0000 Subject: [PATCH] chore: no need to pass autoParam to simp or dsimp (#15968) and with https://github.com/leanprover/lean4/pull/4154 it actually complains, so let's remove them now. --- .../Algebra/Category/ModuleCat/Monoidal/Basic.lean | 12 ++++++------ Mathlib/CategoryTheory/DifferentialObject.lean | 4 ++-- Mathlib/CategoryTheory/Elements.lean | 2 +- Mathlib/Data/List/Intervals.lean | 6 +++--- Mathlib/Topology/Sheaves/Presheaf.lean | 2 +- 5 files changed, 13 insertions(+), 13 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean index 8644e70e9cf72..666c67174d69b 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean @@ -256,21 +256,21 @@ open Opposite -- Porting note: simp wasn't firing but rw was, annoying instance : MonoidalPreadditive (ModuleCat.{u} R) := by refine ⟨?_, ?_, ?_, ?_⟩ - · dsimp only [autoParam]; intros + · intros refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_) simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply] rw [LinearMap.zero_apply] -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 erw [MonoidalCategory.whiskerLeft_apply] rw [LinearMap.zero_apply, TensorProduct.tmul_zero] - · dsimp only [autoParam]; intros + · intros refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_) simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply] rw [LinearMap.zero_apply] -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 erw [MonoidalCategory.whiskerRight_apply] rw [LinearMap.zero_apply, TensorProduct.zero_tmul] - · dsimp only [autoParam]; intros + · intros refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_) simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply] rw [LinearMap.add_apply] @@ -278,7 +278,7 @@ instance : MonoidalPreadditive (ModuleCat.{u} R) := by erw [MonoidalCategory.whiskerLeft_apply, MonoidalCategory.whiskerLeft_apply] erw [MonoidalCategory.whiskerLeft_apply] rw [LinearMap.add_apply, TensorProduct.tmul_add] - · dsimp only [autoParam]; intros + · intros refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_) simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply] rw [LinearMap.add_apply] @@ -290,14 +290,14 @@ instance : MonoidalPreadditive (ModuleCat.{u} R) := by -- Porting note: simp wasn't firing but rw was, annoying instance : MonoidalLinear R (ModuleCat.{u} R) := by refine ⟨?_, ?_⟩ - · dsimp only [autoParam]; intros + · intros refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_) simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply] rw [LinearMap.smul_apply] -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 erw [MonoidalCategory.whiskerLeft_apply, MonoidalCategory.whiskerLeft_apply] rw [LinearMap.smul_apply, TensorProduct.tmul_smul] - · dsimp only [autoParam]; intros + · intros refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_) simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply] rw [LinearMap.smul_apply] diff --git a/Mathlib/CategoryTheory/DifferentialObject.lean b/Mathlib/CategoryTheory/DifferentialObject.lean index ffd8546c41068..324755f59b43d 100644 --- a/Mathlib/CategoryTheory/DifferentialObject.lean +++ b/Mathlib/CategoryTheory/DifferentialObject.lean @@ -181,8 +181,8 @@ def mapDifferentialObject (F : C ⥤ D) slice_lhs 2 3 => rw [← Functor.comp_map F (shiftFunctor D (1 : S)), ← η.naturality f.f] slice_lhs 1 2 => rw [Functor.comp_map, ← F.map_comp, f.comm, F.map_comp] rw [Category.assoc] } - map_id := by intros; ext; simp [autoParam] - map_comp := by intros; ext; simp [autoParam] + map_id := by intros; ext; simp + map_comp := by intros; ext; simp end Functor diff --git a/Mathlib/CategoryTheory/Elements.lean b/Mathlib/CategoryTheory/Elements.lean index 35d3b67264029..78dda58fef9a6 100644 --- a/Mathlib/CategoryTheory/Elements.lean +++ b/Mathlib/CategoryTheory/Elements.lean @@ -265,7 +265,7 @@ theorem costructuredArrow_yoneda_equivalence_naturality {F₁ F₂ : Cᵒᵖ ⥤ congr ext _ f simpa using congr_fun (α.naturality f.op).symm (unop X).snd - · simp [autoParam] + · simp /-- The equivalence `F.elementsᵒᵖ ≌ (yoneda, F)` is compatible with the forgetful functors. -/ @[simps!] diff --git a/Mathlib/Data/List/Intervals.lean b/Mathlib/Data/List/Intervals.lean index 39e9340abd44f..fdfa018a9e884 100644 --- a/Mathlib/Data/List/Intervals.lean +++ b/Mathlib/Data/List/Intervals.lean @@ -42,15 +42,15 @@ theorem zero_bot (n : ℕ) : Ico 0 n = range n := by rw [Ico, Nat.sub_zero, rang @[simp] theorem length (n m : ℕ) : length (Ico n m) = m - n := by dsimp [Ico] - simp [length_range', autoParam] + simp [length_range'] theorem pairwise_lt (n m : ℕ) : Pairwise (· < ·) (Ico n m) := by dsimp [Ico] - simp [pairwise_lt_range', autoParam] + simp [pairwise_lt_range'] theorem nodup (n m : ℕ) : Nodup (Ico n m) := by dsimp [Ico] - simp [nodup_range', autoParam] + simp [nodup_range'] @[simp] theorem mem {n m l : ℕ} : l ∈ Ico n m ↔ n ≤ l ∧ l < m := by diff --git a/Mathlib/Topology/Sheaves/Presheaf.lean b/Mathlib/Topology/Sheaves/Presheaf.lean index 4469bab7e876e..77a9b775aec7d 100644 --- a/Mathlib/Topology/Sheaves/Presheaf.lean +++ b/Mathlib/Topology/Sheaves/Presheaf.lean @@ -303,7 +303,7 @@ def pullbackObjObjOfImageOpen {X Y : TopCat.{v}} (f : X ⟶ Y) (ℱ : Y.Presheaf refine (homOfLE ?_).op apply (Set.image_subset f s.pt.hom.unop.le).trans exact Set.image_preimage.l_u_le (SetLike.coe s.pt.left.unop) - · simp [autoParam, eq_iff_true_of_subsingleton] } + · simp [eq_iff_true_of_subsingleton] } exact IsColimit.coconePointUniqueUpToIso ((Opens.map f).op.isPointwiseLeftKanExtensionLanUnit ℱ (op U)) (colimitOfDiagramTerminal hx _)