-- Module: Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
Goal:
b₀ b₁ : CommRingCat
f : b₀ ⟶ b₁
refine_3 :
  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 ≫ 𝟙 b₁)))
      (Cat.Hom.toFunctor ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f)))
    (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)
          ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) (𝟙 b₁)))
        (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 (𝟙 b₁)))
        (Bicategory.whiskerLeft ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f)
            (Iso.hom
              ((fun (R : CommRingCat.{u}) ↦
                  (Cat.Hom.isoMk (extendScalarsId (↑R : Type u)) :
                    (extendScalars (Hom.hom (𝟙 R))).toCatHom ≅
                      Functor.toCatHom
                        (𝟭
                          (↑((fun (R : CommRingCat.{u}) ↦ Cat.of.{u, u + 1} (ModuleCat (↑R : Type u))) R) :
                            Type (u + 1)))))
                b₁)) ≫
          Iso.hom
            (Bicategory.rightUnitor
              ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f)))))
    (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 ≫ 𝟙 b₁))
      ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f))
    (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) (𝟙 b₁)))
        (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 (𝟙 b₁)))
        (Bicategory.whiskerLeft ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f)
            (Iso.hom
              ((fun (R : CommRingCat.{u}) ↦
                  (Cat.Hom.isoMk (extendScalarsId (↑R : Type u)) :
                    (extendScalars (Hom.hom (𝟙 R))).toCatHom ≅
                      Functor.toCatHom
                        (𝟭
                          (↑((fun (R : CommRingCat.{u}) ↦ Cat.of.{u, u + 1} (ModuleCat (↑R : Type u))) R) :
                            Type (u + 1)))))
                b₁)) ≫
          Iso.hom
            (Bicategory.rightUnitor
              ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f))) :
      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 ≫ 𝟙 b₁))
        ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f))
    (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 ≫ 𝟙 b₁))
        ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f))

Tactic:
ext1