diff --git a/src/algebra/opposites.lean b/src/algebra/opposites.lean
index 70cfa8d311ec4..6199b992ae180 100644
--- a/src/algebra/opposites.lean
+++ b/src/algebra/opposites.lean
@@ -69,8 +69,8 @@ variable {α}
 @[simp] lemma op_inv [has_inv α] (x : α) : op (x⁻¹) = (op x)⁻¹ := rfl
 @[simp] lemma unop_inv [has_inv α] (x : αᵒᵖ) : unop (x⁻¹) = (unop x)⁻¹ := rfl
 
-@[simp] lemma op_sub [add_group α] (x y : α) : op (x - y) = op x - op y := rfl
-@[simp] lemma unop_sub [add_group α] (x y : αᵒᵖ) : unop (x - y) = unop x - unop y := rfl
+@[simp] lemma op_sub [has_sub α] (x y : α) : op (x - y) = op x - op y := rfl
+@[simp] lemma unop_sub [has_sub α] (x y : αᵒᵖ) : unop (x - y) = unop x - unop y := rfl
 
 @[simp] lemma op_smul {R : Type*} [has_scalar R α] (c : R) (a : α) : op (c • a) = c • op a := rfl
 @[simp] lemma unop_smul {R : Type*} [has_scalar R α] (c : R) (a : αᵒᵖ) :
@@ -78,56 +78,50 @@ variable {α}
 
 end
 
-instance [add_semigroup α] : add_semigroup (opposite α) :=
-{ add_assoc := λ x y z, unop_injective $ add_assoc (unop x) (unop y) (unop z),
-  .. opposite.has_add α }
+instance [add_semigroup α] : add_semigroup (αᵒᵖ) :=
+unop_injective.add_semigroup _ (λ x y, rfl)
 
 instance [add_left_cancel_semigroup α] : add_left_cancel_semigroup (opposite α) :=
-{ add_left_cancel := λ x y z H, unop_injective $ add_left_cancel $ op_injective H,
-  .. opposite.add_semigroup α }
+unop_injective.add_left_cancel_semigroup _ (λ x y, rfl)
 
 instance [add_right_cancel_semigroup α] : add_right_cancel_semigroup (opposite α) :=
-{ add_right_cancel := λ x y z H, unop_injective $ add_right_cancel $ op_injective H,
-  .. opposite.add_semigroup α }
+unop_injective.add_right_cancel_semigroup _ (λ x y, rfl)
 
 instance [add_comm_semigroup α] : add_comm_semigroup (opposite α) :=
 { add_comm := λ x y, unop_injective $ add_comm (unop x) (unop y),
   .. opposite.add_semigroup α }
 
-
 instance [nontrivial α] : nontrivial (opposite α) :=
-let ⟨x, y, h⟩ := exists_pair_ne α in nontrivial_of_ne (op x) (op y) (op_injective.ne h)
+op_injective.nontrivial
 
-section
-local attribute [semireducible] opposite
 @[simp] lemma unop_eq_zero_iff {α} [has_zero α] (a : αᵒᵖ) : a.unop = (0 : α) ↔ a = (0 : αᵒᵖ) :=
-iff.refl _
+unop_injective.eq_iff' rfl
 
 @[simp] lemma op_eq_zero_iff {α} [has_zero α] (a : α) : op a = (0 : αᵒᵖ) ↔ a = (0 : α) :=
-iff.refl _
-end
+op_injective.eq_iff' rfl
 
 lemma unop_ne_zero_iff {α} [has_zero α] (a : αᵒᵖ) : a.unop ≠ (0 : α) ↔ a ≠ (0 : αᵒᵖ) :=
-not_iff_not.mpr $ unop_eq_zero_iff a
+not_congr $ unop_eq_zero_iff a
 
 lemma op_ne_zero_iff {α} [has_zero α] (a : α) : op a ≠ (0 : αᵒᵖ) ↔ a ≠ (0 : α) :=
-not_iff_not.mpr $ op_eq_zero_iff a
+not_congr $ op_eq_zero_iff a
 
 instance [add_zero_class α] : add_zero_class (opposite α) :=
-{ zero_add := λ x, unop_injective $ zero_add $ unop x,
-  add_zero := λ x, unop_injective $ add_zero $ unop x,
-  .. opposite.has_add α, .. opposite.has_zero α }
+unop_injective.add_zero_class _ rfl (λ x y, rfl)
 
 instance [add_monoid α] : add_monoid (opposite α) :=
-{ .. opposite.add_semigroup α, .. opposite.add_zero_class α }
+unop_injective.add_monoid_smul _ rfl (λ _ _, rfl) (λ _ _, rfl)
 
 instance [add_comm_monoid α] : add_comm_monoid (opposite α) :=
 { .. opposite.add_monoid α, .. opposite.add_comm_semigroup α }
 
+instance [sub_neg_monoid α] : sub_neg_monoid (opposite α) :=
+unop_injective.sub_neg_monoid_smul _ rfl (λ _ _, rfl) (λ _, rfl)
+  (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)
+
 instance [add_group α] : add_group (opposite α) :=
-{ add_left_neg := λ x, unop_injective $ add_left_neg $ unop x,
-  sub_eq_add_neg := λ x y, unop_injective $ sub_eq_add_neg (unop x) (unop y),
-  .. opposite.add_monoid α, .. opposite.has_neg α, .. opposite.has_sub α }
+unop_injective.add_group_smul _ rfl (λ _ _, rfl) (λ _, rfl)
+  (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)
 
 instance [add_comm_group α] : add_comm_group (opposite α) :=
 { .. opposite.add_group α, .. opposite.add_comm_monoid α }