feat(data/nat/cast): generalize to fun_like (#11128)

Author: ericrbg

archive/100-theorems-list/16_abel_ruffini.lean

@@ -41,7 +41,7 @@ by simp [Φ]
 by simp [Φ, coeff_X_pow]
 
 @[simp] lemma coeff_five_Phi : (Φ R a b).coeff 5 = 1 :=
-by simp [Φ, coeff_X, coeff_C, -C_eq_nat_cast, -ring_hom.map_nat_cast]
+by simp [Φ, coeff_X, coeff_C, -C_eq_nat_cast, -map_nat_cast]
 
 variables [nontrivial R]
 

src/algebra/algebra/basic.lean

@@ -582,9 +582,6 @@ lemma map_finsupp_sum {α : Type*} [has_zero α] {ι : Type*} (f : ι →₀ α)
   φ (f.sum g) = f.sum (λ i a, φ (g i a)) :=
 φ.map_sum _ _
 
-@[simp] lemma map_nat_cast (n : ℕ) : φ n = n :=
-φ.to_ring_hom.map_nat_cast n
-
 lemma map_bit0 (x) : φ (bit0 x) = bit0 (φ x) := map_bit0 _ _
 lemma map_bit1 (x) : φ (bit1 x) = bit1 (φ x) := map_bit1 _ _
 

src/algebra/char_p/basic.lean

@@ -216,7 +216,7 @@ lemma ring_hom.char_p_iff_char_p {K L : Type*} [division_ring K] [semiring L] [n
 begin
   split;
   { introI _c, constructor, intro n,
-    rw [← @char_p.cast_eq_zero_iff _ _ _ p _c n, ← f.injective.eq_iff, f.map_nat_cast, f.map_zero] }
+    rw [← @char_p.cast_eq_zero_iff _ _ _ p _c n, ← f.injective.eq_iff, map_nat_cast f, f.map_zero] }
 end
 
 section frobenius
@@ -278,7 +278,7 @@ theorem frobenius_zero : frobenius R p 0 = 0 := (frobenius R p).map_zero
 theorem frobenius_add : frobenius R p (x + y) = frobenius R p x + frobenius R p y :=
 (frobenius R p).map_add x y
 
-theorem frobenius_nat_cast (n : ℕ) : frobenius R p n = n := (frobenius R p).map_nat_cast n
+theorem frobenius_nat_cast (n : ℕ) : frobenius R p n = n := map_nat_cast (frobenius R p) n
 
 open_locale big_operators
 variables {R}

src/algebra/char_p/pi.lean

@@ -19,8 +19,8 @@ instance pi (ι : Type u) [hi : nonempty ι] (R : Type v) [semiring R] (p : ℕ)
   char_p (ι → R) p :=
 ⟨λ x, let ⟨i⟩ := hi in iff.symm $ (char_p.cast_eq_zero_iff R p x).symm.trans
 ⟨λ h, funext $ λ j, show pi.eval_ring_hom (λ _, R) j (↑x : ι → R) = 0,
-    by rw [ring_hom.map_nat_cast, h],
-  λ h, (pi.eval_ring_hom (λ _: ι, R) i).map_nat_cast x ▸ by rw [h, ring_hom.map_zero]⟩⟩
+    by rw [map_nat_cast, h],
+  λ h, map_nat_cast (pi.eval_ring_hom (λ _: ι, R) i) x ▸ by rw [h, ring_hom.map_zero]⟩⟩
 
 -- diamonds
 instance pi' (ι : Type u) [hi : nonempty ι] (R : Type v) [comm_ring R] (p : ℕ) [char_p R p] :

src/algebra/char_p/quotient.lean

@@ -18,7 +18,7 @@ namespace char_p
 theorem quotient (R : Type u) [comm_ring R] (p : ℕ) [hp1 : fact p.prime] (hp2 : ↑p ∈ nonunits R) :
   char_p (R ⧸ (ideal.span {p} : ideal R)) p :=
 have hp0 : (p : R ⧸ (ideal.span {p} : ideal R)) = 0,
-  from (ideal.quotient.mk (ideal.span {p} : ideal R)).map_nat_cast p ▸
+  from map_nat_cast (ideal.quotient.mk (ideal.span {p} : ideal R)) p ▸
     ideal.quotient.eq_zero_iff_mem.2 (ideal.subset_span $ set.mem_singleton _),
 ring_char.of_eq $ or.resolve_left ((nat.dvd_prime hp1.1).1 $ ring_char.dvd hp0) $ λ h1,
 hp2 $ is_unit_iff_dvd_one.2 $ ideal.mem_span_singleton.1 $ ideal.quotient.eq_zero_iff_mem.1 $
@@ -30,7 +30,7 @@ lemma quotient' {R : Type*} [comm_ring R] (p : ℕ) [char_p R p] (I : ideal R)
   (h : ∀ x : ℕ, (x : R) ∈ I → (x : R) = 0) :
   char_p (R ⧸ I) p :=
 ⟨λ x, begin
-  rw [←cast_eq_zero_iff R p x, ←(ideal.quotient.mk I).map_nat_cast],
+  rw [←cast_eq_zero_iff R p x, ←map_nat_cast (ideal.quotient.mk I)],
   refine quotient.eq'.trans (_ : ↑x - 0 ∈ I ↔ _),
   rw sub_zero,
   exact ⟨h x, λ h', h'.symm ▸ I.zero_mem⟩,

src/algebra/char_p/subring.lean

@@ -18,14 +18,14 @@ namespace char_p
 instance subsemiring (R : Type u) [semiring R] (p : ℕ) [char_p R p] (S : subsemiring R) :
   char_p S p :=
 ⟨λ x, iff.symm $ (char_p.cast_eq_zero_iff R p x).symm.trans
-⟨λ h, subtype.eq $ show S.subtype x = 0, by rw [ring_hom.map_nat_cast, h],
-  λ h, S.subtype.map_nat_cast x ▸ by rw [h, ring_hom.map_zero]⟩⟩
+⟨λ h, subtype.eq $ show S.subtype x = 0, by rw [map_nat_cast, h],
+  λ h, map_nat_cast S.subtype x ▸ by rw [h, ring_hom.map_zero]⟩⟩
 
 instance subring (R : Type u) [ring R] (p : ℕ) [char_p R p] (S : subring R) :
   char_p S p :=
 ⟨λ x, iff.symm $ (char_p.cast_eq_zero_iff R p x).symm.trans
-⟨λ h, subtype.eq $ show S.subtype x = 0, by rw [ring_hom.map_nat_cast, h],
-  λ h, S.subtype.map_nat_cast x ▸ by rw [h, ring_hom.map_zero]⟩⟩
+⟨λ h, subtype.eq $ show S.subtype x = 0, by rw [map_nat_cast, h],
+  λ h, map_nat_cast S.subtype x ▸ by rw [h, ring_hom.map_zero]⟩⟩
 
 instance subring' (R : Type u) [comm_ring R] (p : ℕ) [char_p R p] (S : subring R) :
   char_p S p :=

src/algebra/char_zero.lean

@@ -200,11 +200,11 @@ section ring_hom
 variables {R S : Type*} [semiring R] [semiring S]
 
 lemma ring_hom.char_zero (ϕ : R →+* S) [hS : char_zero S] : char_zero R :=
-⟨λ a b h, char_zero.cast_injective (by rw [←ϕ.map_nat_cast, ←ϕ.map_nat_cast, h])⟩
+⟨λ a b h, char_zero.cast_injective (by rw [←map_nat_cast ϕ, ←map_nat_cast ϕ, h])⟩
 
 lemma ring_hom.char_zero_iff {ϕ : R →+* S} (hϕ : function.injective ϕ) :
   char_zero R ↔ char_zero S :=
-⟨λ hR, ⟨λ a b h, by rwa [←@nat.cast_inj R _ _ hR, ←hϕ.eq_iff, ϕ.map_nat_cast, ϕ.map_nat_cast]⟩,
+⟨λ hR, ⟨λ a b h, by rwa [←@nat.cast_inj R _ _ hR, ←hϕ.eq_iff, map_nat_cast ϕ, map_nat_cast ϕ]⟩,
   λ hS, by exactI ϕ.char_zero⟩
 
 end ring_hom

src/algebra/group_power/lemmas.lean

@@ -24,9 +24,12 @@ section monoid
 variables [monoid M] [monoid N] [add_monoid A] [add_monoid B]
 
 @[simp] theorem nsmul_one [has_one A] : ∀ n : ℕ, n • (1 : A) = n :=
-add_monoid_hom.eq_nat_cast
-  ⟨λ n, n • (1 : A), zero_nsmul _, λ _ _, add_nsmul _ _ _⟩
-  (one_nsmul _)
+begin
+  refine eq_nat_cast' (⟨_, _, _⟩ : ℕ →+ A) _,
+  { simp [zero_nsmul] },
+  { simp [add_nsmul] },
+  { simp }
+end
 
 @[simp, norm_cast, to_additive]
 lemma units.coe_pow (u : Mˣ) (n : ℕ) : ((u ^ n : Mˣ) : M) = u ^ n :=

src/algebra/ne_zero.lean

@@ -50,12 +50,12 @@ instance char_zero [ne_zero n] [add_monoid M] [has_one M] [char_zero M] : ne_zer
 lemma of_map [has_zero R] [has_zero M] [zero_hom_class F R M] (f : F) [ne_zero (f r)] :
   ne_zero r := ⟨λ h, ne (f r) $ by convert map_zero f⟩
 
-lemma of_injective' {r : R} [has_zero R] [h : ne_zero r] [has_zero M] [zero_hom_class F R M]
+lemma of_injective {r : R} [has_zero R] [h : ne_zero r] [has_zero M] [zero_hom_class F R M]
   {f : F} (hf : function.injective f) : ne_zero (f r) :=
 ⟨by { rw ←map_zero f, exact hf.ne (ne r) }⟩
 
-lemma of_injective [non_assoc_semiring M] [non_assoc_semiring R] [h : ne_zero (n : R)]
-  {f : R →+* M} (hf : function.injective f) : ne_zero (n : M) :=
+lemma nat_of_injective [non_assoc_semiring M] [non_assoc_semiring R] [h : ne_zero (n : R)]
+  [ring_hom_class F R M] {f : F} (hf : function.injective f) : ne_zero (n : M) :=
  ⟨λ h, (ne_zero.ne' n R) $ hf $ by simpa⟩
 
 variables (R M)
@@ -65,7 +65,7 @@ lemma of_not_dvd [add_monoid M] [has_one M] [char_p M p] (h : ¬ p ∣ n) : ne_z
 
 lemma of_no_zero_smul_divisors [comm_ring R] [ne_zero (n : R)] [ring M] [nontrivial M]
   [algebra R M] [no_zero_smul_divisors R M] : ne_zero (n : M) :=
-of_injective $ no_zero_smul_divisors.algebra_map_injective R M
+nat_of_injective $ no_zero_smul_divisors.algebra_map_injective R M
 
 lemma of_ne_zero_coe [has_zero R] [has_one R] [has_add R] [h : ne_zero (n : R)] : ne_zero n :=
 ⟨by {casesI h, rintro rfl, contradiction}⟩

src/data/complex/basic.lean

@@ -363,7 +363,7 @@ norm_sq.map_div z w
 /-! ### Cast lemmas -/
 
 @[simp, norm_cast] theorem of_real_nat_cast (n : ℕ) : ((n : ℝ) : ℂ) = n :=
-of_real.map_nat_cast n
+map_nat_cast of_real n
 
 @[simp, norm_cast] lemma nat_cast_re (n : ℕ) : (n : ℂ).re = n :=
 by rw [← of_real_nat_cast, of_real_re]