weird behaviour for LocallyDiscrete.mkPseudofunctor argument

Stream: mathlib4

[Edward van de Meent]

in #31807 i turn 1- and 2-morphisms in Cat into 1-field structures, and i came across the following issue:

import Mathlib

open CategoryTheory ModuleCat

def toFunctor {C D : Cat.{v, u}} (F : C ⟶ D) : C ⥤ D := F

def toNatTrans {C D : Cat.{v, u}} {F G : C ⟶ D} (η : F ⟶ G) : toFunctor F ⟶ toFunctor G := η

@[ext]
lemma ext {C D : Cat.{v,u}} {F G : C ⟶ D} {η₁ η₂ : F ⟶ G} (h : toNatTrans η₁ = toNatTrans η₂) :
  η₁ = η₂ := h

noncomputable def CommRingCat.moduleCatExtendScalarsPseudofunctor' :
    Pseudofunctor (LocallyDiscrete CommRingCat.{u}) Cat :=
  LocallyDiscrete.mkPseudofunctor
    (fun R ↦ Cat.of (ModuleCat.{u} R))
    (fun f ↦ (extendScalars f.hom).toCatHom)
    (fun R ↦ extendScalarsId R)
    (fun f g ↦ extendScalarsComp f.hom g.hom)
    (fun {W X Y Z} f g h ↦ by
      try generalize_proofs h'
      -- failed isDefEq types 4, ?self, (fun {b₀ b₁ b₂} f g => extendScalarsComp (Hom.hom f) (Hom.hom g)) (f ≫ g) h
      try ext1
      --     No applicable extensionality theorem found for type
      -- (fun {b b'} f => (extendScalars (Hom.hom f)).toCatHom) ((f ≫ g) ≫ h) ⟶
      --   (fun {b b'} f => (extendScalars (Hom.hom f)).toCatHom) (f ≫ g ≫ h)
      have foo := @LocallyDiscrete.mkPseudofunctor._proof_1 (CommRingCat.{u}) (Cat.{u,u + 1}) _ _
        (fun R ↦ Cat.of (ModuleCat.{u} R))
        (fun f ↦ (extendScalars (CommRingCat.Hom.hom f))) W X Y Z f g h
      ext1 -- works, suddenly
      -- generalize_proofs h' -- also works, suddenly
      apply extendScalars_assoc')
    (fun _ ↦ by
      ext1
      apply extendScalars_id_comp)
    (fun _ ↦ by
      ext1
      apply extendScalars_comp_id)

(the above is a version of my issue which works on current mathlib)
Does anyone have an idea what causes this issue?

[Edward van de Meent]

the issue seems somehow related to eta-reduction, but i'm having a tough time minimizing the issue in order to pinpoint its source, or even start figuring out a solution...

[Edward van de Meent]

another way i've discovered to circumvent this issue, is to use change _ = _...

[Edward van de Meent]

it makes me wonder if maybe both ext1 and generalize_proofs don't eta-reduce the parts of the goal they use before they do their magic?