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

State before:
self : UnionFind
x : Nat
⊢ root self x < size self ↔ x < size self
Tactic:
simp [root]
State after:
self : UnionFind
x : Nat
⊢ (if h : x < Array.size self.arr then ↑(root' self { val := x, isLt := ⋯ }) else x) < Array.size self.arr ↔
    x < Array.size self.arr

State before:
self : UnionFind
x : Nat
⊢ (if h : x < Array.size self.arr then ↑(root' self { val := x, isLt := ⋯ }) else x) < Array.size self.arr ↔
    x < Array.size self.arr
Tactic:
split <;> simp [*]
State after:
no goals