style(Combinatorics/SimpleGraph/Copy): more proof style improvements

- mapNeighborSet.inj': rw [Subtype.mk_eq_mk] at h ⊢ → Subtype.ext + congrArg
- comp: use/rw/exact tactic proof → term mode with simpa [Hom.coe_comp]

Author: FordUniver

Mathlib/Combinatorics/SimpleGraph/Copy.lean

@@ -121,9 +121,7 @@ def mapEdgeSet (f : Copy A B) : A.edgeSet ↪ B.edgeSet where
 def mapNeighborSet (f : Copy A B) (a : α) :
     A.neighborSet a ↪ B.neighborSet (f a) where
   toFun v := ⟨f v, f.toHom.apply_mem_neighborSet v.prop⟩
-  inj' _ _ h := by
-    rw [Subtype.mk_eq_mk] at h ⊢
-    exact f.injective h
+  inj' _ _ h := Subtype.ext (f.injective (congrArg Subtype.val h))
 
 /-- A copy gives rise to an embedding of vertex types. -/
 @[expose] def toEmbedding (f : Copy A B) : α ↪ β := ⟨f, f.injective⟩
@@ -136,10 +134,8 @@ def mapNeighborSet (f : Copy A B) (a : α) :
 @[simp, norm_cast] lemma coe_id : ⇑(id G) = _root_.id := rfl
 
 /-- The composition of copies is a copy. -/
-def comp (g : Copy B C) (f : Copy A B) : Copy A C := by
-  use g.toHom.comp f.toHom
-  rw [Hom.coe_comp]
-  exact g.injective.comp f.injective
+def comp (g : Copy B C) (f : Copy A B) : Copy A C :=
+  ⟨g.toHom.comp f.toHom, by simpa [Hom.coe_comp] using g.injective.comp f.injective⟩
 
 @[simp]
 theorem comp_apply (g : Copy B C) (f : Copy A B) (a : α) : g.comp f a = g (f a) :=