-- Module: Mathlib.LinearAlgebra.Alternating.DomCoprod
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
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
rw :
  AlternatingMap.domCoprod
      ((alternatization : (a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁) → Mᵢ [⋀^ιa]→ₗ[R'] N₁)
        (↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁))
      ((alternatization : (a : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂) → Mᵢ [⋀^ιb]→ₗ[R'] N₂)
        (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂)) =
    ((Fintype.card ιa).factorial * (Fintype.card ιb).factorial) • a.domCoprod b
rw₁ :
  ((Fintype.card ιa).factorial • a).domCoprod
      ((alternatization : (a : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂) → Mᵢ [⋀^ιb]→ₗ[R'] N₂)
        (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂)) =
    ((Fintype.card ιa).factorial * (Fintype.card ιb).factorial) • a.domCoprod b
rw₂ :
  ((Fintype.card ιa).factorial • a).domCoprod ((Fintype.card ιb).factorial • b) =
    ((Fintype.card ιa).factorial * (Fintype.card ιb).factorial) • a.domCoprod b
rw₃ :
  ((Fintype.card ιa).factorial • a).domCoprod ((Fintype.card ιb).factorial • b) =
    (Fintype.card ιa).factorial • (Fintype.card ιb).factorial • a.domCoprod b
rw₄ :
  (AlternatingMap.domCoprod' : (a : (Mᵢ [⋀^ιa]→ₗ[R'] N₁) ⊗[R'] Mᵢ [⋀^ιb]→ₗ[R'] N₂) → Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂)
      (((Fintype.card ιa).factorial • a) ⊗ₜ[R'] ((Fintype.card ιb).factorial • b)) =
    (Fintype.card ιa).factorial • (Fintype.card ιb).factorial • a.domCoprod b
rw₅ :
  (AlternatingMap.domCoprod' : (a : (Mᵢ [⋀^ιa]→ₗ[R'] N₁) ⊗[R'] Mᵢ [⋀^ιb]→ₗ[R'] N₂) → Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂)
      (((Fintype.card ιa).factorial • a) ⊗ₜ[R'] ((Fintype.card ιb).factorial • b)) =
    (Fintype.card ιa).factorial •
      HSMul.hSMul (β := Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂) (Fintype.card ιb).factorial
        ((AlternatingMap.domCoprod' :
              (a : (Mᵢ [⋀^ιa]→ₗ[R'] N₁) ⊗[R'] Mᵢ [⋀^ιb]→ₗ[R'] N₂) → Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂)
            (a ⊗ₜ[R'] b) :
          Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂)
rw₆ :
  (AlternatingMap.domCoprod' : (a : (Mᵢ [⋀^ιa]→ₗ[R'] N₁) ⊗[R'] Mᵢ [⋀^ιb]→ₗ[R'] N₂) → Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂)
      (HSMul.hSMul (β := (Mᵢ [⋀^ιa]→ₗ[R'] N₁) ⊗[R'] Mᵢ [⋀^ιb]→ₗ[R'] N₂) (Fintype.card ιa).factorial
        (a ⊗ₜ[R'] ((Fintype.card ιb).factorial • b))) =
    (Fintype.card ιa).factorial •
      HSMul.hSMul (β := Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂) (Fintype.card ιb).factorial
        ((AlternatingMap.domCoprod' :
              (a : (Mᵢ [⋀^ιa]→ₗ[R'] N₁) ⊗[R'] Mᵢ [⋀^ιb]→ₗ[R'] N₂) → Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂)
            (a ⊗ₜ[R'] b) :
          Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂)
rw₇ :
  (AlternatingMap.domCoprod' : (a : (Mᵢ [⋀^ιa]→ₗ[R'] N₁) ⊗[R'] Mᵢ [⋀^ιb]→ₗ[R'] N₂) → Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂)
      ((Fintype.card ιa).factorial •
        HSMul.hSMul (β := (Mᵢ [⋀^ιa]→ₗ[R'] N₁) ⊗[R'] Mᵢ [⋀^ιb]→ₗ[R'] N₂) (Fintype.card ιb).factorial (a ⊗ₜ[R'] b)) =
    (Fintype.card ιa).factorial •
      HSMul.hSMul (β := Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂) (Fintype.card ιb).factorial
        ((AlternatingMap.domCoprod' :
              (a : (Mᵢ [⋀^ιa]→ₗ[R'] N₁) ⊗[R'] Mᵢ [⋀^ιb]→ₗ[R'] N₂) → Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂)
            (a ⊗ₜ[R'] b) :
          Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂)
rw₈ :
  HSMul.hSMul (β := Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂) (Fintype.card ιa).factorial
      ((AlternatingMap.domCoprod' :
            (a : (Mᵢ [⋀^ιa]→ₗ[R'] N₁) ⊗[R'] Mᵢ [⋀^ιb]→ₗ[R'] N₂) → Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂)
          (HSMul.hSMul (β := (Mᵢ [⋀^ιa]→ₗ[R'] N₁) ⊗[R'] Mᵢ [⋀^ιb]→ₗ[R'] N₂) (Fintype.card ιb).factorial (a ⊗ₜ[R'] b)) :
        Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂) =
    (Fintype.card ιa).factorial •
      HSMul.hSMul (β := Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂) (Fintype.card ιb).factorial
        ((AlternatingMap.domCoprod' :
              (a : (Mᵢ [⋀^ιa]→ₗ[R'] N₁) ⊗[R'] Mᵢ [⋀^ιb]→ₗ[R'] N₂) → Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂)
            (a ⊗ₜ[R'] b) :
          Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂)
rw₉ rw₁₀ :
  (Fintype.card ιa).factorial •
      HSMul.hSMul (β := Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂) (Fintype.card ιb).factorial
        ((AlternatingMap.domCoprod' :
              (a : (Mᵢ [⋀^ιa]→ₗ[R'] N₁) ⊗[R'] Mᵢ [⋀^ιb]→ₗ[R'] N₂) → Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂)
            (a ⊗ₜ[R'] b) :
          Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂) =
    (Fintype.card ιa).factorial •
      HSMul.hSMul (β := Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂) (Fintype.card ιb).factorial
        ((AlternatingMap.domCoprod' :
              (a : (Mᵢ [⋀^ιa]→ₗ[R'] N₁) ⊗[R'] Mᵢ [⋀^ιb]→ₗ[R'] N₂) → Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂)
            (a ⊗ₜ[R'] b) :
          Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂)
⊢ (alternatization : (a : MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂)) → Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂)
      ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂)) =
    ((Fintype.card ιa).factorial * (Fintype.card ιb).factorial) • a.domCoprod b

Tactic:
rw [MultilinearMap.domCoprod_alternization, coe_alternatization, coe_alternatization, mul_smul,
    ← AlternatingMap.domCoprod'_apply, ← AlternatingMap.domCoprod'_apply,
    ← TensorProduct.smul_tmul', TensorProduct.tmul_smul,
    LinearMap.map_smul_of_tower AlternatingMap.domCoprod',
    LinearMap.map_smul_of_tower AlternatingMap.domCoprod']

Premises used: TensorProduct.tmul_smul, AlternatingMap.domCoprod'_apply, AlternatingMap.coe_alternatization, TensorProduct.smul_tmul', MultilinearMap.domCoprod_alternization, LinearMap.map_smul_of_tower, AlternatingMap.domCoprod', SemigroupAction.mul_smul