Theorem: Array.size_pop? (LeanSAT/Upstream/ToStd.lean)

State before:
α✝ : Type u_1
A' : Array α✝
a : α✝
A : Array α✝
⊢ pop? A = some (A', a) → size A' + 1 = size A
Tactic:
rcases A with ⟨h,t⟩
  <;> simp [pop?, back?, getElem?, pop]
State after:
case mk.cons
α✝ : Type u_1
A' : Array α✝
a head✝ : α✝
tail✝ : List α✝
⊢ { data := List.dropLast (head✝ :: tail✝) } = A' →
    { data := head✝ :: tail✝ }[List.length tail✝] = a → size A' = List.length tail✝

State before:
case mk.cons
α✝ : Type u_1
A' : Array α✝
a head✝ : α✝
tail✝ : List α✝
⊢ { data := List.dropLast (head✝ :: tail✝) } = A' →
    { data := head✝ :: tail✝ }[List.length tail✝] = a → size A' = List.length tail✝
Tactic:
rintro rfl
State after:
case mk.cons
α✝ : Type u_1
a head✝ : α✝
tail✝ : List α✝
⊢ { data := head✝ :: tail✝ }[List.length tail✝] = a →
    size { data := List.dropLast (head✝ :: tail✝) } = List.length tail✝

State before:
case mk.cons
α✝ : Type u_1
a head✝ : α✝
tail✝ : List α✝
⊢ { data := head✝ :: tail✝ }[List.length tail✝] = a →
    size { data := List.dropLast (head✝ :: tail✝) } = List.length tail✝
Tactic:
simp
State after:
no goals