Commit 2025-11-24 17:30 232d2578

fix(Computability/Tape): generalize simplification theorem Tape.write_mk' (#30821) Change the Tape.write_mk' simplification theorem to be more generally applicable, because in its current form, it can get into a simplification dead-end. Also add a theorem that can work with expressions of the form (Tape.mk L R).write b. The problem with the simplification dead-end is as follows: If we have an expression of the form (Tape.mk' L (ListBlank.cons a (ListBlank.mk R))).write b, the theorem Tape.write_mk' would be applicable, but lean instead uses ListBlank.cons_mk, which turns it into (Tape.mk' L (ListBlank.mk (a :: R))).write b and makes Tape.write_mk no longer applicable because it requires ListBlank.cons a R, reaching a dead-end.