-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ChangeOfRings (goal)
Goal:
R_1 : Type u₁
S_1 : Type u₂
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
R : Type u₁
S : Type u₂
inst_2 : Ring R
inst_3 : Ring S
f : R →+* S
Y Y' : ModuleCat S
g : Y ⟶ Y'
y : (↑Y : Type (max u₂ u_1))
s : S
⊢ Eq (α := (↑((restrictScalars f).obj Y') : Type (max u₂ u_1)))
    ((((CoextendScalars.equiv f ((restrictScalars f).obj Y') :
                (a : (↑((coextendScalars f).obj ((restrictScalars f).obj Y')) : Type (max u₂ u_1))) →
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                    (↑((restrictScalars f).obj Y') : Type (max u₂ u_1)))
              ((Hom.hom (CategoryTheory.Functor.map (𝟭 (ModuleCat S)) g ≫ ↟(app' f Y')) :
                  (a : (↑((𝟭 (ModuleCat S)).obj Y) : Type (max u₂ u_1))) →
                    (↑((restrictScalars f ⋙ coextendScalars f).obj Y') : Type (max u₂ u_1)))
                y) :
            (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑((restrictScalars f).obj Y') : Type (max u₂ u_1))) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑((restrictScalars f).obj Y') : Type (max u₂ u_1)))
        s :
      (↑((restrictScalars f).obj Y') : Type (max u₂ u_1)))
    ((((CoextendScalars.equiv f ((restrictScalars f).obj Y') :
                (a : (↑((coextendScalars f).obj ((restrictScalars f).obj Y')) : Type (max u₂ u_1))) →
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                    (↑((restrictScalars f).obj Y') : Type (max u₂ u_1)))
              ((Hom.hom (↟(app' f Y) ≫ (restrictScalars f ⋙ coextendScalars f).map g) :
                  (a : (↑((𝟭 (ModuleCat S)).obj Y) : Type (max u₂ u_1))) →
                    (↑((restrictScalars f ⋙ coextendScalars f).obj Y') : Type (max u₂ u_1)))
                y) :
            (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑((restrictScalars f).obj Y') : Type (max u₂ u_1))) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑((restrictScalars f).obj Y') : Type (max u₂ u_1)))
        s :
      (↑((restrictScalars f).obj Y') : Type (max u₂ u_1)))
have simp : Eq (α := (↑((restrictScalars f).obj Y') : Type (max u₂ u_1)))
  ((((CoextendScalars.equiv f ((restrictScalars f).obj Y') :
              (a : (↑((coextendScalars f).obj ((restrictScalars f).obj Y')) : Type (max u₂ u_1))) →
                (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                  (↑((restrictScalars f).obj Y') : Type (max u₂ u_1)))
            ((Hom.hom (↟(app' f Y')) ∘ₗ Hom.hom g :
                (a : (↑Y : Type (max u₂ u_1))) →
                  (↑((coextendScalars f).obj ((restrictScalars f).obj Y')) : Type (max u₂ u_1)))
              y) :
          (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑((restrictScalars f).obj Y') : Type (max u₂ u_1))) :
        (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑((restrictScalars f).obj Y') : Type (max u₂ u_1)))
      s :
    (↑((restrictScalars f).obj Y') : Type (max u₂ u_1)))
  ((((CoextendScalars.equiv f ((restrictScalars f).obj Y') :
              (a : (↑((coextendScalars f).obj ((restrictScalars f).obj Y')) : Type (max u₂ u_1))) →
                (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R]
                  (↑((restrictScalars f).obj Y') : Type (max u₂ u_1)))
            ((Hom.hom ((coextendScalars f).map ((restrictScalars f).map g)) ∘ₗ Hom.hom (↟(app' f Y)) :
                (a : (↑Y : Type (max u₂ u_1))) →
                  (↑((coextendScalars f).obj ((restrictScalars f).obj Y')) : Type (max u₂ u_1)))
              y) :
          (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑((restrictScalars f).obj Y') : Type (max u₂ u_1))) :
        (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑((restrictScalars f).obj Y') : Type (max u₂ u_1)))
      s :
    (↑((restrictScalars f).obj Y') : Type (max u₂ u_1)))
Tactic: simp only [ModuleCat.hom_comp, Functor.id_map, Functor.id_obj, Functor.comp_obj,
        Functor.comp_map]