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

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

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

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

State before:
i : Nat
self : UnionFind
x : Fin (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) ≠
      i →
    rank self i <
      rank self
        (if i = ↑x then root self ↑x
        else parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i)
Tactic:
split <;> rename_i h <;> intro h'
State after:
case inl
i : Nat
self : UnionFind
x : Fin (size self)
h'✝ : ¬(Array.get self.arr x).parent = ↑x
h : i = ↑x
h' : root self ↑x ≠ i
⊢ rank self i < rank self (root self ↑x)

case inr
i : Nat
self : UnionFind
x : Fin (size self)
h'✝ : ¬(Array.get self.arr x).parent = ↑x
h : ¬i = ↑x
h' : parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i ≠ i
⊢ rank self i < rank self (parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i)

State before:
case inl
i : Nat
self : UnionFind
x : Fin (size self)
h'✝ : ¬(Array.get self.arr x).parent = ↑x
h : i = ↑x
h' : root self ↑x ≠ i
⊢ rank self i < rank self (root self ↑x)
Tactic:
subst i
State after:
case inl
self : UnionFind
x : Fin (size self)
h'✝ : ¬(Array.get self.arr x).parent = ↑x
h' : root self ↑x ≠ ↑x
⊢ rank self ↑x < rank self (root self ↑x)

State before:
case inl
self : UnionFind
x : Fin (size self)
h'✝ : ¬(Array.get self.arr x).parent = ↑x
h' : root self ↑x ≠ ↑x
⊢ rank self ↑x < rank self (root self ↑x)
Tactic:
rwa [lt_rank_root, Ne, ← root_eq_self]
State after:
no goals

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

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