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

State before:
arr : Array UFNode
x y : Fin (Array.size arr)
h : (Array.get arr x).rank < (Array.get arr y).rank
i : Nat
rankD_lt : parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i)
⊢ ∀ {i : Nat},
    rankD (Array.set arr x { parent := ↑y, rank := (Array.get arr x).rank }) i =
      if ↑y = i ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1 else rankD arr i
Tactic:
simp [rankD_set, Nat.ne_of_lt h, rankD_eq]
State after:
no goals