-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem lt_rankD_findAux {self : UnionFind} {x : Fin self.size} :
    parentD (findAux self x).s i ≠ i →
    self.rank i < self.rank (parentD (findAux self x).s i)

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

Tactic:
apply lt_rankD_findAux h'

Result:
no goals

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

Tactic:
split <;> rename_i h <;> intro h'

Result:
case isTrue
i : Nat
self : UnionFind
x : Fin self.size
h'✝ : ¬self.arr[↑x].parent = ↑x
h : i = ↑x
h' : self.rootD ↑x ≠ i
⊢ self.rank i < self.rank (self.rootD ↑x)

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

Proof state:
case isTrue
self : UnionFind
x : Fin self.size
h'✝ : ¬self.arr[↑x].parent = ↑x
h' : self.rootD ↑x ≠ ↑x
⊢ self.rank ↑x < self.rank (self.rootD ↑x)

Tactic:
rwa [lt_rank_root, Ne, ← rootD_eq_self]

Result:
no goals

Proof state:
i : Nat
self : UnionFind
x : Fin self.size
h' : ¬self.arr[↑x].parent = ↑x
⊢ parentD (self.findAux x).s i ≠ i → self.rank i < self.rank (parentD (self.findAux x).s i)

Tactic:
rw [parentD_findAux]

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

Proof state:
i : Nat
self : UnionFind
x : Fin self.size
h' : self.arr[↑x].parent = ↑x
⊢ parentD self.arr i ≠ i → self.rank i < self.rank (parentD self.arr i)

Tactic:
apply self.rank_lt

Result:
no goals

Proof state:
i : Nat
self : UnionFind
x : Fin self.size
h' : self.arr[↑x].parent = ↑x
⊢ parentD (self.findAux x).s i ≠ i → self.rank i < self.rank (parentD (self.findAux x).s i)

Tactic:
rw [findAux_s, if_pos h']

Result:
i : Nat
self : UnionFind
x : Fin self.size
h' : self.arr[↑x].parent = ↑x
⊢ parentD self.arr i ≠ i → self.rank i < self.rank (parentD self.arr i)

Proof state:
case isTrue
i : Nat
self : UnionFind
x : Fin self.size
h'✝ : ¬self.arr[↑x].parent = ↑x
h : i = ↑x
h' : self.rootD ↑x ≠ i
⊢ self.rank i < self.rank (self.rootD ↑x)

Tactic:
subst i

Result:
case isTrue
self : UnionFind
x : Fin self.size
h'✝ : ¬self.arr[↑x].parent = ↑x
h' : self.rootD ↑x ≠ ↑x
⊢ self.rank ↑x < self.rank (self.rootD ↑x)

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

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

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