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

State before:
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
⊢ parentD (findAux self x).s i < size self
Tactic:
if h' : (self.arr.get x).parent = x then
  rw [findAux_s, if_pos h']; apply self.parentD_lt h
else
  rw [parentD_findAux]; split <;> [simp [root_lt]; skip]
  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
  apply parentD_findAux_lt h
State after:
no goals

State before:
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h' : (Array.get self.arr x).parent = ↑x
⊢ parentD (findAux self x).s i < size self
Tactic:
rw [findAux_s, if_pos h']
State after:
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h' : (Array.get self.arr x).parent = ↑x
⊢ parentD self.arr i < size self

State before:
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h' : (Array.get self.arr x).parent = ↑x
⊢ parentD self.arr i < size self
Tactic:
apply self.parentD_lt h
State after:
no goals

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

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

State before:
case inr
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h' : ¬(Array.get self.arr x).parent = ↑x
h✝ : ¬i = ↑x
⊢ parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i < size self
Tactic:
have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
State after:
case inr
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h' : ¬(Array.get self.arr x).parent = ↑x
h✝ : ¬i = ↑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 i < size self

State before:
case inr
i : Nat
self : UnionFind
x : Fin (size self)
h : i < size self
h' : ¬(Array.get self.arr x).parent = ↑x
h✝ : ¬i = ↑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 i < size self
Tactic:
apply parentD_findAux_lt h
State after:
no goals