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

State before:
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
i : Nat
⊢ parentD (Array.set arr x v) i = if ↑x = i then v.parent else parentD arr i
Tactic:
rw [parentD]
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 }).parent
    else i) =
    if ↑x = i then v.parent else parentD 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 }).parent
    else i) =
    if ↑x = i then v.parent else parentD arr i
Tactic:
simp [Array.get_eq_getElem, parentD]
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].parent else i) =
    if ↑x = i then v.parent else if h : i < Array.size arr then arr[i].parent else i

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].parent else i) =
    if ↑x = i then v.parent else if h : i < Array.size arr then arr[i].parent else i
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
⊢ i = v.parent
Tactic:
subst i
State after:
case inr.inl
arr : Array UFNode
x : Fin (Array.size arr)
v : UFNode
h✝ : ¬↑x < Array.size arr
⊢ ↑x = v.parent

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