-- Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
this : Algebra R S := f.toAlgebra
M₁ M₁' : ModuleCat R
g : M₁ ⟶ M₁'
M₂ : ModuleCat R
x : (↑M₁ : Type u)
x_1 : (↑M₂ : Type u)
⊢ Eq (α :=
    (↑(Functor.obj.{max u ?u.11309, max u ?u.11309, max (u + 1) (?u.11309 + 1), max (u + 1) (?u.11309 + 1)}
          (restrictScalars f)
          (tensorObj (𝒞 := moduleCategory S) ((extendScalars f).obj M₁') ((extendScalars f).obj M₂))) :
      Type u))
    (((Hom.hom.{u, u} (R := R) (A := tensorObj (𝒞 := moduleCategory R) M₁ M₂) (B :=
              Functor.obj.{max u ?u.11309, max u ?u.11309, max (u + 1) (?u.11309 + 1), max (u + 1) (?u.11309 + 1)}
                (restrictScalars f)
                (tensorObj (𝒞 := moduleCategory S) ((extendScalars f).obj M₁') ((extendScalars f).obj M₂)))
              (((Adjunction.homEquiv.{max u ?u.11309, max u ?u.11309, max (u + 1) (?u.11309 + 1),
                          max (u + 1) (?u.11309 + 1)}
                        (extendRestrictScalarsAdj f) (tensorObj (𝒞 := moduleCategory R) M₁ M₂)
                        (tensorObj (𝒞 := moduleCategory S) ((extendScalars f).obj M₁') ((extendScalars f).obj M₂)) :
                      Equiv.{(max u ?u.11309) + 1, (max u ?u.11309) + 1}
                        (Quiver.Hom.{max u ?u.11309, max (u + 1) (?u.11309 + 1)}
                          (Functor.obj.{max u ?u.11309, max u ?u.11309, max (u + 1) (?u.11309 + 1),
                              max (u + 1) (?u.11309 + 1)}
                            (extendScalars f) (tensorObj (𝒞 := moduleCategory R) M₁ M₂))
                          (tensorObj (𝒞 := moduleCategory S) ((extendScalars f).obj M₁') ((extendScalars f).obj M₂)))
                        (Quiver.Hom.{max u ?u.11309, max (u + 1) (?u.11309 + 1)}
                          (tensorObj (𝒞 := moduleCategory R) M₁ M₂)
                          (Functor.obj.{max u ?u.11309, max u ?u.11309, max (u + 1) (?u.11309 + 1),
                              max (u + 1) (?u.11309 + 1)}
                            (restrictScalars f)
                            (tensorObj (𝒞 := moduleCategory S) ((extendScalars f).obj M₁')
                              ((extendScalars f).obj M₂))))) :
                    (a : (extendScalars f).obj (M₁ ⊗ M₂) ⟶ (extendScalars f).obj M₁' ⊗ (extendScalars f).obj M₂) →
                      M₁ ⊗ M₂ ⟶ (restrictScalars f).obj ((extendScalars f).obj M₁' ⊗ (extendScalars f).obj M₂))
                  (Iso.inv
                      ((fun (M₁ M₂ : ModuleCat R) ↦
                          (LinearEquiv.toModuleIso ?m.93 :
                            Iso (C := ModuleCat S)
                              (of S
                                ((↑((extendScalars f).obj M₁) : Type u) ⊗[S] (↑((extendScalars f).obj M₂) : Type u)))
                              (of S
                                ((↑((restrictScalars f).obj (of S S)) : Type u) ⊗[R]
                                  (↑(tensorObj (𝒞 := moduleCategory R) M₁ M₂) : Type u)))))
                        M₁ M₂) ≫
                    (extendScalars f).map g ▷ (extendScalars f).obj M₂) :
                Quiver.Hom.{max u ?u.11309, max (u + 1) (?u.11309 + 1)} (tensorObj (𝒞 := moduleCategory R) M₁ M₂)
                  (Functor.obj.{max u ?u.11309, max u ?u.11309, max (u + 1) (?u.11309 + 1), max (u + 1) (?u.11309 + 1)}
                    (restrictScalars f)
                    (tensorObj (𝒞 := moduleCategory S) ((extendScalars f).obj M₁') ((extendScalars f).obj M₂)))) :
            (↑(tensorObj (𝒞 := moduleCategory R) M₁ M₂) : Type u) →ₗ[R]
              (↑(Functor.obj.{max u ?u.11309, max u ?u.11309, max (u + 1) (?u.11309 + 1), max (u + 1) (?u.11309 + 1)}
                    (restrictScalars f)
                    (tensorObj (𝒞 := moduleCategory S) ((extendScalars f).obj M₁') ((extendScalars f).obj M₂))) :
                Type u)) :
          (a : (↑(M₁ ⊗ M₂) : Type u)) →
            (↑((restrictScalars f).obj ((extendScalars f).obj M₁' ⊗ (extendScalars f).obj M₂)) : Type u))
        (x ⊗ₜ[R] x_1) :
      (↑(Functor.obj.{max u ?u.11309, max u ?u.11309, max (u + 1) (?u.11309 + 1), max (u + 1) (?u.11309 + 1)}
            (restrictScalars f)
            (tensorObj (𝒞 := moduleCategory S) ((extendScalars f).obj M₁') ((extendScalars f).obj M₂))) :
        Type u))
    (((Hom.hom.{u, u} (R := R) (A := tensorObj (𝒞 := moduleCategory R) M₁ M₂) (B :=
              Functor.obj.{max u ?u.11309, max u ?u.11309, max (u + 1) (?u.11309 + 1), max (u + 1) (?u.11309 + 1)}
                (restrictScalars f)
                (tensorObj (𝒞 := moduleCategory S) ((extendScalars f).obj M₁') ((extendScalars f).obj M₂)))
              (((Adjunction.homEquiv.{max u ?u.11309, max u ?u.11309, max (u + 1) (?u.11309 + 1),
                          max (u + 1) (?u.11309 + 1)}
                        (extendRestrictScalarsAdj f) (tensorObj (𝒞 := moduleCategory R) M₁ M₂)
                        (tensorObj (𝒞 := moduleCategory S) ((extendScalars f).obj M₁') ((extendScalars f).obj M₂)) :
                      Equiv.{(max u ?u.11309) + 1, (max u ?u.11309) + 1}
                        (Quiver.Hom.{max u ?u.11309, max (u + 1) (?u.11309 + 1)}
                          (Functor.obj.{max u ?u.11309, max u ?u.11309, max (u + 1) (?u.11309 + 1),
                              max (u + 1) (?u.11309 + 1)}
                            (extendScalars f) (tensorObj (𝒞 := moduleCategory R) M₁ M₂))
                          (tensorObj (𝒞 := moduleCategory S) ((extendScalars f).obj M₁') ((extendScalars f).obj M₂)))
                        (Quiver.Hom.{max u ?u.11309, max (u + 1) (?u.11309 + 1)}
                          (tensorObj (𝒞 := moduleCategory R) M₁ M₂)
                          (Functor.obj.{max u ?u.11309, max u ?u.11309, max (u + 1) (?u.11309 + 1),
                              max (u + 1) (?u.11309 + 1)}
                            (restrictScalars f)
                            (tensorObj (𝒞 := moduleCategory S) ((extendScalars f).obj M₁')
                              ((extendScalars f).obj M₂))))) :
                    (a : (extendScalars f).obj (M₁ ⊗ M₂) ⟶ (extendScalars f).obj M₁' ⊗ (extendScalars f).obj M₂) →
                      M₁ ⊗ M₂ ⟶ (restrictScalars f).obj ((extendScalars f).obj M₁' ⊗ (extendScalars f).obj M₂))
                  ((extendScalars f).map (g ▷ M₂) ≫
                    Iso.inv
                      ((fun (M₁ M₂ : ModuleCat R) ↦
                          (LinearEquiv.toModuleIso ?m.93 :
                            Iso (C := ModuleCat S)
                              (of S
                                ((↑((extendScalars f).obj M₁) : Type u) ⊗[S] (↑((extendScalars f).obj M₂) : Type u)))
                              (of S
                                ((↑((restrictScalars f).obj (of S S)) : Type u) ⊗[R]
                                  (↑(tensorObj (𝒞 := moduleCategory R) M₁ M₂) : Type u)))))
                        M₁' M₂)) :
                Quiver.Hom.{max u ?u.11309, max (u + 1) (?u.11309 + 1)} (tensorObj (𝒞 := moduleCategory R) M₁ M₂)
                  (Functor.obj.{max u ?u.11309, max u ?u.11309, max (u + 1) (?u.11309 + 1), max (u + 1) (?u.11309 + 1)}
                    (restrictScalars f)
                    (tensorObj (𝒞 := moduleCategory S) ((extendScalars f).obj M₁') ((extendScalars f).obj M₂)))) :
            (↑(tensorObj (𝒞 := moduleCategory R) M₁ M₂) : Type u) →ₗ[R]
              (↑(Functor.obj.{max u ?u.11309, max u ?u.11309, max (u + 1) (?u.11309 + 1), max (u + 1) (?u.11309 + 1)}
                    (restrictScalars f)
                    (tensorObj (𝒞 := moduleCategory S) ((extendScalars f).obj M₁') ((extendScalars f).obj M₂))) :
                Type u)) :
          (a : (↑(M₁ ⊗ M₂) : Type u)) →
            (↑((restrictScalars f).obj ((extendScalars f).obj M₁' ⊗ (extendScalars f).obj M₂)) : Type u))
        (x ⊗ₜ[R] x_1) :
      (↑(Functor.obj.{max u ?u.11309, max u ?u.11309, max (u + 1) (?u.11309 + 1), max (u + 1) (?u.11309 + 1)}
            (restrictScalars f)
            (tensorObj (𝒞 := moduleCategory S) ((extendScalars f).obj M₁') ((extendScalars f).obj M₂))) :
        Type u))

Tactic:
rfl

Premises used: rfl