α : 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 ≠ i → rank self i < rank self self.arr[i].parent
α : Type u_1
self : UnionFind α
i : ℕ
h : i < Array.size self.arr
⊢ self.arr[i].parent ≠ i → rank self i < rank self self.arr[i].parent
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 ≠ i → rank self i < rank self self.arr[i].parent
simpa [hm.parent_eq, hm.rank_eq, rank, size, h, (m.parent ⟨i, h⟩).2] using m.rank_lt ⟨i, h⟩