-- 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:
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 : parentD arr' i = if ↑x = i then ↑y else parentD arr i
hR : ∀ {i : Nat}, rankD arr' i = if ↑y = i ∧ arr[↑x].rank = arr[↑y].rank then arr[↑y].rank + 1 else rankD arr i
⊢ ¬parentD arr' i = i → rankD arr' i < rankD arr' (parentD arr' i)

Tactic:
simp [hP, hR, -Array.get_eq_getElem] at *

Result:
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
⊢ ¬(if ↑x = i then ↑y else parentD arr i) = i →
    (if ↑y = i ∧ arr[↑x].rank = arr[↑y].rank then arr[↑y].rank + 1 else rankD arr i) <
      if (↑y = if ↑x = i then ↑y else parentD arr i) ∧ arr[↑x].rank = arr[↑y].rank then arr[↑y].rank + 1
      else rankD arr (if ↑x = i then ↑y else parentD arr i)

Proof state:
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

Tactic:
exact Nat.lt_of_le_of_ne H h₃

Result:
no goals

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
⊢ 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:
have := rankD_lt h

Result:
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)

Proof state:
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)

Tactic:
simp only [hroot, parentD_eq y.2, not_true_eq_false] at h

Result:
no goals

Proof state:
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)

Tactic:
exact this

Result:
no goals

Proof state:
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

Tactic:
rw [← 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[↑x].rank + 1

Proof state:
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
⊢ ¬(if ↑x = i then ↑y else parentD arr i) = i →
    (if ↑y = i ∧ arr[↑x].rank = arr[↑y].rank then arr[↑y].rank + 1 else rankD arr i) <
      if (↑y = if ↑x = i then ↑y else parentD arr i) ∧ arr[↑x].rank = arr[↑y].rank then arr[↑y].rank + 1
      else rankD arr (if ↑x = i then ↑y else parentD arr i)

Tactic:
split <;> rename_i h₁ <;> [simp [← h₁]; skip] <;>
split <;> rename_i h₂ <;> intro h

Result:
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

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
⊢ rankD arr ↑x < if arr[↑x].rank = arr[↑y].rank then arr[↑y].rank + 1 else rankD arr ↑y

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)

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
⊢ 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)