awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
h : 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
have 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
Tactic: rcases exists_succAbove_eq hki.symm with ⟨i, rfl⟩
Cleared hypotheses: i, hvij, hij, h, hki
-- 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
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
⊢ 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
have 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
Tactic: rcases exists_succAbove_eq hkj.symm with ⟨j, rfl⟩
Cleared hypotheses: j, hkj, hvij, hij, h
-- 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
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
⊢ 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
have rw : HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑k : ℕ)) 0 = 0
Tactic: rw [(f (v k)).map_eq_zero_of_eq _ hvij (ne_of_apply_ne _ hij), smul_zero]
-- 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
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
⊢ 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
have rw₁ : Eq.{u_4 + 1} (α := N) 0 0
Tactic: rw [(f (v k)).map_eq_zero_of_eq _ hvij (ne_of_apply_ne _ hij), smul_zero]
-- 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)
    (∑ 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
have _ : ∑ 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: 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
-- 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)
⊢ 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
have _₁ : 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: 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
-- 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 g : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
⊢ alternatizeUncurryFin (f + g) = alternatizeUncurryFin f + alternatizeUncurryFin g
have 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)
Tactic: ext
-- 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
⊢ alternatizeUncurryFin f.curryLeft = (n + 1) • f
have 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)
Tactic: ext v
-- 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 : ℕ
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
⊢ alternatizeUncurryFin (c • f) = c • alternatizeUncurryFin f
have 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)
Tactic: ext v
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Uncurry.Fin (hypothesis)
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 →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
i j : Fin (n + 1)
hj : j ∈ Finset.Ici i
⊢ HPow.hPow (α := ℤ) (-1) (↑i : ℕ) •
        HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑j : ℕ))
          ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v i.castSucc) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                      (a : M) → M [⋀^Fin n]→ₗ[R] N)
                    (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v j) :
                  M [⋀^Fin n]→ₗ[R] N) :
                (a : Fin n → M) → N)
              (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
                (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
            N) +
      HPow.hPow (α := ℤ) (-1) ((↑j : ℕ) + 1) •
        HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v j.succ) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                      (a : M) → M [⋀^Fin n]→ₗ[R] N)
                    (j.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v i) :
                  M [⋀^Fin n]→ₗ[R] N) :
                (a : Fin n → M) → N)
              (i.removeNth (α := fun (i : Fin (n + 1)) ↦ M) (j.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
            N) =
    HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)) •
      HSub.hSub (α := N) (β := N)
        ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v i.castSucc) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                    (a : M) → M [⋀^Fin n]→ₗ[R] N)
                  (v j.succ) :
                M [⋀^Fin n]→ₗ[R] N) :
              (a : Fin n → M) → N)
            (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
              (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
          N)
        ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v j.succ) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                    (a : M) → M [⋀^Fin n]→ₗ[R] N)
                  (v i.castSucc) :
                M [⋀^Fin n]→ₗ[R] N) :
              (a : Fin n → M) → N)
            (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
              (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
          N)
have hj₁ : i ≤ j
Tactic: rw [Finset.mem_Ici] at hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Uncurry.Fin (hypothesis)
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 →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
i j : Fin (n + 1)
hj : i ≤ j
⊢ HPow.hPow (α := ℤ) (-1) (↑i : ℕ) •
        HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑j : ℕ))
          ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v i.castSucc) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                      (a : M) → M [⋀^Fin n]→ₗ[R] N)
                    (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v j) :
                  M [⋀^Fin n]→ₗ[R] N) :
                (a : Fin n → M) → N)
              (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
                (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
            N) +
      HPow.hPow (α := ℤ) (-1) ((↑j : ℕ) + 1) •
        HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v j.succ) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                      (a : M) → M [⋀^Fin n]→ₗ[R] N)
                    (j.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v i) :
                  M [⋀^Fin n]→ₗ[R] N) :
                (a : Fin n → M) → N)
              (i.removeNth (α := fun (i : Fin (n + 1)) ↦ M) (j.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
            N) =
    HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)) •
      HSub.hSub (α := N) (β := N)
        ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v i.castSucc) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                    (a : M) → M [⋀^Fin n]→ₗ[R] N)
                  (v j.succ) :
                M [⋀^Fin n]→ₗ[R] N) :
              (a : Fin n → M) → N)
            (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
              (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
          N)
        ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v j.succ) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                    (a : M) → M [⋀^Fin n]→ₗ[R] N)
                  (v i.castSucc) :
                M [⋀^Fin n]→ₗ[R] N) :
              (a : Fin n → M) → N)
            (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
              (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
          N)
have H₁ : i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v j = v j.succ
Tactic: have H₁ : i.castSucc.removeNth v j = v j.succ := by
    simp [Fin.removeNth_apply, Fin.succAbove_of_le_castSucc, hj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Uncurry.Fin (hypothesis)
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 →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
i j : Fin (n + 1)
hj : i ≤ j
H₁ : i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v j = v j.succ
⊢ HPow.hPow (α := ℤ) (-1) (↑i : ℕ) •
        HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑j : ℕ))
          ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v i.castSucc) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                      (a : M) → M [⋀^Fin n]→ₗ[R] N)
                    (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v j) :
                  M [⋀^Fin n]→ₗ[R] N) :
                (a : Fin n → M) → N)
              (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
                (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
            N) +
      HPow.hPow (α := ℤ) (-1) ((↑j : ℕ) + 1) •
        HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
          ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v j.succ) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                      (a : M) → M [⋀^Fin n]→ₗ[R] N)
                    (j.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v i) :
                  M [⋀^Fin n]→ₗ[R] N) :
                (a : Fin n → M) → N)
              (i.removeNth (α := fun (i : Fin (n + 1)) ↦ M) (j.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
            N) =
    HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)) •
      HSub.hSub (α := N) (β := N)
        ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v i.castSucc) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                    (a : M) → M [⋀^Fin n]→ₗ[R] N)
                  (v j.succ) :
                M [⋀^Fin n]→ₗ[R] N) :
              (a : Fin n → M) → N)
            (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
              (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
          N)
        ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v j.succ) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                    (a : M) → M [⋀^Fin n]→ₗ[R] N)
                  (v i.castSucc) :
                M [⋀^Fin n]→ₗ[R] N) :
              (a : Fin n → M) → N)
            (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
              (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
          N)
have H₂ : j.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v i = v i.castSucc
Tactic: have H₂ : j.succ.removeNth v i = v i.castSucc := by
    simp [Fin.removeNth_apply, Fin.succAbove_of_castSucc_lt, hj]
-- 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 →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
i j : Fin (n + 1)
hj : i ≤ j
H₁ : i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v j = v j.succ
H₂ : j.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v i = v i.castSucc
⊢ HPow.hPow (α := ℤ) (-1) (↑i : ℕ) •
        HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑j : ℕ))
          ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v i.castSucc) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                      (a : M) → M [⋀^Fin n]→ₗ[R] N)
                    (v j.succ) :
                  M [⋀^Fin n]→ₗ[R] N) :
                (a : Fin n → M) → N)
              (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
                (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
            N) -
      HPow.hPow (α := ℤ) (-1) (↑i : ℕ) •
        HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑j : ℕ))
          ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v j.succ) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                      (a : M) → M [⋀^Fin n]→ₗ[R] N)
                    (v i.castSucc) :
                  M [⋀^Fin n]→ₗ[R] N) :
                (a : Fin n → M) → N)
              (i.removeNth (α := fun (i : Fin (n + 1)) ↦ M) (j.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
            N) =
    HPow.hPow (α := ℤ) (-1) (↑i : ℕ) •
        HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑j : ℕ))
          ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v i.castSucc) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                      (a : M) → M [⋀^Fin n]→ₗ[R] N)
                    (v j.succ) :
                  M [⋀^Fin n]→ₗ[R] N) :
                (a : Fin n → M) → N)
              (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
                (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
            N) -
      HPow.hPow (α := ℤ) (-1) (↑i : ℕ) •
        HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑j : ℕ))
          ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v j.succ) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                      (a : M) → M [⋀^Fin n]→ₗ[R] N)
                    (v i.castSucc) :
                  M [⋀^Fin n]→ₗ[R] N) :
                (a : Fin n → M) → N)
              (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
                (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
            N)
have e_a : i.removeNth (α := fun (i : Fin (n + 1)) ↦ M) (j.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v) =
  j.removeNth (α := fun (i : Fin (n + 1)) ↦ M) (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)
Tactic: congr 4
-- 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 →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
i j : Fin (n + 1)
hj : i ≤ j
H₁ : i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v j = v j.succ
H₂ : j.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v i = v i.castSucc
⊢ i.removeNth (α := fun (i : Fin (n + 1)) ↦ M) (j.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v) =
    j.removeNth (α := fun (i : Fin (n + 1)) ↦ M) (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)
have e_a : (i.predAbove j.succ).removeNth (α := fun (i : Fin (n + 1)) ↦ M)
    ((j.succ.succAbove i).removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v) =
  j.removeNth (α := fun (i : Fin (n + 1)) ↦ M) (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)
Tactic: rw [removeNth_removeNth_eq_swap]
-- 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 →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
hf :
  ∀ (x y : M),
    Eq (α := M [⋀^Fin n]→ₗ[R] N)
      ((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) x : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) : (a : M) → M [⋀^Fin n]→ₗ[R] N) y :
        M [⋀^Fin n]→ₗ[R] N)
      ((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) y : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) : (a : M) → M [⋀^Fin n]→ₗ[R] N) x :
        M [⋀^Fin n]→ₗ[R] N)
⊢ alternatizeUncurryFin (alternatizeUncurryFinLM ∘ₗ f) = 0
have H : ∀ (v : Fin (n + 1 + 1) → M),
  Eq.{u_4 + 1} (α := N) ((alternatizeUncurryFin (alternatizeUncurryFinLM ∘ₗ f) : (a : Fin (n + 1 + 1) → M) → N) v : N)
    ((0 : (a : Fin (n + 1 + 1) → M) → N) v : N)
Tactic: ext v
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
⊢ Eq (α := Ideal 𝕜[X]) (Ideal.span {annIdealGenerator 𝕜 a}) (annIdeal 𝕜 a)
have pos : ∀ (h : Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0),
  Eq (α := Ideal 𝕜[X]) (Ideal.span {annIdealGenerator 𝕜 a}) (annIdeal 𝕜 a)
Tactic: by_cases h : annIdealGenerator 𝕜 a = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.AnnihilatingPolynomial (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
pos :
  ∀ (h : Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0),
    Eq (α := Ideal 𝕜[X]) (Ideal.span {annIdealGenerator 𝕜 a}) (annIdeal 𝕜 a)
⊢ Eq (α := Ideal 𝕜[X]) (Ideal.span {annIdealGenerator 𝕜 a}) (annIdeal 𝕜 a)
have neg : ∀ (h : ¬Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0),
  Eq (α := Ideal 𝕜[X]) (Ideal.span {annIdealGenerator 𝕜 a}) (annIdeal 𝕜 a)
Tactic: by_cases h : annIdealGenerator 𝕜 a = 0