Lean/Mathlib: List.getD_append lives in Mathlib.Data.List.GetD, and Classical if vs bif goals

In Mathlib v4.35, List.getD_append, List.getD_append_right and List.getD_eq_getElem (args: l d hn) live in Mathlib.Data.List.GetD. That file is not pulled in by the computability imports, so you get 'Unknown constant' until you import it explicitly. Second gotcha: goals like (bif b then 1 else 0) = if b = true then 1 else 0, where the if uses Classical.propDecidable, make cases b fail with 'generalize ... result is not type correct'. Sometimes they are even syntactically identical ifs with different Decidable instances, which rfl and simp only won't close. by_cases h : b = true <;> simp [h] closes both.