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

State before:
self : UnionFind
x : Fin (size self)
⊢ parentD (findAux self x).s (root self ↑x) = root self ↑x
Tactic:
rw [parentD_findAux]
State after:
self : UnionFind
x : Fin (size self)
⊢ (if root self ↑x = ↑x then root self ↑x
    else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s (root self ↑x)) =
    root self ↑x

State before:
self : UnionFind
x : Fin (size self)
⊢ (if root self ↑x = ↑x then root self ↑x
    else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s (root self ↑x)) =
    root self ↑x
Tactic:
split <;> [rfl; rename_i h]
State after:
case inr
self : UnionFind
x : Fin (size self)
h : ¬root self ↑x = ↑x
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s (root self ↑x) = root self ↑x

State before:
case inr
self : UnionFind
x : Fin (size self)
h : ¬root self ↑x = ↑x
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s (root self ↑x) = root self ↑x
Tactic:
rw [root_eq_self, parent, parentD_eq] at h
State after:
case inr
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s (root self ↑x) = root self ↑x

State before:
case inr
self : UnionFind
x : Fin (size self)
h : ¬(Array.get self.arr x).parent = ↑x
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s (root self ↑x) = root self ↑x
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
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s (root self ↑x) = root self ↑x

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
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s (root self ↑x) = root self ↑x
Tactic:
rw [← root_parent, parent, parentD_eq]
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
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s
      (root self (Array.get self.arr x).parent) =
    root self (Array.get self.arr x).parent

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
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s
      (root self (Array.get self.arr x).parent) =
    root self (Array.get self.arr x).parent
Tactic:
exact parentD_findAux_root (x := ⟨_, self.parent'_lt x⟩)
State after:
no goals