-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Pseudofunctor (goal)
Goal:
b₀ b₁ b₂ b₃ : CommRingCat
f : b₀ ⟶ b₁
g : b₁ ⟶ b₂
h : 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) ((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)))
have 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 sorry))
Tactic: ext1