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

State before:
self : Array UFNode
x y : Fin (Array.size self)
⊢ Array.size (linkAux self x y) = Array.size self
Tactic:
simp [linkAux]
State after:
self : Array UFNode
x y : Fin (Array.size self)
⊢ Array.size
      (if ↑x = ↑y then self
      else
        if (Array.get self y).rank < (Array.get self x).rank then
          Array.set self y { parent := ↑x, rank := (Array.get self y).rank }
        else
          if (Array.get self x).rank = (Array.get self y).rank then
            Array.set (Array.set self x { parent := ↑y, rank := (Array.get self x).rank }) { val := ↑y, isLt := ⋯ }
              { parent := (Array.get self y).parent, rank := (Array.get self y).rank + 1 }
          else Array.set self x { parent := ↑y, rank := (Array.get self x).rank }) =
    Array.size self

State before:
self : Array UFNode
x y : Fin (Array.size self)
⊢ Array.size
      (if ↑x = ↑y then self
      else
        if (Array.get self y).rank < (Array.get self x).rank then
          Array.set self y { parent := ↑x, rank := (Array.get self y).rank }
        else
          if (Array.get self x).rank = (Array.get self y).rank then
            Array.set (Array.set self x { parent := ↑y, rank := (Array.get self x).rank }) { val := ↑y, isLt := ⋯ }
              { parent := (Array.get self y).parent, rank := (Array.get self y).rank + 1 }
          else Array.set self x { parent := ↑y, rank := (Array.get self x).rank }) =
    Array.size self
Tactic:
split <;> [rfl; split] <;> [skip; split] <;> simp
State after:
no goals