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

State before:
self : UnionFind
x : Nat
⊢ root self x = x ↔ parent self x = x
Tactic:
refine ⟨fun h => by rw [← h, parent_root], fun h => ?_⟩
State after:
self : UnionFind
x : Nat
h : parent self x = x
⊢ root self x = x

State before:
self : UnionFind
x : Nat
h : parent self x = x
⊢ root self x = x
Tactic:
rw [root]
State after:
self : UnionFind
x : Nat
h : parent self x = x
⊢ (if h : x < size self then ↑(root' self { val := x, isLt := h }) else x) = x

State before:
self : UnionFind
x : Nat
h : parent self x = x
⊢ (if h : x < size self then ↑(root' self { val := x, isLt := h }) else x) = x
Tactic:
split <;> [rw [root', dif_pos (by rwa [parent, parentD_eq' ‹_›] at h)]; rfl]
State after:
no goals

State before:
self : UnionFind
x : Nat
h : root self x = x
⊢ parent self x = x
Tactic:
rw [← h, parent_root]
State after:
no goals

State before:
self : UnionFind
x : Nat
h : parent self x = x
h✝ : x < size self
⊢ (Array.get self.arr { val := x, isLt := h✝ }).parent = ↑{ val := x, isLt := h✝ }
Tactic:
rwa [parent, parentD_eq' ‹_›] at h
State after:
no goals