feat(Combinatorics/SimpleGraph/Connectivity): a graph is either connected or its complement is

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean

@@ -296,6 +296,23 @@ theorem Iso.connected_iff {G : SimpleGraph V} {H : SimpleGraph V'} (e : G ≃g H
     G.Connected ↔ H.Connected :=
   ⟨Connected.map e.toHom e.toEquiv.surjective, Connected.map e.symm.toHom e.symm.toEquiv.surjective⟩
 
+theorem connected_or_compl_connected [Nonempty V] : G.Connected ∨ Gᶜ.Connected := by
+  have ⟨v₀⟩ := ‹Nonempty V›
+  by_cases hreach₀ : ∀ v, G.Reachable v₀ v
+  · exact Or.inl <| G.connected_iff_exists_forall_reachable.mpr ⟨v₀, hreach₀⟩
+  refine Or.inr <| Gᶜ.connected_iff_exists_forall_reachable.mpr ⟨v₀, fun v ↦ ?_⟩
+  have ⟨v₁, hreach₁⟩ := not_forall.mp hreach₀
+  have hcadj₁ : Gᶜ.Adj v₀ v₁ :=
+    ⟨fun heq ↦ heq ▸ hreach₁ <| Reachable.refl _, mt Adj.reachable hreach₁⟩
+  by_cases hreach : G.Reachable v₀ v
+  · by_cases heq : v = v₁
+    · exact heq ▸ Adj.reachable hcadj₁
+    have : Gᶜ.Adj v v₁ := ⟨heq, fun hadj ↦ hreach₁ <| hreach.trans hadj.reachable⟩
+    exact hcadj₁.reachable.trans this.reachable.symm
+  by_cases heq : v₀ = v
+  · exact heq ▸ Reachable.refl _
+  exact Adj.reachable ⟨heq, mt Adj.reachable hreach⟩
+
 /-- The quotient of `V` by the `SimpleGraph.Reachable` relation gives the connected
 components of a graph. -/
 def ConnectedComponent := Quot G.Reachable