I think the equality should be the other way around and named something like mapAccumr_eq_map. Also I'm guessing the ⟨⟩ is type Unit, but I think a similar lemma applies for arbitrary types, as long as we don't depend on that.

You are right. Actually, the reverse lemma is already present as mapAccumr_redundant_state at the bottom of the file. I'll remove these two

I'm not a massive fan of lets in theorem statements, you almost always want to reduce them even if the resulting term is longer.

Hmm, here the let is on the right side of the equation, so I thought it would be fine; these lemmas are intended as rewrite rules, I don't expect a goal of exactly this type to come up. Then again, that does mean we are making the reverse rule <-mapAccumr_mapAccumr more difficult to use.

The reduction is a bit nasty: here is a before/after

  let m := (mapAccumr (fun x s =>
    let r₂ := f₂ x s.snd
    let r₁ := f₁ r₂.snd s.fst
    ((r₁.fst, r₂.fst), r₁.snd)
  ) xs (s₁, s₂))
  (m.fst.fst, m.snd) 

Turns into

(
  (mapAccumr (fun x s => (
    ((f₁ (f₂ x s.snd).snd s.fst).fst, (f₂ x s.snd).fst), (f₁ (f₂ x s.snd).snd s.fst).snd)
  ) xs (s₁, s₂)).fst.fst, 
  (mapAccumr (fun x s => (
    ((f₁ (f₂ x s.snd).snd s.fst).fst, (f₂ x s.snd).fst), (f₁ (f₂ x s.snd).snd s.fst).snd)
  ) xs (s₁, s₂)).snd
) 

I'll defer to you on whether the readability penalty is worth it

Is this not a duplication? It seems like it would already be there.

Neither apply? nor simp seem to find any such existing lemma, so I don't think we have it

I feel like this theorem can be generalized. Are there more general conditions where you can replace the state type with a different state type, that proves this lemma as a special case?

It probably can be, I'll have to think about it a bit more. I choose products in particular, because the earlier folding of nested mapAccumrs has a tendency to produce pairs with redundant state, so this theorem is needed to counterbalance that.

The most general way to relate two applications of mapAccumr, with potentially different states, is bisimulation. I've added bisimulation lemmas, and proven this result in terms of bisimulation

I'm not sure that this is a good simp lemma because we have a hypothesis.

As in, it won't work, or it's not considered appropriate?
I think it does work, but I can always add it to just the aesop ruleset, instead of as a simp-lemma

I think I might have changed my mind about the use of lets. It's very unreadable right now. Maybe the lets should be reintroduced on second thoughts.