-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.DomCoprod (goal)
Goal:
ιa : Type u_1
ιb : Type u_2
inst : Fintype ιa
inst_1 : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst_2 : CommSemiring R'
inst_3 : AddCommGroup N₁
inst_4 : Module R' N₁
inst_5 : AddCommGroup N₂
inst_6 : Module R' N₂
inst_7 : AddCommMonoid Mᵢ
inst_8 : Module R' Mᵢ
inst_9 : DecidableEq ιa
inst_10 : DecidableEq ιb
c : R'
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x : ιa ⊕ ιb → Mᵢ
a : Perm (ιa ⊕ ιb)
⊢ HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) a : ℤˣ)
      ((MultilinearMap.domDomCongr a
              (HSMul.hSMul (β := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂)) c
                ((MultilinearMap.domCoprod' :
                      (a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁ ⊗[R'] MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂) →
                        MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
                    ((↑m : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁) ⊗ₜ[R']
                      (↑n : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂)) :
                  MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))) :
            (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
          x :
        N₁ ⊗[R'] N₂) =
    c •
      HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) a : ℤˣ)
        ((MultilinearMap.domDomCongr a
                ((MultilinearMap.domCoprod' :
                    (a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁ ⊗[R'] MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂) →
                      MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
                  ((↑m : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁) ⊗ₜ[R']
                    (↑n : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))) :
              (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
            x :
          N₁ ⊗[R'] N₂)
have refine_2 : HSMul.hSMul (α := ℤˣ) (β := N₁ ⊗[R'] N₂) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) a : ℤˣ)
    ((MultilinearMap.domDomCongr a
            (HSMul.hSMul (β := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂)) c
              ((MultilinearMap.domCoprod' :
                    (a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁ ⊗[R'] MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂) →
                      MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
                  ((↑m : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁) ⊗ₜ[R']
                    (↑n : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂)) :
                MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))) :
          (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
        x :
      N₁ ⊗[R'] N₂) =
  HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) a : ℤˣ)
    (HSMul.hSMul (β := N₁ ⊗[R'] N₂) c
      ((MultilinearMap.domDomCongr a
              ((MultilinearMap.domCoprod' :
                  (a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁ ⊗[R'] MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂) →
                    MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
                ((↑m : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁) ⊗ₜ[R']
                  (↑n : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))) :
            (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
          x :
        N₁ ⊗[R'] N₂))
Tactic: first | rw [← smul_add] | rw [smul_comm]