awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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₂
σ : Quotient (QuotientGroup.leftRel (sumCongrHom ιa ιb).range)
⊢ Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (∑ y : Perm (ιa ⊕ ιb) with ⟦y⟧ = σ,
      HSMul.hSMul (α := ℤˣ) (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) y : ℤˣ)
        (domDomCongr y (a.domCoprod b)))
    (domCoprod.summand ((alternatization : (a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁) → Mᵢ [⋀^ιa]→ₗ[R'] N₁) a)
      ((alternatization : (a : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂) → Mᵢ [⋀^ιb]→ₗ[R'] N₂) b) σ)
have a₁ : ∀ (σ : Perm (ιa ⊕ ιb)),
  Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    (∑ y : Perm (ιa ⊕ ιb) with ⟦y⟧ = Quotient.mk'' σ,
      HSMul.hSMul (α := ℤˣ) (((sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) y : ℤˣ)
        (domDomCongr y (a.domCoprod b)))
    (domCoprod.summand ((alternatization : (a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁) → Mᵢ [⋀^ιa]→ₗ[R'] N₁) a)
      ((alternatization : (a : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂) → Mᵢ [⋀^ιb]→ₗ[R'] N₂) b) (Quotient.mk'' σ))
Tactic: induction σ using Quotient.inductionOn' with
  | h σ =>
  set f := sumCongrHom ιa ιb
  calc
    ∑ τ ∈ _, sign τ • domDomCongr τ (a.domCoprod b) =
        ∑ τ ∈ {τ | τ⁻¹ * σ ∈ f.range}, sign τ • domDomCongr τ (a.domCoprod b) := by
      simp [QuotientGroup.leftRel_apply, f, Quotient.eq]
    _ = ∑ τ ∈ {τ | τ⁻¹ ∈ f.range}, sign (σ * τ) • domDomCongr (σ * τ) (a.domCoprod b) := by
      conv_lhs => rw [← Finset.map_univ_equiv (Equiv.mulLeft σ), Finset.filter_map, Finset.sum_map]
      simp [-MonoidHom.mem_range]
    _ = ∑ τ, sign (σ * f τ) • domDomCongr (σ * f τ) (a.domCoprod b) := by
      simp_rw [f, Subgroup.inv_mem_iff, MonoidHom.mem_range, Finset.univ_filter_exists,
        Finset.sum_image sumCongrHom_injective.injOn]
    _ = ∑ τ : Perm ιa × Perm ιb,
         sign σ • (domDomCongrEquiv σ) (sign τ.1 • sign τ.2 •
           (domDomCongr τ.1 a).domCoprod (domDomCongr τ.2 b)) := by
      simp [f, domDomCongr_mul, domCoprod_domDomCongr_sumCongr, mul_smul]
    _ = domCoprod.summand (alternatization a) (alternatization b) (Quotient.mk'' σ) := by
      simp [domCoprod.summand_mk'', domCoprod_alternization_coe, ← domDomCongrEquiv_apply,
        Finset.smul_sum, ← Finset.sum_product']
Cleared hypotheses: σ
-- 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
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[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
have 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
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']
-- 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
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
⊢ (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
have 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
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']
-- 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
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
⊢ (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
have rw₂ : ((Fintype.card ιa).factorial • a).domCoprod ((Fintype.card ιb).factorial • b) =
  ((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']
-- 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
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
⊢ (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
have rw₃ : ((Fintype.card ιa).factorial • a).domCoprod ((Fintype.card ιb).factorial • b) =
  (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']
-- 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
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
⊢ (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
have 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
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']
-- 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
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
⊢ (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
have 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₂)
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']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Uncurry.Fin (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : M [⋀^Fin (n + 1)]→ₗ[R] N
p : Fin (n + 1)
x : M
v : Fin n → M
⊢ (f : (a : Fin (n + 1) → M) → N) (p.insertNth (α := fun (a : Fin (n + 1)) ↦ M) x v) =
    HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑p : ℕ)) ((f : (a : Fin (n + 1) → M) → N) (Matrix.vecCons x v) : N)
have rw : HSMul.hSMul (α := ℤˣ) (β := N) ((Equiv.Perm.sign : (a : Equiv.Perm (Fin (n + 1))) → ℤˣ) p.cycleRange : ℤˣ)
    ((f : (a : Fin (n + 1) → M) → N) (cons (α := fun (a : Fin (n + 1)) ↦ M) x v) : N) =
  HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑p : ℕ))
    ((f : (a : Fin (n + 1) → M) → N) (cons (α := fun (a : Fin n.succ) ↦ M) x v) : N)
Tactic: rw [← cons_comp_cycleRange, map_perm, Matrix.vecCons]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Uncurry.Fin (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : M [⋀^Fin (n + 1)]→ₗ[R] N
p : Fin (n + 1)
x : M
v : Fin n → M
⊢ HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑p : ℕ))
      ((f : (a : Fin (n + 1) → M) → N) (p.insertNth (α := fun (a : Fin (n + 1)) ↦ M) x v) : N) =
    (f : (a : Fin (n + 1) → M) → N) (Matrix.vecCons x v)
have rw : Even ((↑p : ℕ) + (↑p : ℕ))
Tactic: rw [map_insertNth, smul_smul, ← pow_add, Even.neg_one_pow, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Uncurry.Fin (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : M [⋀^Fin (n + 1)]→ₗ[R] N
p : Fin (n + 1)
x : M
v : Fin n → M
w : ℕ
⊢ Even ((↑p : ℕ) + (↑p : ℕ))
have h : (↑p : ℕ) + (↑p : ℕ) = (↑p : ℕ) + (↑p : ℕ)
Tactic: use p
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Uncurry.Fin (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
i j : Fin (n + 1)
hvij : v i = v j
hij : i ≠ j
⊢ HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
        ((f : (a : Fin n → M) → N) (i.removeNth (α := fun (i : Fin (n + 1)) ↦ M) v) : N) +
      HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑j : ℕ))
        ((f : (a : Fin n → M) → N) (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M) v) : N) =
    0
have rcases : ∀ (i : Fin n) (hvij : v (j.succAbove i) = v j) (hij : j.succAbove i ≠ j),
  HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑(j.succAbove i) : ℕ))
        ((f : (a : Fin n → M) → N) ((j.succAbove i).removeNth (α := fun (i : Fin (n + 1)) ↦ M) v) : N) +
      HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑j : ℕ))
        ((f : (a : Fin n → M) → N) (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M) v) : N) =
    0
Tactic: rcases exists_succAbove_eq hij with ⟨i, rfl⟩
Cleared hypotheses: i, hvij, hij
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Uncurry.Fin (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
j : Fin (n + 1)
i : Fin n
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑(j.succAbove i) : ℕ))
        ((f : (a : Fin n → M) → N) ((j.succAbove i).removeNth (α := fun (i : Fin (n + 1)) ↦ M) v) : N) +
      HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑j : ℕ))
        ((f : (a : Fin n → M) → N) (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M) v) : N) =
    0
have obtain : ∀ (m : ℕ) (f : M [⋀^Fin (m + 1)]→ₗ[R] N) {v : Fin (m + 1 + 1) → M} {j : Fin (m + 1 + 1)} (i : Fin (m + 1))
  (hvij : v (j.succAbove i) = v j) (hij : j.succAbove i ≠ j),
  HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑(j.succAbove i) : ℕ))
        ((f : (a : Fin (m + 1) → M) → N) ((j.succAbove i).removeNth (α := fun (i : Fin (m + 1 + 1)) ↦ M) v) : N) +
      HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑j : ℕ))
        ((f : (a : Fin (m + 1) → M) → N) (j.removeNth (α := fun (i : Fin (m + 1 + 1)) ↦ M) v) : N) =
    0
Tactic: obtain ⟨m, rfl⟩ : ∃ m, m + 1 = n := by simp [i.pos]
Cleared hypotheses: n, f, v, j, i, hvij, hij
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Uncurry.Fin (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑(j.succAbove i) : ℕ))
        ((f : (a : Fin (m + 1) → M) → N) ((j.succAbove i).removeNth (α := fun (i : Fin (m + 1 + 1)) ↦ M) v) : N) +
      HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑j : ℕ))
        ((f : (a : Fin (m + 1) → M) → N) (j.removeNth (α := fun (i : Fin (m + 1 + 1)) ↦ M) v) : N) =
    0
have rw : v j = j.removeNth (α := fun (i : Fin (m + 1 + 1)) ↦ M) v i
Tactic: rw [← (i.predAbove j).insertNth_self_removeNth (removeNth _ _), ← removeNth_removeNth_eq_swap,
    removeNth, succAbove_succAbove_predAbove, map_insertNth, ← neg_one_pow_smul_map_insertNth,
    insertNth_removeNth, update_eq_self_iff.2, smul_smul, ← pow_add,
    neg_one_pow_succAbove_add_predAbove, neg_smul, pow_add, mul_smul,
    smul_smul (_ ^ i.val), ← sq, ← pow_mul, pow_mul', neg_one_pow_two, one_pow, one_smul,
    neg_add_cancel]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Uncurry.Fin (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
N₂ : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N
inst_4 : AddCommGroup N₂
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module R N
inst_8 : Module R N₂
n : ℕ
f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
i j : Fin (n + 1)
hvij : v i = v j
hij : i ≠ j
⊢ Eq.{u_4 + 1} (α := N)
    (MultilinearMap.toFun.{u_1, 0, u_2, u_4} (R := R) (M₁ := fun (x : Fin (n + 1)) ↦ M)
      (∑ p : Fin (n + 1),
        HSMul.hSMul (β := MultilinearMap.{u_1, 0, u_2, u_4} R (fun (x : Fin (n + 1)) ↦ M) N)
          (HPow.hPow (α := ℤ) (-1) (↑p : ℕ))
          (LinearMap.uncurryMid (M := fun (x : Fin (n + 1)) ↦ M) p (toMultilinearMapLM ∘ₗ f)))
      v)
    0
have suffices : Eq.{u_4 + 1} (α := N)
  (∑ k : Fin (n + 1),
    HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑k : ℕ))
      ((((f : (a : M) → M [⋀^Fin n]→ₗ[R] N) (v k) : M [⋀^Fin n]→ₗ[R] N) : (a : Fin n → M) → N)
          (k.removeNth (α := fun (i : Fin (n + 1)) ↦ M) v) :
        N))
  0
Tactic: suffices ∑ k : Fin (n + 1), (-1) ^ (k : ℕ) • f (v k) (k.removeNth v) = 0 by simpa
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Uncurry.Fin (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
N₂ : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N
inst_4 : AddCommGroup N₂
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module R N
inst_8 : Module R N₂
n : ℕ
f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
i j : Fin (n + 1)
hvij : v i = v j
hij : i ≠ j
⊢ ∑ k : Fin (n + 1),
      HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑k : ℕ))
        ((((f : (a : M) → M [⋀^Fin n]→ₗ[R] N) (v k) : M [⋀^Fin n]→ₗ[R] N) : (a : Fin n → M) → N)
            (k.removeNth (α := fun (i : Fin (n + 1)) ↦ M) v) :
          N) =
    HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
        ((((f : (a : M) → M [⋀^Fin n]→ₗ[R] N) (v i) : M [⋀^Fin n]→ₗ[R] N) : (a : Fin n → M) → N)
            (i.removeNth (α := fun (i : Fin (n + 1)) ↦ M) v) :
          N) +
      HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑j : ℕ))
        ((((f : (a : M) → M [⋀^Fin n]→ₗ[R] N) (v j) : M [⋀^Fin n]→ₗ[R] N) : (a : Fin n → M) → N)
            (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M) v) :
          N)
have refine : ∀ (k : Fin (n + 1)),
  k ≠ i ∧ k ≠ j →
    ∀ (hki : k ≠ i) (hkj : k ≠ j),
      HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑k : ℕ))
          ((((f : (a : M) → M [⋀^Fin n]→ₗ[R] N) (v k) : M [⋀^Fin n]→ₗ[R] N) : (a : Fin n → M) → N)
              (k.removeNth (α := fun (i : Fin (n + 1)) ↦ M) v) :
            N) =
        0
Tactic: refine Fintype.sum_eq_add _ _ hij fun k ⟨hki, hkj⟩ ↦ ?_