feat: missing results about StarAlgHom.codRestrict (#6668)

This is a step towards making sure that all the `codRestrict` APIs are similar, but they're still not similar enough in wether they take bundled subobjects/morphisms or subobject/morphism classes.

Mathlib/Algebra/Star/Subalgebra.lean

@@ -792,6 +792,20 @@ protected def codRestrict (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B) (hf :
   toAlgHom := AlgHom.codRestrict f.toAlgHom S.toSubalgebra hf
   map_star' := fun x => Subtype.ext (map_star f x)
 
+@[simp]
+theorem coe_codRestrict (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B) (hf : ∀ x, f x ∈ S) (x : A) :
+    ↑(f.codRestrict S hf x) = f x :=
+  rfl
+
+@[simp]
+theorem subtype_comp_codRestrict (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B)
+    (hf : ∀ x : A, f x ∈ S) : S.subtype.comp (f.codRestrict S hf) = f :=
+  StarAlgHom.ext <| coe_codRestrict _ S hf
+
+theorem injective_codRestrict (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B) (hf : ∀ x : A, f x ∈ S) :
+    Function.Injective (StarAlgHom.codRestrict f S hf) ↔ Function.Injective f :=
+  ⟨fun H _x _y hxy => H <| Subtype.eq hxy, fun H _x _y hxy => H (congr_arg Subtype.val hxy : _)⟩
+
 /-- Restriction of the codomain of a `StarAlgHom` to its range. -/
 def rangeRestrict (f : A →⋆ₐ[R] B) : A →⋆ₐ[R] f.range :=
   StarAlgHom.codRestrict f _ fun x => ⟨x, rfl⟩