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

State before:
self : UnionFind
i : Nat
⊢ parent self i < size self ↔ i < size self
Tactic:
simp [parentD]
State after:
self : UnionFind
i : Nat
⊢ (if h : i < Array.size self.arr then (Array.get self.arr { val := i, isLt := h }).parent else i) <
      Array.size self.arr ↔
    i < Array.size self.arr

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