-- 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 : CommRing R
inst_3 : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
x y : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑X : Type (max v u₂))
h :
  Eq (α := (↑Y : Type (max u₂ v)))
    ((Hom.hom
            ((Equiv.symm (ExtendRestrictScalarsAdj.homEquiv.{v, u₁, u₂} f) :
                (a : X ⟶ (restrictScalars f).obj Y) → (extendScalars f).obj X ⟶ Y)
              g) :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        x :
      (↑Y : Type (max u₂ v)))
    ((Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit.{v, u₁, u₂} f).app Y) :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        x :
      (↑Y : Type (max u₂ v)))
h_1 :
  Eq (α := (↑Y : Type (max u₂ v)))
    ((Hom.hom
            ((Equiv.symm (ExtendRestrictScalarsAdj.homEquiv.{v, u₁, u₂} f) :
                (a : X ⟶ (restrictScalars f).obj Y) → (extendScalars f).obj X ⟶ Y)
              g) :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        y :
      (↑Y : Type (max u₂ v)))
    ((Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit.{v, u₁, u₂} f).app Y) :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        y :
      (↑Y : Type (max u₂ v)))
⊢ Eq (α := (↑Y : Type (max u₂ v)))
    ((Hom.hom
            ((Equiv.symm (ExtendRestrictScalarsAdj.homEquiv.{v, u₁, u₂} f) :
                (a : X ⟶ (restrictScalars f).obj Y) → (extendScalars f).obj X ⟶ Y)
              g) :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        (x + y) :
      (↑Y : Type (max u₂ v)))
    ((Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit.{v, u₁, u₂} f).app Y) :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        (x + y) :
      (↑Y : Type (max u₂ v)))
have add : HAdd.hAdd (α := (↑Y : Type (max u₂ v))) (β := (↑Y : Type (max u₂ v)))
    ((Hom.hom
            ((Equiv.symm (ExtendRestrictScalarsAdj.homEquiv.{v, u₁, u₂} f) :
                (a : X ⟶ (restrictScalars f).obj Y) → (extendScalars f).obj X ⟶ Y)
              g) :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        x :
      (↑Y : Type (max u₂ v)))
    ((Hom.hom
            ((Equiv.symm (ExtendRestrictScalarsAdj.homEquiv.{v, u₁, u₂} f) :
                (a : X ⟶ (restrictScalars f).obj Y) → (extendScalars f).obj X ⟶ Y)
              g) :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        y :
      (↑Y : Type (max u₂ v))) =
  HAdd.hAdd (α := (↑Y : Type (max u₂ v))) (β := (↑Y : Type (max u₂ v)))
    ((Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit.{v, u₁, u₂} f).app Y) :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        x :
      (↑Y : Type (max u₂ v)))
    ((Hom.hom ((extendScalars f).map g ≫ (ExtendRestrictScalarsAdj.counit.{v, u₁, u₂} f).app Y) :
          (a : (↑((extendScalars f).obj X) : Type (max u₂ v))) → (↑Y : Type (max u₂ v)))
        y :
      (↑Y : Type (max u₂ v)))
Tactic: rw [map_add, map_add]