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

State before:
i : Nat
arr : Array UFNode
⊢ parentD (Array.push arr { parent := Array.size arr, rank := 0 }) i = parentD arr i
Tactic:
simp [parentD, Array.get_eq_getElem, Array.get_push]
State after:
i : Nat
arr : Array UFNode
⊢ (if i < Array.size arr + 1 then
      (if h : i < Array.size arr then arr[i] else { parent := Array.size arr, rank := 0 }).parent
    else i) =
    if h : i < Array.size arr then arr[i].parent else i

State before:
i : Nat
arr : Array UFNode
⊢ (if i < Array.size arr + 1 then
      (if h : i < Array.size arr then arr[i] else { parent := Array.size arr, rank := 0 }).parent
    else i) =
    if h : i < Array.size arr then arr[i].parent else i
Tactic:
split <;> split <;> try simp
State after:
case inl.inr
i : Nat
arr : Array UFNode
h✝¹ : i < Array.size arr + 1
h✝ : ¬i < Array.size arr
⊢ Array.size arr = i

case inr.inl
i : Nat
arr : Array UFNode
h✝¹ : ¬i < Array.size arr + 1
h✝ : i < Array.size arr
⊢ i = arr[i].parent

State before:
case inr.inr
i : Nat
arr : Array UFNode
h✝¹ : ¬i < Array.size arr + 1
h✝ : ¬i < Array.size arr
⊢ i = i
Tactic:
simp
State after:
no goals

State before:
case inl.inr
i : Nat
arr : Array UFNode
h✝¹ : i < Array.size arr + 1
h✝ : ¬i < Array.size arr
⊢ Array.size arr = i
Tactic:
exact Nat.le_antisymm (Nat.ge_of_not_lt ‹_›) (Nat.le_of_lt_succ ‹_›)
State after:
no goals

State before:
case inr.inl
i : Nat
arr : Array UFNode
h✝¹ : ¬i < Array.size arr + 1
h✝ : i < Array.size arr
⊢ i = arr[i].parent
Tactic:
cases ‹¬_› (Nat.lt_succ_of_lt ‹_›)
State after:
no goals