Theorem: Array.back'_eq_data_getLast (Algdata/Data/Array/Basic.lean)

State before:
α : Type u
β : Type v
as : Array α
h✝ : size as > 0
l : List α
h : List.length l > 0
hc : l = []
⊢ False
Tactic:
cases hc
State after:
case refl
α : Type u
β : Type v
as : Array α
h✝ : size as > 0
h : List.length [] > 0
⊢ False

State before:
case refl
α : Type u
β : Type v
as : Array α
h✝ : size as > 0
h : List.length [] > 0
⊢ False
Tactic:
cases h
State after:
no goals

State before:
α : Type u
β : Type v
as : Array α
h : size as > 0
⊢ back' as h = List.getLast as.data (_ : as.data ≠ [])
Tactic:
rw [List.getLast_eq_get]
State after:
α : Type u
β : Type v
as : Array α
h : size as > 0
⊢ back' as h =
    List.get as.data { val := List.length as.data - 1, isLt := (_ : List.length as.data - 1 < List.length as.data) }

State before:
α : Type u
β : Type v
as : Array α
h : size as > 0
⊢ back' as h =
    List.get as.data { val := List.length as.data - 1, isLt := (_ : List.length as.data - 1 < List.length as.data) }
Tactic:
rfl
State after:
no goals