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

State before:
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
i : Nat
⊢ rankD (Array.set arr x v) i = if ↑x = i then v.rank else rankD arr i
Tactic:
rw [rankD]
State after:
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
i : Nat
⊢ (if h : i < Array.size (Array.set arr x v) then (Array.get (Array.set arr x v) { val := i, isLt := h }).rank else 0) =
    if ↑x = i then v.rank else rankD arr i

State before:
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
i : Nat
⊢ (if h : i < Array.size (Array.set arr x v) then (Array.get (Array.set arr x v) { val := i, isLt := h }).rank else 0) =
    if ↑x = i then v.rank else rankD arr i
Tactic:
simp [Array.get_eq_getElem, rankD]
State after:
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
i : Nat
⊢ (if h : i < Array.size arr then (Array.set arr x v)[i].rank else 0) =
    if ↑x = i then v.rank else if h : i < Array.size arr then arr[i].rank else 0

State before:
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
i : Nat
⊢ (if h : i < Array.size arr then (Array.set arr x v)[i].rank else 0) =
    if ↑x = i then v.rank else if h : i < Array.size arr then arr[i].rank else 0
Tactic:
split <;> [split <;> simp [Array.get_set, *]; split <;> [(subst i; cases ‹¬_› x.2); rfl]]
State after:
no goals

State before:
case inr.inl
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
i : Nat
h✝¹ : ¬i < Array.size arr
h✝ : ↑x = i
⊢ 0 = v.rank
Tactic:
subst i
State after:
case inr.inl
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
h✝ : ¬↑x < Array.size arr
⊢ 0 = v.rank

State before:
case inr.inl
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
h✝ : ¬↑x < Array.size arr
⊢ 0 = v.rank
Tactic:
cases ‹¬_› x.2
State after:
no goals