-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Pseudofunctor (goal)
Goal:
b₀ b₁ : CommRingCat
f : b₀ ⟶ b₁
⊢ 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) (𝟙 b₀ ≫ f))
      ((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) (𝟙 b₀))
          ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f))
        (Iso.hom
          ((fun {b₀ b₁ b₂ : CommRingCat.{u}} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) ↦
              Cat.Hom.isoMk (extendScalarsComp (Hom.hom f) (Hom.hom g)))
            (𝟙 b₀) f))
        (Bicategory.whiskerRight
            (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₀))
            ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f) ≫
          Iso.hom
            (Bicategory.leftUnitor
              ((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) (𝟙 b₀ ≫ f))
        ((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) (𝟙 b₀ ≫ f))
        ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f))
have refine_2 : 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) (𝟙 b₀ ≫ f)))
    (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) (𝟙 b₀))
        ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f))
      (Iso.hom
        ((fun {b₀ b₁ b₂ : CommRingCat.{u}} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) ↦
            Cat.Hom.isoMk (extendScalarsComp (Hom.hom f) (Hom.hom g)))
          (𝟙 b₀) f))
      (Bicategory.whiskerRight
          (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₀))
          ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f) ≫
        Iso.hom
          (Bicategory.leftUnitor
            ((fun {b b' : CommRingCat.{u}} (f : b ⟶ b') ↦ (extendScalars (Hom.hom f)).toCatHom) f)))))
  (Cat.Hom₂.toNatTrans (eqToHom sorry))
Tactic: ext1