feat(Combinatorics/SimpleGraph/Hamiltonian): golf getVertEquiv using grind

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

@@ -79,20 +79,14 @@ def IsHamiltonian.supportGetEquiv (hp : p.IsHamiltonian) : Fin p.support.length
 /-- If a path `p` is Hamiltonian, then `p.getVert` defines an equivalence between
 `Fin p.support.length` and `α`. -/
 def IsHamiltonian.getVertEquiv (hp : p.IsHamiltonian) : Fin p.support.length ≃ α where
-  toFun i := p.getVert i
-  invFun := IsHamiltonian.supportGetEquiv hp |>.invFun
+  toFun := p.getVert ∘ Fin.val
+  invFun := supportGetEquiv hp |>.invFun
   left_inv i := by
-    dsimp only
-    have := i.prop.trans_eq p.length_support
-    rw [getVert_eq_support_getElem _ <| by cutsat]
-    have := p.support.idxOf_getElem hp.isPath.support_nodup _ i.prop
-    simp [IsHamiltonian.supportGetEquiv, List.getEquivOfForallCountEqOne,
-      List.Nodup.getEquivOfForallMemList]
-    congr
-  right_inv a := by
-    have := hp.supportGetEquiv.symm a |>.prop
-    exact (getVert_eq_support_getElem _ <| Nat.le_of_lt_add_one <| this.trans_eq p.length_support)
-      |>.trans <| p.support.getElem_idxOf this
+    have := i.prop
+    grind [getVert_eq_support_getElem, supportGetEquiv, List.getEquivOfForallCountEqOne,
+      List.Nodup.getEquivOfForallMemList, Equiv.invFun_as_coe, List.idxOf_getElem, length_support]
+  right_inv a := (getVert_eq_support_getElem _ <| by grind [length_support]).trans <|
+      p.support.getElem_idxOf <| hp.supportGetEquiv.symm a |>.prop
 
 /-- A Hamiltonian cycle is a cycle that visits every vertex once. -/
 structure IsHamiltonianCycle (p : G.Walk a a) : Prop extends p.IsCycle where