awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n₁ n₂ : Mᵢ [⋀^ιb]→ₗ[R'] N₂
refine_3 :
  ∀ (x : ιa ⊕ ιb → Mᵢ),
    Eq (α := N₁ ⊗[R'] N₂) ((m.domCoprod (n₁ + n₂) : (a : ιa ⊕ ιb → Mᵢ) → N₁ ⊗[R'] N₂) x : N₁ ⊗[R'] N₂)
      ((m.domCoprod n₁ + m.domCoprod n₂ : (a : ιa ⊕ ιb → Mᵢ) → N₁ ⊗[R'] N₂) x : N₁ ⊗[R'] N₂)
⊢ m.domCoprod (n₁ + n₂) = m.domCoprod n₁ + m.domCoprod n₂

Tactic:
ext
-- 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
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n₁ n₂ : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x : ιa ⊕ ιb → Mᵢ
refine_3 :
  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₂))
⊢ Eq (α := N₁ ⊗[R'] N₂) ((m.domCoprod (n₁ + n₂) : (a : ιa ⊕ ιb → Mᵢ) → N₁ ⊗[R'] N₂) x : N₁ ⊗[R'] N₂)
    ((m.domCoprod n₁ + m.domCoprod n₂ : (a : ιa ⊕ ιb → Mᵢ) → N₁ ⊗[R'] N₂) x : N₁ ⊗[R'] N₂)

Tactic:
simp only [domCoprod_apply, add_apply, smul_apply, ← Finset.sum_add_distrib,
        Finset.smul_sum, MultilinearMap.sum_apply, domCoprod.summand]

Premises used: AlternatingMap.add_apply, AlternatingMap.smul_apply, Finset.sum_add_distrib, AlternatingMap.domCoprod.summand, Finset.smul_sum, MultilinearMap.sum_apply, AlternatingMap.domCoprod_apply
-- 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
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
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
              (HAdd.hAdd (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂)) (β :=
                MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
                ((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₂))
                ((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 : ℤˣ)
      (HAdd.hAdd (α := N₁ ⊗[R'] N₂) (β := N₁ ⊗[R'] N₂)
        ((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₂)
        ((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:
rfl
-- 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
c : R'
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
refine_4 :
  ∀ (x : ιa ⊕ ιb → Mᵢ),
    Eq (α := N₁ ⊗[R'] N₂) ((m.domCoprod (c • n) : (a : ιa ⊕ ιb → Mᵢ) → N₁ ⊗[R'] N₂) x : N₁ ⊗[R'] N₂)
      ((c • m.domCoprod n : (a : ιa ⊕ ιb → Mᵢ) → N₁ ⊗[R'] N₂) x : N₁ ⊗[R'] N₂)
⊢ m.domCoprod (c • n) = c • m.domCoprod n

Tactic:
ext
-- 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
c : R'
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x : ιa ⊕ ιb → Mᵢ
refine_4 :
  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
                    (↑(c • n) : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
            ⋯ :
          (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
        x)
    (∑ x_1 : Perm.ModSumCongr ιa ιb,
      HSMul.hSMul (β := N₁ ⊗[R'] N₂) c
        ((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₂))
⊢ Eq (α := N₁ ⊗[R'] N₂) ((m.domCoprod (c • n) : (a : ιa ⊕ ιb → Mᵢ) → N₁ ⊗[R'] N₂) x : N₁ ⊗[R'] N₂)
    ((c • m.domCoprod n : (a : ιa ⊕ ιb → Mᵢ) → N₁ ⊗[R'] N₂) x : N₁ ⊗[R'] N₂)

Tactic:
simp only [domCoprod_apply, add_apply, smul_apply, ← Finset.sum_add_distrib,
        Finset.smul_sum, MultilinearMap.sum_apply, domCoprod.summand]

Premises used: AlternatingMap.add_apply, AlternatingMap.smul_apply, Finset.sum_add_distrib, AlternatingMap.domCoprod.summand, Finset.smul_sum, MultilinearMap.sum_apply, AlternatingMap.domCoprod_apply
-- 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
c : R'
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x : ιa ⊕ ιb → Mᵢ
refine_4 :
  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
                    (↑(c • n) : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
            ⋯ :
          (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
        x)
    fun (x_1 : Perm.ModSumCongr ιa ιb) ↦
    HSMul.hSMul (β := N₁ ⊗[R'] N₂) c
      ((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₂)
⊢ 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
                    (↑(c • n) : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
            ⋯ :
          (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
        x)
    (∑ x_1 : Perm.ModSumCongr ιa ιb,
      HSMul.hSMul (β := N₁ ⊗[R'] N₂) c
        ((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₂))

Tactic:
congr
-- 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
c : R'
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x : ιa ⊕ ιb → Mᵢ
refine_4 :
  ∀ (σ : Perm.ModSumCongr ιa ιb),
    (Quotient.liftOn' σ
            (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
                    (↑(c • n) : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
            ⋯ :
          (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
        x =
      HSMul.hSMul (β := N₁ ⊗[R'] N₂) c
        ((Quotient.liftOn' σ
                (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₂)
⊢ 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
                    (↑(c • n) : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
            ⋯ :
          (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
        x)
    fun (x_1 : Perm.ModSumCongr ιa ιb) ↦
    HSMul.hSMul (β := N₁ ⊗[R'] N₂) c
      ((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₂)

Tactic:
ext σ
-- 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
c : R'
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x : ιa ⊕ ιb → Mᵢ
σ : Perm.ModSumCongr ιa ιb
refine_4 :
  ∀ (a : Perm (ιa ⊕ ιb)),
    (Quotient.liftOn' (s₁ := QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range) (Quotient.mk'' 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
                    (↑(c • n) : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
            ⋯ :
          (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
        x =
      HSMul.hSMul (β := N₁ ⊗[R'] N₂) c
        ((Quotient.liftOn' (s₁ := QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range) (Quotient.mk'' 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 : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
                ⋯ :
              (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
            x :
          N₁ ⊗[R'] N₂)
⊢ (Quotient.liftOn' σ
          (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
                  (↑(c • n) : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
          ⋯ :
        (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
      x =
    HSMul.hSMul (β := N₁ ⊗[R'] N₂) c
      ((Quotient.liftOn' σ
              (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₂)

Tactic:
induction σ using Quotient.inductionOn'
-- 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
c : R'
m : Mᵢ [⋀^ιa]→ₗ[R'] N₁
n : Mᵢ [⋀^ιb]→ₗ[R'] N₂
x : ιa ⊕ ιb → Mᵢ
a : Perm (ιa ⊕ ιb)
refine_4 :
  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']
                  (c • (↑n : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) 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₂)
⊢ (Quotient.liftOn' (s₁ := QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range) (Quotient.mk'' 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
                  (↑(c • n) : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
          ⋯ :
        (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
      x =
    HSMul.hSMul (β := N₁ ⊗[R'] N₂) c
      ((Quotient.liftOn' (s₁ := QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range) (Quotient.mk'' 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 : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
              ⋯ :
            (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
          x :
        N₁ ⊗[R'] N₂)

Tactic:
simp only [Quotient.liftOn'_mk'', coe_add, coe_smul, MultilinearMap.smul_apply,
        ← MultilinearMap.domCoprod'_apply]

Premises used: MultilinearMap.smul_apply, Quotient.liftOn'_mk'', AlternatingMap.coe_smul, MultilinearMap.domCoprod'_apply, AlternatingMap.coe_add
-- 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₂
⊢ (domCoprod' : (a : (Mᵢ [⋀^ιa]→ₗ[R'] N₁) ⊗[R'] Mᵢ [⋀^ιb]→ₗ[R'] N₂) → Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] N₁ ⊗[R'] N₂) (a ⊗ₜ[R'] b) =
    a.domCoprod b

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, AlternatingMap.domCoprod, FreeAddMonoid.sumAux, rfl
-- 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 : MultilinearMap.{u_3, u_1, u_4, u_5} R' (fun (x : ιa) ↦ Mᵢ) N₁
b : MultilinearMap.{u_3, u_2, u_4, u_6} R' (fun (x : ιb) ↦ Mᵢ) N₂
simp_rw :
  Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    ((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₂))
        ((∑ σ : Perm ιa,
            HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ιa →* ℤˣ) : (a : Perm ιa) → ℤˣ) σ : ℤˣ) (domDomCongr σ a)) ⊗ₜ[R']
          ∑ σ : Perm ιb,
            HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ιb →* ℤˣ) : (a : Perm ιb) → ℤˣ) σ : ℤˣ) (domDomCongr σ b)) :
      MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (∑ x : Perm ιa,
        ∑ x_1 : Perm ιb,
          HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ιa →* ℤˣ) : (a : Perm ιa) → ℤˣ) x : ℤˣ)
            (HSMul.hSMul (α := ℤˣ) (β := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
              (((Perm.sign : Perm ιb →* ℤˣ) : (a : Perm ιb) → ℤˣ) x_1 : ℤˣ)
              ((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₂))
                  (domDomCongr x a ⊗ₜ[R'] domDomCongr x_1 b) :
                MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))) :
      MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
⊢ Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (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₂))
    (∑ σa : Perm ιa,
      ∑ σb : Perm ιb,
        HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ιa →* ℤˣ) : (a : Perm ιa) → ℤˣ) σa : ℤˣ)
          (HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ιb →* ℤˣ) : (a : Perm ιb) → ℤˣ) σb : ℤˣ)
            ((domDomCongr σa a).domCoprod (domDomCongr σb b))))

Tactic:
simp_rw [← MultilinearMap.domCoprod'_apply, MultilinearMap.alternatization_coe]

Premises used: MultilinearMap.domCoprod'_apply, MultilinearMap.alternatization_coe