hygenic reassoc

Stream: mathlib4

[Matthew Ballard]

I came across the following reassoc'ed variant

example {C : Type u} [inst : Category C] {V W X Y : C}
  [inst : HasBinaryCoproduct X Y] (f : V ⟶ W) (g : X ⟶ V) (h : Y ⟶ V) {Z : C} (h : W ⟶ Z) :
  coprod.desc g h ≫ f ≫ h = coprod.desc (g ≫ f) (h ≫ f) ≫ h

Lean gets confused by the statement due to the two h's. I guess reassoc is not hygenic?

[Scott Morrison]

@Matthew Ballard, could you explain how this came up? (i.e. give an example with @[reassoc] in it). I had a quick look at the code for reassoc and am not immediately seeing the problem.

[Matthew Ballard]

I think I was confused but I will take another look

[Matthew Ballard]

Ah I remember (but haven't gone back and checked). I think it was just an issue with pretty printed version. I was copying declarations to test the claims of simpNF and got one with two h's.