Theorem: Lean4Lean.UnionFind.parent'_root' (Lean4Lean/UnionFind.lean)

State before:
self : UnionFind
x : Fin (size self)
⊢ (Array.get self.arr (root' self x)).parent = ↑(root' self x)
Tactic:
rw [root']
State after:
self : UnionFind
x : Fin (size self)
⊢ (Array.get self.arr
        (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 := ⋯ })).parent =
    ↑(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)
⊢ (Array.get self.arr
        (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 := ⋯ })).parent =
    ↑(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:
split <;> [assumption; skip]
State after:
case inr
self : UnionFind
x : Fin (size self)
h✝ : ¬(Array.get self.arr x).parent = ↑x
⊢ (Array.get self.arr
        (let_fun this := ⋯;
        root' self { val := (Array.get self.arr x).parent, isLt := ⋯ })).parent =
    ↑(let_fun this := ⋯;
      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
⊢ (Array.get self.arr
        (let_fun this := ⋯;
        root' self { val := (Array.get self.arr x).parent, isLt := ⋯ })).parent =
    ↑(let_fun this := ⋯;
      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
⊢ (Array.get self.arr
        (let_fun this := ⋯;
        root' self { val := (Array.get self.arr x).parent, isLt := ⋯ })).parent =
    ↑(let_fun this := ⋯;
      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
⊢ (Array.get self.arr
        (let_fun this := ⋯;
        root' self { val := (Array.get self.arr x).parent, isLt := ⋯ })).parent =
    ↑(let_fun this := ⋯;
      root' self { val := (Array.get self.arr x).parent, isLt := ⋯ })
Tactic:
apply parent'_root'
State after:
no goals