-- Module: Mathlib.RingTheory.Morita.Matrix
Goal:
R : Type u
ι : Type v
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
i : ι
X Y : ModuleCat R
f : X ⟶ Y
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)))
⊢ 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)

Tactic:
ext