`grind` annotations for OFE operations

In our development we have quite a few calc blocks such as:

theorem Agree.includedN {x y : Agree α} : x ≼{n} y ↔ y ≡{n}≡ y • x := by
  refine ⟨fun ⟨z, h⟩ => ?_, fun h => ⟨y, h.trans op_commN⟩⟩
  have hid := idemp (x := x) |>.symm
  calc
    y ≡{n}≡ x • z := h
    _ ≡{n}≡ (x • x) • z := .op_l (hid n)
    _ ≡{n}≡ x • (x • z) := CMRA.op_assocN.symm
    _ ≡{n}≡ x • y := h.symm.op_r
    _ ≡{n}≡ y • x := op_commN

In my opinion, this is a great way to structure these proofs! I even like it better than the the Rocq version which uses setoid rewriting, because you're able to actually read these proofs, without trying to mentally reconstruct what effect each step has on the goal.

I think they could be made even better if the proof terms were (mainly) inferred, and I think that grind might be the right tool to do that. Is it possible to add grind annotations to our codebase so that the bulk of the steps in these calc blocks are all resolved by grind?

Start with the calc block in the issue body and investigate whether Lean's grind can infer the proof terms for its equality steps. Identify representative OFE operations and determine what annotations are needed across the codebase; done means the bulk of these calc-block steps are resolved by grind without reducing proof readability.