fix(algebra/group/{prod,pi}): fix non-defeq has_scalar diamonds (#9584

)

This fixes diamonds in the following instances for nat- and int- actions:

* `has_scalar ℕ (α × β)`
* `has_scalar ℤ (α × β)`
* `has_scalar ℤ (Π a, β a)`

The last one revealed a diamond caused by inconsistent use of `pi_instance_derive_field`:
```lean
-- fails before this change
example [Π a, group $ β a] : group.to_div_inv_monoid (Π a, β a) = pi.div_inv_monoid := rfl
```

src/algebra/group/pi.lean

@@ -58,18 +58,18 @@ tactic.pi_instance_derive_field
 @[to_additive]
 instance div_inv_monoid [∀ i, div_inv_monoid $ f i] :
   div_inv_monoid (Π i : I, f i) :=
-{ div_eq_mul_inv := λ x y, funext (λ i, div_eq_mul_inv (x i) (y i)),
-  .. pi.monoid, .. pi.has_div, .. pi.has_inv }
+by refine_struct { one := (1 : Π i, f i), mul := (*), inv := has_inv.inv, div := has_div.div,
+  npow := npow, gpow := λ z x i, gpow z (x i) }; tactic.pi_instance_derive_field
 
 @[to_additive]
 instance group [∀ i, group $ f i] : group (Π i : I, f i) :=
 by refine_struct { one := (1 : Π i, f i), mul := (*), inv := has_inv.inv, div := has_div.div,
-  npow := λ n x i, npow n (x i), gpow := λ n x i, gpow n (x i) }; tactic.pi_instance_derive_field
+  npow := npow, gpow := gpow }; tactic.pi_instance_derive_field
 
 @[to_additive]
 instance comm_group [∀ i, comm_group $ f i] : comm_group (Π i : I, f i) :=
 by refine_struct { one := (1 : Π i, f i), mul := (*), inv := has_inv.inv, div := has_div.div,
-  npow := λ n x i, npow n (x i), gpow := λ n x i, gpow n (x i) }; tactic.pi_instance_derive_field
+  npow := npow, gpow := gpow }; tactic.pi_instance_derive_field
 
 @[to_additive add_left_cancel_semigroup]
 instance left_cancel_semigroup [∀ i, left_cancel_semigroup $ f i] :
@@ -84,25 +84,25 @@ by refine_struct { mul := (*) }; tactic.pi_instance_derive_field
 @[to_additive add_left_cancel_monoid]
 instance left_cancel_monoid [∀ i, left_cancel_monoid $ f i] :
   left_cancel_monoid (Π i : I, f i) :=
-by refine_struct { one := (1 : Π i, f i), mul := (*), npow := λ n x i, npow n (x i) };
+by refine_struct { one := (1 : Π i, f i), mul := (*), npow := npow };
 tactic.pi_instance_derive_field
 
 @[to_additive add_right_cancel_monoid]
 instance right_cancel_monoid [∀ i, right_cancel_monoid $ f i] :
   right_cancel_monoid (Π i : I, f i) :=
-by refine_struct { one := (1 : Π i, f i), mul := (*), npow := λ n x i, npow n (x i), .. };
+by refine_struct { one := (1 : Π i, f i), mul := (*), npow := npow, .. };
 tactic.pi_instance_derive_field
 
 @[to_additive add_cancel_monoid]
 instance cancel_monoid [∀ i, cancel_monoid $ f i] :
   cancel_monoid (Π i : I, f i) :=
-by refine_struct { one := (1 : Π i, f i), mul := (*), npow := λ n x i, npow n (x i) };
+by refine_struct { one := (1 : Π i, f i), mul := (*), npow := npow };
 tactic.pi_instance_derive_field
 
 @[to_additive add_cancel_comm_monoid]
 instance cancel_comm_monoid [∀ i, cancel_comm_monoid $ f i] :
   cancel_comm_monoid (Π i : I, f i) :=
-by refine_struct { one := (1 : Π i, f i), mul := (*), npow := λ n x i, npow n (x i) };
+by refine_struct { one := (1 : Π i, f i), mul := (*), npow := npow };
 tactic.pi_instance_derive_field
 
 instance mul_zero_class [∀ i, mul_zero_class $ f i] :
@@ -117,12 +117,12 @@ by refine_struct { zero := (0 : Π i, f i), one := (1 : Π i, f i), mul := (*),
 instance monoid_with_zero [∀ i, monoid_with_zero $ f i] :
   monoid_with_zero (Π i : I, f i) :=
 by refine_struct { zero := (0 : Π i, f i), one := (1 : Π i, f i), mul := (*),
-  npow := λ n x i, npow n (x i) }; tactic.pi_instance_derive_field
+  npow := npow }; tactic.pi_instance_derive_field
 
 instance comm_monoid_with_zero [∀ i, comm_monoid_with_zero $ f i] :
   comm_monoid_with_zero (Π i : I, f i) :=
 by refine_struct { zero := (0 : Π i, f i), one := (1 : Π i, f i), mul := (*),
-  npow := λ n x i, npow n (x i) }; tactic.pi_instance_derive_field
+  npow := npow }; tactic.pi_instance_derive_field
 
 section instance_lemmas
 open function

src/algebra/group/prod.lean

@@ -93,13 +93,24 @@ instance [mul_one_class M] [mul_one_class N] : mul_one_class (M × N) :=
 
 @[to_additive]
 instance [monoid M] [monoid N] : monoid (M × N) :=
-{ .. prod.semigroup, .. prod.mul_one_class }
+{ npow := λ z a, ⟨monoid.npow z a.1, monoid.npow z a.2⟩,
+  npow_zero' := λ z, ext (monoid.npow_zero' _) (monoid.npow_zero' _),
+  npow_succ' := λ z a, ext (monoid.npow_succ' _ _) (monoid.npow_succ' _ _),
+  .. prod.semigroup, .. prod.mul_one_class }
+
+@[to_additive]
+instance [div_inv_monoid G] [div_inv_monoid H] : div_inv_monoid (G × H) :=
+{ div_eq_mul_inv := λ a b, mk.inj_iff.mpr ⟨div_eq_mul_inv _ _, div_eq_mul_inv _ _⟩,
+  gpow := λ z a, ⟨div_inv_monoid.gpow z a.1, div_inv_monoid.gpow z a.2⟩,
+  gpow_zero' := λ z, ext (div_inv_monoid.gpow_zero' _) (div_inv_monoid.gpow_zero' _),
+  gpow_succ' := λ z a, ext (div_inv_monoid.gpow_succ' _ _) (div_inv_monoid.gpow_succ' _ _),
+  gpow_neg' := λ z a, ext (div_inv_monoid.gpow_neg' _ _) (div_inv_monoid.gpow_neg' _ _),
+  .. prod.monoid, .. prod.has_inv, .. prod.has_div }
 
 @[to_additive]
 instance [group G] [group H] : group (G × H) :=
 { mul_left_inv := assume a, mk.inj_iff.mpr ⟨mul_left_inv _, mul_left_inv _⟩,
-  div_eq_mul_inv := λ a b, mk.inj_iff.mpr ⟨div_eq_mul_inv _ _, div_eq_mul_inv _ _⟩,
-  .. prod.monoid, .. prod.has_inv, .. prod.has_div }
+  .. prod.div_inv_monoid }
 
 @[to_additive]
 instance [comm_semigroup G] [comm_semigroup H] : comm_semigroup (G × H) :=

test/instance_diamonds.lean

@@ -19,6 +19,18 @@ example :
   (sub_neg_monoid.has_scalar_int : has_scalar ℤ ℂ) = (complex.has_scalar : has_scalar ℤ ℂ) :=
 rfl
 
+example (α β : Type*) [add_monoid α] [add_monoid β] :
+  (prod.has_scalar : has_scalar ℕ (α × β)) = add_monoid.has_scalar_nat := rfl
+
+example (α β : Type*) [sub_neg_monoid α] [sub_neg_monoid β] :
+  (prod.has_scalar : has_scalar ℤ (α × β)) = sub_neg_monoid.has_scalar_int := rfl
+
+example (α : Type*) (β : α → Type*) [Π a, add_monoid (β a)] :
+  (pi.has_scalar : has_scalar ℕ (Π a, β a)) = add_monoid.has_scalar_nat := rfl
+
+example (α : Type*) (β : α → Type*) [Π a, sub_neg_monoid (β a)] :
+  (pi.has_scalar : has_scalar ℤ (Π a, β a)) = sub_neg_monoid.has_scalar_int := rfl
+
 section units
 
 example (α : Type*) [monoid α] :