feat: add to_additive aligns in Algebra.Group.Opposite (#1097)

Adding some additive #aligns in a file ported before the autoporter did this automatically.

Mathlib/Algebra/Group/Opposite.lean

@@ -70,7 +70,7 @@ instance [AddGroupWithOne α] : AddGroupWithOne αᵐᵒᵖ :=
     intCast := fun n => op n,
     intCast_ofNat := fun n => show op ((n : ℤ) : α) = op (n : α) by rw [Int.cast_ofNat],
     intCast_negSucc := fun n =>
-      show op _ = op (-unop (op ((n + 1 : ℕ) : α))) by erw [unop_op, Int.cast_negSucc] }
+      show op _ = op (-unop (op ((n + 1 : ℕ) : α))) by simp }
 
 instance [AddCommGroup α] : AddCommGroup αᵐᵒᵖ :=
   unop_injective.addCommGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
@@ -171,53 +171,63 @@ variable {α}
 theorem unop_div [DivInvMonoid α] (x y : αᵐᵒᵖ) : unop (x / y) = (unop y)⁻¹ * unop x :=
   rfl
 #align mul_opposite.unop_div MulOpposite.unop_div
+#align add_opposite.unop_neg AddOpposite.unop_neg
 
 @[simp, to_additive]
 theorem op_div [DivInvMonoid α] (x y : α) : op (x / y) = (op y)⁻¹ * op x := by simp [div_eq_mul_inv]
 #align mul_opposite.op_div MulOpposite.op_div
+#align add_opposite.op_neg AddOpposite.op_neg
 
 @[simp, to_additive]
 theorem semiconjBy_op [Mul α] {a x y : α} : SemiconjBy (op a) (op y) (op x) ↔ SemiconjBy a x y :=
   by simp only [SemiconjBy, ← op_mul, op_inj, eq_comm]
 #align mul_opposite.semiconj_by_op MulOpposite.semiconjBy_op
+#align add_opposite.semiconj_by_op AddOpposite.semiconjBy_op
 
 @[simp, to_additive]
 theorem semiconjBy_unop [Mul α] {a x y : αᵐᵒᵖ} :
     SemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy a x y := by
   conv_rhs => rw [← op_unop a, ← op_unop x, ← op_unop y, semiconjBy_op]
 #align mul_opposite.semiconj_by_unop MulOpposite.semiconjBy_unop
+#align add_opposite.semiconj_by_unop AddOpposite.semiconjBy_unop
 
 @[to_additive]
 theorem _root_.SemiconjBy.op [Mul α] {a x y : α} (h : SemiconjBy a x y) :
     SemiconjBy (op a) (op y) (op x) :=
   semiconjBy_op.2 h
 #align semiconj_by.op SemiconjBy.op
+#align add_semiconj_by.op AddSemiconjBy.op
 
 @[to_additive]
 theorem _root_.SemiconjBy.unop [Mul α] {a x y : αᵐᵒᵖ} (h : SemiconjBy a x y) :
     SemiconjBy (unop a) (unop y) (unop x) :=
   semiconjBy_unop.2 h
 #align semiconj_by.unop SemiconjBy.unop
+#align add_semiconj_by.unop AddSemiconjBy.unop
 
 @[to_additive]
 theorem _root_.Commute.op [Mul α] {x y : α} (h : Commute x y) : Commute (op x) (op y) :=
   SemiconjBy.op h
 #align commute.op Commute.op
+#align add_commute.op AddCommute.op
 
 @[to_additive]
 theorem Commute.unop [Mul α] {x y : αᵐᵒᵖ} (h : Commute x y) : Commute (unop x) (unop y) :=
   h.unop
 #align mul_opposite.commute.unop MulOpposite.Commute.unop
+#align add_opposite.commute.unop AddOpposite.Commute.unop
 
 @[simp, to_additive]
 theorem commute_op [Mul α] {x y : α} : Commute (op x) (op y) ↔ Commute x y :=
   semiconjBy_op
 #align mul_opposite.commute_op MulOpposite.commute_op
+#align add_opposite.commute_op AddOpposite.commute_op
 
 @[simp, to_additive]
 theorem commute_unop [Mul α] {x y : αᵐᵒᵖ} : Commute (unop x) (unop y) ↔ Commute x y :=
   semiconjBy_unop
 #align mul_opposite.commute_unop MulOpposite.commute_unop
+#align add_opposite.commute_unop AddOpposite.commute_unop
 
 /-- The function `mul_opposite.op` is an additive equivalence. -/
 @[simps (config := { fullyApplied := false, simpRhs := true })]
@@ -310,6 +320,7 @@ open MulOpposite
 def MulEquiv.inv' (G : Type _) [DivisionMonoid G] : G ≃* Gᵐᵒᵖ :=
   { (Equiv.inv G).trans opEquiv with map_mul' := fun x y => unop_injective <| mul_inv_rev x y }
 #align mul_equiv.inv' MulEquiv.inv'
+#align add_equiv.neg' AddEquiv.neg'
 
 /-- A semigroup homomorphism `f : M →ₙ* N` such that `f x` commutes with `f y` for all `x, y`
 defines a semigroup homomorphism to `Nᵐᵒᵖ`. -/
@@ -322,6 +333,7 @@ def MulHom.toOpposite {M N : Type _} [Mul M] [Mul N] (f : M →ₙ* N)
   toFun := op ∘ f
   map_mul' x y := by simp [(hf x y).eq]
 #align mul_hom.to_opposite MulHom.toOpposite
+#align add_hom.to_opposite AddHom.toOpposite
 
 /-- A semigroup homomorphism `f : M →ₙ* N` such that `f x` commutes with `f y` for all `x, y`
 defines a semigroup homomorphism from `Mᵐᵒᵖ`. -/
@@ -334,6 +346,7 @@ def MulHom.fromOpposite {M N : Type _} [Mul M] [Mul N] (f : M →ₙ* N)
   toFun := f ∘ MulOpposite.unop
   map_mul' _ _ := (f.map_mul _ _).trans (hf _ _).eq
 #align mul_hom.from_opposite MulHom.fromOpposite
+#align add_hom.from_opposite AddHom.fromOpposite
 
 /-- A monoid homomorphism `f : M →* N` such that `f x` commutes with `f y` for all `x, y` defines
 a monoid homomorphism to `Nᵐᵒᵖ`. -/
@@ -347,6 +360,7 @@ def MonoidHom.toOpposite {M N : Type _} [MulOneClass M] [MulOneClass N] (f : M 
   map_one' := congrArg op f.map_one
   map_mul' x y := by simp [(hf x y).eq]
 #align monoid_hom.to_opposite MonoidHom.toOpposite
+#align add_monoid_hom.to_opposite AddMonoidHom.toOpposite
 
 /-- A monoid homomorphism `f : M →* N` such that `f x` commutes with `f y` for all `x, y` defines
 a monoid homomorphism from `Mᵐᵒᵖ`. -/
@@ -360,6 +374,7 @@ def MonoidHom.fromOpposite {M N : Type _} [MulOneClass M] [MulOneClass N] (f : M
   map_one' := f.map_one
   map_mul' _ _ := (f.map_mul _ _).trans (hf _ _).eq
 #align monoid_hom.from_opposite MonoidHom.fromOpposite
+#align add_monoid_hom.from_opposite AddMonoidHom.fromOpposite
 
 /-- The units of the opposites are equivalent to the opposites of the units. -/
 @[to_additive
@@ -372,18 +387,21 @@ def Units.opEquiv {M} [Monoid M] : Mᵐᵒᵖˣ ≃* Mˣᵐᵒᵖ where
   left_inv x := Units.ext <| by simp
   right_inv x := unop_injective <| Units.ext <| rfl
 #align units.op_equiv Units.opEquiv
+#align add_units.op_equiv AddUnits.opEquiv
 
 @[simp, to_additive]
 theorem Units.coe_unop_opEquiv {M} [Monoid M] (u : Mᵐᵒᵖˣ) :
     ((Units.opEquiv u).unop : M) = unop (u : Mᵐᵒᵖ) :=
   rfl
 #align units.coe_unop_op_equiv Units.coe_unop_opEquiv
+#align add_units.coe_unop_op_equiv AddUnits.coe_unop_opEquiv
 
 @[simp, to_additive]
 theorem Units.coe_opEquiv_symm {M} [Monoid M] (u : Mˣᵐᵒᵖ) :
     (Units.opEquiv.symm u : Mᵐᵒᵖ) = op (u.unop : M) :=
   rfl
 #align units.coe_op_equiv_symm Units.coe_opEquiv_symm
+#align add_units.coe_op_equiv_symm AddUnits.coe_opEquiv_symm
 
 /-- A semigroup homomorphism `M →ₙ* N` can equivalently be viewed as a semigroup homomorphism
 `Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/
@@ -406,6 +424,7 @@ def MulHom.op {M N} [Mul M] [Mul N] : (M →ₙ* N) ≃ (Mᵐᵒᵖ →ₙ* Nᵐ
     ext x
     simp
 #align mul_hom.op MulHom.op
+#align add_hom.op AddHom.op
 
 /-- The 'unopposite' of a semigroup homomorphism `Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ`. Inverse to `mul_hom.op`. -/
 @[simp,
@@ -415,6 +434,7 @@ def MulHom.op {M N} [Mul M] [Mul N] : (M →ₙ* N) ≃ (Mᵐᵒᵖ →ₙ* Nᵐ
 def MulHom.unop {M N} [Mul M] [Mul N] : (Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) ≃ (M →ₙ* N) :=
   MulHom.op.symm
 #align mul_hom.unop MulHom.unop
+#align add_hom.unop AddHom.unop
 
 /-- An additive semigroup homomorphism `add_hom M N` can equivalently be viewed as an additive
 homomorphism `add_hom Mᵐᵒᵖ Nᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on
@@ -466,6 +486,7 @@ def MonoidHom.op {M N} [MulOneClass M] [MulOneClass N] : (M →* N) ≃ (Mᵐᵒ
     ext x
     simp
 #align monoid_hom.op MonoidHom.op
+#align add_monoid_hom.op AddMonoidHom.op
 
 /-- The 'unopposite' of a monoid homomorphism `Mᵐᵒᵖ →* Nᵐᵒᵖ`. Inverse to `monoid_hom.op`. -/
 @[simp,
@@ -475,6 +496,7 @@ def MonoidHom.op {M N} [MulOneClass M] [MulOneClass N] : (M →* N) ≃ (Mᵐᵒ
 def MonoidHom.unop {M N} [MulOneClass M] [MulOneClass N] : (Mᵐᵒᵖ →* Nᵐᵒᵖ) ≃ (M →* N) :=
   MonoidHom.op.symm
 #align monoid_hom.unop MonoidHom.unop
+#align add_monoid_hom.unop AddMonoidHom.unop
 
 /-- An additive homomorphism `M →+ N` can equivalently be viewed as an additive homomorphism
 `Mᵐᵒᵖ →+ Nᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/
@@ -519,7 +541,7 @@ def AddEquiv.mulOp {α β} [Add α] [Add β] : α ≃+ β ≃ (αᵐᵒᵖ ≃+
   right_inv f := by
     apply AddEquiv.ext
     intro
-    simp [MulOpposite.op, MulOpposite.unop]
+    rfl
 #align add_equiv.mul_op AddEquiv.mulOp
 
 /-- The 'unopposite' of an iso `αᵐᵒᵖ ≃+ βᵐᵒᵖ`. Inverse to `add_equiv.mul_op`. -/
@@ -550,13 +572,15 @@ def MulEquiv.op {α β} [Mul α] [Mul β] : α ≃* β ≃ (αᵐᵒᵖ ≃* β
     simp
     rfl
 #align mul_equiv.op MulEquiv.op
+#align add_equiv.op AddEquiv.op
 
 /-- The 'unopposite' of an iso `αᵐᵒᵖ ≃* βᵐᵒᵖ`. Inverse to `mul_equiv.op`. -/
 @[simp, to_additive
   "The 'unopposite' of an iso `αᵃᵒᵖ ≃+ βᵃᵒᵖ`. Inverse to `add_equiv.op`."]
 def MulEquiv.unop {α β} [Mul α] [Mul β] : αᵐᵒᵖ ≃* βᵐᵒᵖ ≃ (α ≃* β) :=
   MulEquiv.op.symm
 #align mul_equiv.unop MulEquiv.unop
+#align add_equiv.unop AddEquiv.unop
 
 section Ext