Commit 2025-08-12 05:09 a3460c04

feat: better statement of flip_map_app (#28213) The left-hand-side of the @[simps] generated flip_map_app was:

@app C inst E inst_2
  { obj := fun j ↦ (F.obj j).obj X, map := fun {X_1 Y} f ↦ (F.map f).app X, map_id := ⋯, map_comp := ⋯ }
  { obj := fun j ↦ (F.obj j).obj Y, map := fun {X Y_1} f ↦ (F.map f).app Y, map_id := ⋯, map_comp := ⋯ } (F.flip.map f)
  j : { obj := fun j ↦ (F.obj j).obj X, map := fun {X_1 Y} f ↦ (F.map f).app X, map_id := ⋯, map_comp := ⋯ }.obj j ⟶
  { obj := fun j ↦ (F.obj j).obj Y, map := fun {X Y_1} f ↦ (F.map f).app Y, map_id := ⋯, map_comp := ⋯ }.obj j

It should be instead (and now is):

@app C inst E inst_2 (F.flip.obj d) (F.flip.obj d') (F.flip.map f) c : (F.flip.obj d).obj c ⟶ (F.flip.obj d').obj c  

Ideally simps would do this itself. @fpvandoorn, any ideas?