feat(Combinatorics/SimpleGraph/Connectivity/Connected): {Subsingleton, Unique, Nonempty} instances for ConnectedComponent (leanprover-community#30626)

feat(Combinatorics/SimpleGraph/Connectivity/Connected): add {`Subsingleton`, `Unique`, `Nonempty`} instances for `ConnectedComponent`

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean

@@ -332,10 +332,10 @@ namespace ConnectedComponent
 instance inhabited [Inhabited V] : Inhabited G.ConnectedComponent :=
   ⟨G.connectedComponentMk default⟩
 
-instance isEmpty [IsEmpty V] : IsEmpty (ConnectedComponent G) := by
-  by_contra! hc
-  obtain ⟨v, _⟩ := hc.some.exists_rep
-  exact IsEmpty.false v
+instance isEmpty [IsEmpty V] : IsEmpty G.ConnectedComponent := Quot.instIsEmpty
+instance [Subsingleton V] : Subsingleton G.ConnectedComponent := Quot.Subsingleton
+instance [Unique V] : Unique G.ConnectedComponent := Quot.instUnique
+instance [Nonempty V] : Nonempty G.ConnectedComponent := Nonempty.map G.connectedComponentMk ‹_›
 
 @[elab_as_elim]
 protected theorem ind {β : G.ConnectedComponent → Prop}