chore(data/{nat,int,rat}/cast): add bundled version of cast_id lemm…

…as (#13001)

src/data/int/cast.lean

@@ -238,6 +238,9 @@ ext_iff.1 (f.eq_int_cast_hom h1)
 
 end add_monoid_hom
 
+@[simp] lemma int.cast_add_hom_int : int.cast_add_hom ℤ = add_monoid_hom.id ℤ :=
+((add_monoid_hom.id ℤ).eq_int_cast_hom rfl).symm
+
 namespace monoid_hom
 variables {M : Type*} [monoid M]
 open multiplicative
@@ -303,6 +306,9 @@ end ring_hom
 @[simp, norm_cast] theorem int.cast_id (n : ℤ) : ↑n = n :=
 ((ring_hom.id ℤ).eq_int_cast n).symm
 
+@[simp] lemma int.cast_ring_hom_int : int.cast_ring_hom ℤ = ring_hom.id ℤ :=
+(ring_hom.id ℤ).eq_int_cast'.symm
+
 namespace pi
 
 variables {α β : Type*}

src/data/nat/cast.lean

@@ -323,17 +323,28 @@ ext_nat' f g $ by simp only [map_one]
 
 end ring_hom_class
 
+namespace ring_hom
+
+/-- This is primed to match `ring_hom.eq_int_cast'`. -/
+lemma eq_nat_cast' {R} [non_assoc_semiring R] (f : ℕ →+* R) : f = nat.cast_ring_hom R :=
+ring_hom.ext $ eq_nat_cast f
+
+end ring_hom
+
 @[simp, norm_cast] theorem nat.cast_id (n : ℕ) : ↑n = n :=
 (eq_nat_cast (ring_hom.id ℕ) n).symm
 
+@[simp] lemma nat.cast_ring_hom_nat : nat.cast_ring_hom ℕ = ring_hom.id ℕ :=
+((ring_hom.id ℕ).eq_nat_cast').symm
+
 @[simp] theorem nat.cast_with_bot : ∀ (n : ℕ),
   @coe ℕ (with_bot ℕ) (@coe_to_lift _ _ nat.cast_coe) n = n
 | 0     := rfl
 | (n+1) := by rw [with_bot.coe_add, nat.cast_add, nat.cast_with_bot n]; refl
 
 -- I don't think `ring_hom_class` is good here, because of the `subsingleton` TC slowness
-instance nat.subsingleton_ring_hom {R : Type*} [non_assoc_semiring R] : subsingleton (ℕ →+* R) :=
-⟨ext_nat⟩
+instance nat.unique_ring_hom {R : Type*} [non_assoc_semiring R] : unique (ℕ →+* R) :=
+{ default := nat.cast_ring_hom R, uniq := ring_hom.eq_nat_cast' }
 
 namespace mul_opposite
 

src/data/rat/cast.lean

@@ -245,6 +245,9 @@ by rw [← cast_zero, cast_lt]
 @[simp, norm_cast] theorem cast_id : ∀ n : ℚ, ↑n = n
 | ⟨n, d, h, c⟩ := by rw [num_denom', cast_mk, mk_eq_div]
 
+@[simp] lemma cast_hom_rat : cast_hom ℚ = ring_hom.id ℚ :=
+ring_hom.ext cast_id
+
 @[simp, norm_cast] theorem cast_min [linear_ordered_field α] {a b : ℚ} :
   (↑(min a b) : α) = min a b :=
 by by_cases a ≤ b; simp [h, min_def]