Find Collision sound

theorem findCollision_sound (h : α → α → α) {s : Skeleton} (idx : SkeletonLeafIndex s)    (proof₁ proof₂ : List.Vector α idx.depth) (x y l₁ r₁ l₂ r₂ : α)    (hfind : findCollision h idx proof₁ proof₂ x y = some (l₁, r₁, l₂, r₂)) :    Collision h l₁ r₁ l₂ r₂ := by  induction idx generalizing x y l₁ r₁ l₂ r₂ with  | ofLeaf =>      simp [findCollision] at hfind  | ofLeft idxLeft ih =>      -- Unfold findCollision so the `if` conditions become visible to `simp`.      simp only [findCollision] at hfind      by_cases hpair : (getPutativeRootWithHash idxLeft x proof₁.tail h, proof₁.head) =                       (getPutativeRootWithHash idxLeft y proof₂.tail h, proof₂.head)      · simp only [hpair] at hfind        exact ih proof₁.tail proof₂.tail x y l₁ r₁ l₂ r₂ hfind      · simp only [hpair] at hfind        by_cases heqhash : h (getPutativeRootWithHash idxLeft x proof₁.tail h) proof₁.head =                          h (getPutativeRootWithHash idxLeft y proof₂.tail h) proof₂.head        · simp_all [Collision]        · simp [heqhash] at hfind  | ofRight idxRight ih =>      simp only [findCollision] at hfind      by_cases hpair : (proof₁.head, getPutativeRootWithHash idxRight x proof₁.tail h) =                       (proof₂.head, getPutativeRootWithHash idxRight y proof₂.tail h)      · simp only [hpair] at hfind        exact ih proof₁.tail proof₂.tail x y l₁ r₁ l₂ r₂ hfind      · simp only [hpair] at hfind        by_cases heqhash : h proof₁.head (getPutativeRootWithHash idxRight x proof₁.tail h) =                          h proof₂.head (getPutativeRootWithHash idxRight y proof₂.tail h)        · simp_all [Collision]        · simp [heqhash] at hfind