-- 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
Y : ModuleCat S
x x_1 : (↑((restrictScalars f).obj (of S S)) : Type u₂) ⊗[R] (↑((restrictScalars f).obj Y) : Type (max u_1 u₂))
⊢ (lift
          {
            toFun := fun (s : S) ↦
              { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ },
            map_add' := ⋯, map_smul' := ⋯ } :
        (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
      (x + x_1) =
    HAdd.hAdd (α := (↑Y : Type (max u₂ u_1))) (β := (↑Y : Type (max u₂ u_1)))
      ((lift
              {
                toFun := fun (s : S) ↦
                  { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ :
                    (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) },
                map_add' := ⋯, map_smul' := ⋯ : S →ₗ[R] (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
            (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
          x :
        (↑Y : Type (max u₂ u_1)))
      ((lift
              {
                toFun := fun (s : S) ↦
                  { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := ⋯, map_smul' := ⋯ :
                    (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) },
                map_add' := ⋯, map_smul' := ⋯ : S →ₗ[R] (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
            (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
          x_1 :
        (↑Y : Type (max u₂ u_1)))
have rw : HAdd.hAdd (α := (↑Y : Type (max u₂ u_1))) (β := (↑Y : Type (max u₂ u_1)))
    ((lift
            {
              toFun := fun (s : S) ↦
                { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := sorry, map_smul' := sorry :
                  (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) },
              map_add' := sorry, map_smul' := sorry : S →ₗ[R] (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
          (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        x :
      (↑Y : Type (max u₂ u_1)))
    ((lift
            {
              toFun := fun (s : S) ↦
                { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := sorry, map_smul' := sorry :
                  (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) },
              map_add' := sorry, map_smul' := sorry : S →ₗ[R] (↑Y : Type (max u₂ u_1)) →ₗ[R] (↑Y : Type (max u₂ u_1)) } :
          (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        x_1 :
      (↑Y : Type (max u₂ u_1))) =
  HAdd.hAdd (α := (↑Y : Type (max u₂ u_1))) (β := (↑Y : Type (max u₂ u_1)))
    ((lift
            {
              toFun := fun (s : S) ↦
                { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := sorry, map_smul' := sorry },
              map_add' := sorry, map_smul' := sorry } :
          (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        x :
      (↑Y : Type (max u₂ u_1)))
    ((lift
            {
              toFun := fun (s : S) ↦
                { toFun := fun (y : (↑Y : Type (max u₂ u_1))) ↦ s • y, map_add' := sorry, map_smul' := sorry },
              map_add' := sorry, map_smul' := sorry } :
          (a : S ⊗[R] (↑Y : Type (max u₂ u_1))) → (↑Y : Type (max u₂ u_1)))
        x_1 :
      (↑Y : Type (max u₂ u_1)))
Tactic: rw [map_add]