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

case cons
ι : Type ?u.41156
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂ l₁ : List α
x head✝ : α
tail✝ : List α
h : x ∈ getLast? (head✝ :: tail✝)
⊢ x ∈ getLast? (l₁ ++ head✝ :: tail✝)
ι : Type ?u.41156
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ l₁ l₂ : List α
x : α
h : x ∈ getLast? l₂
⊢ x ∈ getLast? (l₁ ++ l₂)
cases l₂
no goals
case nil
ι : Type ?u.41156
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂ l₁ : List α
x : α
h : x ∈ getLast? []
⊢ x ∈ getLast? (l₁ ++ [])
contradiction
case cons
ι : Type ?u.41156
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂ l₁ : List α
x head✝ : α
tail✝ : List α
h : x ∈ getLast? (head✝ :: tail✝)
⊢ x ∈ getLast? (head✝ :: tail✝)
case cons
ι : Type ?u.41156
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂ l₁ : List α
x head✝ : α
tail✝ : List α
h : x ∈ getLast? (head✝ :: tail✝)
⊢ x ∈ getLast? (l₁ ++ head✝ :: tail✝)
rw [List.getLast?_append_cons]
no goals
case cons
ι : Type ?u.41156
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂ l₁ : List α
x head✝ : α
tail✝ : List α
h : x ∈ getLast? (head✝ :: tail✝)
⊢ x ∈ getLast? (head✝ :: tail✝)
exact h