Clean up proofs where we can drop the erw

Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

@@ -386,13 +386,10 @@ noncomputable def forgetToPresheafModuleCatObj
   map f := forgetToPresheafModuleCatObjMap X hX M f
   -- TODO: the lines below were automatic: probably there's some defeq mismatch between `M.obj` and
   -- `forgetToPresheafModuleCatObjObj` in `forgetToPresheafModuleCatObjMap`...
-  map_id Y := by ext; erw [forgetToPresheafModuleCatObjMap_apply]; simp
+  map_id Y := by ext; simp only [forgetToPresheafModuleCatObjMap_apply]; simp
   map_comp f g := by
     ext
-    simp only [ModuleCat.hom_comp, LinearMap.comp_apply]
-    erw [forgetToPresheafModuleCatObjMap_apply _ _ _ f,
-      forgetToPresheafModuleCatObjMap_apply _ _ _ g,
-      forgetToPresheafModuleCatObjMap_apply]
+    simp only [ModuleCat.hom_comp, LinearMap.comp_apply, forgetToPresheafModuleCatObjMap_apply]
     simp
 
 end

Mathlib/Algebra/Homology/ShortComplex/ModuleCat.lean

@@ -48,26 +48,12 @@ lemma moduleCat_exact_iff :
 lemma moduleCat_exact_iff_ker_sub_range :
     S.Exact ↔ LinearMap.ker S.g.hom ≤ LinearMap.range S.f.hom := by
   rw [moduleCat_exact_iff]
-  constructor
-  · intro h x₂ hx₂
-    exact h x₂ hx₂
-  · intro h x₂ hx₂
-    exact h hx₂
+  aesop
 
 lemma moduleCat_exact_iff_range_eq_ker :
     S.Exact ↔ LinearMap.range S.f.hom = LinearMap.ker S.g.hom := by
   rw [moduleCat_exact_iff_ker_sub_range]
-  constructor
-  · intro h
-    ext x
-    constructor
-    · rintro ⟨y, hy⟩
-      rw [← hy]
-      simp only [LinearMap.mem_ker, moduleCat_zero_apply]
-    · intro hx
-      exact h hx
-  · intro h
-    rw [h]
+  aesop
 
 variable {S}
 
@@ -95,9 +81,7 @@ morphisms `f` and `g` and the assumption `LinearMap.range f ≤ LinearMap.ker g`
 @[simps]
 def moduleCatMkOfKerLERange {X₁ X₂ X₃ : ModuleCat.{v} R} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃)
     (hfg : LinearMap.range f.hom ≤ LinearMap.ker g.hom) : ShortComplex (ModuleCat.{v} R) :=
-  ShortComplex.mk f g (by
-    ext
-    exact hfg ⟨_, rfl⟩)
+  ShortComplex.mk f g (by aesop)
 
 lemma Exact.moduleCat_of_range_eq_ker {X₁ X₂ X₃ : ModuleCat.{v} R}
     (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) (hfg : LinearMap.range f.hom = LinearMap.ker g.hom) :
@@ -128,16 +112,9 @@ def moduleCatLeftHomologyData : S.LeftHomologyData where
   H := S.moduleCatHomology
   i := ModuleCat.asHom (LinearMap.ker S.g.hom).subtype
   π := S.moduleCatHomologyπ
-  wi := by
-    ext ⟨_, hx⟩
-    exact hx
+  wi := by aesop
   hi := ModuleCat.kernelIsLimit _
-  wπ := by
-    ext (x : S.X₁)
-    dsimp
-    erw [Submodule.Quotient.mk_eq_zero]
-    rw [LinearMap.mem_range]
-    apply exists_apply_eq_apply
+  wπ := by aesop
   hπ := ModuleCat.cokernelIsColimit (ModuleCat.asHom S.moduleCatToCycles)
 
 @[simp]

Mathlib/AlgebraicGeometry/AffineSpace.lean

@@ -295,9 +295,7 @@ lemma map_comp {S S' S'' : Scheme} (f : S ⟶ S') (g : S' ⟶ S'') :
     map n (f ≫ g) = map n f ≫ map n g := by
   ext1
   · simp
-  · simp only [TopologicalSpace.Opens.map_top, Scheme.comp_coeBase,
-      TopologicalSpace.Opens.map_comp_obj, Scheme.comp_app, CommRingCat.comp_apply]
-    erw [map_appTop_coord, map_appTop_coord, map_appTop_coord]
+  · simp
 
 lemma map_Spec_map {R S : CommRingCat.{max u v}} (φ : R ⟶ S) :
     map n (Spec.map φ) =

Mathlib/Topology/Category/Profinite/Nobeling.lean

@@ -1662,7 +1662,7 @@ theorem maxTail_isGood (l : MaxProducts C ho)
   apply Submodule.add_mem
   · apply Submodule.finsupp_sum_mem
     intro q _
-    erw [LinearMap.map_smul (fₗ := πs C o) (c := w q) (x := eval (π C (ord I · < o)) q)]
+    rw [LinearMap.map_smul]
     apply Submodule.smul_mem
     apply Submodule.subset_span
     dsimp only [eval]
@@ -1703,7 +1703,7 @@ theorem linearIndependent_comp_of_eval
     LinearIndependent ℤ (eval (C' C ho)) →
     LinearIndependent ℤ (ModuleCat.asHom (Linear_CC' C hsC ho) ∘ SumEval C ho ∘ Sum.inr) := by
   dsimp [SumEval, ModuleCat.asHom]
-  erw [max_eq_eval_unapply C hsC ho]
+  rw [max_eq_eval_unapply C hsC ho]
   intro h
   let f := MaxToGood C hC hsC ho h₁
   have hf : f.Injective := maxToGood_injective C hC hsC ho h₁