awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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
rw : Even ((↑p : ℕ) + (↑p : ℕ))
⊢ 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)

Tactic:
rw [map_insertNth, smul_smul, ← pow_add, Even.neg_one_pow, one_smul]

Premises used: pow_add, smul_smul, Even.neg_one_pow, one_smul, AlternatingMap.map_insertNth
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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 : ℕ
h : (↑p : ℕ) + (↑p : ℕ) = (↑p : ℕ) + (↑p : ℕ)
⊢ Even ((↑p : ℕ) + (↑p : ℕ))

Tactic:
use p
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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
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
⊢ 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

Tactic:
rcases exists_succAbove_eq hij with ⟨i, rfl⟩

Premises used: Fin.exists_succAbove_eq, rfl
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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
⊢ ∃ (m : ℕ), m + 1 = n

Tactic:
simp [i.pos]

Premises used: Fin.pos
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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
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
⊢ 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:
obtain ⟨m, rfl⟩ : ∃ m, m + 1 = n := by simp [i.pos]

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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
rw : v j = j.removeNth (α := fun (i : Fin (m + 1 + 1)) ↦ M) v i
⊢ 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:
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]

Premises used: Iff.mpr, one_pow, Fin.succAbove_succAbove_predAbove, neg_one_pow_two, neg_smul, Fin.removeNth_removeNth_eq_swap, Fin.insertNth_self_removeNth, pow_add, smul_smul, Fin.removeNth, sq, Fin.predAbove, Fin.val, pow_mul, one_smul, HPow.hPow, neg_add_cancel, Function.update_eq_self_iff, Fin.insertNth_removeNth, AlternatingMap.neg_one_pow_smul_map_insertNth, AlternatingMap.map_insertNth, pow_mul', SemigroupAction.mul_smul, Fin.neg_one_pow_succAbove_add_predAbove
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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
⊢ v j = j.removeNth (α := fun (i : Fin (m + 1 + 1)) ↦ M) v i

Tactic:
hvij.symm

Premises used: Fin.removeNth, Eq.symm
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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
⊢ v j = j.removeNth (α := fun (i : Fin (m + 1 + 1)) ↦ M) v i

Tactic:
exact hvij.symm

Premises used: Eq.symm
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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
this :
  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
⊢ 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

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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
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
⊢ 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

Tactic:
suffices ∑ k : Fin (n + 1), (-1) ^ (k : ℕ) • f (v k) (k.removeNth v) = 0 by simpa
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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)

Tactic:
Fintype.sum_eq_add _ _ hij fun k ⟨hki, hkj⟩ ↦ ?_

Premises used: _private.0.AlternatingMap.alternatizeUncurryFin.match_1, Fin.removeNth, Fin.val, HPow.hPow, Fintype.sum_eq_add, HSMul.hSMul, OfNat.ofNat, Eq, DFunLike.coe, Neg.neg
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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
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
⊢ ∑ 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)

Tactic:
refine Fintype.sum_eq_add _ _ hij fun k ⟨hki, hkj⟩ ↦ ?_

Premises used: _private.0.AlternatingMap.alternatizeUncurryFin.match_1, Fintype.sum_eq_add, OfNat.ofNat, Eq
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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)
h : k ≠ i ∧ k ≠ j
hki : k ≠ i
hkj : k ≠ j
rcases :
  ∀ (i : Fin n) (hvij : v (k.succAbove i) = v j) (hij : k.succAbove i ≠ j),
    k ≠ k.succAbove i ∧ k ≠ j →
      ∀ (hki : k ≠ k.succAbove i),
        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
⊢ 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:
rcases exists_succAbove_eq hki.symm with ⟨i, rfl⟩

Premises used: Fin.exists_succAbove_eq, Ne.symm, rfl
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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
j k : Fin (n + 1)
hkj : k ≠ j
i : Fin n
hvij : v (k.succAbove i) = v j
hij : k.succAbove i ≠ j
h : k ≠ k.succAbove i ∧ k ≠ j
hki : k ≠ k.succAbove i
rcases :
  ∀ (j : Fin n) (hkj : k ≠ k.succAbove j) (hvij : v (k.succAbove i) = v (k.succAbove j))
    (hij : k.succAbove i ≠ k.succAbove j),
    k ≠ k.succAbove i ∧ k ≠ k.succAbove 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
⊢ 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:
rcases exists_succAbove_eq hkj.symm with ⟨j, rfl⟩

Premises used: Fin.exists_succAbove_eq, Ne.symm, rfl
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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
k : Fin (n + 1)
i : Fin n
hki : k ≠ k.succAbove i
j : Fin n
hkj : k ≠ k.succAbove j
hvij : v (k.succAbove i) = v (k.succAbove j)
hij : k.succAbove i ≠ k.succAbove j
h : k ≠ k.succAbove i ∧ k ≠ k.succAbove j
rw : HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑k : ℕ)) 0 = 0
rw₁ rw₂ : Eq.{u_4 + 1} (α := N) 0 0
⊢ 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:
rw [(f (v k)).map_eq_zero_of_eq _ hvij (ne_of_apply_ne _ hij), smul_zero]

Premises used: smul_zero, ne_of_apply_ne, AlternatingMap.map_eq_zero_of_eq, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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
hvij₁ : v i = v j
hij₁ : i ≠ j
⊢ 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) =
    0

Tactic:
rw [hvij, neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq]

Premises used: AlternatingMap.neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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
⊢ v i = v j

Tactic:
assumption
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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
⊢ i ≠ j

Tactic:
assumption
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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)
_₁ :
  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) =
    0
⊢ 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:
calc
      _ = (-1) ^ (i : ℕ) • f (v i) (i.removeNth v) + (-1) ^ (j : ℕ) • f (v j) (j.removeNth v) := by
        refine Fintype.sum_eq_add _ _ hij fun k ⟨hki, hkj⟩ ↦ ?_
        rcases exists_succAbove_eq hki.symm with ⟨i, rfl⟩
        rcases exists_succAbove_eq hkj.symm with ⟨j, rfl⟩
        rw [(f (v k)).map_eq_zero_of_eq _ hvij (ne_of_apply_ne _ hij), smul_zero]
      _ = 0 := by
        rw [hvij, neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq] <;> assumption

Premises used: Fin.removeNth, Fin.val, OfNat.ofNat, DFunLike.coe, Neg.neg
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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 →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
⊢ Eq.{u_4 + 1} (α := N) ((alternatizeUncurryFin f : (a : Fin (n + 1) → M) → N) v : N)
    (∑ i : Fin (n + 1),
        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) :
      N)

Tactic:
simp [alternatizeUncurryFin]

Premises used: AlternatingMap.alternatizeUncurryFin
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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 g : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
H :
  ∀ (x : Fin (n + 1) → M),
    Eq.{u_4 + 1} (α := N) ((alternatizeUncurryFin (f + g) : (a : Fin (n + 1) → M) → N) x : N)
      ((alternatizeUncurryFin f + alternatizeUncurryFin g : (a : Fin (n + 1) → M) → N) x : N)
⊢ alternatizeUncurryFin (f + g) = alternatizeUncurryFin f + alternatizeUncurryFin g

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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 g : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
x : Fin (n + 1) → M
⊢ Eq.{u_4 + 1} (α := N) ((alternatizeUncurryFin (f + g) : (a : Fin (n + 1) → M) → N) x : N)
    ((alternatizeUncurryFin f + alternatizeUncurryFin g : (a : Fin (n + 1) → M) → N) x : N)

Tactic:
simp [alternatizeUncurryFin_apply, Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib, AlternatingMap.alternatizeUncurryFin_apply
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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
H :
  ∀ (v : Fin (n + 1) → M),
    Eq.{u_4 + 1} (α := N) ((alternatizeUncurryFin f.curryLeft : (a : Fin (n + 1) → M) → N) v : N)
      (((n + 1) • f : (a : Fin (n + 1) → M) → N) v : N)
⊢ alternatizeUncurryFin f.curryLeft = (n + 1) • f

Tactic:
ext v
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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
v : Fin (n + 1) → M
⊢ Eq.{u_4 + 1} (α := N) ((alternatizeUncurryFin f.curryLeft : (a : Fin (n + 1) → M) → N) v : N)
    (((n + 1) • f : (a : Fin (n + 1) → M) → N) v : N)

Tactic:
simp [alternatizeUncurryFin_apply, ← map_insertNth]

Premises used: AlternatingMap.alternatizeUncurryFin_apply, AlternatingMap.map_insertNth
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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 : ℕ
S : Type u_6
inst_5 : Monoid S
inst_6 : DistribMulAction S N
inst_7 : SMulCommClass R S N
c : S
f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
H :
  ∀ (v : Fin (n + 1) → M),
    Eq.{u_4 + 1} (α := N) ((alternatizeUncurryFin (c • f) : (a : Fin (n + 1) → M) → N) v : N)
      ((c • alternatizeUncurryFin f : (a : Fin (n + 1) → M) → N) v : N)
⊢ alternatizeUncurryFin (c • f) = c • alternatizeUncurryFin f

Tactic:
ext v
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
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 : ℕ
S : Type u_6
inst_5 : Monoid S
inst_6 : DistribMulAction S N
inst_7 : SMulCommClass R S N
c : S
f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
⊢ Eq.{u_4 + 1} (α := N) ((alternatizeUncurryFin (c • f) : (a : Fin (n + 1) → M) → N) v : N)
    ((c • alternatizeUncurryFin f : (a : Fin (n + 1) → M) → N) v : N)

Tactic:
simp [alternatizeUncurryFin_apply, smul_comm _ c, Finset.smul_sum]

Premises used: AlternatingMap.alternatizeUncurryFin_apply, Finset.smul_sum, SMulCommClass.smul_comm