-- 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
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n₁ n₂ : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x : ιa ⊕ ιb → Mᵢ
⊢ Eq (α := N₁ ⊗[R'] N₂)
    (∑ a : Perm.ModSumCongr ιa ιb,
      (Quotient.liftOn' a
            (fun (σ : Perm (ιa ⊕ ιb)) ↦
              HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
                (MultilinearMap.domDomCongr σ
                  ((↑m : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
                    (↑(n₁ + n₂) : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
            ⋯ :
          (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
        x)
    (∑ x_1 : Perm.ModSumCongr ιa ιb,
      HAdd.hAdd (α := N₁ ⊗[R'] N₂) (β := N₁ ⊗[R'] N₂)
        ((Quotient.liftOn' x_1
                (fun (σ : Perm (ιa ⊕ ιb)) ↦
                  HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
                    (MultilinearMap.domDomCongr σ
                      ((↑m : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
                        (↑n₁ : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
                ⋯ :
              (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
            x :
          N₁ ⊗[R'] N₂)
        ((Quotient.liftOn' x_1
                (fun (σ : Perm (ιa ⊕ ιb)) ↦
                  HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
                    (MultilinearMap.domDomCongr σ
                      ((↑m : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
                        (↑n₂ : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
                ⋯ :
              (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
            x :
          N₁ ⊗[R'] N₂))
have refine_3 : Eq (α := Perm.ModSumCongr ιa ιb → N₁ ⊗[R'] N₂)
  (fun (a : Perm.ModSumCongr ιa ιb) ↦
    (Quotient.liftOn' a
          (fun (σ : Perm (ιa ⊕ ιb)) ↦
            HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
              (MultilinearMap.domDomCongr σ
                ((↑m : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
                  (↑(n₁ + n₂) : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
          sorry :
        (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
      x)
  fun (x_1 : Perm.ModSumCongr ιa ιb) ↦
  HAdd.hAdd (α := N₁ ⊗[R'] N₂) (β := N₁ ⊗[R'] N₂)
    ((Quotient.liftOn' x_1
            (fun (σ : Perm (ιa ⊕ ιb)) ↦
              HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
                (MultilinearMap.domDomCongr σ
                  ((↑m : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
                    (↑n₁ : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
            sorry :
          (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
        x :
      N₁ ⊗[R'] N₂)
    ((Quotient.liftOn' x_1
            (fun (σ : Perm (ιa ⊕ ιb)) ↦
              HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
                (MultilinearMap.domDomCongr σ
                  ((↑m : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
                    (↑n₂ : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
            sorry :
          (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
        x :
      N₁ ⊗[R'] N₂)
Tactic: congr