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

State before:
self : UnionFind
x : Fin (size self)
i : Nat
⊢ parentD (findAux self x).s i = root self i ∧ root self i = root self ↑x ∨ parentD (findAux self x).s i = parent self i
Tactic:
if h' : (self.arr.get x).parent = x then
  rw [findAux_s, if_pos h']; exact .inr rfl
else
  rw [parentD_findAux]; split <;> [simp [*]; skip]
  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ ‹_›)
  exact (parentD_findAux_or self ⟨_, self.parent'_lt x⟩ i).imp_left <| .imp_right fun h => by
    simp [h, ← parentD_eq, root_parent]
State after:
no goals

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

State before:
self : UnionFind
x : Fin (size self)
i : Nat
h' : (Array.get self.arr x).parent = ↑x
⊢ parentD self.arr i = root self i ∧ root self i = root self ↑x ∨ parentD self.arr i = parent self i
Tactic:
exact .inr rfl
State after:
no goals

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

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

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

State before:
case inr
self : UnionFind
x : Fin (size self)
i : Nat
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 = root self i ∧
      root self i = root self ↑x ∨
    parentD (findAux self { val := (Array.get self.arr x).parent, isLt := ⋯ }).s i = parent self i
Tactic:
exact (parentD_findAux_or self ⟨_, self.parent'_lt x⟩ i).imp_left <| .imp_right fun h => by
  simp [h, ← parentD_eq, root_parent]
State after:
no goals

State before:
self : UnionFind
x : Fin (size self)
i : Nat
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
h : root self i = root self ↑{ val := (Array.get self.arr x).parent, isLt := ⋯ }
⊢ root self i = root self ↑x
Tactic:
simp [h, ← parentD_eq, root_parent]
State after:
no goals