-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem eq_push_pop_back!_of_size_ne_zero [Inhabited α] {as : Array α} (h : as.size ≠ 0) :
    as = as.pop.push as.back!

Proof state:
case h₂
α : Type u_1
inst✝ : Inhabited α
as : Array α
h : as.size ≠ 0
⊢ ∀ (i : Nat) (hi₁ : i < as.size) (hi₂ : i < (as.pop.push as.back!).size), as[i] = (as.pop.push as.back!)[i]

Tactic:
intros i h h'

Result:
case h₂
α : Type u_1
inst✝ : Inhabited α
as : Array α
h✝ : as.size ≠ 0
i : Nat
h : i < as.size
h' : i < (as.pop.push as.back!).size
⊢ as[i] = (as.pop.push as.back!)[i]

Proof state:
case refl
α : Type u_1
inst✝ : Inhabited α
as : Array α
h✝ : as.size ≠ 0
h : as.pop.size < as.size
h' : as.pop.size < (as.pop.push as.back!).size
hlt : ¬as.pop.size < as.pop.size
⊢ as[as.pop.size] = as[as.size - 1]!

Tactic:
simp [← getElem!_pos]

Result:
no goals

Proof state:
case h₂
α : Type u_1
inst✝ : Inhabited α
as : Array α
h✝ : as.size ≠ 0
i : Nat
h : i < as.size
h' : i < (as.pop.push as.back!).size
⊢ as[i] = (as.pop.push as.back!)[i]

Tactic:
if hlt : i < as.pop.size then
  rw [getElem_push_lt (h:=hlt), getElem_pop]
else
  have heq : i = as.pop.size :=
    Nat.le_antisymm (size_pop .. ▸ Nat.le_pred_of_lt h) (Nat.le_of_not_gt hlt)
  cases heq
  rw [getElem_push_eq, back!]
  simp [← getElem!_pos]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Inhabited α
as : Array α
h : as.size ≠ 0
⊢ as = as.pop.push as.back!

Tactic:
apply ext

Result:
case h₁
α : Type u_1
inst✝ : Inhabited α
as : Array α
h : as.size ≠ 0
⊢ as.size = (as.pop.push as.back!).size

case h₂
α : Type u_1
inst✝ : Inhabited α
as : Array α
h : as.size ≠ 0
⊢ ∀ (i : Nat) (hi₁ : i < as.size) (hi₂ : i < (as.pop.push as.back!).size), as[i] = (as.pop.push as.back!)[i]

Proof state:
α : Type u_1
inst✝ : Inhabited α
as : Array α
h✝ : as.size ≠ 0
i : Nat
h : i < as.size
h' : i < (as.pop.push as.back!).size
hlt : ¬i < as.pop.size
heq : i = as.pop.size
⊢ as[i] = (as.pop.push as.back!)[i]

Tactic:
cases heq

Result:
case refl
α : Type u_1
inst✝ : Inhabited α
as : Array α
h✝ : as.size ≠ 0
h : as.pop.size < as.size
h' : as.pop.size < (as.pop.push as.back!).size
hlt : ¬as.pop.size < as.pop.size
⊢ as[as.pop.size] = (as.pop.push as.back!)[as.pop.size]

Proof state:
α : Type u_1
inst✝ : Inhabited α
as : Array α
h✝ : as.size ≠ 0
i : Nat
h : i < as.size
h' : i < (as.pop.push as.back!).size
hlt : ¬i < as.pop.size
⊢ as[i] = (as.pop.push as.back!)[i]

Tactic:
have heq : i = as.pop.size :=
  Nat.le_antisymm (size_pop .. ▸ Nat.le_pred_of_lt h) (Nat.le_of_not_gt hlt)

Result:
α : Type u_1
inst✝ : Inhabited α
as : Array α
h✝ : as.size ≠ 0
i : Nat
h : i < as.size
h' : i < (as.pop.push as.back!).size
hlt : ¬i < as.pop.size
heq : i = as.pop.size
⊢ as[i] = (as.pop.push as.back!)[i]

Proof state:
α : Type u_1
inst✝ : Inhabited α
as : Array α
h✝ : as.size ≠ 0
i : Nat
h : i < as.size
h' : i < (as.pop.push as.back!).size
hlt : i < as.pop.size
⊢ as[i] = (as.pop.push as.back!)[i]

Tactic:
rw [getElem_push_lt (h:=hlt), getElem_pop]

Result:
no goals

Proof state:
case h₁
α : Type u_1
inst✝ : Inhabited α
as : Array α
h : as.size ≠ 0
⊢ as.size = (as.pop.push as.back!).size

Tactic:
simp [Nat.sub_add_cancel (Nat.zero_lt_of_ne_zero h)]

Result:
no goals

Proof state:
case refl
α : Type u_1
inst✝ : Inhabited α
as : Array α
h✝ : as.size ≠ 0
h : as.pop.size < as.size
h' : as.pop.size < (as.pop.push as.back!).size
hlt : ¬as.pop.size < as.pop.size
⊢ as[as.pop.size] = (as.pop.push as.back!)[as.pop.size]

Tactic:
rw [getElem_push_eq, back!]

Result:
case refl
α : Type u_1
inst✝ : Inhabited α
as : Array α
h✝ : as.size ≠ 0
h : as.pop.size < as.size
h' : as.pop.size < (as.pop.push as.back!).size
hlt : ¬as.pop.size < as.pop.size
⊢ as[as.pop.size] = as[as.size - 1]!