feat(data/nat/cast): pi.coe_nat and pi.nat_apply (#7492)

Author: jcommelin

src/data/int/cast.lean

@@ -270,3 +270,19 @@ end ring_hom
 
 @[simp, norm_cast] theorem int.cast_id (n : ℤ) : ↑n = n :=
 ((ring_hom.id ℤ).eq_int_cast n).symm
+
+namespace pi
+
+variables {α β : Type*}
+
+lemma int_apply [has_zero β] [has_one β] [has_add β] [has_neg β] :
+  ∀ (n : ℤ) (a : α), (n : α → β) a = n
+| (n:ℕ)  a := pi.nat_apply n a
+| -[1+n] a :=
+by rw [cast_neg_succ_of_nat, cast_neg_succ_of_nat, neg_apply, add_apply, one_apply, nat_apply]
+
+@[simp] lemma coe_int [has_zero β] [has_one β] [has_add β] [has_neg β] (n : ℤ) :
+  (n : α → β) = λ _, n :=
+by { ext, rw pi.int_apply }
+
+end pi

src/data/nat/cast.lean

@@ -321,3 +321,18 @@ begin
 end
 
 end with_top
+
+namespace pi
+
+variables {α β : Type*}
+
+lemma nat_apply [has_zero β] [has_one β] [has_add β] :
+  ∀ (n : ℕ) (a : α), (n : α → β) a = n
+| 0     a := rfl
+| (n+1) a := by rw [nat.cast_succ, nat.cast_succ, add_apply, nat_apply, one_apply]
+
+@[simp] lemma coe_nat [has_zero β] [has_one β] [has_add β] (n : ℕ) :
+  (n : α → β) = λ _, n :=
+by { ext, rw pi.nat_apply }
+
+end pi