working with reassoc_of%

Stream: mathlib4

[Jack McKoen]

If I have a problem like the following, I can use reassoc_of% to close the goal. However, I would like a way to reduce the goal to proving f ≫ g = f' ≫ g' instead (in my case I don't have a hypothesis H but cat_disch is able to figure it out). How can I accomplish this nicely?

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.Tactic.CategoryTheory.Reassoc

universe v u

open CategoryTheory

variable {C : Type u} [Category.{v} C]

example {A B X Y : C} (f f' : A ⟶ B) (g g' : B ⟶ X) (h : X ⟶ Y) (H : f ≫ g = f' ≫ g') :
    f ≫ g ≫ h = f' ≫ g' ≫ h := by
  apply reassoc_of% H

[Dagur Asgeirsson]

simp only [<- Category.assoc]; congr ?

[Jack McKoen]

of course, but in my option this isn't very nice. then my proof looks like

simp only [a lot of lemmas]
simp only [<- Category.assoc]
congr 1
cat_disch

and I was hoping this could be done in a better way

[Adam Topaz]

suffices … by simp [this] maybe?

[Jack McKoen]

unfortunately ... is very long and cumbersome in my case

[Andrew Yang]

Perhaps it would be useful to have a congr tactic that knows about associativity.
E.g. if I have a goal a >> b >> c >> d = a >> b1 >> b2 >> c >> d', I can do some sort of congr that turns it into b = b1 >> b2 and d = d'.

[Adam Topaz]

Yes please!