no goals
ι : Type ?u.34657
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
⊢ Option.isSome (getLast? []) = true ↔ [] ≠ []
simp
no goals
ι : Type ?u.34657
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
⊢ Option.isSome (getLast? [a]) = true ↔ [a] ≠ []
simp
no goals
ι : Type ?u.34657
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a b : α
l : List α
⊢ Option.isSome (getLast? (a :: b :: l)) = true ↔ a :: b :: l ≠ []
simp [@getLast?_isSome (b :: l)]