Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: 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₁₂)).obj M) ≫
            (extendScalars (f₂₃.comp f₁₂)).map
                (((extendRestrictScalarsAdj f₁₂).comp (extendRestrictScalarsAdj f₂₃)).unit.app M) ≫
              𝟙
                  ((extendScalars (f₂₃.comp f₁₂)).obj
                    ((restrictScalars f₁₂).obj
                      ((restrictScalars f₂₃).obj ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M))))) ≫
                (extendScalars (f₂₃.comp f₁₂)).map
                    (𝟙
                      ((restrictScalars f₁₂).obj
                        ((restrictScalars f₂₃).obj ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj 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)))) ≫
                    (extendScalars (f₂₃.comp f₁₂)).map
                        (𝟙
                          ((restrictScalars (f₂₃.comp f₁₂)).obj
                            ((extendScalars f₂₃).obj ((extendScalars f₁₂).obj M)))) ≫
                      𝟙
                          ((extendScalars (f₂₃.comp f₁₂)).obj
                            ((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))) ≫
          𝟙 ((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 [Functor.comp_obj, 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]

Goal state after:
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