awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst_5 : DecidableEq ι
i j : ι
hij : i ≠ j
rw : v j = update (β := fun (a : ι) ↦ M) v i (v j) j
⊢ update (β := fun (a : ι) ↦ M) v i (v j) i = update (β := fun (a : ι) ↦ M) v i (v j) j
have rw₁ : v j = v j
Tactic: rw [Function.update_self, Function.update_of_ne hij.symm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst_5 : DecidableEq ι
i j : ι
hij : i ≠ j
m : M
⊢ update (β := fun (a : ι) ↦ M) (update (β := fun (a : ι) ↦ M) v i m) j m i =
    update (β := fun (a : ι) ↦ M) (update (β := fun (a : ι) ↦ M) v i m) j m j
have rw : update (β := fun (a : ι) ↦ M) (update (β := fun (a : ι) ↦ M) v i m) j m i = m
Tactic: rw [Function.update_self, Function.update_of_ne hij, Function.update_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst_5 : DecidableEq ι
i j : ι
hij : i ≠ j
m : M
rw : update (β := fun (a : ι) ↦ M) (update (β := fun (a : ι) ↦ M) v i m) j m i = m
⊢ update (β := fun (a : ι) ↦ M) (update (β := fun (a : ι) ↦ M) v i m) j m i =
    update (β := fun (a : ι) ↦ M) (update (β := fun (a : ι) ↦ M) v i m) j m j
have rw₁ : update (β := fun (a : ι) ↦ M) v i m i = m
Tactic: rw [Function.update_self, Function.update_of_ne hij, Function.update_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst_5 : DecidableEq ι
i j : ι
hij : i ≠ j
m : M
rw : update (β := fun (a : ι) ↦ M) (update (β := fun (a : ι) ↦ M) v i m) j m i = m
rw₁ : update (β := fun (a : ι) ↦ M) v i m i = m
⊢ update (β := fun (a : ι) ↦ M) (update (β := fun (a : ι) ↦ M) v i m) j m i =
    update (β := fun (a : ι) ↦ M) (update (β := fun (a : ι) ↦ M) v i m) j m j
have rw₂ : m = m
Tactic: rw [Function.update_self, Function.update_of_ne hij, Function.update_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst_5 : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ HAdd.hAdd (α := N) (β := N) ((f : (a : ι → M) → N) (v ∘ (⇑(Equiv.swap i j) : (a : ι) → ι)) : N)
      ((f : (a : ι → M) → N) v : N) =
    0
have rw : HAdd.hAdd (α := N) (β := N)
    ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) (update (β := fun (a : ι) ↦ M) v j (v i)) i (v j)) : N)
    ((f : (a : ι → M) → N) v : N) =
  0
Tactic: rw [Equiv.comp_swap_eq_update]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst_5 : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ HAdd.hAdd (α := N) (β := N)
      ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) (update (β := fun (a : ι) ↦ M) v j (v i)) i (v j)) : N)
      ((f : (a : ι → M) → N) v : N) =
    0
have h : HAdd.hAdd (α := N) (β := N)
    ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) (update (β := fun (a : ι) ↦ M) v j (v i)) i (v j)) : N)
    ((f : (a : ι → M) → N) v : N) =
  (f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) (update (β := fun (a : ι) ↦ M) v i (v i + v j)) j (v i + v j))
Tactic: convert! f.map_update_update v hij (v i + v j)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst_5 : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ HAdd.hAdd (α := N) (β := N) ((f : (a : ι → M) → N) v : N)
      ((f : (a : ι → M) → N) (v ∘ (⇑(Equiv.swap i j) : (a : ι) → ι)) : N) =
    0
have rw : HAdd.hAdd (α := N) (β := N) ((f : (a : ι → M) → N) (v ∘ (⇑(Equiv.swap i j) : (a : ι) → ι)) : N)
    ((f : (a : ι → M) → N) v : N) =
  0
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N' : Type u_6
inst_3 : AddCommGroup N'
inst_4 : Module R N'
ι : Type u_7
g : M [⋀^ι]→ₗ[R] N'
inst_5 : DecidableEq ι
inst_6 : Fintype ι
v : ι → M
σ : Equiv.Perm ι
⊢ (g : (a : ι → M) → N') (v ∘ (⇑σ : (a : ι) → ι)) =
    HSMul.hSMul (α := ℤˣ) (β := N') (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ)
      ((g : (a : ι → M) → N') v : N')
have one : (g : (a : ι → M) → N') (v ∘ (⇑1 : (a : ι) → ι)) =
  HSMul.hSMul (α := ℤˣ) (β := N') (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) 1)
    ((g : (a : ι → M) → N') v : N')
Tactic: induction σ using Equiv.Perm.swap_induction_on' with
  | one => simp
  | mul_swap s x y hxy hI => simp_all [← Function.comp_assoc, g.map_swap]
Cleared hypotheses: σ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N' : Type u_6
inst_3 : AddCommGroup N'
inst_4 : Module R N'
ι : Type u_7
g : M [⋀^ι]→ₗ[R] N'
inst_5 : DecidableEq ι
inst_6 : Fintype ι
v : ι → M
σ : Equiv.Perm ι
one :
  (g : (a : ι → M) → N') (v ∘ (⇑1 : (a : ι) → ι)) =
    HSMul.hSMul (α := ℤˣ) (β := N') (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) 1)
      ((g : (a : ι → M) → N') v : N')
⊢ (g : (a : ι → M) → N') (v ∘ (⇑σ : (a : ι) → ι)) =
    HSMul.hSMul (α := ℤˣ) (β := N') (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ)
      ((g : (a : ι → M) → N') v : N')
have mul_swap : ∀ (s : Equiv.Perm ι) (x y : ι) (hxy : x ≠ y)
  (hI :
    (g : (a : ι → M) → N') (v ∘ (⇑s : (a : ι) → ι)) =
      HSMul.hSMul (α := ℤˣ) (β := N') (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) s : ℤˣ)
        ((g : (a : ι → M) → N') v : N')),
  (g : (a : ι → M) → N') (v ∘ (⇑(s * Equiv.swap x y) : (a : ι) → ι)) =
    HSMul.hSMul (α := ℤˣ) (β := N')
      (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) (s * Equiv.swap x y) : ℤˣ)
      ((g : (a : ι → M) → N') v : N')
Tactic: induction σ using Equiv.Perm.swap_induction_on' with
  | one => simp
  | mul_swap s x y hxy hI => simp_all [← Function.comp_assoc, g.map_swap]
Cleared hypotheses: σ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N' : Type u_6
inst_3 : AddCommGroup N'
inst_4 : Module R N'
ι : Type u_7
g : M [⋀^ι]→ₗ[R] N'
v : ι → M
inst_5 : DecidableEq ι
inst_6 : Fintype ι
σ : Equiv.Perm ι
⊢ (g : (a : ι → M) → N') v =
    HSMul.hSMul (α := ℤˣ) (β := N') (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ)
      ((g : (a : ι → M) → N') (v ∘ (⇑σ : (a : ι) → ι)) : N')
have rw : (g : (a : ι → M) → N') v =
  HSMul.hSMul (β := N')
    (HMul.hMul (α := ℤˣ) (β := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ)
      (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ))
    ((g : (a : ι → M) → N') v : N')
Tactic: rw [g.map_perm, smul_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
M' : Type u_5
inst_7 : AddCommGroup M'
inst_8 : Module R M'
N' : Type u_6
inst_9 : AddCommGroup N'
inst_10 : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
M₂ : Type u_10
inst_11 : AddCommMonoid M₂
inst_12 : Module R M₂
M₃ : Type u_11
inst_13 : AddCommMonoid M₃
inst_14 : Module R M₃
f_1 f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
σ : ι ≃ ι'
f : M [⋀^ι]→ₗ[R] N
⊢ domDomCongr σ.symm (domDomCongr σ f) = f
have H : ∀ (x : ι → M),
  Eq.{u_3 + 1} (α := N) ((domDomCongr σ.symm (domDomCongr σ f) : (a : ι → M) → N) x : N) ((f : (a : ι → M) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
M' : Type u_5
inst_7 : AddCommGroup M'
inst_8 : Module R M'
N' : Type u_6
inst_9 : AddCommGroup N'
inst_10 : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
M₂ : Type u_10
inst_11 : AddCommMonoid M₂
inst_12 : Module R M₂
M₃ : Type u_11
inst_13 : AddCommMonoid M₃
inst_14 : Module R M₃
f f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
σ : ι ≃ ι'
m : M [⋀^ι']→ₗ[R] N
⊢ domDomCongr σ (domDomCongr σ.symm m) = m
have H : ∀ (x : ι' → M),
  Eq.{u_3 + 1} (α := N) ((domDomCongr σ (domDomCongr σ.symm m) : (a : ι' → M) → N) x : N) ((m : (a : ι' → M) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
M' : Type u_5
inst_7 : AddCommGroup M'
inst_8 : Module R M'
N' : Type u_6
inst_9 : AddCommGroup N'
inst_10 : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
M₂ : Type u_10
inst_11 : AddCommMonoid M₂
inst_12 : Module R M₂
M₃ : Type u_11
inst_13 : AddCommMonoid M₃
inst_14 : Module R M₃
f_1 f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
S : Type u_12
inst_15 : Semiring S
inst_16 : Module S N
inst_17 : SMulCommClass R S N
σ : ι ≃ ι'
f : M [⋀^ι]→ₗ[R] N
⊢ domDomCongr σ.symm (domDomCongr σ f) = f
have H : ∀ (x : ι → M),
  Eq.{u_3 + 1} (α := N) ((domDomCongr σ.symm (domDomCongr σ f) : (a : ι → M) → N) x : N) ((f : (a : ι → M) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
M' : Type u_5
inst_7 : AddCommGroup M'
inst_8 : Module R M'
N' : Type u_6
inst_9 : AddCommGroup N'
inst_10 : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
M₂ : Type u_10
inst_11 : AddCommMonoid M₂
inst_12 : Module R M₂
M₃ : Type u_11
inst_13 : AddCommMonoid M₃
inst_14 : Module R M₃
f f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
S : Type u_12
inst_15 : Semiring S
inst_16 : Module S N
inst_17 : SMulCommClass R S N
σ : ι ≃ ι'
m : M [⋀^ι']→ₗ[R] N
⊢ domDomCongr σ (domDomCongr σ.symm m) = m
have H : ∀ (x : ι' → M),
  Eq.{u_3 + 1} (α := N) ((domDomCongr σ (domDomCongr σ.symm m) : (a : ι' → M) → N) x : N) ((m : (a : ι' → M) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
ι : Type u_7
K : Type u_12
M : Type u_13
N : Type u_14
inst : Ring K
inst_1 : IsDomain K
inst_2 : AddCommGroup M
inst_3 : Module K M
inst_4 : AddCommGroup N
inst_5 : Module K N
inst_6 : IsTorsionFree K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h : ¬LinearIndependent K v
⊢ Eq.{u_14 + 1} (α := N) ((f : (a : ι → M) → N) v : N) (0 : N)
have obtain : ∀ (s : Finset ι) (g : ι → K) (h : Eq.{u_13 + 1} (α := M) (∑ i ∈ s, g i • v i) 0) (i : ι) (hi : i ∈ s) (hz : g i ≠ 0),
  Eq.{u_14 + 1} (α := N) ((f : (a : ι → M) → N) v : N) (0 : N)
Tactic: obtain ⟨s, g, h, i, hi, hz⟩ := not_linearIndependent_iff.mp h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (hypothesis)
Goal:
ι : Type u_7
K : Type u_12
M : Type u_13
N : Type u_14
inst : Ring K
inst_1 : IsDomain K
inst_2 : AddCommGroup M
inst_3 : Module K M
inst_4 : AddCommGroup N
inst_5 : Module K N
inst_6 : IsTorsionFree K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h_1 : ¬LinearIndependent K v
s : Finset ι
g : ι → K
h : Eq.{u_13 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
hz : g i ≠ 0
this_1 : DecidableEq ι := Classical.decEq ι
this : Eq.{u_14 + 1} (α := N) ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) v i (g i • v i)) : N) (0 : N)
⊢ Eq.{u_14 + 1} (α := N) ((f : (a : ι → M) → N) v : N) (0 : N)
have this₁ : g i = 0 ∨ Eq.{u_14 + 1} (α := N) ((f : (a : ι → M) → N) v : N) (0 : N)
Tactic: rw [f.map_update_smul, Function.update_eq_self, smul_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
ι : Type u_7
K : Type u_12
M : Type u_13
N : Type u_14
inst : Ring K
inst_1 : IsDomain K
inst_2 : AddCommGroup M
inst_3 : Module K M
inst_4 : AddCommGroup N
inst_5 : Module K N
inst_6 : IsTorsionFree K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h_1 : ¬LinearIndependent K v
s : Finset ι
g : ι → K
h : Eq.{u_13 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ Eq.{u_14 + 1} (α := N) ((f : (a : ι → M) → N) v : N) (0 : N)
have suffices : Eq.{u_14 + 1} (α := N) ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) v i (g i • v i)) : N) (0 : N)
Tactic: suffices f (update v i (g i • v i)) = 0 by
    rw [f.map_update_smul, Function.update_eq_self, smul_eq_zero] at this
    exact Or.resolve_left this hz
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (hypothesis)
Goal:
ι : Type u_7
K : Type u_12
M : Type u_13
N : Type u_14
inst : Ring K
inst_1 : IsDomain K
inst_2 : AddCommGroup M
inst_3 : Module K M
inst_4 : AddCommGroup N
inst_5 : Module K N
inst_6 : IsTorsionFree K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h_1 : ¬LinearIndependent K v
s : Finset ι
g : ι → K
h : Eq.{u_13 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ Eq.{u_14 + 1} (α := N) ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) v i (g i • v i)) : N) (0 : N)
have h₁ : g i • v i = -∑ x ∈ s.erase i, g x • v x
Tactic: rw [← Finset.insert_erase hi, Finset.sum_insert (s.notMem_erase i), add_eq_zero_iff_eq_neg] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
ι : Type u_7
K : Type u_12
M : Type u_13
N : Type u_14
inst : Ring K
inst_1 : IsDomain K
inst_2 : AddCommGroup M
inst_3 : Module K M
inst_4 : AddCommGroup N
inst_5 : Module K N
inst_6 : IsTorsionFree K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h_1 : ¬LinearIndependent K v
s : Finset ι
g : ι → K
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
h : g i • v i = -∑ x ∈ s.erase i, g x • v x
⊢ Eq.{u_14 + 1} (α := N) (∑ a ∈ s.erase i, (f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) v i (g a • v a))) 0
have h₁ : ∀ x ∈ s.erase i,
  Eq.{u_14 + 1} (α := N) ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) v i (g x • v x)) : N) (0 : N)
Tactic: apply Finset.sum_eq_zero
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (hypothesis)
Goal:
ι : Type u_7
K : Type u_12
M : Type u_13
N : Type u_14
inst : Ring K
inst_1 : IsDomain K
inst_2 : AddCommGroup M
inst_3 : Module K M
inst_4 : AddCommGroup N
inst_5 : Module K N
inst_6 : IsTorsionFree K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h_1 : ¬LinearIndependent K v
s : Finset ι
g : ι → K
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
h : g i • v i = -∑ x ∈ s.erase i, g x • v x
j : ι
hj : j ∈ s.erase i
⊢ Eq.{u_14 + 1} (α := N) ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) v i (g j • v j)) : N) (0 : N)
have hij : j ≠ i
Tactic: obtain ⟨hij, _⟩ := Finset.mem_erase.mp hj
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (hypothesis)
Goal:
ι : Type u_7
K : Type u_12
M : Type u_13
N : Type u_14
inst : Ring K
inst_1 : IsDomain K
inst_2 : AddCommGroup M
inst_3 : Module K M
inst_4 : AddCommGroup N
inst_5 : Module K N
inst_6 : IsTorsionFree K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h_1 : ¬LinearIndependent K v
s : Finset ι
g : ι → K
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
h : g i • v i = -∑ x ∈ s.erase i, g x • v x
j : ι
hj : j ∈ s.erase i
hij : j ≠ i
⊢ Eq.{u_14 + 1} (α := N) ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) v i (g j • v j)) : N) (0 : N)
have right : j ∈ s
Tactic: obtain ⟨hij, _⟩ := Finset.mem_erase.mp hj
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
ι : Type u_7
K : Type u_12
M : Type u_13
N : Type u_14
inst : Ring K
inst_1 : IsDomain K
inst_2 : AddCommGroup M
inst_3 : Module K M
inst_4 : AddCommGroup N
inst_5 : Module K N
inst_6 : IsTorsionFree K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h_1 : ¬LinearIndependent K v
s : Finset ι
g : ι → K
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
h : g i • v i = -∑ x ∈ s.erase i, g x • v x
j : ι
hj : j ∈ s.erase i
hij : j ≠ i
right : j ∈ s
⊢ Eq.{u_14 + 1} (α := N) ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) v i (g j • v j)) : N) (0 : N)
have h₁ : HSMul.hSMul (β := N) (g j) ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) v i (v j)) : N) = 0
Tactic: rw [f.map_update_smul, f.map_update_self _ hij.symm, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
ι : Type u_7
K : Type u_12
M : Type u_13
N : Type u_14
inst : Ring K
inst_1 : IsDomain K
inst_2 : AddCommGroup M
inst_3 : Module K M
inst_4 : AddCommGroup N
inst_5 : Module K N
inst_6 : IsTorsionFree K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h_1 : ¬LinearIndependent K v
s : Finset ι
g : ι → K
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
h : g i • v i = -∑ x ∈ s.erase i, g x • v x
j : ι
hj : j ∈ s.erase i
hij : j ≠ i
right : j ∈ s
h₁ : HSMul.hSMul (β := N) (g j) ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) v i (v j)) : N) = 0
⊢ Eq.{u_14 + 1} (α := N) ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) v i (g j • v j)) : N) (0 : N)
have h₂ : HSMul.hSMul (β := N) (g j) 0 = 0
Tactic: rw [f.map_update_smul, f.map_update_self _ hij.symm, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
ι : Type u_7
K : Type u_12
M : Type u_13
N : Type u_14
inst : Ring K
inst_1 : IsDomain K
inst_2 : AddCommGroup M
inst_3 : Module K M
inst_4 : AddCommGroup N
inst_5 : Module K N
inst_6 : IsTorsionFree K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h_1 : ¬LinearIndependent K v
s : Finset ι
g : ι → K
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
h : g i • v i = -∑ x ∈ s.erase i, g x • v x
j : ι
hj : j ∈ s.erase i
hij : j ≠ i
right : j ∈ s
h₁ : HSMul.hSMul (β := N) (g j) ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) v i (v j)) : N) = 0
h₂ : HSMul.hSMul (β := N) (g j) 0 = 0
⊢ Eq.{u_14 + 1} (α := N) ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) v i (g j • v j)) : N) (0 : N)
have h₃ : Eq.{u_14 + 1} (α := N) 0 0
Tactic: rw [f.map_update_smul, f.map_update_self _ hij.symm, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N' : Type u_6
inst_3 : AddCommGroup N'
inst_4 : Module R N'
ι : Type u_7
inst_5 : Fintype ι
inst_6 : DecidableEq ι
m : MultilinearMap.{u_1, u_7, u_2, u_6} R (fun (x : ι) ↦ M) N'
v : ι → M
i j : ι
i_ne_j : i ≠ j
hv : v i = v j
⊢ Eq.{u_6 + 1} (α := N')
    ((∑ σ : Perm ι, HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ m) :
          (a : (i : ι) → M) → N')
        v :
      N')
    (0 : N')
have rw : Eq.{u_6 + 1} (α := N')
  (∑ a : Perm ι,
    (HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) a : ℤˣ) (domDomCongr a m) :
        (a : (i : ι) → M) → N')
      v)
  0
Tactic: rw [sum_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
M' : Type u_5
inst_7 : AddCommGroup M'
inst_8 : Module R M'
N' : Type u_6
inst_9 : AddCommGroup N'
inst_10 : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
inst_11 : Fintype ι
inst_12 : DecidableEq ι
⊢ Eq (α := M [⋀^ι]→ₗ[R] N')
    (let __src : MultilinearMap.{u_1, u_7, u_2, u_6} R (fun (x : ι) ↦ M) N' :=
      ∑ σ : Perm ι,
        HSMul.hSMul (α := ℤˣ) (β := MultilinearMap.{u_1, u_7, u_2, u_6} R (fun (x : ι) ↦ M) N')
          (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ 0);
    {
      toFun :=
        (⇑(∑ σ : Perm ι,
              HSMul.hSMul (α := ℤˣ) (β := MultilinearMap.{u_1, u_7, u_2, u_6} R (fun (x : ι) ↦ M) N')
                (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ 0)) :
          (a : (i : ι) → M) → N'),
      map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := ⋯ })
    0
have H : ∀ (x : ι → M),
  Eq.{u_6 + 1} (α := N')
    ((let __src : MultilinearMap.{u_1, u_7, u_2, u_6} R (fun (x : ι) ↦ M) N' :=
            ∑ σ : Perm ι,
              HSMul.hSMul (α := ℤˣ) (β := MultilinearMap.{u_1, u_7, u_2, u_6} R (fun (x : ι) ↦ M) N')
                (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ 0);
          {
            toFun :=
              (⇑(∑ σ : Perm ι,
                    HSMul.hSMul (α := ℤˣ) (β := MultilinearMap.{u_1, u_7, u_2, u_6} R (fun (x : ι) ↦ M) N')
                      (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ 0)) :
                (a : (i : ι) → M) → N'),
            map_update_add' := sorry, map_update_smul' := sorry, map_eq_zero_of_eq' := sorry } :
          (a : ι → M) → N')
        x :
      N')
    ((0 : (a : ι → M) → N') x : N')
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N' : Type u_6
inst_3 : AddCommGroup N'
inst_4 : Module R N'
ι : Type u_7
inst_5 : DecidableEq ι
inst_6 : Fintype ι
a : M [⋀^ι]→ₗ[R] N'
⊢ (MultilinearMap.alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N') → M [⋀^ι]→ₗ[R] N')
      (↑a : MultilinearMap R (fun (x : ι) ↦ M) N') =
    (Fintype.card ι).factorial • a
have a₁ : Eq (α := (a : ι → M) → N')
  (⇑((MultilinearMap.alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N') → M [⋀^ι]→ₗ[R] N')
          (↑a : MultilinearMap R (fun (x : ι) ↦ M) N') :
        M [⋀^ι]→ₗ[R] N') :
    (a : ι → M) → N')
  (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
Tactic: apply AlternatingMap.coe_injective
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N' : Type u_6
inst_3 : AddCommGroup N'
inst_4 : Module R N'
ι : Type u_7
inst_5 : DecidableEq ι
inst_6 : Fintype ι
a : M [⋀^ι]→ₗ[R] N'
⊢ Eq (α := (a : ι → M) → N')
    (⇑((MultilinearMap.alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N') → M [⋀^ι]→ₗ[R] N')
            (↑a : MultilinearMap R (fun (x : ι) ↦ M) N') :
          M [⋀^ι]→ₗ[R] N') :
      (a : ι → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
have a₁ : Eq (α := (a : ι → M) → N')
  (⇑(∑ σ : Equiv.Perm ι,
        HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ)
          (MultilinearMap.domDomCongr σ (↑a : MultilinearMap R (fun (x : ι) ↦ M) N'))) :
    (a : (i : ι) → M) → N')
  (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
Tactic: simp_rw [MultilinearMap.alternatization_def, ← coe_domDomCongr, domDomCongr_perm, coe_smul,
    smul_smul, Int.units_mul_self, one_smul, Finset.sum_const, Finset.card_univ, Fintype.card_perm,
    ← coe_multilinearMap, coe_smul]