-- 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
⊢ Eq.{max (u + 1) (?u.11309 + 1)} (α :=
    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₂))))
    (((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₂))))
    (((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₂))))

Tactic:
tensor_ext

Premises used: ModuleCat.MonoidalCategory.tensor_ext