-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem pop_eq_of_push_eq {a b : α} {xs ys : Vector α n} (h : xs.push a = ys.push b) : xs = ys

Proof state:
α : Type u_1
n : Nat
a b : α
xs ys : Vector α n
h : xs.push a = ys.push b
⊢ xs = ys

Tactic:
cases xs

Result:
case mk
α : Type u_1
n : Nat
a b : α
ys : Vector α n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : { toArray := toArray✝, size_toArray := size_toArray✝ }.push a = ys.push b
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ } = ys

Proof state:
case mk
α : Type u_1
n : Nat
a b : α
ys : Vector α n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : { toArray := toArray✝, size_toArray := size_toArray✝ }.push a = ys.push b
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ } = ys

Tactic:
cases ys

Result:
case mk.mk
α : Type u_1
n : Nat
a b : α
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h :
  { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.push a =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.push b
⊢ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } = { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk.mk
α : Type u_1
n : Nat
a b : α
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : toArray✝¹.push a = toArray✝.push b
⊢ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } = { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simpa using Array.pop_eq_of_push_eq h

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
n : Nat
a b : α
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h :
  ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.push a).toArray =
    ({ toArray := toArray✝, size_toArray := size_toArray✝ }.push b).toArray
⊢ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } = { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp only [push_mk] at h

Result:
case mk.mk
α : Type u_1
n : Nat
a b : α
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : toArray✝¹.push a = toArray✝.push b
⊢ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } = { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk.mk
α : Type u_1
n : Nat
a b : α
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h :
  { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.push a =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.push b
⊢ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } = { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
replace h := congrArg Vector.toArray h

Result:
case mk.mk
α : Type u_1
n : Nat
a b : α
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h :
  ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.push a).toArray =
    ({ toArray := toArray✝, size_toArray := size_toArray✝ }.push b).toArray
⊢ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } = { toArray := toArray✝, size_toArray := size_toArray✝ }