chore(data/equiv/mul_add): add more equiv lemmas to mul_equiv nam…

…espace (#4380)

Also make `apply_eq_iff_eq` and `apply_eq_iff_eq_symm_apply` use
implicit arguments.

src/category_theory/limits/types.lean

@@ -349,7 +349,7 @@ let t' := colimit_cocone F,
     e' : t'.X ≅ t.X := (cocones.forget _).map_iso e in
 begin
   refine iff.trans _ (colimit_eq_iff_aux F),
-  convert equiv.apply_eq_iff_eq e'.to_equiv _ _; rw ←e.hom.w; refl
+  convert e'.to_equiv.apply_eq_iff_eq; rw ←e.hom.w; refl
 end
 
 lemma colimit_eq_iff {i j : J} {xi : F.obj i} {xj : F.obj j} :

src/data/equiv/basic.lean

@@ -182,10 +182,10 @@ e.left_inv x
 @[simp] lemma symm_trans_apply (f : α ≃ β) (g : β ≃ γ) (a : γ) :
   (f.trans g).symm a = f.symm (g.symm a) := rfl
 
-@[simp] theorem apply_eq_iff_eq (f : α ≃ β) (x y : α) : f x = f y ↔ x = y :=
+@[simp] theorem apply_eq_iff_eq (f : α ≃ β) {x y : α} : f x = f y ↔ x = y :=
 f.injective.eq_iff
 
-theorem apply_eq_iff_eq_symm_apply {α β : Sort*} (f : α ≃ β) (x : α) (y : β) :
+theorem apply_eq_iff_eq_symm_apply {α β : Sort*} (f : α ≃ β) {x : α} {y : β} :
   f x = y ↔ x = f.symm y :=
 begin
   conv_lhs { rw ←apply_symm_apply f y, },

src/data/equiv/encodable/basic.lean

@@ -292,10 +292,10 @@ def up (a : ulower α) : α := (equiv α).symm a
 @[simp] lemma up_down {a : α} : (down a).up = a := equiv.left_inv _ _
 
 @[simp] lemma up_eq_up {a b : ulower α} : a.up = b.up ↔ a = b :=
-equiv.apply_eq_iff_eq _ _ _
+equiv.apply_eq_iff_eq _
 
 @[simp] lemma down_eq_down {a b : α} : down a = down b ↔ a = b :=
-equiv.apply_eq_iff_eq _ _ _
+equiv.apply_eq_iff_eq _
 
 @[ext] protected lemma ext {a b : ulower α} : a.up = b.up → a = b :=
 up_eq_up.1

src/data/equiv/mul_add.lean

@@ -80,6 +80,15 @@ instance (h : M ≃* N) : is_mul_hom h := ⟨h.map_mul⟩
 def mk' (f : M ≃ N) (h : ∀ x y, f (x * y) = f x * f y) : M ≃* N :=
 ⟨f.1, f.2, f.3, f.4, h⟩
 
+@[to_additive]
+protected lemma bijective (e : M ≃* N) : function.bijective e := e.to_equiv.bijective
+
+@[to_additive]
+protected lemma injective (e : M ≃* N) : function.injective e := e.to_equiv.injective
+
+@[to_additive]
+protected lemma surjective (e : M ≃* N) : function.surjective e := e.to_equiv.surjective
+
 /-- The identity map is a multiplicative isomorphism. -/
 @[refl, to_additive "The identity map is an additive isomorphism."]
 def refl (M : Type*) [has_mul M] : M ≃* M :=
@@ -91,13 +100,12 @@ instance : inhabited (M ≃* M) := ⟨refl M⟩
 /-- The inverse of an isomorphism is an isomorphism. -/
 @[symm, to_additive "The inverse of an isomorphism is an isomorphism."]
 def symm (h : M ≃* N) : N ≃* M :=
-{ map_mul' := λ n₁ n₂, h.left_inv.injective begin
-    show h.to_equiv (h.to_equiv.symm (n₁ * n₂)) =
-      h ((h.to_equiv.symm n₁) * (h.to_equiv.symm n₂)),
-   rw h.map_mul,
-   show _ = h.to_equiv (_) * h.to_equiv (_),
-   rw [h.to_equiv.apply_symm_apply, h.to_equiv.apply_symm_apply, h.to_equiv.apply_symm_apply], end,
-  ..h.to_equiv.symm}
+{ map_mul' := λ n₁ n₂, h.injective $
+    begin
+      have : ∀ x, h (h.to_equiv.symm.to_fun x) = x := h.to_equiv.apply_symm_apply,
+      simp only [this, h.map_mul]
+    end,
+  .. h.to_equiv.symm}
 
 @[simp, to_additive]
 theorem to_equiv_symm (f : M ≃* N) : f.symm.to_equiv = f.to_equiv.symm := rfl
@@ -131,6 +139,21 @@ theorem refl_apply (m : M) : refl M m = m := rfl
 @[simp, to_additive]
 theorem trans_apply (e₁ : M ≃* N) (e₂ : N ≃* P) (m : M) : e₁.trans e₂ m = e₂ (e₁ m) := rfl
 
+@[simp, to_additive] theorem apply_eq_iff_eq (e : M ≃* N) {x y : M} : e x = e y ↔ x = y :=
+e.injective.eq_iff
+
+@[to_additive]
+lemma apply_eq_iff_symm_apply (e : M ≃* N) {x : M} {y : N} : e x = y ↔ x = e.symm y :=
+e.to_equiv.apply_eq_iff_eq_symm_apply
+
+@[to_additive]
+lemma symm_apply_eq (e : M ≃* N) {x y} : e.symm x = y ↔ x = e y :=
+e.to_equiv.symm_apply_eq
+
+@[to_additive]
+lemma eq_symm_apply (e : M ≃* N) {x y} : y = e.symm x ↔ e y = x :=
+e.to_equiv.eq_symm_apply
+
 /-- a multiplicative equiv of monoids sends 1 to 1 (and is hence a monoid isomorphism) -/
 @[simp, to_additive]
 lemma map_one {M N} [monoid M] [monoid N] (h : M ≃* N) : h 1 = 1 :=
@@ -139,7 +162,7 @@ by rw [←mul_one (h 1), ←h.apply_symm_apply 1, ←h.map_mul, one_mul]
 @[simp, to_additive]
 lemma map_eq_one_iff {M N} [monoid M] [monoid N] (h : M ≃* N) {x : M} :
   h x = 1 ↔ x = 1 :=
-h.map_one ▸ h.to_equiv.apply_eq_iff_eq x 1
+h.map_one ▸ h.to_equiv.apply_eq_iff_eq
 
 @[to_additive]
 lemma map_ne_one_iff {M N} [monoid M] [monoid N] (h : M ≃* N) {x : M} :

src/data/opposite.lean

@@ -83,10 +83,10 @@ lemma equiv_to_opposite_apply (a : α) : equiv_to_opposite a = op a := rfl
 lemma equiv_to_opposite_symm_apply (a : αᵒᵖ) : equiv_to_opposite.symm a = unop a := rfl
 
 lemma op_eq_iff_eq_unop {x : α} {y} : op x = y ↔ x = unop y :=
-equiv_to_opposite.apply_eq_iff_eq_symm_apply _ _
+equiv_to_opposite.apply_eq_iff_eq_symm_apply
 
 lemma unop_eq_iff_eq_op {x} {y : α} : unop x = y ↔ x = op y :=
-equiv_to_opposite.symm.apply_eq_iff_eq_symm_apply _ _
+equiv_to_opposite.symm.apply_eq_iff_eq_symm_apply
 
 instance [inhabited α] : inhabited αᵒᵖ := ⟨op (default _)⟩
 

src/group_theory/monoid_localization.lean

@@ -869,7 +869,7 @@ def of_mul_equiv_of_localizations (k : N ≃* P) : localization_map S P :=
 (k.to_monoid_hom.comp f.to_map).to_localization_map (λ y, is_unit_comp f k.to_monoid_hom y)
 (λ v, let ⟨z, hz⟩ := k.to_equiv.surjective v in
   let ⟨x, hx⟩ := f.surj z in ⟨x, show v * k _ = k _, by rw [←hx, k.map_mul, ←hz]; refl⟩)
-(λ x y, (k.to_equiv.apply_eq_iff_eq _ _).trans $ f.eq_iff_exists)
+(λ x y, k.apply_eq_iff_eq.trans f.eq_iff_exists)
 
 @[to_additive, simp] lemma of_mul_equiv_of_localizations_apply {k : N ≃* P} (x) :
   (f.of_mul_equiv_of_localizations k).to_map x = k (f.to_map x) := rfl