no goals
s : String
⊢ back s = List.getLastD s.data default
match s, s.1.eq_nil_or_concat with
| ⟨_⟩, .inl rfl => rfl
| ⟨_⟩, .inr ⟨cs, c, rfl⟩ => simp [back, prev_of_valid, get_of_valid]
no goals
s : String
⊢ back { data := [] } = List.getLastD { data := [] }.data default
rfl
no goals
s : String
cs : List Char
c : Char
⊢ back { data := cs ++ [c] } = List.getLastD { data := cs ++ [c] }.data default
simp [back, prev_of_valid, get_of_valid]