α : Type u_1
a b : α
l : List α
⊢ Option.getD (some b) a = b
α : Type u_1
a b : α
l : List α
⊢ getLastD (l ++ [b]) a = b
rw [getLastD_eq_getLast?, getLast?_concat]
no goals
α : Type u_1
a b : α
l : List α
⊢ Option.getD (some b) a = b
rfl