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

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