-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem setParentBump_rankD_lt {arr : Array UFNode} {x y : Fin arr.size}
    (hroot : arr[x.1].rank < arr[y.1].rank ∨ arr[y.1].parent = y)
    (H : arr[x.1].rank ≤ arr[y.1].rank) {i : Nat}
    (rankD_lt : parentD arr i ≠ i → rankD arr i < rankD arr (parentD arr i))
    (hP : parentD arr' i = if x.1 = i then y.1 else parentD arr i)
    (hR : ∀ {i}, rankD arr' i =
      if y.1 = i ∧ arr[x.1].rank = arr[y.1].rank then
        arr[y.1].rank + 1
      else rankD arr i) :
    ¬parentD arr' i = i → rankD arr' i < rankD arr' (parentD arr' i)

Proof state:
case isFalse.isFalse
arr' arr : Array UFNode
x y : Fin arr.size
hroot : arr[↑x].rank < arr[↑y].rank ∨ arr[↑y].parent = ↑y
H : arr[↑x].rank ≤ arr[↑y].rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ¬↑x = i
h₂ : ¬(↑y = i ∧ arr[↑x].rank = arr[↑y].rank)
h : ¬parentD arr i = i
this : rankD arr i < rankD arr (parentD arr i)
⊢ rankD arr i < if ↑y = parentD arr i ∧ arr[↑x].rank = arr[↑y].rank then arr[↑y].rank + 1 else rankD arr (parentD arr i)

Tactic:
split <;> rename_i h₃

Result:
case isFalse.isFalse.isTrue
arr' arr : Array UFNode
x y : Fin arr.size
hroot : arr[↑x].rank < arr[↑y].rank ∨ arr[↑y].parent = ↑y
H : arr[↑x].rank ≤ arr[↑y].rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ¬↑x = i
h₂ : ¬(↑y = i ∧ arr[↑x].rank = arr[↑y].rank)
h : ¬parentD arr i = i
this : rankD arr i < rankD arr (parentD arr i)
h₃ : ↑y = parentD arr i ∧ arr[↑x].rank = arr[↑y].rank
⊢ rankD arr i < arr[↑y].rank + 1

case isFalse.isFalse.isFalse
arr' arr : Array UFNode
x y : Fin arr.size
hroot : arr[↑x].rank < arr[↑y].rank ∨ arr[↑y].parent = ↑y
H : arr[↑x].rank ≤ arr[↑y].rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ¬↑x = i
h₂ : ¬(↑y = i ∧ arr[↑x].rank = arr[↑y].rank)
h : ¬parentD arr i = i
this : rankD arr i < rankD arr (parentD arr i)
h₃ : ¬(↑y = parentD arr i ∧ arr[↑x].rank = arr[↑y].rank)
⊢ rankD arr i < rankD arr (parentD arr i)

Proof state:
case isFalse.isTrue.refl
arr' arr : Array UFNode
x y : Fin arr.size
hroot : arr[↑x].rank < arr[↑y].rank ∨ arr[↑y].parent = ↑y
H : arr[↑x].rank ≤ arr[↑y].rank
hP hR : True
rankD_lt : ¬parentD arr ↑y = ↑y → rankD arr ↑y < rankD arr (parentD arr ↑y)
h₁ : ¬↑x = ↑y
h₂ : ↑y = ↑y ∧ arr[↑x].rank = arr[↑y].rank
h : ¬parentD arr ↑y = ↑y
⊢ arr[↑y].rank + 1 <
    if ↑y = parentD arr ↑y ∧ arr[↑x].rank = arr[↑y].rank then arr[↑y].rank + 1 else rankD arr (parentD arr ↑y)

Tactic:
simp only [h₂.2, false_or, Nat.lt_irrefl] at hroot

Result:
case isFalse.isTrue.refl
arr' arr : Array UFNode
x y : Fin arr.size
H : arr[↑x].rank ≤ arr[↑y].rank
hP hR : True
rankD_lt : ¬parentD arr ↑y = ↑y → rankD arr ↑y < rankD arr (parentD arr ↑y)
h₁ : ¬↑x = ↑y
h₂ : ↑y = ↑y ∧ arr[↑x].rank = arr[↑y].rank
h : ¬parentD arr ↑y = ↑y
hroot : arr[↑y].parent = ↑y
⊢ arr[↑y].rank + 1 <
    if ↑y = parentD arr ↑y ∧ arr[↑x].rank = arr[↑y].rank then arr[↑y].rank + 1 else rankD arr (parentD arr ↑y)

Proof state:
case isTrue.isFalse
arr' arr : Array UFNode
x y : Fin arr.size
hroot : arr[↑x].rank < arr[↑y].rank ∨ arr[↑y].parent = ↑y
H : arr[↑x].rank ≤ arr[↑y].rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ↑x = i
h₂ : ¬(↑y = ↑x ∧ arr[↑x].rank = arr[↑y].rank)
h : ¬↑y = ↑x
⊢ arr[↑x].rank < if arr[↑x].rank = arr[↑y].rank then arr[↑y].rank + 1 else arr[↑y].rank

Tactic:
split <;> rename_i h₃

Result:
case isTrue.isFalse.isTrue
arr' arr : Array UFNode
x y : Fin arr.size
hroot : arr[↑x].rank < arr[↑y].rank ∨ arr[↑y].parent = ↑y
H : arr[↑x].rank ≤ arr[↑y].rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ↑x = i
h₂ : ¬(↑y = ↑x ∧ arr[↑x].rank = arr[↑y].rank)
h : ¬↑y = ↑x
h₃ : arr[↑x].rank = arr[↑y].rank
⊢ arr[↑x].rank < arr[↑y].rank + 1

case isTrue.isFalse.isFalse
arr' arr : Array UFNode
x y : Fin arr.size
hroot : arr[↑x].rank < arr[↑y].rank ∨ arr[↑y].parent = ↑y
H : arr[↑x].rank ≤ arr[↑y].rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ↑x = i
h₂ : ¬(↑y = ↑x ∧ arr[↑x].rank = arr[↑y].rank)
h : ¬↑y = ↑x
h₃ : ¬arr[↑x].rank = arr[↑y].rank
⊢ arr[↑x].rank < arr[↑y].rank

Proof state:
case isFalse.isFalse.isTrue
arr' arr : Array UFNode
x y : Fin arr.size
hroot : arr[↑x].rank < arr[↑y].rank ∨ arr[↑y].parent = ↑y
H : arr[↑x].rank ≤ arr[↑y].rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ¬↑x = i
h₂ : ¬(↑y = i ∧ arr[↑x].rank = arr[↑y].rank)
h : ¬parentD arr i = i
this : rankD arr i < rankD arr (parentD arr i)
h₃ : ↑y = parentD arr i ∧ arr[↑x].rank = arr[↑y].rank
⊢ rankD arr i < arr[↑y].rank + 1

Tactic:
rw [← rankD_eq, h₃.1]

Result:
case isFalse.isFalse.isTrue
arr' arr : Array UFNode
x y : Fin arr.size
hroot : arr[↑x].rank < arr[↑y].rank ∨ arr[↑y].parent = ↑y
H : arr[↑x].rank ≤ arr[↑y].rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ¬↑x = i
h₂ : ¬(↑y = i ∧ arr[↑x].rank = arr[↑y].rank)
h : ¬parentD arr i = i
this : rankD arr i < rankD arr (parentD arr i)
h₃ : ↑y = parentD arr i ∧ arr[↑x].rank = arr[↑y].rank
⊢ rankD arr i < rankD arr (parentD arr i) + 1

Proof state:
case isTrue.isTrue
arr' arr : Array UFNode
x y : Fin arr.size
hroot : arr[↑x].rank < arr[↑y].rank ∨ arr[↑y].parent = ↑y
H : arr[↑x].rank ≤ arr[↑y].rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ↑x = i
h₂ : ↑y = ↑x ∧ arr[↑x].rank = arr[↑y].rank
h : ¬↑y = ↑x
⊢ arr[↑y].rank + 1 < if arr[↑x].rank = arr[↑y].rank then arr[↑y].rank + 1 else rankD arr ↑y

Tactic:
simp [h₂] at h

Result:
no goals

Proof state:
case isFalse.isTrue
arr' arr : Array UFNode
x y : Fin arr.size
hroot : arr[↑x].rank < arr[↑y].rank ∨ arr[↑y].parent = ↑y
H : arr[↑x].rank ≤ arr[↑y].rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ¬↑x = i
h₂ : ↑y = i ∧ arr[↑x].rank = arr[↑y].rank
h : ¬parentD arr i = i
⊢ arr[↑y].rank + 1 <
    if ↑y = parentD arr i ∧ arr[↑x].rank = arr[↑y].rank then arr[↑y].rank + 1 else rankD arr (parentD arr i)

Tactic:
cases h₂.1

Result:
case isFalse.isTrue.refl
arr' arr : Array UFNode
x y : Fin arr.size
hroot : arr[↑x].rank < arr[↑y].rank ∨ arr[↑y].parent = ↑y
H : arr[↑x].rank ≤ arr[↑y].rank
hP hR : True
rankD_lt : ¬parentD arr ↑y = ↑y → rankD arr ↑y < rankD arr (parentD arr ↑y)
h₁ : ¬↑x = ↑y
h₂ : ↑y = ↑y ∧ arr[↑x].rank = arr[↑y].rank
h : ¬parentD arr ↑y = ↑y
⊢ arr[↑y].rank + 1 <
    if ↑y = parentD arr ↑y ∧ arr[↑x].rank = arr[↑y].rank then arr[↑y].rank + 1 else rankD arr (parentD arr ↑y)

Proof state:
case isFalse.isFalse.isTrue
arr' arr : Array UFNode
x y : Fin arr.size
hroot : arr[↑x].rank < arr[↑y].rank ∨ arr[↑y].parent = ↑y
H : arr[↑x].rank ≤ arr[↑y].rank
i : Nat
rankD_lt : ¬parentD arr i = i → rankD arr i < rankD arr (parentD arr i)
hP hR : True
h₁ : ¬↑x = i
h₂ : ¬(↑y = i ∧ arr[↑x].rank = arr[↑y].rank)
h : ¬parentD arr i = i
this : rankD arr i < rankD arr (parentD arr i)
h₃ : ↑y = parentD arr i ∧ arr[↑x].rank = arr[↑y].rank
⊢ rankD arr i < rankD arr (parentD arr i) + 1

Tactic:
exact Nat.lt_succ_of_lt this

Result:
no goals