α : Type u_1
self : UnionFind α
i : ℕ
h : i < Array.size self.arr
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
⊢ self.arr[i].parent < size self
α : Type u_1
self : UnionFind α
i : ℕ
h : i < Array.size self.arr
⊢ self.arr[i].parent < size self
let ⟨m, hm⟩ := self.model'
no goals
α : Type u_1
self : UnionFind α
i : ℕ
h : i < Array.size self.arr
m : UFModel (Array.size self.arr)
hm : UFModel.Models self.arr m
⊢ self.arr[i].parent < size self
simp [hm.parent_eq, size, (m.parent ⟨i, h⟩).2, h]