-- Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
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
X : ModuleCat R
Y : ModuleCat S
g : (restrictScalars f).obj Y ⟶ X
y1 y2 : (↑Y : Type (max u₂ u_1))
s : S
⊢ Eq (α := (↑X : Type (max u₂ u_1)))
    ((((CoextendScalars.equiv f X :
                (a : (↑((coextendScalars f).obj X) : Type (max u₂ u_1))) →
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u₂ u_1)))
              (((CoextendScalars.equiv f X).symm :
                  (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u₂ u_1))) →
                    (↑((coextendScalars f).obj X) : Type (max u₂ u_1)))
                {
                  toFun := fun (s : S) ↦
                    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦
                          (↑x1 : Type (max u₂ u_1)) →ₗ[R] (↑x2 : Type (max u₂ u_1))) (CC := carrier) g :
                        (a : (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) → (↑X : Type (max u₂ u_1)))
                      (s • (y1 + y2)),
                  map_add' := ⋯, map_smul' := ⋯ }) :
            (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u₂ u_1))) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑X : Type (max u₂ u_1)))
        s :
      (↑X : Type (max u₂ u_1)))
    ((((CoextendScalars.equiv f X :
                (a : (↑((coextendScalars f).obj X) : Type (max u₂ u_1))) →
                  (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u₂ u_1)))
              (HAdd.hAdd (α := (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u_1 u₂))) (β :=
                (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u_1 u₂)))
                (((CoextendScalars.equiv f X).symm :
                      (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u₂ u_1))) →
                        (↑((coextendScalars f).obj X) : Type (max u₂ u_1)))
                    {
                      toFun := fun (s : S) ↦
                        (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦
                              (↑x1 : Type (max u₂ u_1)) →ₗ[R] (↑x2 : Type (max u₂ u_1))) (CC := carrier) g :
                            (a : (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) → (↑X : Type (max u₂ u_1)))
                          (s • y1),
                      map_add' := ⋯, map_smul' := ⋯ } :
                  (↑((coextendScalars f).obj X) : Type (max u₂ u_1)))
                (((CoextendScalars.equiv f X).symm :
                      (a : (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u₂ u_1))) →
                        (↑((coextendScalars f).obj X) : Type (max u₂ u_1)))
                    {
                      toFun := fun (s : S) ↦
                        (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦
                              (↑x1 : Type (max u₂ u_1)) →ₗ[R] (↑x2 : Type (max u₂ u_1))) (CC := carrier) g :
                            (a : (↑((restrictScalars f).obj Y) : Type (max u₂ u_1))) → (↑X : Type (max u₂ u_1)))
                          (s • y2),
                      map_add' := ⋯, map_smul' := ⋯ } :
                  (↑((coextendScalars f).obj X) : Type (max u₂ u_1)))) :
            (↑((restrictScalars f).obj (of S S)) : Type u₂) →ₗ[R] (↑X : Type (max u₂ u_1))) :
          (a : (↑((restrictScalars f).obj (of S S)) : Type u₂)) → (↑X : Type (max u₂ u_1)))
        s :
      (↑X : Type (max u₂ u_1)))

Tactic:
simp