awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
h₃ h₄ : Eq.{u_14 + 1} (α := N) 0 0
⊢ Eq.{u_14 + 1} (α := N) ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) v i (g j • v j)) : N) (0 : N)

Tactic:
rw [f.map_update_smul, f.map_update_self _ hij.symm, smul_zero]

Premises used: AlternatingMap.map_update_smul, smul_zero, Ne.symm, AlternatingMap.map_update_self
-- 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
n : ℕ
f : M [⋀^Fin n.succ]→ₗ[R] N
m : Fin n → M
x y : M
⊢ (f : (a : Fin n.succ → M) → N) (Matrix.vecCons (x + y) m) =
    HAdd.hAdd (α := N) (β := N) ((f : (a : Fin n.succ → M) → N) (Matrix.vecCons x m) : N)
      ((f : (a : Fin n.succ → M) → N) (Matrix.vecCons y m) : N)

Tactic:
f.toMultilinearMap.cons_add _ _ _

Premises used: AlternatingMap.toMultilinearMap, MultilinearMap.cons_add, Matrix.vecCons
-- 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
n : ℕ
f : M [⋀^Fin n.succ]→ₗ[R] N
m : Fin n → M
c : R
x : M
⊢ (f : (a : Fin n.succ → M) → N) (Matrix.vecCons (c • x) m) =
    HSMul.hSMul (β := N) c ((f : (a : Fin n.succ → M) → N) (Matrix.vecCons x m) : N)

Tactic:
f.toMultilinearMap.cons_smul _ _ _

Premises used: AlternatingMap.toMultilinearMap, MultilinearMap.cons_smul, Matrix.vecCons
-- 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
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
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
⊢ Eq.{u_6 + 1} (α := N')
    ((∑ σ : Perm ι, HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ m) :
          (a : (i : ι) → M) → N')
        v :
      N')
    (0 : N')

Tactic:
rw [sum_apply]

Premises used: MultilinearMap.sum_apply
-- 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
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
σ : Perm ι
h : Membership.mem (γ := Finset (Perm ι)) Finset.univ σ
⊢ HAdd.hAdd (α := N') (β := N')
      ((HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ m) :
            (a : (i : ι) → M) → N')
          v :
        N')
      ((HSMul.hSMul (α := ℤˣ) (β := MultilinearMap.{u_1, u_7, u_2, u_6} R (fun (x : ι) ↦ M) N')
              (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ)
                ((fun (σ : Perm ι) (x : Membership.mem (γ := Finset (Perm ι)) Finset.univ σ) ↦ swap i j * σ) σ h))
              (domDomCongr
                ((fun (σ : Perm ι) (x : Membership.mem (γ := Finset (Perm ι)) Finset.univ σ) ↦ swap i j * σ) σ h) m) :
            (a : (i : ι) → M) → N')
          v :
        N') =
    0

Tactic:
simp [Perm.sign_swap i_ne_j, apply_swap_eq_self hv]

Premises used: Equiv.apply_swap_eq_self, Equiv.Perm.sign_swap
-- 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
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')
    (∑ a : Perm ι,
      (HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) a : ℤˣ) (domDomCongr a m) :
          (a : (i : ι) → M) → N')
        v)
    0

Tactic:
exact
    Finset.sum_involution (fun σ _ => swap i j * σ)
      (fun σ _ => by simp [Perm.sign_swap i_ne_j, apply_swap_eq_self hv])
      (fun σ _ _ => (not_congr swap_mul_eq_iff).mpr i_ne_j) (fun σ _ => Finset.mem_univ _)
      fun σ _ => swap_mul_involutive i j σ

Premises used: Iff.mpr, Finset.mem_univ, HMul.hMul, Equiv.swap, Equiv.swap_mul_involutive, Equiv.swap_mul_eq_iff, Finset.sum_involution, not_congr
-- 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
inst_11 : Fintype ι
inst_12 : DecidableEq ι
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' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := ⋯ } :
            (a : ι → M) → N')
          x :
        N')
      ((0 : (a : ι → M) → N') x : N')
⊢ 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

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
inst_11 : Fintype ι
inst_12 : DecidableEq ι
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' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := ⋯ } :
          (a : ι → M) → N')
        x :
      N')
    ((0 : (a : ι → M) → N') x : 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
inst_11 : Fintype ι
inst_12 : DecidableEq ι
a b : MultilinearMap.{u_1, u_7, u_2, u_6} R (fun (x : ι) ↦ M) N'
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 (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ (a + b));
          {
            toFun :=
              (⇑(∑ σ : Perm ι,
                    HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ)
                      (domDomCongr σ (a + b))) :
                (a : (i : ι) → M) → N'),
            map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := ⋯ } :
          (a : ι → M) → N')
        x :
      N')
    ((HAdd.hAdd (α := M [⋀^ι]→ₗ[R] N')
            (let __src : MultilinearMap.{u_1, u_7, u_2, u_6} R (fun (x : ι) ↦ M) N' :=
              ∑ σ : Perm ι,
                HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ a);
            {
              toFun :=
                (⇑(∑ σ : Perm ι,
                      HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ)
                        (domDomCongr σ a)) :
                  (a : (i : ι) → M) → N'),
              map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := ⋯ : M [⋀^ι]→ₗ[R] N' })
            (let __src : MultilinearMap.{u_1, u_7, u_2, u_6} R (fun (x : ι) ↦ M) N' :=
              ∑ σ : Perm ι,
                HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ b);
            {
              toFun :=
                (⇑(∑ σ : Perm ι,
                      HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ)
                        (domDomCongr σ b)) :
                  (a : (i : ι) → M) → N'),
              map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := ⋯ : M [⋀^ι]→ₗ[R] N' }) :
          (a : ι → M) → N')
        x :
      N')

Tactic:
simp [Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- 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
inst_5 : Fintype ι
inst_6 : DecidableEq ι
m : MultilinearMap.{u_1, u_7, u_2, u_6} R (fun (x : ι) ↦ M) N'
⊢ Eq (α := (a : ι → M) → N')
    (⇑((alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N') → M [⋀^ι]→ₗ[R] N') m : M [⋀^ι]→ₗ[R] N') :
      (a : ι → M) → N')
    (⇑(∑ σ : Perm ι,
          HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ m)) :
      (a : (i : ι) → M) → N')

Tactic:
rfl

Premises used: 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_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'
⊢ Eq (α := MultilinearMap.{u_1, u_7, u_2, u_6} R (fun (x : ι) ↦ M) N')
    (↑((alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N') → M [⋀^ι]→ₗ[R] N') m) :
      MultilinearMap R (fun (x : ι) ↦ M) N')
    (∑ σ : Perm ι, HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ m))

Tactic:
coe_injective rfl

Premises used: MultilinearMap.coe_injective, 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_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
⊢ Eq.{u_6 + 1} (α := N')
    ((((alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N') → M [⋀^ι]→ₗ[R] N') m : M [⋀^ι]→ₗ[R] N') :
          (a : ι → M) → N')
        v :
      N')
    (∑ σ : Perm ι,
        HSMul.hSMul (α := ℤˣ) (β := N') (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ)
          ((domDomCongr σ m : (a : (i : ι) → M) → N') v : N') :
      N')

Tactic:
simp only [alternatization_def, smul_apply, sum_apply]

Premises used: MultilinearMap.smul_apply, MultilinearMap.sum_apply, MultilinearMap.alternatization_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_6
inst_3 : AddCommGroup N'
inst_4 : Module R N'
ι : Type u_7
inst_5 : DecidableEq ι
inst_6 : Fintype ι
a : M [⋀^ι]→ₗ[R] N'
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')
⊢ (MultilinearMap.alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N') → M [⋀^ι]→ₗ[R] N')
      (↑a : MultilinearMap R (fun (x : ι) ↦ M) N') =
    (Fintype.card ι).factorial • a

Tactic:
apply AlternatingMap.coe_injective

Premises used: AlternatingMap.coe_injective
-- 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
N'₂ : Type u_10
inst_5 : AddCommGroup N'₂
inst_6 : Module R N'₂
inst_7 : DecidableEq ι
inst_8 : Fintype ι
g : N' →ₗ[R] N'₂
f : MultilinearMap.{u_1, u_7, u_2, u_6} R (fun (x : ι) ↦ M) N'
H :
  ∀ (x : ι → M),
    Eq.{u_10 + 1} (α := N'₂)
      ((((MultilinearMap.alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N'₂) → M [⋀^ι]→ₗ[R] N'₂)
                (g.compMultilinearMap (M₁ := fun (x : ι) ↦ M) f) :
              M [⋀^ι]→ₗ[R] N'₂) :
            (a : ι → M) → N'₂)
          x :
        N'₂)
      ((g.compAlternatingMap
              ((MultilinearMap.alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N') → M [⋀^ι]→ₗ[R] N') f) :
            (a : ι → M) → N'₂)
          x :
        N'₂)
⊢ Eq (α := M [⋀^ι]→ₗ[R] N'₂)
    ((MultilinearMap.alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N'₂) → M [⋀^ι]→ₗ[R] N'₂)
        (g.compMultilinearMap (M₁ := fun (x : ι) ↦ M) f) :
      M [⋀^ι]→ₗ[R] N'₂)
    (g.compAlternatingMap
        ((MultilinearMap.alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N') → M [⋀^ι]→ₗ[R] N') f) :
      M [⋀^ι]→ₗ[R] N'₂)

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_6
inst_3 : AddCommGroup N'
inst_4 : Module R N'
ι : Type u_7
N'₂ : Type u_10
inst_5 : AddCommGroup N'₂
inst_6 : Module R N'₂
inst_7 : DecidableEq ι
inst_8 : Fintype ι
g : N' →ₗ[R] N'₂
f : MultilinearMap.{u_1, u_7, u_2, u_6} R (fun (x : ι) ↦ M) N'
x : ι → M
⊢ Eq.{u_10 + 1} (α := N'₂)
    ((((MultilinearMap.alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N'₂) → M [⋀^ι]→ₗ[R] N'₂)
              (g.compMultilinearMap (M₁ := fun (x : ι) ↦ M) f) :
            M [⋀^ι]→ₗ[R] N'₂) :
          (a : ι → M) → N'₂)
        x :
      N'₂)
    ((g.compAlternatingMap
            ((MultilinearMap.alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N') → M [⋀^ι]→ₗ[R] N') f) :
          (a : ι → M) → N'₂)
        x :
      N'₂)

Tactic:
simp [MultilinearMap.alternatization_def]

Premises used: MultilinearMap.alternatization_def
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
Goal:
ι : Type u_7
ι₁ : Type u_10
inst : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst_1 : CommSemiring R'
inst_2 : AddCommMonoid N₁
inst_3 : AddCommMonoid N₂
inst_4 : Module R' N₁
inst_5 : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h :
  ∀ (v : ι → ι₁),
    Function.Injective v →
      Eq.{u_13 + 1} (α := N₂) ((f : (a : ι → N₁) → N₂) fun (i : ι) ↦ (e : (a : ι₁) → N₁) (v i) : N₂)
        ((g : (a : ι → N₁) → N₂) fun (i : ι) ↦ (e : (a : ι₁) → N₁) (v i) : N₂)
⊢ f = g

Tactic:
AlternatingMap.coe_multilinearMap_injective (Basis.ext_multilinear (fun _ ↦ e) fun v => ?_)

Premises used: AlternatingMap.coe_multilinearMap_injective, Module.Basis.ext_multilinear
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
Goal:
ι : Type u_7
ι₁ : Type u_10
inst : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst_1 : CommSemiring R'
inst_2 : AddCommMonoid N₁
inst_3 : AddCommMonoid N₂
inst_4 : Module R' N₁
inst_5 : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h :
  ∀ (v : ι → ι₁),
    Function.Injective v →
      Eq.{u_13 + 1} (α := N₂) ((f : (a : ι → N₁) → N₂) fun (i : ι) ↦ (e : (a : ι₁) → N₁) (v i) : N₂)
        ((g : (a : ι → N₁) → N₂) fun (i : ι) ↦ (e : (a : ι₁) → N₁) (v i) : N₂)
refine :
  ∀ (v : (i : ι) → ι₁),
    Eq.{u_13 + 1} (α := N₂)
      (((↑f : MultilinearMap R' (fun (x : ι) ↦ N₁) N₂) : (a : (i : ι) → N₁) → N₂) fun (i : ι) ↦
          ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) :
        N₂)
      (((↑g : MultilinearMap R' (fun (x : ι) ↦ N₁) N₂) : (a : (i : ι) → N₁) → N₂) fun (i : ι) ↦
          ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) :
        N₂)
⊢ f = g

Tactic:
refine AlternatingMap.coe_multilinearMap_injective (Basis.ext_multilinear (fun _ ↦ e) fun v => ?_)

Premises used: AlternatingMap.coe_multilinearMap_injective, Module.Basis.ext_multilinear
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
Goal:
ι : Type u_7
ι₁ : Type u_10
inst : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst_1 : CommSemiring R'
inst_2 : AddCommMonoid N₁
inst_3 : AddCommMonoid N₂
inst_4 : Module R' N₁
inst_5 : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h :
  ∀ (v : ι → ι₁),
    Function.Injective v →
      Eq.{u_13 + 1} (α := N₂) ((f : (a : ι → N₁) → N₂) fun (i : ι) ↦ (e : (a : ι₁) → N₁) (v i) : N₂)
        ((g : (a : ι → N₁) → N₂) fun (i : ι) ↦ (e : (a : ι₁) → N₁) (v i) : N₂)
v : (i : ι) → ι₁
pos :
  ∀ (hi : Function.Injective v),
    Eq.{u_13 + 1} (α := N₂)
      (((↑f : MultilinearMap R' (fun (x : ι) ↦ N₁) N₂) : (a : (i : ι) → N₁) → N₂) fun (i : ι) ↦
          ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) :
        N₂)
      (((↑g : MultilinearMap R' (fun (x : ι) ↦ N₁) N₂) : (a : (i : ι) → N₁) → N₂) fun (i : ι) ↦
          ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) :
        N₂)
neg :
  ∀ (hi : ¬Function.Injective v),
    Eq.{u_13 + 1} (α := N₂)
      (((↑f : MultilinearMap R' (fun (x : ι) ↦ N₁) N₂) : (a : (i : ι) → N₁) → N₂) fun (i : ι) ↦
          ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) :
        N₂)
      (((↑g : MultilinearMap R' (fun (x : ι) ↦ N₁) N₂) : (a : (i : ι) → N₁) → N₂) fun (i : ι) ↦
          ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) :
        N₂)
⊢ Eq.{u_13 + 1} (α := N₂)
    (((↑f : MultilinearMap R' (fun (x : ι) ↦ N₁) N₂) : (a : (i : ι) → N₁) → N₂) fun (i : ι) ↦
        ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) :
      N₂)
    (((↑g : MultilinearMap R' (fun (x : ι) ↦ N₁) N₂) : (a : (i : ι) → N₁) → N₂) fun (i : ι) ↦
        ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) :
      N₂)

Tactic:
by_cases hi : Function.Injective v

Premises used: Function.Injective
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
Goal:
ι : Type u_7
ι₁ : Type u_10
inst : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst_1 : CommSemiring R'
inst_2 : AddCommMonoid N₁
inst_3 : AddCommMonoid N₂
inst_4 : Module R' N₁
inst_5 : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h :
  ∀ (v : ι → ι₁),
    Function.Injective v →
      Eq.{u_13 + 1} (α := N₂) ((f : (a : ι → N₁) → N₂) fun (i : ι) ↦ (e : (a : ι₁) → N₁) (v i) : N₂)
        ((g : (a : ι → N₁) → N₂) fun (i : ι) ↦ (e : (a : ι₁) → N₁) (v i) : N₂)
v : (i : ι) → ι₁
hi : Function.Injective v
⊢ Eq.{u_13 + 1} (α := N₂)
    (((↑f : MultilinearMap R' (fun (x : ι) ↦ N₁) N₂) : (a : (i : ι) → N₁) → N₂) fun (i : ι) ↦
        ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) :
      N₂)
    (((↑g : MultilinearMap R' (fun (x : ι) ↦ N₁) N₂) : (a : (i : ι) → N₁) → N₂) fun (i : ι) ↦
        ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) :
      N₂)

Tactic:
h v hi
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
Goal:
ι : Type u_7
ι₁ : Type u_10
inst : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst_1 : CommSemiring R'
inst_2 : AddCommMonoid N₁
inst_3 : AddCommMonoid N₂
inst_4 : Module R' N₁
inst_5 : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h :
  ∀ (v : ι → ι₁),
    Function.Injective v →
      Eq.{u_13 + 1} (α := N₂) ((f : (a : ι → N₁) → N₂) fun (i : ι) ↦ (e : (a : ι₁) → N₁) (v i) : N₂)
        ((g : (a : ι → N₁) → N₂) fun (i : ι) ↦ (e : (a : ι₁) → N₁) (v i) : N₂)
v : (i : ι) → ι₁
hi : Function.Injective v
⊢ Eq.{u_13 + 1} (α := N₂)
    (((↑f : MultilinearMap R' (fun (x : ι) ↦ N₁) N₂) : (a : (i : ι) → N₁) → N₂) fun (i : ι) ↦
        ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) :
      N₂)
    (((↑g : MultilinearMap R' (fun (x : ι) ↦ N₁) N₂) : (a : (i : ι) → N₁) → N₂) fun (i : ι) ↦
        ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) :
      N₂)

Tactic:
exact h v hi
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
Goal:
ι : Type u_7
ι₁ : Type u_10
inst : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst_1 : CommSemiring R'
inst_2 : AddCommMonoid N₁
inst_3 : AddCommMonoid N₂
inst_4 : Module R' N₁
inst_5 : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h :
  ∀ (v : ι → ι₁),
    Function.Injective v →
      Eq.{u_13 + 1} (α := N₂) ((f : (a : ι → N₁) → N₂) fun (i : ι) ↦ (e : (a : ι₁) → N₁) (v i) : N₂)
        ((g : (a : ι → N₁) → N₂) fun (i : ι) ↦ (e : (a : ι₁) → N₁) (v i) : N₂)
v : (i : ι) → ι₁
hi : ¬Function.Injective v
⊢ ¬Function.Injective.{u_7 + 1, u_12 + 1} (β := N₁) fun (i : ι) ↦ (e : (a : ι₁) → N₁) (v i)

Tactic:
have : ¬Function.Injective fun i => e (v i) := hi.imp Function.Injective.of_comp