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

State before:
self : UnionFind
i : Nat
⊢ rankD self.arr i < rankMax self
Tactic:
simp [rankD]
State after:
self : UnionFind
i : Nat
⊢ (if h : i < Array.size self.arr then (Array.get self.arr { val := i, isLt := h }).rank else 0) < rankMax self

State before:
self : UnionFind
i : Nat
⊢ (if h : i < Array.size self.arr then (Array.get self.arr { val := i, isLt := h }).rank else 0) < rankMax self
Tactic:
split <;> [apply rank'_lt_rankMax; apply Nat.succ_pos]
State after:
no goals