feat(Combinatorics/SimpleGraph/Hamiltonian): p.getVert is surjective

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

@@ -74,6 +74,13 @@ end
 theorem isHamiltonian_iff_support_get_bijective : p.IsHamiltonian ↔ (p.support.get ·).Bijective :=
   p.support.get_bijective_iff.symm
 
+theorem IsHamiltonian.getVert_surjective (hp : p.IsHamiltonian) : (p.getVert ·).Surjective := by
+  intro v
+  have ⟨n, h⟩ := List.mem_iff_get.mp <| p.support.one_le_count_iff.mp <| le_of_eq <| hp v |>.symm
+  refine ⟨n, p.getVert_eq_support_getElem ?_ |>.trans h⟩
+  have := p.length_support
+  cutsat
+
 /-- A Hamiltonian cycle is a cycle that visits every vertex once. -/
 structure IsHamiltonianCycle (p : G.Walk a a) : Prop extends p.IsCycle where
   isHamiltonian_tail : p.tail.IsHamiltonian