Theorem: Lean.PersistentArray.size_push (Lean4Lean/Verify/Axioms.lean)

State before:
α : Type u_1
arr : PersistentArray α
x : α
⊢ (push arr x).size = arr.size + 1
Tactic:
simp [push]
State after:
α : Type u_1
arr : PersistentArray α
x : α
⊢ (if Array.size arr.tail + 1 < USize.toNat branching ∨ tooBig ≤ arr.size then
        { root := arr.root, tail := Array.push arr.tail x, size := arr.size + 1, shift := arr.shift,
          tailOff := arr.tailOff }
      else
        mkNewTail
          { root := arr.root, tail := Array.push arr.tail x, size := arr.size + 1, shift := arr.shift,
            tailOff := arr.tailOff }).size =
    arr.size + 1

State before:
α : Type u_1
arr : PersistentArray α
x : α
⊢ (if Array.size arr.tail + 1 < USize.toNat branching ∨ tooBig ≤ arr.size then
        { root := arr.root, tail := Array.push arr.tail x, size := arr.size + 1, shift := arr.shift,
          tailOff := arr.tailOff }
      else
        mkNewTail
          { root := arr.root, tail := Array.push arr.tail x, size := arr.size + 1, shift := arr.shift,
            tailOff := arr.tailOff }).size =
    arr.size + 1
Tactic:
split <;> [rfl; (simp [mkNewTail]; split <;> rfl)]
State after:
no goals

State before:
case inr
α : Type u_1
arr : PersistentArray α
x : α
h✝ : ¬(Array.size arr.tail + 1 < USize.toNat branching ∨ tooBig ≤ arr.size)
⊢ (mkNewTail
        { root := arr.root, tail := Array.push arr.tail x, size := arr.size + 1, shift := arr.shift,
          tailOff := arr.tailOff }).size =
    arr.size + 1
Tactic:
simp [mkNewTail]
State after:
case inr
α : Type u_1
arr : PersistentArray α
x : α
h✝ : ¬(Array.size arr.tail + 1 < USize.toNat branching ∨ tooBig ≤ arr.size)
⊢ (if arr.size + 1 ≤ USize.toNat (mul2Shift 1 (arr.shift + initShift)) then
        { root := insertNewLeaf arr.root (USize.ofNat arr.size) arr.shift (Array.push arr.tail x), tail := mkEmptyArray,
          size := arr.size + 1, shift := arr.shift, tailOff := arr.size + 1 }
      else
        {
          root :=
            PersistentArrayNode.node
              (Array.push (Array.push mkEmptyArray arr.root) (mkNewPath arr.shift (Array.push arr.tail x))),
          tail := #[], size := arr.size + 1, shift := arr.shift + initShift, tailOff := arr.size + 1 }).size =
    arr.size + 1

State before:
case inr
α : Type u_1
arr : PersistentArray α
x : α
h✝ : ¬(Array.size arr.tail + 1 < USize.toNat branching ∨ tooBig ≤ arr.size)
⊢ (if arr.size + 1 ≤ USize.toNat (mul2Shift 1 (arr.shift + initShift)) then
        { root := insertNewLeaf arr.root (USize.ofNat arr.size) arr.shift (Array.push arr.tail x), tail := mkEmptyArray,
          size := arr.size + 1, shift := arr.shift, tailOff := arr.size + 1 }
      else
        {
          root :=
            PersistentArrayNode.node
              (Array.push (Array.push mkEmptyArray arr.root) (mkNewPath arr.shift (Array.push arr.tail x))),
          tail := #[], size := arr.size + 1, shift := arr.shift + initShift, tailOff := arr.size + 1 }).size =
    arr.size + 1
Tactic:
split <;> rfl
State after:
no goals