case nil
ι : Type ?u.30314
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂✝ l₂ : List α
h : l₂ ≠ []
⊢ getLast ([] ++ l₂) (_ : [] ++ l₂ ≠ []) = getLast l₂ h

case cons
ι : Type ?u.30314
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂✝ l₂ : List α
h : l₂ ≠ []
head✝ : α
tail✝ : List α
ih : getLast (tail✝ ++ l₂) (_ : tail✝ ++ l₂ ≠ []) = getLast l₂ h
⊢ getLast (head✝ :: tail✝ ++ l₂) (_ : head✝ :: tail✝ ++ l₂ ≠ []) = getLast l₂ h
ι : Type ?u.30314
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ l₁ l₂ : List α
h : l₂ ≠ []
⊢ getLast (l₁ ++ l₂) (_ : l₁ ++ l₂ ≠ []) = getLast l₂ h
induction' l₁ with _ _ ih
no goals
case nil
ι : Type ?u.30314
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂✝ l₂ : List α
h : l₂ ≠ []
⊢ getLast ([] ++ l₂) (_ : [] ++ l₂ ≠ []) = getLast l₂ h
simp
case cons
ι : Type ?u.30314
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂✝ l₂ : List α
h : l₂ ≠ []
head✝ : α
tail✝ : List α
ih : getLast (tail✝ ++ l₂) (_ : tail✝ ++ l₂ ≠ []) = getLast l₂ h
⊢ getLast (head✝ :: (tail✝ ++ l₂)) (_ : head✝ :: (tail✝ ++ l₂) ≠ []) = getLast l₂ h
case cons
ι : Type ?u.30314
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂✝ l₂ : List α
h : l₂ ≠ []
head✝ : α
tail✝ : List α
ih : getLast (tail✝ ++ l₂) (_ : tail✝ ++ l₂ ≠ []) = getLast l₂ h
⊢ getLast (head✝ :: tail✝ ++ l₂) (_ : head✝ :: tail✝ ++ l₂ ≠ []) = getLast l₂ h
simp only [cons_append]
case cons
ι : Type ?u.30314
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂✝ l₂ : List α
h : l₂ ≠ []
head✝ : α
tail✝ : List α
ih : getLast (tail✝ ++ l₂) (_ : tail✝ ++ l₂ ≠ []) = getLast l₂ h
⊢ getLast (tail✝ ++ l₂) ?cons = getLast l₂ h

case cons
ι : Type ?u.30314
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂✝ l₂ : List α
h : l₂ ≠ []
head✝ : α
tail✝ : List α
ih : getLast (tail✝ ++ l₂) (_ : tail✝ ++ l₂ ≠ []) = getLast l₂ h
⊢ tail✝ ++ l₂ ≠ []
case cons
ι : Type ?u.30314
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂✝ l₂ : List α
h : l₂ ≠ []
head✝ : α
tail✝ : List α
ih : getLast (tail✝ ++ l₂) (_ : tail✝ ++ l₂ ≠ []) = getLast l₂ h
⊢ getLast (head✝ :: (tail✝ ++ l₂)) (_ : head✝ :: (tail✝ ++ l₂) ≠ []) = getLast l₂ h
rw [List.getLast_cons]
no goals
case cons
ι : Type ?u.30314
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂✝ l₂ : List α
h : l₂ ≠ []
head✝ : α
tail✝ : List α
ih : getLast (tail✝ ++ l₂) (_ : tail✝ ++ l₂ ≠ []) = getLast l₂ h
⊢ getLast (tail✝ ++ l₂) ?cons = getLast l₂ h

case cons
ι : Type ?u.30314
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂✝ l₂ : List α
h : l₂ ≠ []
head✝ : α
tail✝ : List α
ih : getLast (tail✝ ++ l₂) (_ : tail✝ ++ l₂ ≠ []) = getLast l₂ h
⊢ tail✝ ++ l₂ ≠ []
exact ih