no goals
α : Type u_1
arr : Array (UFNode α)
n : ℕ
m : UFModel n
hm : Models arr m
i j : Fin n
H : rank m ↑i < rank m ↑j
hi : ↑i < Array.size arr
x : UFNode α
hp : x.parent = ↑j
hrk : x.rank = arr[i].rank
k : Fin n
h : ↑k ≠ ↑i
⊢ ↑(parent (UFModel.setParent m i j H) k) = ↑(parent m k)
simp [UFModel.setParent, h.symm]
no goals
α : Type u_1
arr : Array (UFNode α)
n : ℕ
m : UFModel n
hm : Models arr m
i j : Fin n
H : rank m ↑i < rank m ↑j
hi : ↑i < Array.size arr
x : UFNode α
hp : x.parent = ↑j
hrk : x.rank = arr[i].rank
h : ↑{ val := ↑i, isLt := hi } < n
⊢ x.parent = ↑(parent (UFModel.setParent m i j H) { val := ↑{ val := ↑i, isLt := hi }, isLt := h })
simp [UFModel.setParent, hp]