refactor(algebra/*): Make monoid_hom.ext etc use ∀ x, f x = g x a…

…s an assumption (#1476)

src/algebra/category/CommRing/adjunctions.lean

@@ -32,8 +32,8 @@ def free : Type u ⥤ CommRing.{u} :=
   -- TODO this should just be `ring_hom.of (rename f)`, but this causes a mysterious deterministic timeout!
   map := λ X Y f, @ring_hom.of _ _ _ _ (rename f) (by apply_instance),
   -- TODO these next two fields can be done by `tidy`, but the calls in `dsimp` and `simp` it generates are too slow.
-  map_id' := λ X, ring_hom.ext $ funext $ rename_id,
-  map_comp' := λ X Y Z f g, ring_hom.ext $ funext $ λ p, (rename_rename f g p).symm }
+  map_id' := λ X, ring_hom.ext $ rename_id,
+  map_comp' := λ X Y Z f g, ring_hom.ext $ λ p, (rename_rename f g p).symm }
 
 @[simp] lemma free_obj_coe {α : Type u} :
   (free.obj α : Type u) = mv_polynomial α ℤ := rfl

src/algebra/category/CommRing/basic.lean

@@ -35,7 +35,7 @@ def of (R : Type u) [semiring R] : SemiRing := bundled.of R
 instance (R : SemiRing) : semiring R := R.str
 
 instance bundled_hom : bundled_hom @ring_hom :=
-⟨@ring_hom.to_fun, @ring_hom.id, @ring_hom.comp, @ring_hom.ext⟩
+⟨@ring_hom.to_fun, @ring_hom.id, @ring_hom.comp, @ring_hom.coe_inj⟩
 
 instance has_forget_to_Mon : has_forget₂ SemiRing.{u} Mon.{u} :=
 bundled_hom.mk_has_forget₂ @semiring.to_monoid (λ R₁ R₂ f, f.to_monoid_hom) (λ _ _ _, rfl)

src/algebra/category/CommRing/limits.lean

@@ -103,7 +103,7 @@ private def limit (F : J ⥤ CommRing.{u}) : cone F :=
   π :=
   { app := λ j, ring_hom.of $ limit.π (F ⋙ forget _) j,
     naturality' := λ j j' f,
-      ring_hom.ext ((limit.cone (F ⋙ forget _)).π.naturality f) } }
+      ring_hom.coe_inj ((limit.cone (F ⋙ forget _)).π.naturality f) } }
 
 private def limit_is_limit (F : J ⥤ CommRing.{u}) : is_limit (limit F) :=
 begin

src/algebra/category/Mon/basic.lean

@@ -37,7 +37,7 @@ def of (M : Type u) [monoid M] : Mon := bundled.of M
 
 @[to_additive]
 instance bundled_hom : bundled_hom @monoid_hom :=
-⟨@monoid_hom.to_fun, @monoid_hom.id, @monoid_hom.comp, @monoid_hom.ext⟩
+⟨@monoid_hom.to_fun, @monoid_hom.id, @monoid_hom.comp, @monoid_hom.coe_inj⟩
 
 end Mon
 

src/algebra/group/hom.lean

@@ -262,10 +262,18 @@ def of (f : M → N) [h : is_monoid_hom f] : M →* N :=
 lemma coe_of (f : M → N) [is_monoid_hom f] : ⇑ (monoid_hom.of f) = f :=
 rfl
 
-@[extensionality, to_additive]
-lemma ext ⦃f g : M →* N⦄ (h : (f : M → N) = g) : f = g :=
+@[to_additive]
+lemma coe_inj ⦃f g : M →* N⦄ (h : (f : M → N) = g) : f = g :=
 by cases f; cases g; cases h; refl
 
+@[extensionality, to_additive]
+lemma ext ⦃f g : M →* N⦄ (h : ∀ x, f x = g x) : f = g :=
+coe_inj (funext h)
+
+@[to_additive]
+lemma ext_iff {f g : M →* N} : f = g ↔ ∀ x, f x = g x :=
+⟨λ h x, h ▸ rfl, λ h, ext h⟩
+
 /-- If f is a monoid homomorphism then f 1 = 1. -/
 @[simp, to_additive]
 lemma map_one (f : M →* N) : f 1 = 1 := f.map_one'

src/algebra/ring.lean

@@ -334,9 +334,15 @@ def of (f : α → β) [is_semiring_hom f] : α →+* β :=
 
 variables (f : α →+* β) {x y : α}
 
-@[extensionality] theorem ext ⦃f g : α →+* β⦄ (h : (f : α → β) = g) : f = g :=
+theorem coe_inj ⦃f g : α →+* β⦄ (h : (f : α → β) = g) : f = g :=
 by cases f; cases g; cases h; refl
 
+@[extensionality] theorem ext ⦃f g : α →+* β⦄ (h : ∀ x, f x = g x) : f = g :=
+coe_inj (funext h)
+
+theorem ext_iff {f g : α →+* β} : f = g ↔ ∀ x, f x = g x :=
+⟨λ h x, h ▸ rfl, λ h, ext h⟩
+
 /-- Ring homomorphisms map zero to zero. -/
 @[simp] lemma map_zero (f : α →+* β) : f 0 = 0 := f.map_zero'
 

src/data/mv_polynomial.lean

@@ -780,7 +780,7 @@ functiosn out of the the type `σ`, -/
 def hom_equiv : (mv_polynomial σ ℤ →+* β) ≃ (σ → β) :=
 { to_fun := λ f, ⇑f ∘ X,
   inv_fun := λ f, ring_hom.of (eval₂ (λ n : ℤ, (n : β)) f),
-  left_inv := λ f, ring_hom.ext $ funext $ eval₂_hom_X _ _,
+  left_inv := λ f, ring_hom.ext  $ eval₂_hom_X _ _,
   right_inv := λ f, funext $ λ x, by simp only [ring_hom.coe_of, function.comp_app, eval₂_X] }
 
 end eval₂