feat(SimpleGraph): the cycle graph and complete graph are Hamiltonian

Mathlib/Combinatorics/SimpleGraph/Copy.lean

@@ -296,6 +296,11 @@ theorem isContained_iff_exists_iso_subgraph :
   mp := fun ⟨f⟩ ↦ ⟨.map f.toHom ⊤, ⟨f.isoToSubgraph⟩⟩
   mpr := fun ⟨B', ⟨e⟩⟩ ↦ B'.coe_isContained.trans' ⟨e.toCopy⟩
 
+theorem isContained_completeGraph_of_card_le_card [Fintype V] [Fintype W]
+    (h : Fintype.card V ≤ Fintype.card W) : G ⊑ completeGraph W := by
+  obtain ⟨f, hf⟩ := Function.Embedding.nonempty_of_card_le h
+  exact ⟨⟨f, by grind [top_adj, SimpleGraph.irrefl]⟩, hf⟩
+
 alias ⟨IsContained.exists_iso_subgraph, IsContained.of_exists_iso_subgraph⟩ :=
   isContained_iff_exists_iso_subgraph
 

Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.GroupWithZero.Nat
 public import Mathlib.Algebra.Order.Group.Nat
 public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
+public import Mathlib.Combinatorics.SimpleGraph.Circulant
 
 /-!
 # Hamiltonian Graphs
@@ -158,6 +159,10 @@ lemma IsHamiltonianCycle.support_count_of_ne (hp : p.IsHamiltonianCycle) (h : a
     p.support.count b = 1 := by
   rw [← cons_support_tail p hp.1.not_nil, List.count_cons_of_ne h, hp.isHamiltonian_tail]
 
+theorem cycleGraph_EulerianCircuit_isHamiltonianCycle {n : ℕ} :
+    (cycleGraph_EulerianCircuit n).IsHamiltonianCycle :=
+  isHamiltonianCycle_iff_isCycle_and_length_eq.mpr ⟨cycleGraph_EulerianCircuit_isCycle, by simp⟩
+
 end Walk
 
 variable [Fintype α]
@@ -189,6 +194,25 @@ lemma IsHamiltonian.of_card_eq_one (h : Fintype.card α = 1) : G.IsHamiltonian :
 lemma IsHamiltonian.of_unique [Unique α] : G.IsHamiltonian :=
   of_card_eq_one <| Fintype.card_unique
 
+theorem isHamiltonian_iff_cycleGraph_isContained (h : 2 < Fintype.card α) :
+    G.IsHamiltonian ↔ cycleGraph (Fintype.card α) ⊑ G := by
+  refine ⟨fun h' ↦ ?_, fun h' ↦ ?_⟩
+  · obtain ⟨a, p, hp⟩ := h' (by grind)
+    exact cycleGraph_isContained_iff h |>.mpr ⟨a, p, hp.isCycle, hp.length_eq⟩
+  · obtain ⟨a, p, hp₁, hp₂⟩ := cycleGraph_isContained_iff h |>.mp h'
+    exact fun _ ↦ ⟨a, p, Walk.isHamiltonianCycle_iff_isCycle_and_length_eq.mpr ⟨hp₁, hp₂⟩⟩
+
+@[simp]
+theorem isHamiltonian_cycleGraph (n : ℕ) (hn : 2 < n) : (cycleGraph n).IsHamiltonian := by
+  apply isHamiltonian_iff_cycleGraph_isContained (by simp [hn]) |>.mpr
+  rw [Fintype.card_fin]
+  exact IsContained.rfl
+
+@[simp]
+theorem isHamiltonian_top (h : 2 < Fintype.card α) : (completeGraph α).IsHamiltonian :=
+  isHamiltonian_iff_cycleGraph_isContained h |>.mpr <|
+    isContained_completeGraph_of_card_le_card (by simp)
+
 variable {V : Type*} [Fintype V] [DecidableEq V]
 
 /--