From eb9d7107394f8a66305180a488e0fe1ec1a9c966 Mon Sep 17 00:00:00 2001
From: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Date: Mon, 11 Feb 2019 16:26:28 +0000
Subject: [PATCH] fix(group_theory/quotient_group): remove duplicate group_hom
 instance

---
 src/group_theory/quotient_group.lean | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/src/group_theory/quotient_group.lean b/src/group_theory/quotient_group.lean
index 7b6b3523e2972..7c7b0b225940b 100644
--- a/src/group_theory/quotient_group.lean
+++ b/src/group_theory/quotient_group.lean
@@ -79,11 +79,6 @@ attribute [to_additive quotient_add_group.coe_neg] coe_inv
 
 local notation ` Q ` := quotient N
 
-instance is_group_hom_quotient_group_mk : is_group_hom (mk : G → Q) :=
-by refine {..}; intros; refl
-attribute [to_additive quotient_add_group.is_add_group_hom_quotient_add_group_mk] quotient_group.is_group_hom_quotient_group_mk
-attribute [to_additive quotient_add_group.is_add_group_hom_quotient_add_group_mk.equations._eqn_1] quotient_group.is_group_hom_quotient_group_mk.equations._eqn_1
-
 def lift (φ : G → H) [is_group_hom φ] (HN : ∀x∈N, φ x = 1) (q : Q) : H :=
 q.lift_on' φ $ assume a b (hab : a⁻¹ * b ∈ N),
 (calc φ a = φ a * 1           : by simp