-- Lean 4 proof step from Mathlib.LinearAlgebra.PiTensorProduct (goal)
Goal:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (s i)
inst_2 : (i : ι) → Module.{u_4, u_7} R (s i)
M : Type u_8
inst_3 : AddCommMonoid M
inst_4 : Module R M
E : Type u_9
inst_5 : AddCommMonoid E
inst_6 : Module R E
F : Type u_10
inst_7 : AddCommMonoid F
t : ι → Type u_11
inst_8 : (i : ι) → AddCommMonoid (t i)
inst_9 : (i : ι) → Module.{u_4, u_11} R (t i)
inst_10 : IsEmpty ι
x_1 x y : ⨂[R] (i : ι), s i
hx :
  HSMul.hSMul (α := R) (β := ⨂[R] (i : ι), s i)
      ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
              (⨂[R] (i : ι), s i) →ₗ[R] R) :
            (a : ⨂[R] (i : ι), s i) → R)
          x :
        R)
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))) =
    x
hy :
  HSMul.hSMul (α := R) (β := ⨂[R] (i : ι), s i)
      ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
              (⨂[R] (i : ι), s i) →ₗ[R] R) :
            (a : ⨂[R] (i : ι), s i) → R)
          y :
        R)
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))) =
    y
refine_2 :
  HSMul.hSMul (β := ⨂[R] (i : ι), s i)
      (HAdd.hAdd (α := R) (β := R)
        ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
                (⨂[R] (i : ι), s i) →ₗ[R] R) :
              (a : ⨂[R] (i : ι), s i) → R)
            x :
          R)
        ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
                (⨂[R] (i : ι), s i) →ₗ[R] R) :
              (a : ⨂[R] (i : ι), s i) → R)
            y :
          R))
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))) =
    x + y
refine_2₁ :
  HSMul.hSMul (α := R) (β := ⨂[R] (i : ι), s i)
        ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
                (⨂[R] (i : ι), s i) →ₗ[R] R) :
              (a : ⨂[R] (i : ι), s i) → R)
            x :
          R)
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))) +
      HSMul.hSMul (α := R) (β := ⨂[R] (i : ι), s i)
        ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
                (⨂[R] (i : ι), s i) →ₗ[R] R) :
              (a : ⨂[R] (i : ι), s i) → R)
            y :
          R)
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))) =
    x + y
refine_2₂ :
  x +
      HSMul.hSMul (α := R) (β := ⨂[R] (i : ι), s i)
        ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
                (⨂[R] (i : ι), s i) →ₗ[R] R) :
              (a : ⨂[R] (i : ι), s i) → R)
            y :
          R)
        ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))) =
    x + y
⊢ HSMul.hSMul (α := R) (β := ⨂[R] (i : ι), s i)
      ((((lift (s := s) : (a : MultilinearMap R s R) → (⨂[R] (i : ι), s i) →ₗ[R] R) (constOfIsEmpty R s 1) :
              (⨂[R] (i : ι), s i) →ₗ[R] R) :
            (a : ⨂[R] (i : ι), s i) → R)
          (x + y) :
        R)
      ((tprod R (s := s) : (a : (i : ι) → s i) → ⨂[R] (i : ι), s i) (isEmptyElim (p := s))) =
    x + y
have refine_2₃ : x + y = x + y
Tactic: rw [map_add, add_smul, hx, hy]