Theorem: Lean4Lean.UnionFind.parent_link (Lean4Lean/Verify/UnionFind.lean)

State before:
self : UnionFind
x y : Fin (size self)
yroot : parent self ↑y = ↑y
i : Nat
⊢ parent (link self x y yroot) i =
    if ↑x = ↑y then parent self i
    else
      if rank self ↑y < rank self ↑x then if ↑y = i then ↑x else parent self i else if ↑x = i then ↑y else parent self i
Tactic:
simp [rankD_eq]
State after:
self : UnionFind
x y : Fin (size self)
yroot : parent self ↑y = ↑y
i : Nat
⊢ parent (link self x y yroot) i =
    if ↑x = ↑y then parent self i
    else
      if (Array.get self.arr y).rank < (Array.get self.arr x).rank then if ↑y = i then ↑x else parent self i
      else if ↑x = i then ↑y else parent self i

State before:
self : UnionFind
x y : Fin (size self)
yroot : parent self ↑y = ↑y
i : Nat
⊢ parent (link self x y yroot) i =
    if ↑x = ↑y then parent self i
    else
      if (Array.get self.arr y).rank < (Array.get self.arr x).rank then if ↑y = i then ↑x else parent self i
      else if ↑x = i then ↑y else parent self i
Tactic:
exact parentD_linkAux
State after:
no goals