chore: golf some simp based proofs (#31266)

Author: euprunin

Mathlib/Algebra/FreeAbelianGroup/Finsupp.lean

@@ -51,10 +51,8 @@ theorem Finsupp.toFreeAbelianGroup_comp_singleAddHom (x : X) :
 @[simp]
 theorem FreeAbelianGroup.toFinsupp_comp_toFreeAbelianGroup :
     toFinsupp.comp toFreeAbelianGroup = AddMonoidHom.id (X →₀ ℤ) := by
-  ext x y; simp only [AddMonoidHom.id_comp]
-  rw [AddMonoidHom.comp_assoc, Finsupp.toFreeAbelianGroup_comp_singleAddHom]
-  simp only [toFinsupp, AddMonoidHom.coe_comp, Finsupp.singleAddHom_apply, Function.comp_apply,
-    one_smul, lift_apply_of, AddMonoidHom.flip_apply, smulAddHom_apply]
+  ext
+  simp
 
 @[simp]
 theorem Finsupp.toFreeAbelianGroup_comp_toFinsupp :

Mathlib/CategoryTheory/Limits/HasLimits.lean

@@ -790,7 +790,7 @@ def colimit.homIso' (F : J ⥤ C) [HasColimit F] (W : C) :
   (colimit.isColimit F).homIso' W
 
 theorem colimit.desc_extend (F : J ⥤ C) [HasColimit F] (c : Cocone F) {X : C} (f : c.pt ⟶ X) :
-    colimit.desc F (c.extend f) = colimit.desc F c ≫ f := by ext1; rw [← Category.assoc]; simp
+    colimit.desc F (c.extend f) = colimit.desc F c ≫ f := by ext; simp
 
 -- This has the isomorphism pointing in the opposite direction than in `has_limit_of_iso`.
 -- This is intentional; it seems to help with elaboration.
@@ -885,7 +885,8 @@ theorem colimit.ι_inv_pre [IsIso (pre F E)] (k : K) :
 @[reassoc (attr := simp)]
 theorem colimit.pre_desc (c : Cocone F) :
     colimit.pre F E ≫ colimit.desc F c = colimit.desc (E ⋙ F) (c.whisker E) := by
-  ext; rw [← assoc, colimit.ι_pre]; simp
+  ext
+  simp
 
 variable {L : Type u₃} [Category.{v₃} L]
 variable (D : L ⥤ K)

Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean

@@ -395,7 +395,7 @@ theorem lift_comp_kernelIsoOfEq_inv {Z} {f g : X ⟶ Y} [HasKernel f] [HasKernel
 @[simp]
 theorem kernelIsoOfEq_trans {f g h : X ⟶ Y} [HasKernel f] [HasKernel g] [HasKernel h] (w₁ : f = g)
     (w₂ : g = h) : kernelIsoOfEq w₁ ≪≫ kernelIsoOfEq w₂ = kernelIsoOfEq (w₁.trans w₂) := by
-  cases w₁; cases w₂; ext; simp [kernelIsoOfEq]
+  cases w₁; simp
 
 variable {f}
 
@@ -877,7 +877,7 @@ theorem cokernelIsoOfEq_inv_comp_desc {Z} {f g : X ⟶ Y} [HasCokernel f] [HasCo
 theorem cokernelIsoOfEq_trans {f g h : X ⟶ Y} [HasCokernel f] [HasCokernel g] [HasCokernel h]
     (w₁ : f = g) (w₂ : g = h) :
     cokernelIsoOfEq w₁ ≪≫ cokernelIsoOfEq w₂ = cokernelIsoOfEq (w₁.trans w₂) := by
-  cases w₁; cases w₂; ext; simp [cokernelIsoOfEq]
+  cases w₁; simp
 
 variable {f}
 

Mathlib/Data/Stream/Init.lean

@@ -666,9 +666,8 @@ theorem inits_eq (s : Stream' α) :
     rfl
 
 theorem zip_inits_tails (s : Stream' α) : zip appendStream' (inits s) (tails s) = const s := by
-  apply Stream'.ext; intro n
-  rw [get_zip, get_inits, get_tails, get_const, take_succ, cons_append_stream, append_take_drop,
-    Stream'.eta]
+  ext
+  simp
 
 theorem identity (s : Stream' α) : pure id ⊛ s = s :=
   rfl

Mathlib/Probability/Kernel/Composition/MapComap.lean

@@ -161,10 +161,10 @@ theorem comap_apply' (κ : Kernel α β) (hg : Measurable g) (c : γ) (s : Set 
 
 @[simp]
 lemma comap_zero (hg : Measurable g) : Kernel.comap (0 : Kernel α β) g hg = 0 := by
-  ext; rw [Kernel.comap_apply]; simp
+  ext; simp
 
 @[simp]
-lemma comap_id (κ : Kernel α β) : comap κ id measurable_id = κ := by ext a; rw [comap_apply]; simp
+lemma comap_id (κ : Kernel α β) : comap κ id measurable_id = κ := by ext; simp
 
 @[simp]
 lemma comap_id' (κ : Kernel α β) : comap κ (fun a ↦ a) measurable_id = κ := comap_id κ

Mathlib/Topology/Category/TopCat/Opens.lean

@@ -209,8 +209,8 @@ theorem op_map_comp_obj (f : X ⟶ Y) (g : Y ⟶ Z) (U) :
 
 theorem map_iSup (f : X ⟶ Y) {ι : Type*} (U : ι → Opens Y) :
     (map f).obj (iSup U) = iSup ((map f).obj ∘ U) := by
-  ext1; rw [iSup_def, iSup_def, map_obj]
-  dsimp; rw [Set.preimage_iUnion]
+  ext
+  simp
 
 section