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

State before:
self : UnionFind
x : Fin (size self)
⊢ parent (find self x).fst ↑x = root self ↑x
Tactic:
simp [find, parent]
State after:
self : UnionFind
x : Fin (size self)
⊢ parentD (findAux self x).s ↑x = root self ↑x

State before:
self : UnionFind
x : Fin (size self)
⊢ parentD (findAux self x).s ↑x = root self ↑x
Tactic:
rw [parentD_findAux, if_pos rfl]
State after:
no goals