-- 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 : CommRing R
inst_3 : CommRing S
f : R →+* S
Y Y' : ModuleCat S
g : Y ⟶ Y'
m1 : Module R S := Module.compHom S f
m2_1 : Module R (↑Y : Type (max u₂ v)) := Module.compHom (↑Y : Type (max u₂ v)) f
m2 : Module R (↑Y' : Type (max u₂ v)) := Module.compHom (↑Y' : Type (max u₂ v)) f
x y : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑((restrictScalars f).obj Y) : Type (max u₂ v))
ih₁ :
  Eq (α := (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v)))
    ((Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map.{u₁, u₂, v} f) :
          (a : (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v))) →
            (↑((𝟭 (ModuleCat S)).obj Y') : Type (max u₂ v)))
        x :
      (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v)))
    (((Hom.hom (Counit.map.{u₁, u₂, v} f ≫ CategoryTheory.Functor.map (𝟭 (ModuleCat S)) g) :
            (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v)) →ₗ[S]
              (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v))) :
          (a : (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v))) →
            (↑((𝟭 (ModuleCat S)).obj Y') : Type (max u₂ v)))
        x :
      (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v)))
ih₂ :
  Eq (α := (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v)))
    ((Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map.{u₁, u₂, v} f) :
          (a : (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v))) →
            (↑((𝟭 (ModuleCat S)).obj Y') : Type (max u₂ v)))
        y :
      (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v)))
    (((Hom.hom (Counit.map.{u₁, u₂, v} f ≫ CategoryTheory.Functor.map (𝟭 (ModuleCat S)) g) :
            (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v)) →ₗ[S]
              (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v))) :
          (a : (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v))) →
            (↑((𝟭 (ModuleCat S)).obj Y') : Type (max u₂ v)))
        y :
      (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v)))
⊢ HAdd.hAdd (α := (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v))) (β :=
      (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v)))
      ((Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map.{u₁, u₂, v} f) :
            (a : (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v))) →
              (↑((𝟭 (ModuleCat S)).obj Y') : Type (max u₂ v)))
          x :
        (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v)))
      ((Hom.hom ((restrictScalars f ⋙ extendScalars f).map g ≫ Counit.map.{u₁, u₂, v} f) :
            (a : (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v))) →
              (↑((𝟭 (ModuleCat S)).obj Y') : Type (max u₂ v)))
          y :
        (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v))) =
    HAdd.hAdd (α := (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v))) (β :=
      (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v)))
      (((Hom.hom (Counit.map.{u₁, u₂, v} f ≫ CategoryTheory.Functor.map (𝟭 (ModuleCat S)) g) :
              (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v)) →ₗ[S]
                (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v))) :
            (a : (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v))) →
              (↑((𝟭 (ModuleCat S)).obj Y') : Type (max u₂ v)))
          x :
        (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v)))
      (((Hom.hom (Counit.map.{u₁, u₂, v} f ≫ CategoryTheory.Functor.map (𝟭 (ModuleCat S)) g) :
              (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v)) →ₗ[S]
                (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v))) :
            (a : (↑((restrictScalars f ⋙ extendScalars f).obj Y) : Type (max u₂ v))) →
              (↑((𝟭 (ModuleCat S)).obj Y') : Type (max u₂ v)))
          y :
        (↑(Functor.obj (𝟭 (ModuleCat S)) Y') : Type (max u₂ v)))

Tactic:
congr 1