-- Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
lemma homEquiv_extendScalarsComp (M : ModuleCat R₁) :
    (extendRestrictScalarsAdj (f₂₃.comp f₁₂)).homEquiv _ _
      ((extendScalarsComp f₁₂ f₂₃).hom.app M) =
      (extendRestrictScalarsAdj f₁₂).unit.app M ≫
        (restrictScalars f₁₂).map ((extendRestrictScalarsAdj f₂₃).unit.app _) ≫
        (restrictScalarsComp f₁₂ f₂₃).inv.app _

Proof state:
R₁ R₂ R₃ : Type u₁
inst✝² : CommRing R₁
inst✝¹ : CommRing R₂
inst✝ : CommRing R₃
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
M : ModuleCat R₁
⊢ ((extendRestrictScalarsAdj (f₂₃.comp f₁₂)).homEquiv M ((extendScalars f₁₂ ⋙ extendScalars f₂₃).obj M))
      ((extendScalarsComp f₁₂ f₂₃).hom.app M) =
    (extendRestrictScalarsAdj f₁₂).unit.app M ≫
      (restrictScalars f₁₂).map ((extendRestrictScalarsAdj f₂₃).unit.app (ExtendScalars.obj' f₁₂ M)) ≫
        (restrictScalarsComp f₁₂ f₂₃).inv.app ((extendScalars f₂₃).obj (ExtendScalars.obj' f₁₂ M))

Tactic:
dsimp [extendScalarsComp, conjugateIsoEquiv, conjugateEquiv]

Result:
R₁ R₂ R₃ : Type u₁
inst✝² : CommRing R₁
inst✝¹ : CommRing R₂
inst✝ : CommRing R₃
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
M : ModuleCat R₁
⊢ ((extendRestrictScalarsAdj (f₂₃.comp f₁₂)).homEquiv M ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M)))
      (𝟙 ((extendScalars (f₂₃.comp f₁₂)).obj M) ≫
        ((extendScalars (f₂₃.comp f₁₂)).map
              (((extendRestrictScalarsAdj f₁₂).comp (extendRestrictScalarsAdj f₂₃)).unit.app M) ≫
            (extendScalars (f₂₃.comp f₁₂)).map
                (𝟙
                    ((restrictScalars f₁₂).obj
                      ((restrictScalars f₂₃).obj ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M)))) ≫
                  (restrictScalarsComp'App f₁₂ f₂₃ (f₂₃.comp f₁₂) ⋯
                        ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M))).inv ≫
                    𝟙 ((restrictScalars (f₂₃.comp f₁₂)).obj ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M)))) ≫
              (extendRestrictScalarsAdj (f₂₃.comp f₁₂)).counit.app
                ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M))) ≫
          𝟙 ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M))) =
    (extendRestrictScalarsAdj f₁₂).unit.app M ≫
      (restrictScalars f₁₂).map ((extendRestrictScalarsAdj f₂₃).unit.app (ExtendScalars.obj' f₁₂ M)) ≫
        (restrictScalarsComp'App f₁₂ f₂₃ (f₂₃.comp f₁₂) ⋯ ((extendScalars f₂₃).obj (ExtendScalars.obj' f₁₂ M))).inv

Proof state:
R₁ R₂ R₃ : Type u₁
inst✝² : CommRing R₁
inst✝¹ : CommRing R₂
inst✝ : CommRing R₃
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
M : ModuleCat R₁
⊢ (extendRestrictScalarsAdj f₁₂).unit.app M ≫
      (restrictScalars f₁₂).map ((extendRestrictScalarsAdj f₂₃).unit.app ((extendScalars f₁₂).obj M)) ≫
        (restrictScalarsComp'App f₁₂ f₂₃ (f₂₃.comp f₁₂) ⋯ ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M))).inv =
    (extendRestrictScalarsAdj f₁₂).unit.app M ≫
      (restrictScalars f₁₂).map ((extendRestrictScalarsAdj f₂₃).unit.app (ExtendScalars.obj' f₁₂ M)) ≫
        (restrictScalarsComp'App f₁₂ f₂₃ (f₂₃.comp f₁₂) ⋯ ((extendScalars f₂₃).obj (ExtendScalars.obj' f₁₂ M))).inv

Tactic:
rfl

Result:
no goals

Proof state:
R₁ R₂ R₃ : Type u₁
inst✝² : CommRing R₁
inst✝¹ : CommRing R₂
inst✝ : CommRing R₃
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
M : ModuleCat R₁
⊢ ((extendRestrictScalarsAdj (f₂₃.comp f₁₂)).homEquiv M ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M)))
      (𝟙 ((extendScalars (f₂₃.comp f₁₂)).obj M) ≫
        ((extendScalars (f₂₃.comp f₁₂)).map
              (((extendRestrictScalarsAdj f₁₂).comp (extendRestrictScalarsAdj f₂₃)).unit.app M) ≫
            (extendScalars (f₂₃.comp f₁₂)).map
                (𝟙
                    ((restrictScalars f₁₂).obj
                      ((restrictScalars f₂₃).obj ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M)))) ≫
                  (restrictScalarsComp'App f₁₂ f₂₃ (f₂₃.comp f₁₂) ⋯
                        ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M))).inv ≫
                    𝟙 ((restrictScalars (f₂₃.comp f₁₂)).obj ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M)))) ≫
              (extendRestrictScalarsAdj (f₂₃.comp f₁₂)).counit.app
                ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M))) ≫
          𝟙 ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M))) =
    (extendRestrictScalarsAdj f₁₂).unit.app M ≫
      (restrictScalars f₁₂).map ((extendRestrictScalarsAdj f₂₃).unit.app (ExtendScalars.obj' f₁₂ M)) ≫
        (restrictScalarsComp'App f₁₂ f₂₃ (f₂₃.comp f₁₂) ⋯ ((extendScalars f₂₃).obj (ExtendScalars.obj' f₁₂ M))).inv

Tactic:
simp only [Category.assoc, Category.id_comp, Category.comp_id,
  Adjunction.comp_unit_app, Adjunction.homEquiv_unit,
  Functor.map_comp, Adjunction.unit_naturality_assoc,
  Adjunction.right_triangle_components]

Result:
R₁ R₂ R₃ : Type u₁
inst✝² : CommRing R₁
inst✝¹ : CommRing R₂
inst✝ : CommRing R₃
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
M : ModuleCat R₁
⊢ (extendRestrictScalarsAdj f₁₂).unit.app M ≫
      (restrictScalars f₁₂).map ((extendRestrictScalarsAdj f₂₃).unit.app ((extendScalars f₁₂).obj M)) ≫
        (restrictScalarsComp'App f₁₂ f₂₃ (f₂₃.comp f₁₂) ⋯ ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M))).inv =
    (extendRestrictScalarsAdj f₁₂).unit.app M ≫
      (restrictScalars f₁₂).map ((extendRestrictScalarsAdj f₂₃).unit.app (ExtendScalars.obj' f₁₂ M)) ≫
        (restrictScalarsComp'App f₁₂ f₂₃ (f₂₃.comp f₁₂) ⋯ ((extendScalars f₂₃).obj (ExtendScalars.obj' f₁₂ M))).inv