fix(algebra/group/prod): fixes for #5563 (#5577)

* rename `prod.units` to `mul_equiv.prod_units`;
* rewrite it with better definitional equalities;
* now `@[to_additive]` works: fixes #5566;
* make `M` and `N` implicit in `mul_equiv.prod_comm`

src/algebra/group/prod.lean

@@ -118,24 +118,6 @@ instance [comm_monoid M] [comm_monoid N] : comm_monoid (M × N) :=
 instance [comm_group G] [comm_group H] : comm_group (G × H) :=
 { .. prod.comm_semigroup, .. prod.group }
 
-/-- The monoid equivalence between units of a product of two monoids, and the product of the
-    units of each monoid. -/
-def units [monoid M] [monoid N] : units (M × N) ≃* units M × units N :=
-mul_equiv.mk'
-{ to_fun := λ ⟨⟨u₁, u₂⟩, ⟨v₁, v₂⟩, huv, hvu⟩,
-              ⟨⟨u₁, v₁, by {rw [prod.mk_mul_mk, prod.mk_eq_one] at huv, exact huv.1},
-                        by {rw [prod.mk_mul_mk, prod.mk_eq_one] at hvu, exact hvu.1}⟩,
-               ⟨u₂, v₂, by {rw [prod.mk_mul_mk, prod.mk_eq_one] at huv, exact huv.2},
-                        by {rw [prod.mk_mul_mk, prod.mk_eq_one] at hvu, exact hvu.2}⟩⟩,
-  inv_fun := λ ⟨⟨u₁, v₁, huv₁, hvu₁⟩, ⟨u₂, v₂, huv₂, hvu₂⟩⟩,
-               ⟨(u₁, u₂), (v₁, v₂), by {rw [prod.mk_mul_mk, prod.mk_eq_one], exact ⟨huv₁, huv₂⟩},
-                                    by {rw [prod.mk_mul_mk, prod.mk_eq_one], exact ⟨hvu₁, hvu₂⟩}⟩,
-  left_inv := by {rintro ⟨⟨u₁, u₂⟩, ⟨v₁, v₂⟩, huv, hvu⟩, simpa, },
-  right_inv := by {rintro ⟨⟨u₁, v₁, huv₁, hvu₁⟩, ⟨u₂, v₂, huv₂, hvu₂⟩⟩, simpa, } }
-   (λ ⟨⟨ux, ux₂⟩, ⟨vx₁, vx₂⟩, hxuv, hxvu⟩ ⟨⟨uy₁, uy₂⟩, ⟨vy₁, vy₂⟩, hyuv, hyvu⟩, rfl)
-
--- TODO attribute [to_additive add_units] units fails
-
 end prod
 
 namespace monoid_hom
@@ -268,16 +250,27 @@ end coprod
 end monoid_hom
 
 namespace mul_equiv
-variables (M N) [monoid M] [monoid N]
+variables {M N} [monoid M] [monoid N]
 
 /-- The equivalence between `M × N` and `N × M` given by swapping the components is multiplicative. -/
 @[to_additive prod_comm "The equivalence between `M × N` and `N × M` given by swapping the components is
 additive."]
 def prod_comm : M × N ≃* N × M :=
 { map_mul' := λ ⟨x₁, y₁⟩ ⟨x₂, y₂⟩, rfl, ..equiv.prod_comm M N }
 
-@[simp, to_additive coe_prod_comm] lemma coe_prod_comm : ⇑(prod_comm M N) = prod.swap := rfl
+@[simp, to_additive coe_prod_comm] lemma coe_prod_comm : ⇑(prod_comm : M × N ≃* N × M) = prod.swap := rfl
 @[simp, to_additive coe_prod_comm_symm] lemma coe_prod_comm_symm :
-  ⇑((prod_comm M N).symm) = prod.swap := rfl
+  ⇑((prod_comm : M × N ≃* N × M).symm) = prod.swap := rfl
+
+/-- The monoid equivalence between units of a product of two monoids, and the product of the
+    units of each monoid. -/
+@[to_additive prod_add_units "The additive monoid equivalence between additive units of a product
+of two additive monoids, and the product of the additive units of each additive monoid."]
+def prod_units : units (M × N) ≃* units M × units N :=
+{ to_fun := (units.map (monoid_hom.fst M N)).prod (units.map (monoid_hom.snd M N)),
+  inv_fun := λ u, ⟨(u.1, u.2), (↑u.1⁻¹, ↑u.2⁻¹), by simp, by simp⟩,
+  left_inv := λ u, by simp,
+  right_inv := λ ⟨u₁, u₂⟩, by simp [units.map],
+  map_mul' := monoid_hom.map_mul _ }
 
 end mul_equiv

src/algebra/group/units.lean

@@ -56,6 +56,10 @@ variables [monoid α]
 @[to_additive] instance [decidable_eq α] : decidable_eq (units α) :=
 λ a b, decidable_of_iff' _ ext_iff
 
+@[simp, to_additive] theorem mk_coe (u : units α) (y h₁ h₂) :
+  mk (u : α) y h₁ h₂ = u :=
+ext rfl
+
 /-- Units of a monoid form a group. -/
 @[to_additive] instance : group (units α) :=
 { mul := λ u₁ u₂, ⟨u₁.val * u₂.val, u₂.inv * u₁.inv,
@@ -78,6 +82,8 @@ attribute [norm_cast] add_units.coe_zero
 @[simp, norm_cast, to_additive] lemma coe_eq_one {a : units α} : (a : α) = 1 ↔ a = 1 :=
 by rw [←units.coe_one, eq_iff]
 
+@[simp, to_additive] lemma inv_mk (x y : α) (h₁ h₂) : (mk x y h₁ h₂)⁻¹ = mk y x h₂ h₁ := rfl
+
 @[to_additive] lemma val_coe : (↑a : α) = a.val := rfl
 
 @[norm_cast, to_additive] lemma coe_inv : ((a⁻¹ : units α) : α) = a.inv := rfl

src/algebra/ring/prod.lean

@@ -106,22 +106,21 @@ end prod_map
 end ring_hom
 
 namespace ring_equiv
-variables (R S) [semiring R] [semiring S]
+variables {R S} [semiring R] [semiring S]
 
 /-- Swapping components as an equivalence of (semi)rings. -/
 def prod_comm : R × S ≃+* S × R :=
-{ ..add_equiv.prod_comm R S, ..mul_equiv.prod_comm R S }
+{ ..add_equiv.prod_comm, ..mul_equiv.prod_comm }
 
-@[simp] lemma coe_prod_comm : ⇑(prod_comm R S) = prod.swap := rfl
-@[simp] lemma coe_prod_comm_symm : ⇑((prod_comm R S).symm) = prod.swap := rfl
-@[simp] lemma coe_coe_prod_comm : ⇑(prod_comm R S : R × S →+* S × R) = prod.swap := rfl
-@[simp] lemma coe_coe_prod_comm_symm : ⇑((prod_comm R S).symm : S × R →+* R × S) = prod.swap := rfl
+@[simp] lemma coe_prod_comm : ⇑(prod_comm : R × S ≃+* S × R) = prod.swap := rfl
+@[simp] lemma coe_prod_comm_symm : ⇑((prod_comm : R × S ≃+* S × R).symm) = prod.swap := rfl
 
 @[simp] lemma fst_comp_coe_prod_comm :
-  (ring_hom.fst S R).comp (prod_comm R S : R × S →+* S × R) = ring_hom.snd R S :=
+  (ring_hom.fst S R).comp ↑(prod_comm : R × S ≃+* S × R) = ring_hom.snd R S :=
 ring_hom.ext $ λ _, rfl
+
 @[simp] lemma snd_comp_coe_prod_comm :
-  (ring_hom.snd S R).comp (prod_comm R S : R × S →+* S × R) = ring_hom.fst R S :=
+  (ring_hom.snd S R).comp ↑(prod_comm : R × S ≃+* S × R) = ring_hom.fst R S :=
 ring_hom.ext $ λ _, rfl
 
 end ring_equiv

src/ring_theory/ideal/prod.lean

@@ -70,9 +70,9 @@ begin
 end
 
 @[simp] lemma map_prod_comm_prod :
-  map (ring_equiv.prod_comm R S : R × S →+* S × R) (prod I J) = prod J I :=
+  map ↑(ring_equiv.prod_comm : R × S ≃+* S × R) (prod I J) = prod J I :=
 begin
-  rw [ideal_prod_eq (map (ring_equiv.prod_comm R S : R × S →+* S × R) (prod I J))],
+  rw [ideal_prod_eq (map _ _)],
   simp [map_map]
 end