-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem parentD_findAux_or (self : UnionFind) (x : Fin self.size) (i) :
    parentD (findAux self x).s i = self.rootD i ∧ self.rootD i = self.rootD x ∨
    parentD (findAux self x).s i = self.parent i

Proof state:
self : UnionFind
x : Fin self.size
i : Nat
h' : self.arr[↑x].parent = ↑x
⊢ parentD (self.findAux x).s i = self.rootD i ∧ self.rootD i = self.rootD ↑x ∨
    parentD (self.findAux x).s i = self.parent i

Tactic:
rw [findAux_s, if_pos h']

Result:
self : UnionFind
x : Fin self.size
i : Nat
h' : self.arr[↑x].parent = ↑x
⊢ parentD self.arr i = self.rootD i ∧ self.rootD i = self.rootD ↑x ∨ parentD self.arr i = self.parent i

Proof state:
case isFalse
self : UnionFind
x : Fin self.size
i : Nat
h' : ¬self.arr[↑x].parent = ↑x
h✝ : ¬i = ↑x
⊢ parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i = self.rootD i ∧ self.rootD i = self.rootD ↑x ∨
    parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i = self.parent i

Tactic:
have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank'_lt _ _ ‹_›)

Result:
case isFalse
self : UnionFind
x : Fin self.size
i : Nat
h' : ¬self.arr[↑x].parent = ↑x
h✝ : ¬i = ↑x
this : self.rankMax - self.rank self.arr[↑x].parent < self.rankMax - self.rank ↑x
⊢ parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i = self.rootD i ∧ self.rootD i = self.rootD ↑x ∨
    parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i = self.parent i

Proof state:
case isTrue
self : UnionFind
x : Fin self.size
i : Nat
h' : ¬self.arr[↑x].parent = ↑x
h✝ : i = ↑x
⊢ self.rootD ↑x = self.rootD i ∧ self.rootD i = self.rootD ↑x ∨ self.rootD ↑x = self.parent i

Tactic:
simp [*]

Result:
no goals

Proof state:
case isFalse
self : UnionFind
x : Fin self.size
i : Nat
h' : ¬self.arr[↑x].parent = ↑x
h✝ : ¬i = ↑x
this : self.rankMax - self.rank self.arr[↑x].parent < self.rankMax - self.rank ↑x
h : self.rootD i = self.rootD ↑⟨self.arr[↑x].parent, ⋯⟩
⊢ self.rootD i = self.rootD ↑x

Tactic:
simp only [h, ← parentD_eq, rootD_parent, Array.length_toList]

Result:
no goals

Proof state:
case isFalse
self : UnionFind
x : Fin self.size
i : Nat
h' : ¬self.arr[↑x].parent = ↑x
h✝ : ¬i = ↑x
this : self.rankMax - self.rank self.arr[↑x].parent < self.rankMax - self.rank ↑x
⊢ parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i = self.rootD i ∧ self.rootD i = self.rootD ↑x ∨
    parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i = self.parent i

Tactic:
refine (parentD_findAux_or self ⟨_, self.parent'_lt _ x.2⟩ i)
  |>.imp_left (.imp_right fun h => ?_)

Result:
case isFalse
self : UnionFind
x : Fin self.size
i : Nat
h' : ¬self.arr[↑x].parent = ↑x
h✝ : ¬i = ↑x
this : self.rankMax - self.rank self.arr[↑x].parent < self.rankMax - self.rank ↑x
h : self.rootD i = self.rootD ↑⟨self.arr[↑x].parent, ⋯⟩
⊢ self.rootD i = self.rootD ↑x

Proof state:
self : UnionFind
x : Fin self.size
i : Nat
h' : ¬self.arr[↑x].parent = ↑x
⊢ parentD (self.findAux x).s i = self.rootD i ∧ self.rootD i = self.rootD ↑x ∨
    parentD (self.findAux x).s i = self.parent i

Tactic:
rw [parentD_findAux]

Result:
self : UnionFind
x : Fin self.size
i : Nat
h' : ¬self.arr[↑x].parent = ↑x
⊢ (if i = ↑x then self.rootD ↑x else parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i) = self.rootD i ∧
      self.rootD i = self.rootD ↑x ∨
    (if i = ↑x then self.rootD ↑x else parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i) = self.parent i

Proof state:
self : UnionFind
x : Fin self.size
i : Nat
h' : ¬self.arr[↑x].parent = ↑x
⊢ (if i = ↑x then self.rootD ↑x else parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i) = self.rootD i ∧
      self.rootD i = self.rootD ↑x ∨
    (if i = ↑x then self.rootD ↑x else parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i) = self.parent i

Tactic:
split

Result:
case isTrue
self : UnionFind
x : Fin self.size
i : Nat
h' : ¬self.arr[↑x].parent = ↑x
h✝ : i = ↑x
⊢ self.rootD ↑x = self.rootD i ∧ self.rootD i = self.rootD ↑x ∨ self.rootD ↑x = self.parent i

case isFalse
self : UnionFind
x : Fin self.size
i : Nat
h' : ¬self.arr[↑x].parent = ↑x
h✝ : ¬i = ↑x
⊢ parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i = self.rootD i ∧ self.rootD i = self.rootD ↑x ∨
    parentD (self.findAux ⟨self.arr[↑x].parent, ⋯⟩).s i = self.parent i

Proof state:
self : UnionFind
x : Fin self.size
i : Nat
h' : self.arr[↑x].parent = ↑x
⊢ parentD self.arr i = self.rootD i ∧ self.rootD i = self.rootD ↑x ∨ parentD self.arr i = self.parent i

Tactic:
exact .inr rfl

Result:
no goals