TW: violence

Stream: new members

[Martin Dvořák]

Would you punch me into my face for writing a spaghetti proof like the following?

  repeat {
    rw list.map_append at hyppp,
  },
  rw list.join_append at hyppp,
  rw list.join_append at hyppp,
  repeat {
    rw list.append_assoc at hyppp,
  },
  rw list.map_take at hyppp,
  rw list.map_take at hyppp,
  rw list.append_right_inj at hyppp,
  repeat {
    rw ←list.append_assoc at hyppp,
  },
  rw list.map_drop at hyppp,
  rw list.map_drop at hyppp,
  rw list.append_left_inj at hyppp,
  rw list.map_singleton at hyppp,
  rw list.map_singleton at hyppp,
  rw list.join_singleton at hyppp,
  rw list.append_left_inj at hyppp,
  rw list.nth_le_nth mltx,
  apply congr_arg,
  apply wrap_str_inj,
  rw hyppp,
  rw list.map_append_append,
  rw list.map_take,
  rw list.nth_le_map,
  swap, {
    exact mltx,
  },
  rw list.map_drop,
  rw list.map_append_append,
  rw list.map_singleton,
  repeat {
    rw ←list.append_assoc,
  },
  refl,

[Kyle Miller]

No need for violence of course, but this looks like a great place to use simp. Like

  simp only [list.map_append, list.join_append, list.append_assoc, list.map_take, list.append_right_inj] at hyppp,
  simp only [←list.append_assoc, list.map_drop, list.append_left_inj, list.map_singleton, list.join_singleton] at hyppp,
  -- etc...

I'd also wonder whether there are some sub-lemmas that might be useful.

Floris also suggests tactic#simp_rw

[Martin Dvořák]

I am yet to refactor it a little bit, but that's not my point. As for sub-lemmas, I usually do a several levels of decomposition, but then I typically beat "leaf lemmas" in such an awkward way.

[Martin Dvořák]

As for simp_rw I only learnt it existed a few days ago, but I already made use of it!