[Merged by Bors] - refactor(algebra/hom/group): generalize a few lemmas to monoid_hom_class

src/algebra/algebra/basic.lean

@@ -414,7 +414,7 @@ lemma of_algebra_map_injective
   [semiring A] [algebra R A] [no_zero_divisors A]
   (h : function.injective (algebra_map R A)) : no_zero_smul_divisors R A :=
 ⟨λ c x hcx, (mul_eq_zero.mp ((smul_def c x).symm.trans hcx)).imp_left
-  ((algebra_map R A).injective_iff.mp h _)⟩
+  ((injective_iff_map_eq_zero (algebra_map R A)).mp h _)⟩
 
 variables (R A)
 lemma algebra_map_injective [ring A] [nontrivial A]
@@ -744,11 +744,6 @@ variables [algebra R A] [algebra R B] (φ : A →ₐ[R] B)
 
 end division_ring
 
-theorem injective_iff {R A B : Type*} [comm_semiring R] [ring A] [semiring B]
-  [algebra R A] [algebra R B] (f : A →ₐ[R] B) :
-  function.injective f ↔ (∀ x, f x = 0 → x = 0) :=
-ring_hom.injective_iff (f : A →+* B)
-
 end alg_hom
 
 @[simp] lemma rat.smul_one_eq_coe {A : Type*} [division_ring A] [algebra ℚ A] (m : ℚ) :
@@ -1434,7 +1429,7 @@ begin
   { have : function.injective (algebra_map R A) :=
       no_zero_smul_divisors.iff_algebra_map_injective.1 infer_instance,
     left,
-    exact (ring_hom.injective_iff _).1 this _ H },
+    exact (injective_iff_map_eq_zero _).1 this _ H },
   { right,
     exact H }
 end

src/algebra/field/basic.lean

@@ -307,7 +307,8 @@ lemma map_inv : g x⁻¹ = (g x)⁻¹ := g.to_monoid_with_zero_hom.map_inv x
 
 lemma map_div : g (x / y) = g x / g y := g.to_monoid_with_zero_hom.map_div x y
 
-protected lemma injective : function.injective f := f.injective_iff.2 $ λ x, f.map_eq_zero.1
+protected lemma injective : function.injective f :=
+(injective_iff_map_eq_zero f).2 $ λ x, f.map_eq_zero.1
 
 end
 

src/algebra/group/ext.lean

@@ -114,7 +114,7 @@ begin
     exact @monoid_hom.map_zpow' M M m₁ m₂ f (congr_fun h_inv) x m },
   have hdiv : m₁.div = m₂.div,
   { ext a b,
-    exact @monoid_hom.map_div' M M m₁ m₂ f (congr_fun h_inv) a b },
+    exact @map_div' M M _ m₁ m₂ _ f (congr_fun h_inv) a b },
   unfreezingI { cases m₁, cases m₂ },
   congr, exacts [h_mul, h₁, hpow, h_inv, hdiv, hzpow]
 end

src/algebra/hom/group.lean

@@ -307,6 +307,11 @@ lemma map_div [group G] [group H] [monoid_hom_class F G H]
   (f : F) (x y : G) : f (x / y) = f x / f y :=
 by rw [div_eq_mul_inv, div_eq_mul_inv, map_mul_inv]
 
+@[to_additive]
+theorem map_div' [div_inv_monoid G] [div_inv_monoid H] [monoid_hom_class F G H] (f : F)
+  (hf : ∀ x, f (x⁻¹) = (f x)⁻¹) (a b : G) : f (a / b) = f a / f b :=
+by rw [div_eq_mul_inv, div_eq_mul_inv, map_mul, hf]
+
 -- to_additive puts the arguments in the wrong order, so generate an auxiliary lemma, then
 -- swap its arguments.
 @[to_additive map_nsmul.aux, simp] theorem map_pow [monoid G] [monoid H] [monoid_hom_class F G H]
@@ -662,30 +667,26 @@ add_decl_doc add_monoid_hom.map_add
 
 namespace monoid_hom
 variables {mM : mul_one_class M} {mN : mul_one_class N} {mP : mul_one_class P}
-variables [group G] [comm_group H]
+variables [group G] [comm_group H] [monoid_hom_class F M N]
 
 include mM mN
 
-@[to_additive]
-lemma map_mul_eq_one (f : M →* N) {a b : M} (h : a * b = 1) : f a * f b = 1 :=
-map_mul_eq_one f h
-
 /-- Given a monoid homomorphism `f : M →* N` and an element `x : M`, if `x` has a right inverse,
 then `f x` has a right inverse too. For elements invertible on both sides see `is_unit.map`. -/
 @[to_additive "Given an add_monoid homomorphism `f : M →+ N` and an element `x : M`, if `x` has
 a right inverse, then `f x` has a right inverse too."]
-lemma map_exists_right_inv (f : M →* N) {x : M} (hx : ∃ y, x * y = 1) :
+lemma map_exists_right_inv (f : F) {x : M} (hx : ∃ y, x * y = 1) :
   ∃ y, f x * y = 1 :=
-let ⟨y, hy⟩ := hx in ⟨f y, f.map_mul_eq_one hy⟩
+let ⟨y, hy⟩ := hx in ⟨f y, map_mul_eq_one f hy⟩
 
 /-- Given a monoid homomorphism `f : M →* N` and an element `x : M`, if `x` has a left inverse,
 then `f x` has a left inverse too. For elements invertible on both sides see `is_unit.map`. -/
 @[to_additive "Given an add_monoid homomorphism `f : M →+ N` and an element `x : M`, if `x` has
 a left inverse, then `f x` has a left inverse too. For elements invertible on both sides see
 `is_add_unit.map`."]
-lemma map_exists_left_inv (f : M →* N) {x : M} (hx : ∃ y, y * x = 1) :
+lemma map_exists_left_inv (f : F) {x : M} (hx : ∃ y, y * x = 1) :
   ∃ y, y * f x = 1 :=
-let ⟨y, hy⟩ := hx in ⟨f y, f.map_mul_eq_one hy⟩
+let ⟨y, hy⟩ := hx in ⟨f y, map_mul_eq_one f hy⟩
 
 end monoid_hom
 
@@ -885,11 +886,6 @@ protected theorem monoid_hom.map_zpow' [div_inv_monoid M] [div_inv_monoid N] (f
   f (a ^ n) = (f a) ^ n :=
 map_zpow' f hf a n
 
-@[to_additive]
-theorem monoid_hom.map_div' [div_inv_monoid M] [div_inv_monoid N] (f : M →* N)
-  (hf : ∀ x, f (x⁻¹) = (f x)⁻¹) (a b : M) : f (a / b) = f a / f b :=
-by rw [div_eq_mul_inv, div_eq_mul_inv, f.map_mul, hf]
-
 section End
 
 namespace monoid
@@ -1055,10 +1051,10 @@ by { ext, simp only [mul_apply, function.comp_app, map_mul, coe_comp] }
 /-- If two homomorphism from a group to a monoid are equal at `x`, then they are equal at `x⁻¹`. -/
 @[to_additive "If two homomorphism from an additive group to an additive monoid are equal at `x`,
 then they are equal at `-x`." ]
-lemma eq_on_inv {G} [group G] [monoid M] {f g : G →* M} {x : G} (h : f x = g x) :
-  f x⁻¹ = g x⁻¹ :=
+lemma eq_on_inv {G} [group G] [monoid M] [monoid_hom_class F G M] {f g : F} {x : G}
+  (h : f x = g x) : f x⁻¹ = g x⁻¹ :=
 left_inv_eq_right_inv (map_mul_eq_one f $ inv_mul_self x) $
-  h.symm ▸ g.map_mul_eq_one $ mul_inv_self x
+  h.symm ▸ map_mul_eq_one g $ mul_inv_self x
 
 /-- Group homomorphisms preserve inverse. -/
 @[to_additive]
@@ -1084,24 +1080,24 @@ protected theorem map_mul_inv {G H} [group G] [group H] (f : G →* H) (g h : G)
 map_mul_inv f g h
 
 /-- A homomorphism from a group to a monoid is injective iff its kernel is trivial.
-For the iff statement on the triviality of the kernel, see `monoid_hom.injective_iff'`.  -/
+For the iff statement on the triviality of the kernel, see `injective_iff_map_eq_one'`.  -/
 @[to_additive "A homomorphism from an additive group to an additive monoid is injective iff
 its kernel is trivial. For the iff statement on the triviality of the kernel,
-see `add_monoid_hom.injective_iff'`."]
-lemma injective_iff {G H} [group G] [mul_one_class H] (f : G →* H) :
-  function.injective f ↔ (∀ a, f a = 1 → a = 1) :=
+see `injective_iff_map_eq_zero'`."]
+lemma _root_.injective_iff_map_eq_one {G H} [group G] [mul_one_class H] [monoid_hom_class F G H]
+  (f : F) : function.injective f ↔ (∀ a, f a = 1 → a = 1) :=
 ⟨λ h x, (map_eq_one_iff f h).mp,
- λ h x y hxy, mul_inv_eq_one.1 $ h _ $ by rw [f.map_mul, hxy, ← f.map_mul, mul_inv_self, f.map_one]⟩
+ λ h x y hxy, mul_inv_eq_one.1 $ h _ $ by rw [map_mul, hxy, ← map_mul, mul_inv_self, map_one]⟩
 
 /-- A homomorphism from a group to a monoid is injective iff its kernel is trivial,
 stated as an iff on the triviality of the kernel.
-For the implication, see `monoid_hom.injective_iff`. -/
+For the implication, see `injective_iff_map_eq_one`. -/
 @[to_additive "A homomorphism from an additive group to an additive monoid is injective iff its
 kernel is trivial, stated as an iff on the triviality of the kernel. For the implication, see
-`add_monoid_hom.injective_iff`."]
-lemma injective_iff' {G H} [group G] [mul_one_class H] (f : G →* H) :
-  function.injective f ↔ (∀ a, f a = 1 ↔ a = 1) :=
-f.injective_iff.trans $ forall_congr $ λ a, ⟨λ h, ⟨h, λ H, H.symm ▸ f.map_one⟩, iff.mp⟩
+`injective_iff_map_eq_zero`."]
+lemma _root_.injective_iff_map_eq_one' {G H} [group G] [mul_one_class H] [monoid_hom_class F G H]
+  (f : F) : function.injective f ↔ (∀ a, f a = 1 ↔ a = 1) :=
+(injective_iff_map_eq_one f).trans $ forall_congr $ λ a, ⟨λ h, ⟨h, λ H, H.symm ▸ map_one f⟩, iff.mp⟩
 
 include mM
 /-- Makes a group homomorphism from a proof that the map preserves multiplication. -/

src/algebra/module/basic.lean

@@ -550,7 +550,7 @@ variables (M)
 
 lemma smul_right_injective [no_zero_smul_divisors R M] {c : R} (hc : c ≠ 0) :
   function.injective ((•) c : M → M) :=
-(smul_add_hom R M c).injective_iff.2 $ λ a ha, (smul_eq_zero.mp ha).resolve_left hc
+(injective_iff_map_eq_zero (smul_add_hom R M c)).2 $ λ a ha, (smul_eq_zero.mp ha).resolve_left hc
 
 variables {M}
 

src/algebra/ring/basic.lean

@@ -985,16 +985,6 @@ map_neg f x
 protected theorem map_sub {α β} [non_assoc_ring α] [non_assoc_ring β] (f : α →+* β) (x y : α) :
   f (x - y) = (f x) - (f y) := map_sub f x y
 
-/-- A ring homomorphism is injective iff its kernel is trivial. -/
-theorem injective_iff {α β} [non_assoc_ring α] [non_assoc_semiring β] (f : α →+* β) :
-  function.injective f ↔ (∀ a, f a = 0 → a = 0) :=
-(f : α →+ β).injective_iff
-
-/-- A ring homomorphism is injective iff its kernel is trivial. -/
-theorem injective_iff' {α β} [non_assoc_ring α] [non_assoc_semiring β] (f : α →+* β) :
-  function.injective f ↔ (∀ a, f a = 0 ↔ a = 0) :=
-(f : α →+ β).injective_iff'
-
 /-- Makes a ring homomorphism from a monoid homomorphism of rings which preserves addition. -/
 def mk' {γ} [non_assoc_semiring α] [non_assoc_ring γ] (f : α →* γ)
   (map_add : ∀ a b : α, f (a + b) = f a + f b) :

src/algebraic_geometry/function_field.lean

@@ -65,7 +65,7 @@ end
 lemma germ_injective_of_is_integral [is_integral X] {U : opens X.carrier} (x : U) :
   function.injective (X.presheaf.germ x) :=
 begin
-  rw ring_hom.injective_iff,
+  rw injective_iff_map_eq_zero,
   intros y hy,
   rw ← (X.presheaf.germ x).map_zero at hy,
   obtain ⟨W, hW, iU, iV, e⟩ := X.presheaf.germ_eq _ x.prop x.prop _ _ hy,

src/algebraic_geometry/properties.lean

@@ -336,7 +336,7 @@ lemma map_injective_of_is_integral [is_integral X] {U V : opens X.carrier} (i :
   [H : nonempty U] :
   function.injective (X.presheaf.map i.op) :=
 begin
-  rw ring_hom.injective_iff,
+  rw injective_iff_map_eq_zero,
   intros x hx,
   rw ← basic_open_eq_bot_iff at ⊢ hx,
   rw Scheme.basic_open_res at hx,

src/data/polynomial/eval.lean

@@ -866,7 +866,7 @@ by rw [is_root, eval_map, eval₂_hom, h.eq_zero, f.map_zero]
 
 lemma is_root.of_map {R} [comm_ring R] {f : R →+* S} {x : R} {p : R[X]}
   (h : is_root (p.map f) (f x)) (hf : function.injective f) : is_root p x :=
-by rwa [is_root, ←f.injective_iff'.mp hf, ←eval₂_hom, ←eval_map]
+by rwa [is_root, ←(injective_iff_map_eq_zero' f).mp hf, ←eval₂_hom, ←eval_map]
 
 lemma is_root_map_iff {R : Type*} [comm_ring R] {f : R →+* S} {x : R} {p : R[X]}
   (hf : function.injective f) : is_root (p.map f) (f x) ↔ is_root p x :=

src/data/zmod/basic.lean

@@ -368,7 +368,7 @@ variables (R)
 
 lemma cast_hom_injective : function.injective (zmod.cast_hom (dvd_refl n) R) :=
 begin
-  rw ring_hom.injective_iff,
+  rw injective_iff_map_eq_zero,
   intro x,
   obtain ⟨k, rfl⟩ := zmod.int_cast_surjective x,
   rw [ring_hom.map_int_cast, char_p.int_cast_eq_zero_iff R n,

src/field_theory/abel_ruffini.lean

@@ -123,7 +123,7 @@ begin
   { rw [ha, C_0, sub_zero],
     exact gal_X_pow_is_solvable n },
   have ha' : algebra_map F (X ^ n - C a).splitting_field a ≠ 0 :=
-    mt ((ring_hom.injective_iff _).mp (ring_hom.injective _) a) ha,
+    mt ((injective_iff_map_eq_zero _).mp (ring_hom.injective _) a) ha,
   by_cases hn : n = 0,
   { rw [hn, pow_zero, ←C_1, ←C_sub],
     exact gal_C_is_solvable (1 - a) },
@@ -159,7 +159,7 @@ end
 lemma splits_X_pow_sub_one_of_X_pow_sub_C {F : Type*} [field F] {E : Type*} [field E]
   (i : F →+* E) (n : ℕ) {a : F} (ha : a ≠ 0) (h : (X ^ n - C a).splits i) : (X ^ n - 1).splits i :=
 begin
-  have ha' : i a ≠ 0 := mt (i.injective_iff.mp (i.injective) a) ha,
+  have ha' : i a ≠ 0 := mt ((injective_iff_map_eq_zero i).mp (i.injective) a) ha,
   by_cases hn : n = 0,
   { rw [hn, pow_zero, sub_self],
     exact splits_zero i },

src/field_theory/intermediate_field.lean

@@ -310,7 +310,7 @@ lemma coe_is_integral_iff {R : Type*} [comm_ring R] [algebra R K] [algebra R L]
 begin
   refine ⟨λ h, _, λ h, _⟩,
   { obtain ⟨P, hPmo, hProot⟩ := h,
-    refine ⟨P, hPmo, (ring_hom.injective_iff _).1 (algebra_map ↥S L).injective _ _⟩,
+    refine ⟨P, hPmo, (injective_iff_map_eq_zero _).1 (algebra_map ↥S L).injective _ _⟩,
     letI : is_scalar_tower R S L := is_scalar_tower.of_algebra_map_eq (congr_fun rfl),
     rwa [eval₂_eq_eval_map, ← eval₂_at_apply, eval₂_eq_eval_map, polynomial.map_map,
       ← is_scalar_tower.algebra_map_eq, ← eval₂_eq_eval_map] },

src/field_theory/mv_polynomial.lean

@@ -29,7 +29,7 @@ variables (σ K) [field K]
 lemma quotient_mk_comp_C_injective (I : ideal (mv_polynomial σ K)) (hI : I ≠ ⊤) :
   function.injective ((ideal.quotient.mk I).comp mv_polynomial.C) :=
 begin
-  refine (ring_hom.injective_iff _).2 (λ x hx, _),
+  refine (injective_iff_map_eq_zero _).2 (λ x hx, _),
   rw [ring_hom.comp_apply, ideal.quotient.eq_zero_iff_mem] at hx,
   refine classical.by_contradiction (λ hx0, absurd (I.eq_top_iff_one.2 _) hI),
   have := I.mul_mem_left (mv_polynomial.C x⁻¹) hx,

src/field_theory/polynomial_galois_group.lean

@@ -199,7 +199,7 @@ restrict_smul ϕ x
 lemma gal_action_hom_injective [fact (p.splits (algebra_map F E))] :
   function.injective (gal_action_hom p E) :=
 begin
-  rw monoid_hom.injective_iff,
+  rw injective_iff_map_eq_one,
   intros ϕ hϕ,
   ext x hx,
   have key := equiv.perm.ext_iff.mp hϕ (roots_equiv_roots p E ⟨x, hx⟩),

src/field_theory/ratfunc.lean

@@ -751,7 +751,7 @@ end
 
 @[simp] lemma algebra_map_eq_zero_iff {x : K[X]} :
   algebra_map K[X] (ratfunc K) x = 0 ↔ x = 0 :=
-⟨(ring_hom.injective_iff _).mp (algebra_map_injective K) _, λ hx, by rw [hx, ring_hom.map_zero]⟩
+⟨(injective_iff_map_eq_zero _).mp (algebra_map_injective K) _, λ hx, by rw [hx, ring_hom.map_zero]⟩
 
 variables {K}
 

src/field_theory/splitting_field.lean

@@ -68,7 +68,7 @@ f = 0 ∨ ∀ {g : L[X]}, irreducible g → g ∣ f.map i → degree g = 1
 @[simp] lemma splits_C (a : K) : splits i (C a) :=
 if ha : a = 0 then ha.symm ▸ (@C_0 K _).symm ▸ splits_zero i
 else
-have hia : i a ≠ 0, from mt ((i.injective_iff).1
+have hia : i a ≠ 0, from mt ((injective_iff_map_eq_zero i).1
   i.injective _) ha,
 or.inr $ λ g hg ⟨p, hp⟩, absurd hg.1 (not_not.2 (is_unit_iff_degree_eq_zero.2 $
   by have := congr_arg degree hp;
@@ -546,7 +546,7 @@ alg_equiv.symm $ alg_equiv.of_bijective
     (λ p, adjoin_root.induction_on _ p $ λ p,
       (algebra.adjoin_singleton_eq_range_aeval F x).symm ▸
         (polynomial.aeval _).mem_range.mpr ⟨p, rfl⟩))
-  ⟨(alg_hom.injective_cod_restrict _ _ _).2 $ (alg_hom.injective_iff _).2 $ λ p,
+  ⟨(alg_hom.injective_cod_restrict _ _ _).2 $ (injective_iff_map_eq_zero _).2 $ λ p,
     adjoin_root.induction_on _ p $ λ p hp, ideal.quotient.eq_zero_iff_mem.2 $
     ideal.mem_span_singleton.2 $ minpoly.dvd F x hp,
   λ y,

src/group_theory/free_product.lean

@@ -688,7 +688,7 @@ theorem lift_injective_of_ping_pong:
   function.injective (lift f) :=
 begin
   classical,
-  apply (monoid_hom.injective_iff (lift f)).mpr,
+  apply (injective_iff_map_eq_one (lift f)).mpr,
   rw free_product.word.equiv.forall_congr_left',
   { intros w Heq,
     dsimp [word.equiv] at *,

src/group_theory/perm/basic.lean

@@ -203,12 +203,12 @@ extend_domain_trans _ _ _
   map_mul' := λ e e', (extend_domain_mul f e e').symm }
 
 lemma extend_domain_hom_injective : function.injective (extend_domain_hom f) :=
-((extend_domain_hom f).injective_iff).mpr (λ e he, ext (λ x, f.injective (subtype.ext
+(injective_iff_map_eq_one (extend_domain_hom f)).mpr (λ e he, ext (λ x, f.injective (subtype.ext
   ((extend_domain_apply_image e f x).symm.trans (ext_iff.mp he (f x))))))
 
 @[simp] lemma extend_domain_eq_one_iff {e : perm α} {f : α ≃ subtype p} :
   e.extend_domain f = 1 ↔ e = 1 :=
-(extend_domain_hom f).injective_iff'.mp (extend_domain_hom_injective f) e
+(injective_iff_map_eq_one' (extend_domain_hom f)).mp (extend_domain_hom_injective f) e
 
 end extend_domain
 

src/linear_algebra/linear_independent.lean

@@ -438,7 +438,8 @@ variables {a b : R} {x y : M}
 
 theorem linear_independent_iff_injective_total : linear_independent R v ↔
   function.injective (finsupp.total ι M R v) :=
-linear_independent_iff.trans (finsupp.total ι M R v).to_add_monoid_hom.injective_iff.symm
+linear_independent_iff.trans
+  (injective_iff_map_eq_zero (finsupp.total ι M R v).to_add_monoid_hom).symm
 
 alias linear_independent_iff_injective_total ↔ linear_independent.injective_total _
 

src/linear_algebra/matrix/charpoly/coeff.lean

@@ -259,7 +259,7 @@ lemma charpoly_left_mul_matrix {K S : Type*} [field K] [comm_ring S] [algebra K
 begin
   apply minpoly.unique,
   { apply matrix.charpoly_monic },
-  { apply (left_mul_matrix _).injective_iff.mp (left_mul_matrix_injective h.basis),
+  { apply (injective_iff_map_eq_zero (left_mul_matrix _)).mp (left_mul_matrix_injective h.basis),
     rw [← polynomial.aeval_alg_hom_apply, aeval_self_charpoly] },
   { intros q q_monic root_q,
     rw [matrix.charpoly_degree_eq_dim, fintype.card_fin, degree_eq_nat_degree q_monic.ne_zero],

src/number_theory/class_number/finite.lean

@@ -62,7 +62,8 @@ begin
   { by_contra' h,
     obtain ⟨i⟩ := bS.index_nonempty,
     apply bS.ne_zero i,
-    apply (algebra.left_mul_matrix bS).injective_iff.mp (algebra.left_mul_matrix_injective bS),
+    apply (injective_iff_map_eq_zero (algebra.left_mul_matrix bS)).mp
+      (algebra.left_mul_matrix_injective bS),
     ext j k,
     simp [h, dmatrix.zero_apply] },
   simp only [norm_bound, algebra.smul_def, eq_nat_cast, int.nat_cast_eq_coe_nat],
@@ -278,7 +279,7 @@ end real
 
 lemma prod_finset_approx_ne_zero : algebra_map R S (∏ m in finset_approx bS adm, m) ≠ 0 :=
 begin
-  refine mt ((ring_hom.injective_iff _).mp bS.algebra_map_injective _) _,
+  refine mt ((injective_iff_map_eq_zero _).mp bS.algebra_map_injective _) _,
   simp only [finset.prod_eq_zero_iff, not_exists],
   rintros x hx rfl,
   exact finset_approx.zero_not_mem bS adm hx

src/number_theory/function_field.lean

@@ -114,10 +114,10 @@ begin
   { rw is_scalar_tower.algebra_map_eq Fq[X] (ratfunc Fq) F,
     exact function.injective.comp ((algebra_map (ratfunc Fq) F).injective)
       (is_fraction_ring.injective Fq[X] (ratfunc Fq)), },
-  rw (algebra_map Fq[X] ↥(ring_of_integers Fq F)).injective_iff,
+  rw injective_iff_map_eq_zero (algebra_map Fq[X] ↥(ring_of_integers Fq F)),
   intros p hp,
   rw [← subtype.coe_inj, subalgebra.coe_zero] at hp,
-  rw (algebra_map Fq[X] F).injective_iff at hinj,
+  rw injective_iff_map_eq_zero (algebra_map Fq[X] F) at hinj,
   exact hinj p hp,
 end
 

src/number_theory/zsqrtd/basic.lean

@@ -757,7 +757,7 @@ def lift {d : ℤ} : {r : R // r * r = ↑d} ≃ (ℤ√d →+* R) :=
 `ℤ` into `R` is injective). -/
 lemma lift_injective [char_zero R] {d : ℤ} (r : {r : R // r * r = ↑d}) (hd : ∀ n : ℤ, d ≠ n*n) :
   function.injective (lift r) :=
-(lift r).injective_iff.mpr $ λ a ha,
+(injective_iff_map_eq_zero (lift r)).mpr $ λ a ha,
 begin
   have h_inj : function.injective (coe : ℤ → R) := int.cast_injective,
   suffices : lift r a.norm = 0,