Theorem: Array.get_pop (GMLInit/Data/Array/Basic.lean)

State before:
α : Type u_1
as : Array α
i : Nat
hi : i < as.pop.size
⊢ as.pop[i] = as[i]
Tactic:
rw [←as.get_eq_getElem ⟨i, get_pop.aux as hi⟩]
State after:
α : Type u_1
as : Array α
i : Nat
hi : i < as.pop.size
⊢ as.pop[i] = as.get ⟨i, ⋯⟩

State before:
α : Type u_1
as : Array α
i : Nat
hi : i < as.pop.size
⊢ as.pop[i] = as.get ⟨i, ⋯⟩
Tactic:
rw [←as.pop.get_eq_getElem ⟨i, hi⟩]
State after:
α : Type u_1
as : Array α
i : Nat
hi : i < as.pop.size
⊢ as.pop.get ⟨i, hi⟩ = as.get ⟨i, ⋯⟩

State before:
α : Type u_1
as : Array α
i : Nat
hi : i < as.pop.size
⊢ as.pop.get ⟨i, hi⟩ = as.get ⟨i, ⋯⟩
Tactic:
rw [get, get]
State after:
α : Type u_1
as : Array α
i : Nat
hi : i < as.pop.size
⊢ as.pop.data.get ⟨i, hi⟩ = as.data.get ⟨i, ⋯⟩

State before:
α : Type u_1
as : Array α
i : Nat
hi : i < as.pop.size
⊢ as.pop.data.get ⟨i, hi⟩ = as.data.get ⟨i, ⋯⟩
Tactic:
unfold pop
State after:
α : Type u_1
as : Array α
i : Nat
hi : i < as.pop.size
⊢ { data := as.data.dropLast }.data.get ⟨i, hi⟩ = as.data.get ⟨i, ⋯⟩

State before:
α : Type u_1
as : Array α
i : Nat
hi : i < as.pop.size
⊢ { data := as.data.dropLast }.data.get ⟨i, hi⟩ = as.data.get ⟨i, ⋯⟩
Tactic:
rw [List.get_dropLast]
State after:
no goals