refactor(*): remove duplicate subobject instances

src/algebra/algebra/subalgebra/basic.lean

@@ -166,49 +166,6 @@ to_subring_injective.eq_iff
 
 instance : inhabited S := ⟨(0 : S.to_subsemiring)⟩
 
-section
-
-/-! `subalgebra`s inherit structure from their `subsemiring` / `semiring` coercions. -/
-
-instance to_semiring {R A}
-  [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
-  semiring S := S.to_subsemiring.to_semiring
-instance to_comm_semiring {R A}
-  [comm_semiring R] [comm_semiring A] [algebra R A] (S : subalgebra R A) :
-  comm_semiring S := S.to_subsemiring.to_comm_semiring
-instance to_ring {R A}
-  [comm_ring R] [ring A] [algebra R A] (S : subalgebra R A) :
-  ring S := S.to_subring.to_ring
-instance to_comm_ring {R A}
-  [comm_ring R] [comm_ring A] [algebra R A] (S : subalgebra R A) :
-  comm_ring S := S.to_subring.to_comm_ring
-
-instance to_ordered_semiring {R A}
-  [comm_semiring R] [ordered_semiring A] [algebra R A] (S : subalgebra R A) :
-  ordered_semiring S := S.to_subsemiring.to_ordered_semiring
-instance to_ordered_comm_semiring {R A}
-  [comm_semiring R] [ordered_comm_semiring A] [algebra R A] (S : subalgebra R A) :
-  ordered_comm_semiring S := S.to_subsemiring.to_ordered_comm_semiring
-instance to_ordered_ring {R A}
-  [comm_ring R] [ordered_ring A] [algebra R A] (S : subalgebra R A) :
-  ordered_ring S := S.to_subring.to_ordered_ring
-instance to_ordered_comm_ring {R A}
-  [comm_ring R] [ordered_comm_ring A] [algebra R A] (S : subalgebra R A) :
-  ordered_comm_ring S := S.to_subring.to_ordered_comm_ring
-
-instance to_linear_ordered_semiring {R A}
-  [comm_semiring R] [linear_ordered_semiring A] [algebra R A] (S : subalgebra R A) :
-  linear_ordered_semiring S := S.to_subsemiring.to_linear_ordered_semiring
-/-! There is no `linear_ordered_comm_semiring`. -/
-instance to_linear_ordered_ring {R A}
-  [comm_ring R] [linear_ordered_ring A] [algebra R A] (S : subalgebra R A) :
-  linear_ordered_ring S := S.to_subring.to_linear_ordered_ring
-instance to_linear_ordered_comm_ring {R A}
-  [comm_ring R] [linear_ordered_comm_ring A] [algebra R A] (S : subalgebra R A) :
-  linear_ordered_comm_ring S := S.to_subring.to_linear_ordered_comm_ring
-
-end
-
 /-- Convert a `subalgebra` to `submodule` -/
 def to_submodule : submodule R A :=
 { carrier := S,
@@ -359,14 +316,6 @@ iff.rfl
   (S.comap' f : set A) = f ⁻¹' (S : set B) :=
 rfl
 
-instance no_zero_divisors {R A : Type*} [comm_semiring R] [semiring A] [no_zero_divisors A]
-  [algebra R A] (S : subalgebra R A) : no_zero_divisors S :=
-S.to_subsemiring.no_zero_divisors
-
-instance is_domain {R A : Type*} [comm_ring R] [ring A] [is_domain A] [algebra R A]
-  (S : subalgebra R A) : is_domain S :=
-subring.is_domain S.to_subring
-
 end subalgebra
 
 namespace submodule
@@ -653,7 +602,7 @@ set_like.coe_injective $
 eq_top_iff.2 $ λ x, mem_top
 
 /-- `alg_hom` to `⊤ : subalgebra R A`. -/
-def to_top : A →ₐ[R] (⊤ : subalgebra R A) :=
+@[simps] def to_top : A →ₐ[R] (⊤ : subalgebra R A) :=
 (alg_hom.id R A).cod_restrict ⊤ (λ _, mem_top)
 
 theorem surjective_algebra_map_iff :
@@ -680,6 +629,14 @@ noncomputable def bot_equiv (F R : Type*) [field F] [semiring R] [nontrivial R]
   (⊥ : subalgebra F R) ≃ₐ[F] F :=
 bot_equiv_of_injective (ring_hom.injective _)
 
+<<<<<<< HEAD:src/algebra/algebra/subalgebra/basic.lean
+=======
+/-- The top subalgebra is isomorphic to the field. -/
+@[simps apply symm_apply {rhs_md := semireducible}]
+def top_equiv : (⊤ : subalgebra R A) ≃ₐ[R] A :=
+alg_equiv.of_alg_hom (subalgebra.val ⊤) to_top rfl $ alg_hom.ext $ λ x, subtype.ext rfl
+
+>>>>>>> aeb63ac259 (refactor(*): remove duplicate subobject instances):src/algebra/algebra/subalgebra.lean
 end algebra
 
 namespace subalgebra

src/algebra/module/submodule.lean

@@ -158,8 +158,6 @@ sum_mem (λ i hi, smul_mem _ _ (hyp i hi))
   (g : G) : g • x ∈ p ↔ x ∈ p :=
 p.to_sub_mul_action.smul_mem_iff' g
 
-instance : has_add p := ⟨λx y, ⟨x.1 + y.1, add_mem x.2 y.2⟩⟩
-instance : has_zero p := ⟨⟨0, zero_mem _⟩⟩
 instance : inhabited p := ⟨0⟩
 instance [has_scalar S R] [has_scalar S M] [is_scalar_tower S R M] :
   has_scalar S p := ⟨λ c x, ⟨c • x.1, smul_of_tower_mem _ c x.2⟩⟩
@@ -180,22 +178,22 @@ protected lemma nonempty : (p : set M).nonempty := ⟨0, p.zero_mem⟩
 variables {p}
 @[simp, norm_cast] lemma coe_eq_zero {x : p} : (x : M) = 0 ↔ x = 0 :=
 (set_like.coe_eq_coe : (x : M) = (0 : p) ↔ x = 0)
-@[simp, norm_cast] lemma coe_add (x y : p) : (↑(x + y) : M) = ↑x + ↑y := rfl
-@[simp, norm_cast] lemma coe_zero : ((0 : p) : M) = 0 := rfl
+protected lemma coe_add (x y : p) : (↑(x + y) : M) = ↑x + ↑y := add_submonoid_class.coe_add _ _ _
+protected lemma coe_zero : ((0 : p) : M) = 0 := add_submonoid_class.coe_zero _
 @[norm_cast] lemma coe_smul (r : R) (x : p) : ((r • x : p) : M) = r • ↑x := rfl
 @[simp, norm_cast] lemma coe_smul_of_tower [has_scalar S R] [has_scalar S M] [is_scalar_tower S R M]
   (r : S) (x : p) : ((r • x : p) : M) = r • ↑x := rfl
 @[simp, norm_cast] lemma coe_mk (x : M) (hx : x ∈ p) : ((⟨x, hx⟩ : p) : M) = x := rfl
-@[simp] lemma coe_mem (x : p) : (x : M) ∈ p := x.2
+@[simp] lemma coe_mem (x : p) : (x : M) ∈ p := set_like.coe_mem _
 
 variables (p)
 
-instance : add_comm_monoid p :=
-{ add := (+), zero := 0, .. p.to_add_submonoid.to_add_comm_monoid }
-
 instance module' [semiring S] [has_scalar S R] [module S M] [is_scalar_tower S R M] : module S p :=
 by refine {smul := (•), ..p.to_sub_mul_action.mul_action', ..};
-   { intros, apply set_coe.ext, simp [smul_add, add_smul, mul_smul] }
+   { intros, apply set_coe.ext,
+     simp only [smul_add, add_smul, smul_zero, zero_smul, mul_smul, coe_smul_of_tower,
+                add_submonoid_class.coe_add, add_submonoid_class.coe_zero] }
+
 instance : module R p := p.module'
 
 instance no_zero_smul_divisors [no_zero_smul_divisors R M] : no_zero_smul_divisors R p :=
@@ -331,9 +329,6 @@ by rw [sub_eq_add_neg, p.add_mem_iff_left (p.neg_mem hy)]
 lemma sub_mem_iff_right (hx : x ∈ p) : (x - y) ∈ p ↔ y ∈ p :=
 by rw [sub_eq_add_neg, p.add_mem_iff_right hx, p.neg_mem_iff]
 
-instance : add_comm_group p :=
-{ add := (+), zero := 0, neg := has_neg.neg, ..p.to_add_subgroup.to_add_comm_group }
-
 end add_comm_group
 
 section is_domain

src/field_theory/intermediate_field.lean

@@ -203,28 +203,6 @@ def subfield.to_intermediate_field (S : subfield L)
 
 namespace intermediate_field
 
-/-- An intermediate field inherits a field structure -/
-instance to_field : field S :=
-S.to_subfield.to_field
-
-@[simp, norm_cast]
-lemma coe_sum {ι : Type*} [fintype ι] (f : ι → S) : (↑∑ i, f i : L) = ∑ i, (f i : L) :=
-begin
-  classical,
-  induction finset.univ using finset.induction_on with i s hi H,
-  { simp },
-  { rw [finset.sum_insert hi, add_submonoid_class.coe_add, H, finset.sum_insert hi] }
-end
-
-@[simp, norm_cast]
-lemma coe_prod {ι : Type*} [fintype ι] (f : ι → S) : (↑∏ i, f i : L) = ∏ i, (f i : L) :=
-begin
-  classical,
-  induction finset.univ using finset.induction_on with i s hi H,
-  { simp },
-  { rw [finset.prod_insert hi, submonoid_class.coe_mul, H, finset.prod_insert hi] }
-end
-
 /-! `intermediate_field`s inherit structure from their `subalgebra` coercions. -/
 
 instance module' {R} [semiring R] [has_scalar R K] [module R L] [is_scalar_tower R K L] :

src/field_theory/subfield.lean

@@ -220,40 +220,15 @@ sum_mem h
 protected lemma pow_mem {x : K} (hx : x ∈ s) (n : ℕ) : x^n ∈ s := pow_mem hx n
 protected lemma zsmul_mem {x : K} (hx : x ∈ s) (n : ℤ) : n • x ∈ s := zsmul_mem hx n
 protected lemma coe_int_mem (n : ℤ) : (n : K) ∈ s := coe_int_mem s n
-
-lemma zpow_mem {x : K} (hx : x ∈ s) (n : ℤ) : x^n ∈ s :=
-begin
-  cases n,
-  { simpa using s.pow_mem hx n },
-  { simpa [pow_succ] using s.inv_mem (s.mul_mem hx (s.pow_mem hx n)) },
-end
-
-instance : ring s := s.to_subring.to_ring
-instance : has_div s := ⟨λ x y, ⟨x / y, s.div_mem x.2 y.2⟩⟩
-instance : has_inv s := ⟨λ x, ⟨x⁻¹, s.inv_mem x.2⟩⟩
-instance : has_pow s ℤ := ⟨λ x z, ⟨x ^ z, s.zpow_mem x.2 z⟩⟩
-
-/-- A subfield inherits a field structure -/
-instance to_field : field s :=
-subtype.coe_injective.field coe
-  rfl rfl (λ _ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl)
-  (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)
-
-/-- A subfield of a `linear_ordered_field` is a `linear_ordered_field`. -/
-instance to_linear_ordered_field {K} [linear_ordered_field K] (s : subfield K) :
-  linear_ordered_field s :=
-subtype.coe_injective.linear_ordered_field coe
-  rfl rfl (λ _ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl)
-  (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)
-
-@[simp, norm_cast] lemma coe_add (x y : s) : (↑(x + y) : K) = ↑x + ↑y := rfl
-@[simp, norm_cast] lemma coe_sub (x y : s) : (↑(x - y) : K) = ↑x - ↑y := rfl
-@[simp, norm_cast] lemma coe_neg (x : s) : (↑(-x) : K) = -↑x := rfl
-@[simp, norm_cast] lemma coe_mul (x y : s) : (↑(x * y) : K) = ↑x * ↑y := rfl
-@[simp, norm_cast] lemma coe_div (x y : s) : (↑(x / y) : K) = ↑x / ↑y := rfl
-@[simp, norm_cast] lemma coe_inv (x : s) : (↑(x⁻¹) : K) = (↑x)⁻¹ := rfl
-@[simp, norm_cast] lemma coe_zero : ((0 : s) : K) = 0 := rfl
-@[simp, norm_cast] lemma coe_one : ((1 : s) : K) = 1 := rfl
+protected lemma zpow_mem {x : K} (hx : x ∈ s) (n : ℤ) : x^n ∈ s := zpow_mem hx n
+protected lemma coe_add (x y : s) : (↑(x + y) : K) = ↑x + ↑y := rfl
+protected lemma coe_sub (x y : s) : (↑(x - y) : K) = ↑x - ↑y := rfl
+protected lemma coe_neg (x : s) : (↑(-x) : K) = -↑x := rfl
+protected lemma coe_mul (x y : s) : (↑(x * y) : K) = ↑x * ↑y := rfl
+protected lemma coe_div (x y : s) : (↑(x / y) : K) = ↑x / ↑y := rfl
+protected lemma coe_inv (x : s) : (↑(x⁻¹) : K) = (↑x)⁻¹ := rfl
+protected lemma coe_zero : ((0 : s) : K) = 0 := rfl
+protected lemma coe_one : ((1 : s) : K) = 1 := rfl
 
 end derived_from_subfield_class
 

src/group_theory/subgroup/basic.lean

@@ -502,108 +502,31 @@ have inv_mem : ∀ x, x ∈ s → x⁻¹ ∈ s, from λ x hx, by simpa using hs
   inv_mem' := inv_mem,
   mul_mem' := λ x y hx hy, by simpa using hs x hx y⁻¹ (inv_mem y hy) }
 
-/-- A subgroup of a group inherits a multiplication. -/
-@[to_additive "An `add_subgroup` of an `add_group` inherits an addition."]
-instance has_mul : has_mul H := H.to_submonoid.has_mul
+/-- The natural group hom from a subgroup of group `M` to `M`.
 
-/-- A subgroup of a group inherits a 1. -/
-@[to_additive "An `add_subgroup` of an `add_group` inherits a zero."]
-instance has_one : has_one H := H.to_submonoid.has_one
-
-/-- A subgroup of a group inherits an inverse. -/
-@[to_additive "A `add_subgroup` of a `add_group` inherits an inverse."]
-instance has_inv : has_inv H := ⟨λ a, ⟨a⁻¹, H.inv_mem a.2⟩⟩
-
-/-- A subgroup of a group inherits a division -/
-@[to_additive "An `add_subgroup` of an `add_group` inherits a subtraction."]
-instance has_div : has_div H := ⟨λ a b, ⟨a / b, H.div_mem a.2 b.2⟩⟩
-
-/-- An `add_subgroup` of an `add_group` inherits a natural scaling. -/
-instance _root_.add_subgroup.has_nsmul {G} [add_group G] {H : add_subgroup G} : has_scalar ℕ H :=
-⟨λ n a, ⟨n • a, H.nsmul_mem a.2 n⟩⟩
-
-/-- A subgroup of a group inherits a natural power -/
-@[to_additive]
-instance has_npow : has_pow H ℕ := ⟨λ a n, ⟨a ^ n, H.pow_mem a.2 n⟩⟩
-
-/-- An `add_subgroup` of an `add_group` inherits an integer scaling. -/
-instance _root_.add_subgroup.has_zsmul {G} [add_group G] {H : add_subgroup G} : has_scalar ℤ H :=
-⟨λ n a, ⟨n • a, H.zsmul_mem a.2 n⟩⟩
-
-/-- A subgroup of a group inherits an integer power -/
-@[to_additive]
-instance has_zpow : has_pow H ℤ := ⟨λ a n, ⟨a ^ n, H.zpow_mem a.2 n⟩⟩
-
-@[simp, norm_cast, to_additive] lemma coe_mul (x y : H) : (↑(x * y) : G) = ↑x * ↑y := rfl
-@[simp, norm_cast, to_additive] lemma coe_one : ((1 : H) : G) = 1 := rfl
-@[simp, norm_cast, to_additive] lemma coe_inv (x : H) : ↑(x⁻¹ : H) = (x⁻¹ : G) := rfl
-@[simp, norm_cast, to_additive] lemma coe_div (x y : H) : (↑(x / y) : G) = ↑x / ↑y := rfl
-@[simp, norm_cast, to_additive] lemma coe_mk (x : G) (hx : x ∈ H) : ((⟨x, hx⟩ : H) : G) = x := rfl
-@[simp, norm_cast, to_additive] lemma coe_pow (x : H) (n : ℕ) : ((x ^ n : H) : G) = x ^ n := rfl
-@[simp, norm_cast, to_additive] lemma coe_zpow (x : H) (n : ℤ) : ((x ^ n : H) : G) = x ^ n := rfl
-
-/-- A subgroup of a group inherits a group structure. -/
-@[to_additive "An `add_subgroup` of an `add_group` inherits an `add_group` structure."]
-instance to_group {G : Type*} [group G] (H : subgroup G) : group H :=
-subtype.coe_injective.group _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)
-
-/-- A subgroup of a `comm_group` is a `comm_group`. -/
-@[to_additive "An `add_subgroup` of an `add_comm_group` is an `add_comm_group`."]
-instance to_comm_group {G : Type*} [comm_group G] (H : subgroup G) : comm_group H :=
-subtype.coe_injective.comm_group _
-  rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)
-
-/-- A subgroup of an `ordered_comm_group` is an `ordered_comm_group`. -/
-@[to_additive "An `add_subgroup` of an `add_ordered_comm_group` is an `add_ordered_comm_group`."]
-instance to_ordered_comm_group {G : Type*} [ordered_comm_group G] (H : subgroup G) :
-  ordered_comm_group H :=
-subtype.coe_injective.ordered_comm_group _
-  rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)
-
-/-- A subgroup of a `linear_ordered_comm_group` is a `linear_ordered_comm_group`. -/
-@[to_additive "An `add_subgroup` of a `linear_ordered_add_comm_group` is a
-  `linear_ordered_add_comm_group`."]
-instance to_linear_ordered_comm_group {G : Type*} [linear_ordered_comm_group G]
-  (H : subgroup G) : linear_ordered_comm_group H :=
-subtype.coe_injective.linear_ordered_comm_group _
-  rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)
-
-/-- The natural group hom from a subgroup of group `G` to `G`. -/
-@[to_additive "The natural group hom from an `add_subgroup` of `add_group` `G` to `G`."]
-def subtype : H →* G := ⟨coe, rfl, λ _ _, rfl⟩
+See also `subgroup_class.subtype`, which is more general at the expense of no dot notation.
+-/
+@[to_additive "The natural group hom from an `add_subgroup` of `add_group` `M` to `M`.
 
-@[simp, to_additive] theorem coe_subtype : ⇑H.subtype = coe := rfl
+See also `add_subgroup_class.subtype`, which is more general at the expense of no dot notation.
+"]
+abbreviation subtype (S : subgroup G) : S →* G := subgroup_class.subtype S
 
-@[simp, norm_cast, to_additive] theorem coe_list_prod (l : list H) :
-  (l.prod : G) = (l.map coe).prod :=
-submonoid_class.coe_list_prod l
+@[simp, to_additive] theorem coe_subtype (S : subgroup G) : (S.subtype : S → G) = coe := rfl
 
-@[simp, norm_cast, to_additive] theorem coe_multiset_prod {G} [comm_group G] (H : subgroup G)
-  (m : multiset H) : (m.prod : G) = (m.map coe).prod :=
-submonoid_class.coe_multiset_prod m
+/-- The inclusion homomorphism from a subgroup `H` contained in `K` to `K`.
 
-@[simp, norm_cast, to_additive] theorem coe_finset_prod {ι G} [comm_group G] (H : subgroup G)
-  (f : ι → H) (s : finset ι) :
-  ↑(∏ i in s, f i) = (∏ i in s, f i : G) :=
-submonoid_class.coe_finset_prod f s
+See also `subgroup_class.inclusion`, which is more general at the expense of no dot notation.
+-/
+@[to_additive "The inclusion homomorphism from a additive subgroup `H` contained in `K` to `K`.
 
-/-- The inclusion homomorphism from a subgroup `H` contained in `K` to `K`. -/
-@[to_additive "The inclusion homomorphism from a additive subgroup `H` contained in `K` to `K`."]
-def inclusion {H K : subgroup G} (h : H ≤ K) : H →* K :=
-monoid_hom.mk' (λ x, ⟨x, h x.prop⟩) (λ ⟨a, ha⟩  ⟨b, hb⟩, rfl)
+See also `add_subgroup_class.inclusion`, which is more general at the expense of no dot notation.
+"]
+abbreviation inclusion {H K : subgroup G} (h : H ≤ K) : H →* K := subgroup_class.inclusion h
 
 @[simp, to_additive]
 lemma coe_inclusion {H K : subgroup G} {h : H ≤ K} (a : H) : (inclusion h a : G) = a :=
-by { cases a, simp only [inclusion, coe_mk, monoid_hom.mk'_apply] }
-
-@[to_additive] lemma inclusion_injective {H K : subgroup G} (h : H ≤ K) :
-  function.injective $ inclusion h :=
-set.inclusion_injective h
-
-@[simp, to_additive]
-lemma subtype_comp_inclusion {H K : subgroup G} (hH : H ≤ K) :
-  K.subtype.comp (inclusion hH) = H.subtype :=
-by { ext, simp }
+subgroup_class.coe_inclusion a
 
 /-- The subgroup `G` of the group `G`. -/
 @[to_additive "The `add_subgroup G` of the `add_group G`."]
@@ -646,7 +569,7 @@ end
 begin
   rw subgroup.eq_bot_iff_forall,
   intros y hy,
-  rw [← subgroup.coe_mk H y hy, subsingleton.elim (⟨y, hy⟩ : H) 1, subgroup.coe_one],
+  rw [← set_like.coe_mk y hy, subsingleton.elim (⟨y, hy⟩ : H) 1, submonoid_class.coe_one],
 end
 
 @[to_additive] lemma coe_eq_univ {H : subgroup G} : (H : set G) = set.univ ↔ H = ⊤ :=
@@ -1808,7 +1731,7 @@ attribute [class] add_subgroup.is_commutative
 
 /-- A commutative subgroup is commutative -/
 @[to_additive] instance is_commutative.comm_group [h : H.is_commutative] : comm_group H :=
-{ mul_comm := h.is_comm.comm, .. H.to_group }
+{ mul_comm := h.is_comm.comm, .. subgroup_class.to_group H }
 
 instance center.is_commutative : (center G).is_commutative :=
 ⟨⟨λ a b, subtype.ext (b.2 a)⟩⟩
@@ -2558,7 +2481,8 @@ instance subgroup.normal_inf (H N : subgroup G) [hN : N.normal] :
   ((H ⊓ N).comap H.subtype).normal :=
 ⟨λ x hx g, begin
   simp only [subgroup.mem_inf, coe_subtype, subgroup.mem_comap] at hx,
-  simp only [subgroup.coe_mul, subgroup.mem_inf, coe_subtype, subgroup.coe_inv, subgroup.mem_comap],
+  simp only [submonoid_class.coe_mul, subgroup.mem_inf, coe_subtype, subgroup_class.coe_inv,
+    subgroup.mem_comap],
   exact ⟨H.mul_mem (H.mul_mem g.2 hx.1) (H.inv_mem g.2), hN.1 x hx.2 g⟩,
 end⟩
 
@@ -2713,7 +2637,7 @@ end, by rintro ⟨y, hy, z, hz, rfl⟩; exact mul_mem_sup hy hz⟩
 
 @[to_additive]
 lemma mem_sup' : x ∈ s ⊔ t ↔ ∃ (y : s) (z : t), (y:C) * z = x :=
-mem_sup.trans $ by simp only [set_like.exists, coe_mk]
+mem_sup.trans $ by simp only [set_like.exists, set_like.coe_mk]
 
 @[to_additive]
 lemma mem_closure_pair {x y z : C} : z ∈ closure ({x, y} : set C) ↔ ∃ m n : ℤ, x ^ m * y ^ n = z :=
@@ -3032,14 +2956,15 @@ begin
     { have h := hn.conj_mem _ hx c⁻¹,
       rwa [inv_inv] at h },
     simp only [monoid_hom.cod_restrict_apply, mul_equiv.coe_to_monoid_hom, mul_aut.conj_apply,
-      coe_mk, monoid_hom.restrict_apply, subtype.mk_eq_mk, ← mul_assoc, mul_inv_self, one_mul],
+      set_like.coe_mk, monoid_hom.restrict_apply, subtype.mk_eq_mk, ← mul_assoc, mul_inv_self,
+      one_mul],
     rw [mul_assoc, mul_inv_self, mul_one] },
   have ht' := map_mono (eq_top_iff.1 ht),
   rw [← monoid_hom.range_eq_map, monoid_hom.range_top_of_surjective _ hs] at ht',
   refine eq_top_iff.2 (le_trans ht' (map_le_iff_le_comap.2 (normal_closure_le_normal _))),
   rw [set.singleton_subset_iff, set_like.mem_coe],
-  simp only [monoid_hom.cod_restrict_apply, mul_equiv.coe_to_monoid_hom, mul_aut.conj_apply, coe_mk,
-    monoid_hom.restrict_apply, mem_comap],
+  simp only [monoid_hom.cod_restrict_apply, mul_equiv.coe_to_monoid_hom, mul_aut.conj_apply,
+    set_like.coe_mk, monoid_hom.restrict_apply, mem_comap],
   exact subset_normal_closure (set.mem_singleton _),
 end