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

State before:
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1 else rankD arr i
⊢ ¬parentD arr' i = i → rankD arr' i < rankD arr' (parentD arr' i)
Tactic:
simp [hP, hR] at *
State after:
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1 else rankD arr i) <
      if (↑y = if ↑x = i then ↑y else parentD arr i) ∧ (Array.get arr x).rank = (Array.get arr y).rank then
        (Array.get arr y).rank + 1
      else rankD arr (if ↑x = i then ↑y else parentD arr i)

State before:
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1 else rankD arr i) <
      if (↑y = if ↑x = i then ↑y else parentD arr i) ∧ (Array.get arr x).rank = (Array.get arr y).rank then
        (Array.get 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
State after:
case inl.inl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank
h : ¬↑y = ↑x
⊢ (Array.get arr y).rank + 1 <
    if (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1 else rankD arr ↑y

case inl.inr
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬↑y = ↑x
⊢ rankD arr ↑x < if (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1 else rankD arr ↑y

case inr.inl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank
h : ¬parentD arr i = i
⊢ (Array.get arr y).rank + 1 <
    if ↑y = parentD arr i ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1
    else rankD arr (parentD arr i)

case inr.inr
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬parentD arr i = i
⊢ rankD arr i <
    if ↑y = parentD arr i ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1
    else rankD arr (parentD arr i)

State before:
case inl.inl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank
h : ¬↑y = ↑x
⊢ (Array.get arr y).rank + 1 <
    if (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1 else rankD arr ↑y
Tactic:
simp [h₂] at h
State after:
no goals

State before:
case inl.inr
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬↑y = ↑x
⊢ rankD arr ↑x < if (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1 else rankD arr ↑y
Tactic:
simp [rankD_eq]
State after:
case inl.inr
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬↑y = ↑x
⊢ (Array.get arr x).rank <
    if (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1 else (Array.get arr y).rank

State before:
case inl.inr
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬↑y = ↑x
⊢ (Array.get arr x).rank <
    if (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1 else (Array.get arr y).rank
Tactic:
split <;> rename_i h₃
State after:
case inl.inr.inl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬↑y = ↑x
h₃ : (Array.get arr x).rank = (Array.get arr y).rank
⊢ (Array.get arr x).rank < (Array.get arr y).rank + 1

case inl.inr.inr
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬↑y = ↑x
h₃ : ¬(Array.get arr x).rank = (Array.get arr y).rank
⊢ (Array.get arr x).rank < (Array.get arr y).rank

State before:
case inl.inr.inl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬↑y = ↑x
h₃ : (Array.get arr x).rank = (Array.get arr y).rank
⊢ (Array.get arr x).rank < (Array.get arr y).rank + 1
Tactic:
rw [← h₃]
State after:
case inl.inr.inl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬↑y = ↑x
h₃ : (Array.get arr x).rank = (Array.get arr y).rank
⊢ (Array.get arr x).rank < (Array.get arr x).rank + 1

State before:
case inl.inr.inl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬↑y = ↑x
h₃ : (Array.get arr x).rank = (Array.get arr y).rank
⊢ (Array.get arr x).rank < (Array.get arr x).rank + 1
Tactic:
apply Nat.lt_succ_self
State after:
no goals

State before:
case inl.inr.inr
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬↑y = ↑x
h₃ : ¬(Array.get arr x).rank = (Array.get arr y).rank
⊢ (Array.get arr x).rank < (Array.get arr y).rank
Tactic:
exact Nat.lt_of_le_of_ne H h₃
State after:
no goals

State before:
case inr.inl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank
h : ¬parentD arr i = i
⊢ (Array.get arr y).rank + 1 <
    if ↑y = parentD arr i ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1
    else rankD arr (parentD arr i)
Tactic:
cases h₂.1
State after:
case inr.inl.refl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank
h : ¬parentD arr ↑y = ↑y
⊢ (Array.get arr y).rank + 1 <
    if ↑y = parentD arr ↑y ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1
    else rankD arr (parentD arr ↑y)

State before:
case inr.inl.refl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank
h : ¬parentD arr ↑y = ↑y
⊢ (Array.get arr y).rank + 1 <
    if ↑y = parentD arr ↑y ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1
    else rankD arr (parentD arr ↑y)
Tactic:
simp [h₂.2] at hroot
State after:
case inr.inl.refl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank
h : ¬parentD arr ↑y = ↑y
hroot : (Array.get arr y).parent = ↑y
⊢ (Array.get arr y).rank + 1 <
    if ↑y = parentD arr ↑y ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1
    else rankD arr (parentD arr ↑y)

State before:
case inr.inl.refl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank
h : ¬parentD arr ↑y = ↑y
hroot : (Array.get arr y).parent = ↑y
⊢ (Array.get arr y).rank + 1 <
    if ↑y = parentD arr ↑y ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1
    else rankD arr (parentD arr ↑y)
Tactic:
simp [hroot, parentD_eq] at h
State after:
no goals

State before:
case inr.inr
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬parentD arr i = i
⊢ rankD arr i <
    if ↑y = parentD arr i ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1
    else rankD arr (parentD arr i)
Tactic:
have := rankD_lt h
State after:
case inr.inr
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1
    else rankD arr (parentD arr i)

State before:
case inr.inr
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank then (Array.get arr y).rank + 1
    else rankD arr (parentD arr i)
Tactic:
split <;> rename_i h₃
State after:
case inr.inr.inl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬parentD arr i = i
this : rankD arr i < rankD arr (parentD arr i)
h₃ : ↑y = parentD arr i ∧ (Array.get arr x).rank = (Array.get arr y).rank
⊢ rankD arr i < (Array.get arr y).rank + 1

case inr.inr.inr
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬parentD arr i = i
this : rankD arr i < rankD arr (parentD arr i)
h₃ : ¬(↑y = parentD arr i ∧ (Array.get arr x).rank = (Array.get arr y).rank)
⊢ rankD arr i < rankD arr (parentD arr i)

State before:
case inr.inr.inl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬parentD arr i = i
this : rankD arr i < rankD arr (parentD arr i)
h₃ : ↑y = parentD arr i ∧ (Array.get arr x).rank = (Array.get arr y).rank
⊢ rankD arr i < (Array.get arr y).rank + 1
Tactic:
rw [← rankD_eq, h₃.1]
State after:
case inr.inr.inl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬parentD arr i = i
this : rankD arr i < rankD arr (parentD arr i)
h₃ : ↑y = parentD arr i ∧ (Array.get arr x).rank = (Array.get arr y).rank
⊢ rankD arr i < rankD arr (parentD arr i) + 1

State before:
case inr.inr.inl
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬parentD arr i = i
this : rankD arr i < rankD arr (parentD arr i)
h₃ : ↑y = parentD arr i ∧ (Array.get arr x).rank = (Array.get arr y).rank
⊢ rankD arr i < rankD arr (parentD arr i) + 1
Tactic:
exact Nat.lt_succ_of_lt this
State after:
no goals

State before:
case inr.inr.inr
arr' arr : Array UFNode
x y : Fin (Array.size arr)
hroot : (Array.get arr x).rank < (Array.get arr y).rank ∨ (Array.get arr y).parent = ↑y
H : (Array.get arr x).rank ≤ (Array.get 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 ∧ (Array.get arr x).rank = (Array.get arr y).rank)
h : ¬parentD arr i = i
this : rankD arr i < rankD arr (parentD arr i)
h₃ : ¬(↑y = parentD arr i ∧ (Array.get arr x).rank = (Array.get arr y).rank)
⊢ rankD arr i < rankD arr (parentD arr i)
Tactic:
exact this
State after:
no goals