feat(algebra/*/opposite): Missing instances (#18602)

A few missing instances about `nat.cast`/`int.cast`/`rat.cast` and `mul_opposite`/`add_opposite`.
Also add the (weirdly) missing `add_comm_group_with_one → add_comm_monoid_with_one`.

Finally, this changes the defeq of `rat.cast` on `mul_opposite` to be simpler.

src/algebra/field/opposite.lean

@@ -5,6 +5,7 @@ Authors: Kenny Lau
 -/
 import algebra.field.defs
 import algebra.ring.opposite
+import data.int.cast.lemmas
 
 /-!
 # Field structure on the multiplicative/additive opposite
@@ -15,18 +16,39 @@ import algebra.ring.opposite
 
 variables (α : Type*)
 
+namespace mul_opposite
+
+@[to_additive] instance [has_rat_cast α] : has_rat_cast αᵐᵒᵖ := ⟨λ n, op n⟩
+
+variables {α}
+
+@[simp, norm_cast, to_additive]
+lemma op_rat_cast [has_rat_cast α] (q : ℚ) : op (q : α) = q := rfl
+
+@[simp, norm_cast, to_additive]
+lemma unop_rat_cast [has_rat_cast α] (q : ℚ) : unop (q : αᵐᵒᵖ) = q := rfl
+
+variables (α)
+
 instance [division_semiring α] : division_semiring αᵐᵒᵖ :=
 { .. mul_opposite.group_with_zero α, .. mul_opposite.semiring α }
 
 instance [division_ring α] : division_ring αᵐᵒᵖ :=
-{ .. mul_opposite.group_with_zero α, .. mul_opposite.ring α }
+{ rat_cast := λ q, op q,
+  rat_cast_mk := λ a b hb h, by { rw [rat.cast_def, op_div, op_nat_cast, op_int_cast],
+    exact int.commute_cast _ _ },
+  ..mul_opposite.division_semiring α, ..mul_opposite.ring α }
 
 instance [semifield α] : semifield αᵐᵒᵖ :=
 { .. mul_opposite.division_semiring α, .. mul_opposite.comm_semiring α }
 
 instance [field α] : field αᵐᵒᵖ :=
 { .. mul_opposite.division_ring α, .. mul_opposite.comm_ring α }
 
+end mul_opposite
+
+namespace add_opposite
+
 instance [division_semiring α] : division_semiring αᵃᵒᵖ :=
 { ..add_opposite.group_with_zero α, ..add_opposite.semiring α }
 
@@ -38,3 +60,5 @@ instance [semifield α] : semifield αᵃᵒᵖ :=
 
 instance [field α] : field αᵃᵒᵖ :=
 { ..add_opposite.division_ring α, ..add_opposite.comm_ring α }
+
+end add_opposite

src/algebra/group/opposite.lean

@@ -24,6 +24,9 @@ namespace mul_opposite
 ### Additive structures on `αᵐᵒᵖ`
 -/
 
+@[to_additive] instance [has_nat_cast α] : has_nat_cast αᵐᵒᵖ := ⟨λ n, op n⟩
+@[to_additive] instance [has_int_cast α] : has_int_cast αᵐᵒᵖ := ⟨λ n, op n⟩
+
 instance [add_semigroup α] : add_semigroup (αᵐᵒᵖ) :=
 unop_injective.add_semigroup _ (λ x y, rfl)
 
@@ -42,30 +45,35 @@ unop_injective.add_zero_class _ rfl (λ x y, rfl)
 instance [add_monoid α] : add_monoid αᵐᵒᵖ :=
 unop_injective.add_monoid _ rfl (λ _ _, rfl) (λ _ _, rfl)
 
+instance [add_comm_monoid α] : add_comm_monoid αᵐᵒᵖ :=
+unop_injective.add_comm_monoid _ rfl (λ _ _, rfl) (λ _ _, rfl)
+
 instance [add_monoid_with_one α] : add_monoid_with_one αᵐᵒᵖ :=
-{ nat_cast := λ n, op n,
-  nat_cast_zero := show op ((0 : ℕ) : α) = 0, by simp,
+{ nat_cast_zero := show op ((0 : ℕ) : α) = 0, by rw [nat.cast_zero, op_zero],
   nat_cast_succ := show ∀ n, op ((n + 1 : ℕ) : α) = op (n : ℕ) + 1, by simp,
-  .. mul_opposite.add_monoid α, .. mul_opposite.has_one α }
+  .. mul_opposite.add_monoid α, .. mul_opposite.has_one α, ..mul_opposite.has_nat_cast _ }
 
-instance [add_comm_monoid α] : add_comm_monoid αᵐᵒᵖ :=
-unop_injective.add_comm_monoid _ rfl (λ _ _, rfl) (λ _ _, rfl)
+instance [add_comm_monoid_with_one α] : add_comm_monoid_with_one αᵐᵒᵖ :=
+{ .. mul_opposite.add_monoid_with_one α, ..mul_opposite.add_comm_monoid α }
 
 instance [sub_neg_monoid α] : sub_neg_monoid αᵐᵒᵖ :=
 unop_injective.sub_neg_monoid _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)
 
 instance [add_group α] : add_group αᵐᵒᵖ :=
 unop_injective.add_group _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)
 
+instance [add_comm_group α] : add_comm_group αᵐᵒᵖ :=
+unop_injective.add_comm_group _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)
+
 instance [add_group_with_one α] : add_group_with_one αᵐᵒᵖ :=
 { int_cast := λ n, op n,
   int_cast_of_nat := λ n, show op ((n : ℤ) : α) = op n, by rw int.cast_coe_nat,
   int_cast_neg_succ_of_nat := λ n, show op _ = op (- unop (op ((n + 1 : ℕ) : α))),
     by erw [unop_op, int.cast_neg_succ_of_nat]; refl,
   .. mul_opposite.add_monoid_with_one α, .. mul_opposite.add_group α }
 
-instance [add_comm_group α] : add_comm_group αᵐᵒᵖ :=
-unop_injective.add_comm_group _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)
+instance [add_comm_group_with_one α] : add_comm_group_with_one αᵐᵒᵖ :=
+{ .. mul_opposite.add_group_with_one α, ..mul_opposite.add_comm_group α }
 
 /-!
 ### Multiplicative structures on `αᵐᵒᵖ`
@@ -142,6 +150,15 @@ We also generate additive structures on `αᵃᵒᵖ` using `to_additive`
 
 variable {α}
 
+@[simp, norm_cast, to_additive] lemma op_nat_cast [has_nat_cast α] (n : ℕ) : op (n : α) = n := rfl
+@[simp, norm_cast, to_additive] lemma op_int_cast [has_int_cast α] (n : ℤ) : op (n : α) = n := rfl
+
+@[simp, norm_cast, to_additive]
+lemma unop_nat_cast [has_nat_cast α] (n : ℕ) : unop (n : αᵐᵒᵖ) = n := rfl
+
+@[simp, norm_cast, to_additive]
+lemma unop_int_cast [has_int_cast α] (n : ℤ) : unop (n : αᵐᵒᵖ) = n := rfl
+
 @[simp, to_additive] lemma unop_div [div_inv_monoid α] (x y : αᵐᵒᵖ) :
   unop (x / y) = (unop y)⁻¹ * unop x :=
 rfl
@@ -232,6 +249,16 @@ unop_injective.group _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl)
 instance [comm_group α] : comm_group αᵃᵒᵖ :=
 unop_injective.comm_group _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)
 
+-- NOTE: `add_monoid_with_one α → add_monoid_with_one αᵃᵒᵖ` does not hold
+
+instance [add_comm_monoid_with_one α] : add_comm_monoid_with_one αᵃᵒᵖ :=
+{ nat_cast_zero := show op ((0 : ℕ) : α) = 0, by rw [nat.cast_zero, op_zero],
+  nat_cast_succ := show ∀ n, op ((n + 1 : ℕ) : α) = op (n : ℕ) + 1, by simp [add_comm],
+  ..add_opposite.add_comm_monoid α, ..add_opposite.has_one, ..add_opposite.has_nat_cast _ }
+
+instance [add_comm_group_with_one α] : add_comm_group_with_one αᵃᵒᵖ :=
+{ ..add_opposite.add_comm_monoid_with_one _, ..add_opposite.add_comm_group α }
+
 variable {α}
 
 /-- The function `add_opposite.op` is a multiplicative equivalence. -/

src/algebra/ring/opposite.lean

@@ -123,7 +123,8 @@ instance [non_unital_semiring α] : non_unital_semiring αᵃᵒᵖ :=
 { .. add_opposite.semigroup_with_zero α, .. add_opposite.non_unital_non_assoc_semiring α }
 
 instance [non_assoc_semiring α] : non_assoc_semiring αᵃᵒᵖ :=
-{ .. add_opposite.mul_zero_one_class α, .. add_opposite.non_unital_non_assoc_semiring α }
+{ ..add_opposite.mul_zero_one_class α, ..add_opposite.non_unital_non_assoc_semiring α,
+  ..add_opposite.add_comm_monoid_with_one _ }
 
 instance [semiring α] : semiring αᵃᵒᵖ :=
 { .. add_opposite.non_unital_semiring α, .. add_opposite.non_assoc_semiring α,

src/data/int/cast/defs.lean

@@ -52,8 +52,9 @@ class add_group_with_one (R : Type u)
 (int_cast_neg_succ_of_nat : ∀ n : ℕ, int_cast (-(n+1 : ℕ)) = -((n+1 : ℕ) : R) . control_laws_tac)
 
 /-- An `add_comm_group_with_one` is an `add_group_with_one` satisfying `a + b = b + a`. -/
-@[protect_proj, ancestor add_comm_group add_group_with_one]
-class add_comm_group_with_one (R : Type u) extends add_comm_group R, add_group_with_one R
+@[protect_proj, ancestor add_comm_group add_group_with_one add_comm_monoid_with_one]
+class add_comm_group_with_one (R : Type u)
+  extends add_comm_group R, add_group_with_one R, add_comm_monoid_with_one R
 
 /-- Canonical homomorphism from the integers to any ring(-like) structure `R` -/
 protected def int.cast {R : Type u} [has_int_cast R] (i : ℤ) : R := has_int_cast.int_cast i

src/data/int/cast/lemmas.lean

@@ -290,15 +290,6 @@ by refine_struct { .. }; tactic.pi_instance_derive_field
 
 end pi
 
-namespace mul_opposite
-variables [add_group_with_one α]
-
-@[simp, norm_cast] lemma op_int_cast (z : ℤ) : op (z : α) = z := rfl
-
-@[simp, norm_cast] lemma unop_int_cast (n : ℤ) : unop (n : αᵐᵒᵖ) = n := rfl
-
-end mul_opposite
-
 /-! ### Order dual -/
 
 open order_dual

src/data/nat/cast/basic.lean

@@ -223,15 +223,6 @@ rfl
 instance nat.unique_ring_hom {R : Type*} [non_assoc_semiring R] : unique (ℕ →+* R) :=
 { default := nat.cast_ring_hom R, uniq := ring_hom.eq_nat_cast' }
 
-namespace mul_opposite
-variables [add_monoid_with_one α]
-
-@[simp, norm_cast] lemma op_nat_cast (n : ℕ) : op (n : α) = n := rfl
-
-@[simp, norm_cast] lemma unop_nat_cast (n : ℕ) : unop (n : αᵐᵒᵖ) = n := rfl
-
-end mul_opposite
-
 namespace pi
 variables {π : α → Type*} [Π a, has_nat_cast (π a)]
 

src/data/rat/cast.lean

@@ -310,20 +310,6 @@ monoid_with_zero_hom.ext_rat' $ ring_hom.congr_fun $
 instance rat.subsingleton_ring_hom {R : Type*} [semiring R] : subsingleton (ℚ →+* R) :=
 ⟨ring_hom.ext_rat⟩
 
-namespace mul_opposite
-
-variables [division_ring α]
-
-@[simp, norm_cast] lemma op_rat_cast (r : ℚ) : op (r : α) = (↑r : αᵐᵒᵖ) :=
-by rw [cast_def, div_eq_mul_inv, op_mul, op_inv, op_nat_cast, op_int_cast,
-    (commute.cast_int_right _ r.num).eq, cast_def, div_eq_mul_inv]
-
-@[simp, norm_cast] lemma unop_rat_cast (r : ℚ) : unop (r : αᵐᵒᵖ) = r :=
-by rw [cast_def, div_eq_mul_inv, unop_mul, unop_inv, unop_nat_cast, unop_int_cast,
-    (commute.cast_int_right _ r.num).eq, cast_def, div_eq_mul_inv]
-
-end mul_opposite
-
 section smul
 
 namespace rat