no goals
ι : Type ?u.38004
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : Inhabited α
⊢ getLastI [] = Option.iget (getLast? [])
simp [getLastI, Inhabited.default]
no goals
ι : Type ?u.38004
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : Inhabited α
head✝¹ head✝ c : α
l : List α
⊢ getLastI (head✝¹ :: head✝ :: c :: l) = Option.iget (getLast? (head✝¹ :: head✝ :: c :: l))
simp [getLastI, getLastI_eq_getLast? (c :: l)]