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

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

State before:
self : UnionFind
x : Nat
⊢ (if h : x < Array.size self.arr then ↑(root' self { val := parent self x, isLt := ⋯ }) else parent self x) =
    if h : x < Array.size self.arr then ↑(root' self { val := x, isLt := ⋯ }) else x
Tactic:
split <;> simp [parentD, parentD_of_not_lt, *]
State after:
case inl
self : UnionFind
x : Nat
h✝ : x < Array.size self.arr
⊢ ↑(root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ }) =
    ↑(root' self { val := x, isLt := ⋯ })

State before:
case inl
self : UnionFind
x : Nat
h✝ : x < Array.size self.arr
⊢ ↑(root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ }) =
    ↑(root' self { val := x, isLt := ⋯ })
Tactic:
(conv => rhs; rw [root'])
State after:
case inl
self : UnionFind
x : Nat
h✝ : x < Array.size self.arr
⊢ ↑(root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ }) =
    ↑(if h : (Array.get self.arr { val := x, isLt := ⋯ }).parent = ↑{ val := x, isLt := ⋯ } then { val := x, isLt := ⋯ }
      else
        let_fun this := ⋯;
        root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ })

State before:
case inl
self : UnionFind
x : Nat
h✝ : x < Array.size self.arr
⊢ ↑(root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ }) =
    ↑(if h : (Array.get self.arr { val := x, isLt := ⋯ }).parent = ↑{ val := x, isLt := ⋯ } then { val := x, isLt := ⋯ }
      else
        let_fun this := ⋯;
        root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ })
Tactic:
split
State after:
case inl.inl
self : UnionFind
x : Nat
h✝¹ : x < Array.size self.arr
h✝ : (Array.get self.arr { val := x, isLt := ⋯ }).parent = ↑{ val := x, isLt := ⋯ }
⊢ ↑(root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ }) = ↑{ val := x, isLt := ⋯ }

case inl.inr
self : UnionFind
x : Nat
h✝¹ : x < Array.size self.arr
h✝ : ¬(Array.get self.arr { val := x, isLt := ⋯ }).parent = ↑{ val := x, isLt := ⋯ }
⊢ ↑(root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ }) =
    ↑(let_fun this := ⋯;
      root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ })

State before:
case inl
self : UnionFind
x : Nat
h✝ : x < Array.size self.arr
⊢ ↑(root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ }) =
    ↑(root' self { val := x, isLt := ⋯ })
Tactic:
conv => rhs; rw [root']
State after:
case inl
self : UnionFind
x : Nat
h✝ : x < Array.size self.arr
⊢ ↑(root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ }) =
    ↑(if h : (Array.get self.arr { val := x, isLt := ⋯ }).parent = ↑{ val := x, isLt := ⋯ } then { val := x, isLt := ⋯ }
      else
        let_fun this := ⋯;
        root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ })

State before:
case inl.inl
self : UnionFind
x : Nat
h✝¹ : x < Array.size self.arr
h✝ : (Array.get self.arr { val := x, isLt := ⋯ }).parent = ↑{ val := x, isLt := ⋯ }
⊢ ↑(root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ }) = ↑{ val := x, isLt := ⋯ }
Tactic:
rw [root', dif_pos] <;> simp [*]
State after:
no goals

State before:
case inl.inr
self : UnionFind
x : Nat
h✝¹ : x < Array.size self.arr
h✝ : ¬(Array.get self.arr { val := x, isLt := ⋯ }).parent = ↑{ val := x, isLt := ⋯ }
⊢ ↑(root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ }) =
    ↑(let_fun this := ⋯;
      root' self { val := (Array.get self.arr { val := x, isLt := ⋯ }).parent, isLt := ⋯ })
Tactic:
simp
State after:
no goals