Theorem: Lean4Lean.UnionFind.rankD_push (Lean4Lean/Verify/UnionFind.lean)

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

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

State before:
case inr.inl
a : Nat
arr : Array UFNode
h✝¹ : ¬a < Array.size arr + 1
h✝ : a < Array.size arr
⊢ 0 = arr[a].rank
Tactic:
next h1 h2 => cases h1 (Nat.lt_succ_of_lt h2)
State after:
no goals

State before:
case inr.inr
a : Nat
arr : Array UFNode
h✝¹ : ¬a < Array.size arr + 1
h✝ : ¬a < Array.size arr
⊢ 0 = 0
Tactic:
simp [Array.get_push, *]
State after:
no goals

State before:
a : Nat
arr : Array UFNode
h1 : ¬a < Array.size arr + 1
h2 : a < Array.size arr
⊢ 0 = arr[a].rank
Tactic:
cases h1 (Nat.lt_succ_of_lt h2)
State after:
no goals