-- Lean 4 proof step from Mathlib.RingTheory.Morita.Matrix (goal)
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i : ι
X Y : ModuleCat R
f : X ⟶ Y
⊢ Eq (α :=
    Functor.obj (Functor.comp (D := ModuleCat (Matrix ι ι R)) (ModuleCat.toMatrixModCat R ι) (toModuleCat R i)) X ⟶
      Functor.obj (𝟭 (ModuleCat R)) Y)
    (CategoryTheory.Functor.map
        (Functor.comp (D := ModuleCat (Matrix ι ι R)) (ModuleCat.toMatrixModCat R ι) (toModuleCat R i)) f ≫
      Iso.hom
        ((fun (X : ModuleCat R) ↦
            (LinearEquiv.toModuleIso
                (fromModuleCatToModuleCatLinearEquivtoModuleCatObj R (↑X : Type (max v u_1)) i ≪≫ₗ
                  fromModuleCatToModuleCatLinearEquiv R (↑X : Type (max v u_1)) i) :
              Iso (C := ModuleCat R)
                (ModuleCat.of R
                  (↑(Functor.obj
                        (Functor.comp (D := ModuleCat (Matrix ι ι R)) (ModuleCat.toMatrixModCat R ι) (toModuleCat R i))
                        (ModuleCat.of R (↑X : Type (max v u_1)))) :
                    Type (max v u_1)))
                (ModuleCat.of R (↑X : Type (max v u_1)))))
          Y))
    (Iso.hom
        ((fun (X : ModuleCat R) ↦
            (LinearEquiv.toModuleIso
                (fromModuleCatToModuleCatLinearEquivtoModuleCatObj R (↑X : Type (max v u_1)) i ≪≫ₗ
                  fromModuleCatToModuleCatLinearEquiv R (↑X : Type (max v u_1)) i) :
              Iso (C := ModuleCat R)
                (ModuleCat.of R
                  (↑(Functor.obj
                        (Functor.comp (D := ModuleCat (Matrix ι ι R)) (ModuleCat.toMatrixModCat R ι) (toModuleCat R i))
                        (ModuleCat.of R (↑X : Type (max v u_1)))) :
                    Type (max v u_1)))
                (ModuleCat.of R (↑X : Type (max v u_1)))))
          X) ≫
      CategoryTheory.Functor.map (𝟭 (ModuleCat R)) f)
have hf : ∀
  (x :
    (↑(Functor.obj (Functor.comp (D := ModuleCat (Matrix ι ι R)) (ModuleCat.toMatrixModCat R ι) (toModuleCat R i)) X) :
      Type (max v u_1))),
  Eq (α := (↑(Functor.obj (𝟭 (ModuleCat R)) Y) : Type (max v u_1)))
    ((ModuleCat.Hom.hom
            (CategoryTheory.Functor.map
                (Functor.comp (D := ModuleCat (Matrix ι ι R)) (ModuleCat.toMatrixModCat R ι) (toModuleCat R i)) f ≫
              Iso.hom
                ((fun (X : ModuleCat R) ↦
                    (LinearEquiv.toModuleIso
                        (fromModuleCatToModuleCatLinearEquivtoModuleCatObj R (↑X : Type (max v u_1)) i ≪≫ₗ
                          fromModuleCatToModuleCatLinearEquiv R (↑X : Type (max v u_1)) i) :
                      Iso (C := ModuleCat R)
                        (ModuleCat.of R
                          (↑(Functor.obj
                                (Functor.comp (D := ModuleCat (Matrix ι ι R)) (ModuleCat.toMatrixModCat R ι)
                                  (toModuleCat R i))
                                (ModuleCat.of R (↑X : Type (max v u_1)))) :
                            Type (max v u_1)))
                        (ModuleCat.of R (↑X : Type (max v u_1)))))
                  Y)) :
          (a : (↑((ModuleCat.toMatrixModCat R ι ⋙ toModuleCat R i).obj X) : Type (max v u_1))) →
            (↑((𝟭 (ModuleCat R)).obj Y) : Type (max v u_1)))
        x :
      (↑(Functor.obj (𝟭 (ModuleCat R)) Y) : Type (max v u_1)))
    ((ModuleCat.Hom.hom
            (Iso.hom
                ((fun (X : ModuleCat R) ↦
                    (LinearEquiv.toModuleIso
                        (fromModuleCatToModuleCatLinearEquivtoModuleCatObj R (↑X : Type (max v u_1)) i ≪≫ₗ
                          fromModuleCatToModuleCatLinearEquiv R (↑X : Type (max v u_1)) i) :
                      Iso (C := ModuleCat R)
                        (ModuleCat.of R
                          (↑(Functor.obj
                                (Functor.comp (D := ModuleCat (Matrix ι ι R)) (ModuleCat.toMatrixModCat R ι)
                                  (toModuleCat R i))
                                (ModuleCat.of R (↑X : Type (max v u_1)))) :
                            Type (max v u_1)))
                        (ModuleCat.of R (↑X : Type (max v u_1)))))
                  X) ≫
              CategoryTheory.Functor.map (𝟭 (ModuleCat R)) f) :
          (a : (↑((ModuleCat.toMatrixModCat R ι ⋙ toModuleCat R i).obj X) : Type (max v u_1))) →
            (↑((𝟭 (ModuleCat R)).obj Y) : Type (max v u_1)))
        x :
      (↑(Functor.obj (𝟭 (ModuleCat R)) Y) : Type (max v u_1)))
Tactic: ext