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

State before:
self : UnionFind
x : Fin (size self)
⊢ (findAux self x).root = root' self x
Tactic:
rw [findAux, root']
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 := ⋯ }).root =
    if h : (Array.get self.arr x).parent = ↑x then x
    else
      let_fun this := ⋯;
      root' self { val := (Array.get self.arr x).parent, isLt := ⋯ }

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 := ⋯ }).root =
    if h : (Array.get self.arr x).parent = ↑x then x
    else
      let_fun this := ⋯;
      root' self { val := (Array.get self.arr x).parent, isLt := ⋯ }
Tactic:
simp
State after:
self : UnionFind
x : Fin (size self)
⊢ (if (Array.get self.arr x).parent = ↑x then { s := self.arr, root := x, size_eq := ⋯ }
      else
        {
          s :=
            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 },
          root := (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root, size_eq := ⋯ }).root =
    if (Array.get self.arr x).parent = ↑x then x else root' self { val := (Array.get self.arr x).parent, isLt := ⋯ }

State before:
self : UnionFind
x : Fin (size self)
⊢ (if (Array.get self.arr x).parent = ↑x then { s := self.arr, root := x, size_eq := ⋯ }
      else
        {
          s :=
            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 },
          root := (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root, size_eq := ⋯ }).root =
    if (Array.get self.arr x).parent = ↑x then x else root' self { val := (Array.get self.arr x).parent, isLt := ⋯ }
Tactic:
split <;> simp
State after:
case inr
self : UnionFind
x : Fin (size self)
h✝ : ¬(Array.get self.arr x).parent = ↑x
⊢ (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root =
    root' self { val := (Array.get self.arr x).parent, isLt := ⋯ }

State before:
case inr
self : UnionFind
x : Fin (size self)
h✝ : ¬(Array.get self.arr x).parent = ↑x
⊢ (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root =
    root' self { val := (Array.get self.arr x).parent, isLt := ⋯ }
Tactic:
have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
State after:
case inr
self : UnionFind
x : Fin (size self)
h✝ : ¬(Array.get self.arr x).parent = ↑x
this : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
⊢ (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root =
    root' self { val := (Array.get self.arr x).parent, isLt := ⋯ }

State before:
case inr
self : UnionFind
x : Fin (size self)
h✝ : ¬(Array.get self.arr x).parent = ↑x
this : rankMax self - rank self (Array.get self.arr x).parent < rankMax self - rank self ↑x
⊢ (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).root =
    root' self { val := (Array.get self.arr x).parent, isLt := ⋯ }
Tactic:
exact findAux_root
State after:
no goals