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

State before:
i : Nat
arr : Array UFNode
⊢ rankD (Array.push arr { parent := Array.size arr, rank := 0 }) i = rankD arr i
Tactic:
simp [rankD, 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 }).rank
    else 0) =
    if h : i < Array.size arr then arr[i].rank else 0

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 }).rank
    else 0) =
    if h : i < Array.size arr then arr[i].rank else 0
Tactic:
split <;> split <;> first | simp | cases ‹¬_› (Nat.lt_succ_of_lt ‹_›)
State after:
no goals

State before:
case inr.inr
i : Nat
arr : Array UFNode
h✝¹ : ¬i < Array.size arr + 1
h✝ : ¬i < Array.size arr
⊢ 0 = 0
Tactic:
simp
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
⊢ 0 = arr[i].rank
Tactic:
cases ‹¬_› (Nat.lt_succ_of_lt ‹_›)
State after:
no goals