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

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

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].parent else a) =
    if h : a < Array.size arr then arr[a].parent else a
Tactic:
split <;> split <;> try simp [Array.get_push, *]
State after:
case inl.inr
a : Nat
arr : Array UFNode
h✝¹ : a < Array.size arr + 1
h✝ : ¬a < Array.size arr
⊢ Array.size arr = a

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

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

State before:
case inl.inr
a : Nat
arr : Array UFNode
h✝¹ : a < Array.size arr + 1
h✝ : ¬a < Array.size arr
⊢ Array.size arr = a
Tactic:
next h1 h2 =>
simp [Nat.lt_succ] at h1 h2
exact Nat.le_antisymm h2 h1
State after:
no goals

State before:
a : Nat
arr : Array UFNode
h1 : a < Array.size arr + 1
h2 : ¬a < Array.size arr
⊢ Array.size arr = a
Tactic:
simp [Nat.lt_succ] at h1 h2
State after:
a : Nat
arr : Array UFNode
h1 : a ≤ Array.size arr
h2 : Array.size arr ≤ a
⊢ Array.size arr = a

State before:
a : Nat
arr : Array UFNode
h1 : a ≤ Array.size arr
h2 : Array.size arr ≤ a
⊢ Array.size arr = a
Tactic:
exact Nat.le_antisymm h2 h1
State after:
no goals

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

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