Theorem: Lean4Lean.UnionFind.rank'_lt (Lean4Lean/UnionFind.lean)

State before:
self : UnionFind
i : Fin (size self)
⊢ (Array.get self.arr i).parent ≠ ↑i → rank self ↑i < rank self (Array.get self.arr i).parent
Tactic:
simpa [← parentD_eq] using self.rankD_lt
State after:
no goals