chore(algebra/group,logic/relator): review some explicit/implicit args (

#1441)

* chore(algebra/group,logic/relator): review some explicit/implicit arguments

* ring_hom.ext too

src/algebra/group/hom.lean

@@ -264,7 +264,7 @@ variables {M : Type*} {N : Type*} {P : Type*} [monoid M] [monoid N] [monoid P]
 variables {G : Type*} {H : Type*} [group G] [comm_group H]
 
 @[extensionality, to_additive]
-lemma ext (f g : M →* N) (h : (f : M → N) = g) : f = g :=
+lemma ext ⦃f g : M →* N⦄ (h : (f : M → N) = g) : f = g :=
 by cases f; cases g; cases h; refl
 
 /-- If f is a monoid homomorphism then f 1 = 1. -/

src/algebra/group/units.lean

@@ -6,7 +6,7 @@ Authors: Kenny Lau, Mario Carneiro, Johannes, Hölzl, Chris Hughes
 Units (i.e., invertible elements) of a multiplicative monoid.
 -/
 
-import tactic.basic
+import tactic.basic logic.function
 
 universe u
 variable {α : Type u}
@@ -22,13 +22,13 @@ variables [monoid α] {a b c : units α}
 
 instance : has_coe (units α) α := ⟨val⟩
 
-@[extensionality] theorem ext : ∀ {a b : units α}, (a : α) = b → a = b
+@[extensionality] theorem ext : function.injective (coe : units α → α)
 | ⟨v, i₁, vi₁, iv₁⟩ ⟨v', i₂, vi₂, iv₂⟩ e :=
   by change v = v' at e; subst v'; congr;
       simpa only [iv₂, vi₁, one_mul, mul_one] using mul_assoc i₂ v i₁
 
 theorem ext_iff {a b : units α} : a = b ↔ (a : α) = b :=
-⟨congr_arg _, ext⟩
+ext.eq_iff.symm
 
 instance [decidable_eq α] : decidable_eq (units α)
 | a b := decidable_of_iff' _ ext_iff
@@ -125,10 +125,10 @@ section monoid
   theorem divp_divp_eq_divp_mul (x : α) (u₁ u₂ : units α) : (x /ₚ u₁) /ₚ u₂ = x /ₚ (u₂ * u₁) :=
   by simp only [divp, mul_inv_rev, units.coe_mul, mul_assoc]
 
-  theorem divp_eq_iff_mul_eq (x : α) (u : units α) (y : α) : x /ₚ u = y ↔ y * u = x :=
+  theorem divp_eq_iff_mul_eq {x : α} {u : units α} {y : α} : x /ₚ u = y ↔ y * u = x :=
   u.mul_right_inj.symm.trans $ by rw [divp_mul_cancel]; exact ⟨eq.symm, eq.symm⟩
 
-  theorem divp_eq_one_iff_eq (a : α) (u : units α) : a /ₚ u = 1 ↔ a = u :=
+  theorem divp_eq_one_iff_eq {a : α} {u : units α} : a /ₚ u = 1 ↔ a = u :=
   (units.mul_right_inj u).symm.trans $ by rw [divp_mul_cancel, one_mul]
 
   @[simp] theorem one_divp (u : units α) : 1 /ₚ u = ↑u⁻¹ :=

src/algebra/ring.lean

@@ -315,7 +315,7 @@ namespace ring_hom
 variables {β : Type v} [semiring α] [semiring β]
 variables (f : α →+* β) {x y : α}
 
-@[extensionality] theorem ext (f g : α →+* β) (h : (f : α → β) = g) : f = g :=
+@[extensionality] theorem ext ⦃f g : α →+* β⦄ (h : (f : α → β) = g) : f = g :=
 by cases f; cases g; cases h; refl
 
 /-- Ring homomorphisms map zero to zero. -/

src/data/list/basic.lean

@@ -2648,7 +2648,7 @@ lemma rel_filter_map {f : α → option γ} {q : β → option δ} :
 @[to_additive]
 lemma rel_prod [monoid α] [monoid β]
   (h : r 1 1) (hf : (r ⇒ r ⇒ r) (*) (*)) : (forall₂ r ⇒ r) prod prod :=
-assume a b, rel_foldl (assume a b, hf) h
+rel_foldl hf h
 
 end forall₂
 

src/data/multiset.lean

@@ -2062,7 +2062,7 @@ end
 
 lemma rel_map {p : γ → δ → Prop} {s t} {f : α → γ} {g : β → δ} (h : (r ⇒ p) f g) (hst : rel r s t) :
   rel p (s.map f) (t.map g) :=
-by rw [rel_map_left, rel_map_right]; exact hst.mono (assume a b, h)
+by rw [rel_map_left, rel_map_right]; exact hst.mono h
 
 lemma rel_bind {p : γ → δ → Prop} {s t} {f : α → multiset γ} {g : β → multiset δ}
   (h : (r ⇒ rel p) f g) (hst : rel r s t) :

src/logic/relator.lean

@@ -24,7 +24,7 @@ variables {α : Type u₁} {β : Type u₂} {γ : Type v₁} {δ : Type v₂}
 variables (R : α → β → Prop) (S : γ → δ → Prop)
 
 def lift_fun (f : α → γ) (g : β → δ) : Prop :=
-∀{a b}, R a b → S (f a) (g b)
+∀⦃a b⦄, R a b → S (f a) (g b)
 
 infixr ⇒ := lift_fun