Chain of compositions

Stream: general

[Antoine Labelle]

Let's say I have a goal of the form f1 ≫ f2 ≫ ... ≫ h = g1 ≫ g2 ≫ ... ≫ h with some long chain of compositions on both sides. What is the simplest way to remove the h and replace it by f1 ≫ f2 ≫ ... = g1 ≫ g2 ≫ ... ?

[Adam Topaz]

simp only [\l category.assoc], congr' 1, simp only [category.assoc] should work

[Adam Topaz]

Or you could do

suffices : f1  ≫ f2  ≫ ...   = g1  ≫ g2  ≫ ..., by rw reassoc_of this,

[Adam Topaz]

assuming f1 ≫ f2 ≫ ... = g1 ≫ g2 ≫ ... can be written down reasonably.

[Antoine Labelle]

Yeah, the thing is that f1, etc. all stand for long expressions, so I don't want to write them down. I'll try the first solution.

[Eric Wieser]

I assume apply assoc_of doesn't work?