-- Module: Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
Goal:
b₀ b₁ b₂ b₃ : CommRingCat
f : b₀ ⟶ b₁
g : b₁ ⟶ b₂
h : b₂ ⟶ b₃
refine_1 :
  Eq.{u + 2} (α :=
    Quiver.Hom (V :=
      (↑(Cat.of (ModuleCat (↑b₀ : Type u))) : Type (u + 1)) ⥤ (↑(Cat.of (ModuleCat (↑b₃ : Type u))) : Type (u + 1)))
      (Cat.Hom.toFunctor
        ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) ((f ≫ g) ≫ h)))
      (Cat.Hom.toFunctor
        ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) (f ≫ g ≫ h))))
    (Cat.Hom₂.toNatTrans
      (CategoryStruct.comp (Y :=
        CategoryStruct.comp (Y := (fun (R : CommRingCat.{u}) ↦ Cat.of.{u, u + 1} (ModuleCat (↑R : Type u))) b₂)
          ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) (f ≫ g))
          ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) h))
        (Iso.hom
          ((fun {b₀ b₁ b₂ : CommRingCat.{u}} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) ↦
              Cat.Hom.isoMk (extendScalarsComp (Hom.hom f) (Hom.hom g)))
            (f ≫ g) h))
        (CategoryStruct.comp (Y :=
          CategoryStruct.comp (Y := (fun (R : CommRingCat.{u}) ↦ Cat.of.{u, u + 1} (ModuleCat (↑R : Type u))) b₂)
            (CategoryStruct.comp (Y := (fun (R : CommRingCat.{u}) ↦ Cat.of.{u, u + 1} (ModuleCat (↑R : Type u))) b₁)
              ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f)
              ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) g))
            ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) h))
          (Bicategory.whiskerRight
            (Iso.hom
              ((fun {b₀ b₁ b₂ : CommRingCat.{u}} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) ↦
                  Cat.Hom.isoMk (extendScalarsComp (Hom.hom f) (Hom.hom g)))
                f g))
            ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) h))
          (Iso.hom
              (Bicategory.associator
                ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f)
                ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) g)
                ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) h)) ≫
            CategoryStruct.comp (Y :=
              CategoryStruct.comp (Y := (fun (R : CommRingCat.{u}) ↦ Cat.of.{u, u + 1} (ModuleCat (↑R : Type u))) b₁)
                ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f)
                ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) (g ≫ h)))
              (Bicategory.whiskerLeft
                ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f)
                (Iso.inv
                  ((fun {b₀ b₁ b₂ : CommRingCat.{u}} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) ↦
                      Cat.Hom.isoMk (extendScalarsComp (Hom.hom f) (Hom.hom g)))
                    g h)))
              (Iso.inv
                ((fun {b₀ b₁ b₂ : CommRingCat.{u}} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) ↦
                    Cat.Hom.isoMk (extendScalarsComp (Hom.hom f) (Hom.hom g)))
                  f (g ≫ h)))))))
    (Cat.Hom₂.toNatTrans (eqToHom ⋯))
⊢ Eq (α :=
    Quiver.Hom (V :=
      Quiver.Hom (V := Cat) ((fun (R : CommRingCat.{u}) ↦ Cat.of.{u, u + 1} (ModuleCat (↑R : Type u))) b₀)
        ((fun (R : CommRingCat.{u}) ↦ Cat.of.{u, u + 1} (ModuleCat (↑R : Type u))) b₃))
      ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) ((f ≫ g) ≫ h))
      ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) (f ≫ g ≫ h)))
    (CategoryStruct.comp (Y :=
        CategoryStruct.comp (Y := (fun (R : CommRingCat.{u}) ↦ Cat.of.{u, u + 1} (ModuleCat (↑R : Type u))) b₂)
          ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) (f ≫ g))
          ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) h))
        (Iso.hom
          ((fun {b₀ b₁ b₂ : CommRingCat.{u}} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) ↦
              Cat.Hom.isoMk (extendScalarsComp (Hom.hom f) (Hom.hom g)))
            (f ≫ g) h))
        (CategoryStruct.comp (Y :=
          CategoryStruct.comp (Y := (fun (R : CommRingCat.{u}) ↦ Cat.of.{u, u + 1} (ModuleCat (↑R : Type u))) b₂)
            (CategoryStruct.comp (Y := (fun (R : CommRingCat.{u}) ↦ Cat.of.{u, u + 1} (ModuleCat (↑R : Type u))) b₁)
              ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f)
              ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) g))
            ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) h))
          (Bicategory.whiskerRight
            (Iso.hom
              ((fun {b₀ b₁ b₂ : CommRingCat.{u}} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) ↦
                  Cat.Hom.isoMk (extendScalarsComp (Hom.hom f) (Hom.hom g)))
                f g))
            ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) h))
          (Iso.hom
              (Bicategory.associator
                ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f)
                ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) g)
                ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) h)) ≫
            CategoryStruct.comp (Y :=
              CategoryStruct.comp (Y := (fun (R : CommRingCat.{u}) ↦ Cat.of.{u, u + 1} (ModuleCat (↑R : Type u))) b₁)
                ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f)
                ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) (g ≫ h)))
              (Bicategory.whiskerLeft
                ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f)
                (Iso.inv
                  ((fun {b₀ b₁ b₂ : CommRingCat.{u}} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) ↦
                      Cat.Hom.isoMk (extendScalarsComp (Hom.hom f) (Hom.hom g)))
                    g h)))
              (Iso.inv
                ((fun {b₀ b₁ b₂ : CommRingCat.{u}} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) ↦
                    Cat.Hom.isoMk (extendScalarsComp (Hom.hom f) (Hom.hom g)))
                  f (g ≫ h))))) :
      Quiver.Hom (V :=
        Quiver.Hom (V := Cat) ((fun (R : CommRingCat.{u}) ↦ Cat.of.{u, u + 1} (ModuleCat (↑R : Type u))) b₀)
          ((fun (R : CommRingCat.{u}) ↦ Cat.of.{u, u + 1} (ModuleCat (↑R : Type u))) b₃))
        ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) ((f ≫ g) ≫ h))
        ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) (f ≫ g ≫ h)))
    (eqToHom ⋯ :
      Quiver.Hom (V :=
        Quiver.Hom (V := Cat) ((fun (R : CommRingCat.{u}) ↦ Cat.of.{u, u + 1} (ModuleCat (↑R : Type u))) b₀)
          ((fun (R : CommRingCat.{u}) ↦ Cat.of.{u, u + 1} (ModuleCat (↑R : Type u))) b₃))
        ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) ((f ≫ g) ≫ h))
        ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) (f ≫ g ≫ h)))

Tactic:
ext1