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

State before:
self : UnionFind
x : Fin (size self)
⊢ (findAux self x).s =
    if (Array.get self.arr x).parent = ↑x then self.arr
    else
      Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := root self ↑x, rank := s.rank }
Tactic:
rw [show self.root _ = (self.findAux ⟨_, self.parent'_lt x⟩).root from _]
State after:
self : UnionFind
x : Fin (size self)
⊢ (findAux self x).s =
    if (Array.get self.arr x).parent = ↑x then self.arr
    else
      Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := ↑(findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root, rank := s.rank }

self : UnionFind
x : Fin (size self)
⊢ root self ↑x = ↑(findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root

State before:
self : UnionFind
x : Fin (size self)
⊢ (findAux self x).s =
    if (Array.get self.arr x).parent = ↑x then self.arr
    else
      Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := ↑(findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root, rank := s.rank }
Tactic:
rw [findAux]
State after:
self : UnionFind
x : Fin (size self)
⊢ (if h : (Array.get self.arr x).parent = ↑x then { s := self.arr, root := x, size_eq := ⋯ }
      else
        let_fun this := ⋯;
        match findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ } with
        | { s := arr₁, root := root, size_eq := H } =>
          { s := Array.modify arr₁ ↑x fun s => { parent := ↑root, rank := s.rank }, root := root, size_eq := ⋯ }).s =
    if (Array.get self.arr x).parent = ↑x then self.arr
    else
      Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := ↑(findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root, rank := s.rank }

State before:
self : UnionFind
x : Fin (size self)
⊢ (if h : (Array.get self.arr x).parent = ↑x then { s := self.arr, root := x, size_eq := ⋯ }
      else
        let_fun this := ⋯;
        match findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ } with
        | { s := arr₁, root := root, size_eq := H } =>
          { s := Array.modify arr₁ ↑x fun s => { parent := ↑root, rank := s.rank }, root := root, size_eq := ⋯ }).s =
    if (Array.get self.arr x).parent = ↑x then self.arr
    else
      Array.modify (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s ↑x fun s =>
        { parent := ↑(findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root, rank := s.rank }
Tactic:
split <;> rfl
State after:
no goals

State before:
self : UnionFind
x : Fin (size self)
⊢ root self ↑x = ↑(findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root
Tactic:
rw [← root_parent, parent, parentD_eq]
State after:
self : UnionFind
x : Fin (size self)
⊢ root self (Array.get self.arr x).parent = ↑(findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root

State before:
self : UnionFind
x : Fin (size self)
⊢ root self (Array.get self.arr x).parent = ↑(findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root
Tactic:
simp [findAux_root, root, parent'_lt]
State after:
no goals