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

State before:
a b : Nat
self : UnionFind
x : Fin (size self)
⊢ Equiv (find self x).fst a b ↔ Equiv self a b
Tactic:
simp [Equiv, find_root_1]
State after:
no goals