Theorem: Lean4Lean.UnionFind.rank_lt (Lean4Lean/UnionFind.lean)

State before:
self : UnionFind
i : Nat
⊢ parent self i ≠ i → rank self i < rank self (parent self i)
Tactic:
simpa [rank] using self.rankD_lt
State after:
no goals