awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
⊢ (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:
simp
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
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:
simp_all [← Function.comp_assoc, g.map_swap]

Premises used: AlternatingMap.map_swap, Function.comp_assoc
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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')
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')
⊢ (g : (a : ι → M) → N') (v ∘ (⇑σ : (a : ι) → ι)) =
    HSMul.hSMul (α := ℤˣ) (β := N') (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ)
      ((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]

Premises used: AlternatingMap.map_swap, Function.comp_assoc
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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 ι
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')
⊢ (g : (a : ι → M) → N') v =
    HSMul.hSMul (α := ℤˣ) (β := N') (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ)
      ((g : (a : ι → M) → N') (v ∘ (⇑σ : (a : ι) → ι)) : N')

Tactic:
rw [g.map_perm, smul_smul]

Premises used: AlternatingMap.map_perm, smul_smul
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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')
      (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:
simp
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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_1 : ι → M
v' : ι → M'
σ : ι ≃ ι'
f : M [⋀^ι]→ₗ[R] N
v : ι' → M
i j : ι'
hv : v i = v j
hij : i ≠ j
⊢ comp.{u_7 + 1, u_8 + 1, u_2 + 1} (α := ι) v ((⇑σ : (a : ι) → ι') : (a : ι) → ι') ((σ.symm : (a : ι') → ι) i : ι) =
    comp.{u_7 + 1, u_8 + 1, u_2 + 1} (α := ι) v ((⇑σ : (a : ι) → ι') : (a : ι) → ι') ((σ.symm : (a : ι') → ι) j : ι)

Tactic:
simpa using hv
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
⊢ domDomCongr (Equiv.refl ι) f = f

Tactic:
rfl

Premises used: AlternatingMap.domDomCongr, rfl
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
ι' : Type u_8
ι'' : Type u_9
σ₁ : ι ≃ ι'
σ₂ : ι' ≃ ι''
f : M [⋀^ι]→ₗ[R] N
⊢ domDomCongr (σ₁.trans σ₂) f = domDomCongr σ₂ (domDomCongr σ₁ f)

Tactic:
rfl

Premises used: Equiv.trans, AlternatingMap.domDomCongr, rfl
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
ι' : Type u_8
σ : ι ≃ ι'
⊢ Eq (α := M [⋀^ι']→ₗ[R] N) (domDomCongr σ 0) 0

Tactic:
rfl

Premises used: AlternatingMap.domDomCongr, rfl
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
ι' : Type u_8
σ : ι ≃ ι'
f g : M [⋀^ι]→ₗ[R] N
⊢ domDomCongr σ (f + g) = domDomCongr σ f + domDomCongr σ g

Tactic:
rfl

Premises used: AlternatingMap.domDomCongr, rfl
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
ι' : Type u_8
S : Type u_12
inst_5 : Monoid S
inst_6 : DistribMulAction S N
inst_7 : SMulCommClass R S N
σ : ι ≃ ι'
c : S
f : M [⋀^ι]→ₗ[R] N
⊢ domDomCongr σ (c • f) = c • domDomCongr σ f

Tactic:
rfl

Premises used: AlternatingMap.domDomCongr, rfl
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
H :
  ∀ (x : ι → M),
    Eq.{u_3 + 1} (α := N) ((domDomCongr σ.symm (domDomCongr σ f) : (a : ι → M) → N) x : N) ((f : (a : ι → M) → N) x : N)
⊢ domDomCongr σ.symm (domDomCongr σ f) = f

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
x : ι → M
⊢ Eq.{u_3 + 1} (α := N) ((domDomCongr σ.symm (domDomCongr σ f) : (a : ι → M) → N) x : N) ((f : (a : ι → M) → N) x : N)

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
H :
  ∀ (x : ι' → M),
    Eq.{u_3 + 1} (α := N) ((domDomCongr σ (domDomCongr σ.symm m) : (a : ι' → M) → N) x : N)
      ((m : (a : ι' → M) → N) x : N)
⊢ domDomCongr σ (domDomCongr σ.symm m) = m

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
x : ι' → M
⊢ Eq.{u_3 + 1} (α := N) ((domDomCongr σ (domDomCongr σ.symm m) : (a : ι' → M) → N) x : N) ((m : (a : ι' → M) → N) x : N)

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
H :
  ∀ (x : ι → M),
    Eq.{u_3 + 1} (α := N) ((domDomCongr σ.symm (domDomCongr σ f) : (a : ι → M) → N) x : N) ((f : (a : ι → M) → N) x : N)
⊢ domDomCongr σ.symm (domDomCongr σ f) = f

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
x : ι → M
⊢ Eq.{u_3 + 1} (α := N) ((domDomCongr σ.symm (domDomCongr σ f) : (a : ι → M) → N) x : N) ((f : (a : ι → M) → N) x : N)

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
H :
  ∀ (x : ι' → M),
    Eq.{u_3 + 1} (α := N) ((domDomCongr σ (domDomCongr σ.symm m) : (a : ι' → M) → N) x : N)
      ((m : (a : ι' → M) → N) x : N)
⊢ domDomCongr σ (domDomCongr σ.symm m) = m

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
x : ι' → M
⊢ Eq.{u_3 + 1} (α := N) ((domDomCongr σ (domDomCongr σ.symm m) : (a : ι' → M) → N) x : N) ((m : (a : ι' → M) → N) x : N)

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
S : Type u_12
inst_5 : Semiring S
inst_6 : Module S N
inst_7 : SMulCommClass R S N
⊢ Eq (α := M [⋀^ι]→ₗ[R] N ≃ₗ[S] M [⋀^ι]→ₗ[R] N) (domDomCongrₗ S (Equiv.refl ι)) (LinearEquiv.refl S (M [⋀^ι]→ₗ[R] N))

Tactic:
rfl

Premises used: AlternatingMap.domDomCongrₗ, AlternatingMap.domDomCongr, LinearEquiv.refl, rfl
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
ι' : Type u_8
S : Type u_12
inst_5 : Semiring S
inst_6 : Module S N
inst_7 : SMulCommClass R S N
σ : ι ≃ ι'
⊢ (↑(domDomCongrₗ S σ) : M [⋀^ι]→ₗ[R] N ≃+ M [⋀^ι']→ₗ[R] N) = domDomCongrEquiv σ

Tactic:
rfl

Premises used: AddEquivClass.toAddEquiv, AlternatingMap.domDomCongr, AlternatingMap.domDomCongrEquiv, EquivLike.toEquiv, rfl
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
ι' : Type u_8
σ : ι ≃ ι'
f g : M [⋀^ι]→ₗ[R] N
⊢ domDomCongr σ f = domDomCongr σ g ↔ f = g

Tactic:
(domDomCongrEquiv σ : _ ≃+ M [⋀^ι']→ₗ[R] N).apply_eq_iff_eq

Premises used: AlternatingMap.domDomCongr, AddEquiv.apply_eq_iff_eq, AlternatingMap.domDomCongrEquiv
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
ι' : Type u_8
σ : ι ≃ ι'
f : M [⋀^ι]→ₗ[R] N
⊢ domDomCongr σ f = 0 ↔ f = 0

Tactic:
(domDomCongrEquiv σ : M [⋀^ι]→ₗ[R] N ≃+ M [⋀^ι']→ₗ[R] N).map_eq_zero_iff

Premises used: AddEquiv.map_eq_zero_iff, AlternatingMap.domDomCongr, AlternatingMap.domDomCongrEquiv
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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 : Fintype ι
inst_6 : DecidableEq ι
σ : Equiv.Perm ι
⊢ domDomCongr σ g = HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ) g

Tactic:
AlternatingMap.ext fun v => g.map_perm v σ

Premises used: AlternatingMap.map_perm, AlternatingMap.ext
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
ι' : Type u_8
f : M [⋀^ι]→ₗ[R] N
σ : ι ≃ ι'
⊢ (↑(domDomCongr σ f) : MultilinearMap R (fun (x : ι') ↦ M) N) =
    MultilinearMap.domDomCongr σ (↑f : MultilinearMap R (fun (x : ι) ↦ M) N)

Tactic:
MultilinearMap.ext fun _ => rfl

Premises used: MultilinearMap.ext, rfl
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
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)
⊢ 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

Premises used: Iff.mp, not_linearIndependent_iff
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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)
⊢ 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

Premises used: Function.update_eq_self, AlternatingMap.map_update_smul, smul_eq_zero
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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 : g i = 0 ∨ Eq.{u_14 + 1} (α := N) ((f : (a : ι → M) → N) v : N) (0 : N)
⊢ Eq.{u_14 + 1} (α := N) ((f : (a : ι → M) → N) v : N) (0 : N)

Tactic:
Or.resolve_left this hz

Premises used: Or.resolve_left
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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 : g i = 0 ∨ Eq.{u_14 + 1} (α := N) ((f : (a : ι → M) → N) v : N) (0 : N)
⊢ Eq.{u_14 + 1} (α := N) ((f : (a : ι → M) → N) v : N) (0 : N)

Tactic:
exact Or.resolve_left this hz

Premises used: Or.resolve_left
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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 ι
suffices : 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)

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
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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 ι
⊢ 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

Premises used: add_eq_zero_iff_eq_neg, Finset.notMem_erase, Finset.sum_insert, Finset.insert_erase
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
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)
⊢ Eq.{u_14 + 1} (α := N) (∑ a ∈ s.erase i, (f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) v i (g a • v a))) 0

Tactic:
apply Finset.sum_eq_zero

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
⊢ j ≠ i

Tactic:
obtain ⟨hij, _⟩ := Finset.mem_erase.mp hj

Premises used: Finset.mem_erase, Iff.mp
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
⊢ j ∈ s

Tactic:
obtain ⟨hij, _⟩ := Finset.mem_erase.mp hj

Premises used: Finset.mem_erase, Iff.mp