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

State before:
self : UnionFind
x : Nat
⊢ parent self (root self x) = root self x
Tactic:
rw [root]
State after:
self : UnionFind
x : Nat
⊢ parent self (if h : x < size self then ↑(root' self { val := x, isLt := h }) else x) =
    if h : x < size self then ↑(root' self { val := x, isLt := h }) else x

State before:
self : UnionFind
x : Nat
⊢ parent self (if h : x < size self then ↑(root' self { val := x, isLt := h }) else x) =
    if h : x < size self then ↑(root' self { val := x, isLt := h }) else x
Tactic:
split <;> [simp [parentD, parent'_root']; simp [parentD_of_not_lt, *]]
State after:
no goals