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

State before:
a : Nat
m : UnionFind
⊢ rank (push m) a = rank m a
Tactic:
simp [rank]
State after:
no goals