refactor(algebra/category/Group/limits): simp -> refl (#5911)

Co-authors: `lean-gptf`, Stanislas Polu
leanprover-community · Jan 27, 2021 · 38f6e05 · 38f6e05
1 parent 6eae630
commit 38f6e05
Showing 1 changed file with 1 addition and 4 deletions.
diff --git a/src/algebra/category/Group/limits.lean b/src/algebra/category/Group/limits.lean
@@ -247,10 +247,7 @@ def kernel_iso_ker {G H : AddCommGroup} (f : G ⟶ H) :
 @[simp]
 lemma kernel_iso_ker_hom_comp_subtype {G H : AddCommGroup} (f : G ⟶ H) :
   (kernel_iso_ker f).hom ≫ add_subgroup.subtype f.ker = kernel.ι f :=
-begin
-  ext,
-  simp [kernel_iso_ker],
-end
+by ext; refl
 
 @[simp]
 lemma kernel_iso_ker_inv_comp_ι {G H : AddCommGroup} (f : G ⟶ H) :