chore(algebra/group/type_tags): Use ≃ instead of → (#4346)

These functions are all equivalences, so we may as well expose that in their type

This also fills in some conversions that were missing.

Unfortunately this requires some type ascriptions in a handful of places.
It might be possible to remove these somehow.
This zulip thread contains a mwe: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Type.20inference.20on.20.60.E2.86.92.60.20vs.20.60.E2.89.83.60/near/211922501.

src/algebra/group/type_tags.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import algebra.group.hom
+import data.equiv.basic
 /-!
 # Type tags that turn additive structures into multiplicative, and vice versa
 
@@ -28,22 +29,16 @@ multiplicative structure. -/
 def multiplicative (α : Type*) := α
 
 /-- Reinterpret `x : α` as an element of `additive α`. -/
-def additive.of_mul (x : α) : additive α := x
+def additive.of_mul : α ≃ additive α := ⟨λ x, x, λ x, x, λ x, rfl, λ x, rfl⟩
 
 /-- Reinterpret `x : additive α` as an element of `α`. -/
-def additive.to_mul (x : additive α) : α := x
-
-lemma of_mul_injective : function.injective (@additive.of_mul α) := λ _ _, id
-lemma to_mul_injective : function.injective (@additive.to_mul α) := λ _ _, id
+def additive.to_mul : additive α ≃ α := additive.of_mul.symm
 
 /-- Reinterpret `x : α` as an element of `multiplicative α`. -/
-def multiplicative.of_add (x : α) : multiplicative α := x
+def multiplicative.of_add : α ≃ multiplicative α := ⟨λ x, x, λ x, x, λ x, rfl, λ x, rfl⟩
 
 /-- Reinterpret `x : multiplicative α` as an element of `α`. -/
-def multiplicative.to_add (x : multiplicative α) : α := x
-
-lemma of_add_injective : function.injective (@multiplicative.of_add α) := λ _ _, id
-lemma to_add_injective : function.injective (@multiplicative.to_add α) := λ _ _, id
+def multiplicative.to_add : multiplicative α ≃ α := multiplicative.of_add.symm
 
 @[simp] lemma to_add_of_add (x : α) : (multiplicative.of_add x).to_add = x := rfl
 @[simp] lemma of_add_to_add (x : multiplicative α) : multiplicative.of_add x.to_add = x := rfl
@@ -166,21 +161,32 @@ instance [comm_group α] : add_comm_group (additive α) :=
 instance [add_comm_group α] : comm_group (multiplicative α) :=
 { .. multiplicative.group, .. multiplicative.comm_monoid }
 
-/-- Reinterpret `f : α →+ β` as `multiplicative α →* multiplicative β`. -/
-def add_monoid_hom.to_multiplicative [add_monoid α] [add_monoid β] (f : α →+ β) :
-  multiplicative α →* multiplicative β :=
-⟨f.1, f.2, f.3⟩
-
-/-- Reinterpret `f : α →* β` as `additive α →+ additive β`. -/
-def monoid_hom.to_additive [monoid α] [monoid β] (f : α →* β) : additive α →+ additive β :=
-⟨f.1, f.2, f.3⟩
-
-/-- Reinterpret `f : additive α →+ β` as `α →* multiplicative β`. -/
-def add_monoid_hom.to_multiplicative' [monoid α] [add_monoid β] (f : additive α →+ β) :
-  α →* multiplicative β :=
-⟨f.1, f.2, f.3⟩
-
-/-- Reinterpret `f : α →* multiplicative β` as `additive α →+ β`. -/
-def monoid_hom.to_additive' [monoid α] [add_monoid β] (f : α →* multiplicative β) :
-  additive α →+ β :=
-⟨f.1, f.2, f.3⟩
+/-- Reinterpret `α →+ β` as `multiplicative α →* multiplicative β`. -/
+def add_monoid_hom.to_multiplicative [add_monoid α] [add_monoid β] :
+  (α →+ β) ≃ (multiplicative α →* multiplicative β) :=
+⟨λ f, ⟨f.1, f.2, f.3⟩, λ f, ⟨f.1, f.2, f.3⟩, λ x, by { ext, refl, }, λ x, by { ext, refl, }⟩
+
+/-- Reinterpret `α →* β` as `additive α →+ additive β`. -/
+def monoid_hom.to_additive [monoid α] [monoid β] :
+  (α →* β) ≃ (additive α →+ additive β) :=
+⟨λ f, ⟨f.1, f.2, f.3⟩, λ f, ⟨f.1, f.2, f.3⟩, λ x, by { ext, refl, }, λ x, by { ext, refl, }⟩
+
+/-- Reinterpret `additive α →+ β` as `α →* multiplicative β`. -/
+def add_monoid_hom.to_multiplicative' [monoid α] [add_monoid β] :
+  (additive α →+ β) ≃ (α →* multiplicative β) :=
+⟨λ f, ⟨f.1, f.2, f.3⟩, λ f, ⟨f.1, f.2, f.3⟩, λ x, by { ext, refl, }, λ x, by { ext, refl, }⟩
+
+/-- Reinterpret `α →* multiplicative β` as `additive α →+ β`. -/
+def monoid_hom.to_additive' [monoid α] [add_monoid β] :
+  (α →* multiplicative β) ≃ (additive α →+ β) :=
+add_monoid_hom.to_multiplicative'.symm
+
+/-- Reinterpret `α →+ additive β` as `multiplicative α →* β`. -/
+def add_monoid_hom.to_multiplicative'' [add_monoid α] [monoid β] :
+  (α →+ additive β) ≃ (multiplicative α →* β) :=
+⟨λ f, ⟨f.1, f.2, f.3⟩, λ f, ⟨f.1, f.2, f.3⟩, λ x, by { ext, refl, }, λ x, by { ext, refl, }⟩
+
+/-- Reinterpret `multiplicative α →* β` as `α →+ additive β`. -/
+def monoid_hom.to_additive'' [add_monoid α] [monoid β] :
+  (multiplicative α →* β) ≃ (α →+ additive β) :=
+add_monoid_hom.to_multiplicative''.symm

src/data/equiv/mul_add.lean

@@ -437,13 +437,46 @@ end equiv
 
 section type_tags
 
-/-- Reinterpret `f : G ≃+ H` as `multiplicative G ≃* multiplicative H`. -/
-def add_equiv.to_multiplicative [add_monoid G] [add_monoid H] (f : G ≃+ H) :
-  multiplicative G ≃* multiplicative H :=
-⟨f.to_add_monoid_hom.to_multiplicative, f.symm.to_add_monoid_hom.to_multiplicative, f.3, f.4, f.5⟩
-
-/-- Reinterpret `f : G ≃* H` as `additive G ≃+ additive H`. -/
-def mul_equiv.to_additive [monoid G] [monoid H] (f : G ≃* H) : additive G ≃+ additive H :=
-⟨f.to_monoid_hom.to_additive, f.symm.to_monoid_hom.to_additive, f.3, f.4, f.5⟩
+/-- Reinterpret `G ≃+ H` as `multiplicative G ≃* multiplicative H`. -/
+def add_equiv.to_multiplicative [add_monoid G] [add_monoid H] :
+  (G ≃+ H) ≃ (multiplicative G ≃* multiplicative H) :=
+{ to_fun := λ f, ⟨f.to_add_monoid_hom.to_multiplicative, f.symm.to_add_monoid_hom.to_multiplicative, f.3, f.4, f.5⟩,
+  inv_fun := λ f, ⟨f.to_monoid_hom, f.symm.to_monoid_hom, f.3, f.4, f.5⟩,
+  left_inv := λ x, by { ext, refl, },
+  right_inv := λ x, by { ext, refl, }, }
+
+/-- Reinterpret `G ≃* H` as `additive G ≃+ additive H`. -/
+def mul_equiv.to_additive [monoid G] [monoid H] :
+  (G ≃* H) ≃ (additive G ≃+ additive H) :=
+{ to_fun := λ f, ⟨f.to_monoid_hom.to_additive, f.symm.to_monoid_hom.to_additive, f.3, f.4, f.5⟩,
+  inv_fun := λ f, ⟨f.to_add_monoid_hom, f.symm.to_add_monoid_hom, f.3, f.4, f.5⟩,
+  left_inv := λ x, by { ext, refl, },
+  right_inv := λ x, by { ext, refl, }, }
+
+/-- Reinterpret `additive G ≃+ H` as `G ≃* multiplicative H`. -/
+def add_equiv.to_multiplicative' [monoid G] [add_monoid H] :
+  (additive G ≃+ H) ≃ (G ≃* multiplicative H) :=
+{ to_fun := λ f, ⟨f.to_add_monoid_hom.to_multiplicative', f.symm.to_add_monoid_hom.to_multiplicative'', f.3, f.4, f.5⟩,
+  inv_fun := λ f, ⟨f.to_monoid_hom, f.symm.to_monoid_hom, f.3, f.4, f.5⟩,
+  left_inv := λ x, by { ext, refl, },
+  right_inv := λ x, by { ext, refl, }, }
+
+/-- Reinterpret `G ≃* multiplicative H` as `additive G ≃+ H` as. -/
+def mul_equiv.to_additive' [monoid G] [add_monoid H] :
+  (G ≃* multiplicative H) ≃ (additive G ≃+ H) :=
+add_equiv.to_multiplicative'.symm
+
+/-- Reinterpret `G ≃+ additive H` as `multiplicative G ≃* H`. -/
+def add_equiv.to_multiplicative'' [add_monoid G] [monoid H] :
+  (G ≃+ additive H) ≃ (multiplicative G ≃* H) :=
+{ to_fun := λ f, ⟨f.to_add_monoid_hom.to_multiplicative'', f.symm.to_add_monoid_hom.to_multiplicative', f.3, f.4, f.5⟩,
+  inv_fun := λ f, ⟨f.to_monoid_hom, f.symm.to_monoid_hom, f.3, f.4, f.5⟩,
+  left_inv := λ x, by { ext, refl, },
+  right_inv := λ x, by { ext, refl, }, }
+
+/-- Reinterpret `multiplicative G ≃* H` as `G ≃+ additive H` as. -/
+def mul_equiv.to_additive'' [add_monoid G] [monoid H] :
+  (multiplicative G ≃* H) ≃ (G ≃+ additive H) :=
+add_equiv.to_multiplicative''.symm
 
 end type_tags

src/dynamics/circle/rotation_number/translation_number.lean

@@ -139,15 +139,15 @@ by refine (units.map _).comp to_units.to_monoid_hom; exact
 lemma translate_inv_apply (x y : ℝ) : (translate $ multiplicative.of_add x)⁻¹ y = -x + y := rfl
 
 @[simp] lemma translate_gpow (x : ℝ) (n : ℤ) :
-  (translate (multiplicative.of_add x))^n = translate (multiplicative.of_add $ n * x) :=
+  (translate (multiplicative.of_add x))^n = translate (multiplicative.of_add $ ↑n * x) :=
 by simp only [← gsmul_eq_mul, of_add_gsmul, monoid_hom.map_gpow]
 
 @[simp] lemma translate_pow (x : ℝ) (n : ℕ) :
-  (translate (multiplicative.of_add x))^n = translate (multiplicative.of_add $ n * x) :=
+  (translate (multiplicative.of_add x))^n = translate (multiplicative.of_add $ ↑n * x) :=
 translate_gpow x n
 
 @[simp] lemma translate_iterate (x : ℝ) (n : ℕ) :
-  (translate (multiplicative.of_add x))^[n] = translate (multiplicative.of_add $ n * x) :=
+  (translate (multiplicative.of_add x))^[n] = translate (multiplicative.of_add $ ↑n * x) :=
 by rw [← units_coe, ← coe_pow, ← units.coe_pow, translate_pow, units_coe]
 
 /-!

src/ring_theory/roots_of_unity.lean

@@ -412,7 +412,7 @@ def zmod_equiv_gpowers (h : is_primitive_root ζ k) : zmod k ≃+ additive (subg
 add_equiv.of_bijective
 (add_monoid_hom.lift_of_surjective (int.cast_add_hom _)
   zmod.int_cast_surjective
-  { to_fun := λ i, additive.of_mul ⟨_, i, rfl⟩,
+  { to_fun := λ i, additive.of_mul (⟨_, i, rfl⟩ : subgroup.gpowers ζ),
     map_zero' := by { simp only [gpow_zero], refl },
     map_add' := by { intros i j, simp only [gpow_add], refl } }
   (λ i hi,
@@ -438,7 +438,7 @@ begin
 end
 
 @[simp] lemma zmod_equiv_gpowers_apply_coe_int (i : ℤ) :
-  h.zmod_equiv_gpowers i = additive.of_mul ⟨ζ ^ i, i, rfl⟩ :=
+  h.zmod_equiv_gpowers i = additive.of_mul (⟨ζ ^ i, i, rfl⟩ : subgroup.gpowers ζ) :=
 begin
   apply add_monoid_hom.lift_of_surjective_comp_apply,
   intros j hj,
@@ -450,23 +450,23 @@ begin
 end
 
 @[simp] lemma zmod_equiv_gpowers_apply_coe_nat (i : ℕ) :
-  h.zmod_equiv_gpowers i = additive.of_mul ⟨ζ ^ i, i, rfl⟩ :=
+  h.zmod_equiv_gpowers i = additive.of_mul (⟨ζ ^ i, i, rfl⟩ : subgroup.gpowers ζ) :=
 begin
   have : (i : zmod k) = (i : ℤ), by norm_cast,
   simp only [this, zmod_equiv_gpowers_apply_coe_int, gpow_coe_nat],
   refl
 end
 
 @[simp] lemma zmod_equiv_gpowers_symm_apply_gpow (i : ℤ) :
-  h.zmod_equiv_gpowers.symm (additive.of_mul ⟨ζ ^ i, i, rfl⟩) = i :=
+  h.zmod_equiv_gpowers.symm (additive.of_mul (⟨ζ ^ i, i, rfl⟩ : subgroup.gpowers ζ)) = i :=
 by rw [← h.zmod_equiv_gpowers.symm_apply_apply i, zmod_equiv_gpowers_apply_coe_int]
 
 @[simp] lemma zmod_equiv_gpowers_symm_apply_gpow' (i : ℤ) :
   h.zmod_equiv_gpowers.symm ⟨ζ ^ i, i, rfl⟩ = i :=
 h.zmod_equiv_gpowers_symm_apply_gpow i
 
 @[simp] lemma zmod_equiv_gpowers_symm_apply_pow (i : ℕ) :
-  h.zmod_equiv_gpowers.symm (additive.of_mul ⟨ζ ^ i, i, rfl⟩) = i :=
+  h.zmod_equiv_gpowers.symm (additive.of_mul (⟨ζ ^ i, i, rfl⟩ : subgroup.gpowers ζ)) = i :=
 by rw [← h.zmod_equiv_gpowers.symm_apply_apply i, zmod_equiv_gpowers_apply_coe_nat]
 
 @[simp] lemma zmod_equiv_gpowers_symm_apply_pow' (i : ℕ) :