More [autoParam]

leanprover-community · Aug 16, 2024 · 3151f57 · 3151f57
1 parent 54a6616
commit 3151f57
Show file tree

Hide file tree

Showing 5 changed files with 11 additions and 11 deletions.
diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
@@ -256,29 +256,29 @@ 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]
     -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
     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/Algebra/Homology/ExactSequence.lean b/Mathlib/Algebra/Homology/ExactSequence.lean
@@ -159,7 +159,7 @@ lemma exact_iff_of_iso {S₁ S₂ : ComposableArrows C n} (e : S₁ ≅ S₂) :
 lemma exact₀ (S : ComposableArrows C 0) : S.Exact where
   toIsComplex := S.isComplex₀
   -- See https://github.com/leanprover/lean4/issues/2862
-  exact i hi := by simp [autoParam] at hi
+  exact i hi := by simp at hi
 
 lemma exact₁ (S : ComposableArrows C 1) : S.Exact where
   toIsComplex := S.isComplex₁

diff --git 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
@@ -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/PFunctor/Multivariate/W.lean b/Mathlib/Data/PFunctor/Multivariate/W.lean
@@ -169,7 +169,7 @@ theorem wRec_eq {α : TypeVec n} {C : Type*}
     (g : ∀ a : P.A, P.drop.B a ⟹ α → (P.last.B a → P.W α) → (P.last.B a → C) → C) (a : P.A)
     (f' : P.drop.B a ⟹ α) (f : P.last.B a → P.W α) :
     P.wRec g (P.wMk a f' f) = g a f' f fun i => P.wRec g (f i) := by
-  rw [wMk, wRec]; dsimp; rw [wpRec_eq]
+  rw [wMk, wRec]; rw [wpRec_eq]
   dsimp only [wPathDestLeft_wPathCasesOn, wPathDestRight_wPathCasesOn]
   congr