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_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
x y : ι → M
h : x = y
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) x : N) ((f : (a : ι → M) → N) y : N)

Tactic:
congr_arg (fun x : ι → M => f x) h

Premises used: congr_arg, DFunLike.coe
-- 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
⊢ Injective (α := M [⋀^ι]→ₗ[R] N) (β := (a : ι → M) → N) (DFunLike.coe (β := fun (x : ι → M) ↦ N))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.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_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
f g : M [⋀^ι]→ₗ[R] N
⊢ Eq (α := (a : ι → M) → N) (⇑f : (a : ι → M) → N) (⇑g : (a : ι → M) → N) ↔ f = g

Tactic:
coe_injective.eq_iff

Premises used: Function.Injective.eq_iff, 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_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
f f' : M [⋀^ι]→ₗ[R] N
H : ∀ (x : ι → M), Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) x : N) ((f' : (a : ι → M) → N) x : N)
⊢ f = f'

Tactic:
DFunLike.ext _ _ H

Premises used: DFunLike.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
f : M [⋀^ι]→ₗ[R] N
⊢ Eq (α := (a : (i : ι) → M) → N) (⇑(↑f : MultilinearMap R (fun (x : ι) ↦ M) N) : (a : (i : ι) → M) → N)
    (⇑f : (a : ι → 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_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
⊢ Injective (α := M [⋀^ι]→ₗ[R] N) toMultilinearMap

Tactic:
fun _ _ h => ext <| MultilinearMap.congr_fun h

Premises used: MultilinearMap.congr_fun, Function.Injective, 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
f : (ι → M) → N
h₁ :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M) (i : ι) (x y : M),
    f (update (β := fun (x : ι) ↦ M) m i (x + y)) =
      f (update (β := fun (x : ι) ↦ M) m i x) + f (update (β := fun (x : ι) ↦ M) m i y)
h₂ :
  ∀ [inst_5 : DecidableEq ι] (m : (i : ι) → M) (i : ι) (c : R) (x : M),
    f (update (β := fun (x : ι) ↦ M) m i (c • x)) = c • f (update (β := fun (x : ι) ↦ M) m i x)
h₃ :
  ∀ (v : ι → M) (i j : ι),
    v i = v j →
      i ≠ j →
        MultilinearMap.toFun.{u_1, u_7, u_2, u_3} (R := R) (M₁ := fun (x : ι) ↦ M)
            (MultilinearMap.mk (M₁ := fun (x : ι) ↦ M) f ⋯ ⋯) v =
          0
⊢ (↑{ toFun := f, map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := h₃ : M [⋀^ι]→ₗ[R] N } :
      MultilinearMap R (fun (x : ι) ↦ M) N) =
    MultilinearMap.mk (M₁ := fun (x : ι) ↦ M) f h₁ h₂

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
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst_5 : DecidableEq ι
i : ι
x y : M
⊢ (f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) v i (x + y)) =
    HAdd.hAdd (α := N) (β := N) ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) v i x) : N)
      ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) v i y) : N)

Tactic:
f.map_update_add' v i x y

Premises used: MultilinearMap.map_update_add', AlternatingMap.toMultilinearMap
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
Goal:
R : Type u_1
inst : Semiring R
M' : Type u_5
inst_1 : AddCommGroup 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 ι
i : ι
x y : M'
⊢ (g' : (a : ι → M') → N') (update (β := fun (a : ι) ↦ M') v' i (x - y)) =
    HSub.hSub (α := N') (β := N') ((g' : (a : ι → M') → N') (update (β := fun (a : ι) ↦ M') v' i x) : N')
      ((g' : (a : ι → M') → N') (update (β := fun (a : ι) ↦ M') v' i y) : N')

Tactic:
g'.toMultilinearMap.map_update_sub v' i x y

Premises used: AlternatingMap.toMultilinearMap, MultilinearMap.map_update_sub
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
Goal:
R : Type u_1
inst : Semiring R
M' : Type u_5
inst_1 : AddCommGroup 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 ι
i : ι
x : M'
⊢ Eq.{u_6 + 1} (α := N') ((g' : (a : ι → M') → N') (update (β := fun (a : ι) ↦ M') v' i (-x)) : N')
    (-(g' : (a : ι → M') → N') (update (β := fun (a : ι) ↦ M') v' i x) : N')

Tactic:
g'.toMultilinearMap.map_update_neg v' i x

Premises used: MultilinearMap.map_update_neg, AlternatingMap.toMultilinearMap
-- 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
v : ι → M
inst_5 : DecidableEq ι
i : ι
r : R
x : M
⊢ (f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) v i (r • x)) =
    HSMul.hSMul (β := N) r ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) v i x) : N)

Tactic:
f.map_update_smul' v i r x

Premises used: AlternatingMap.toMultilinearMap, MultilinearMap.map_update_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_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) v : N) (0 : N)

Tactic:
f.map_eq_zero_of_eq' v i j h hij

Premises used: AlternatingMap.map_eq_zero_of_eq'
-- 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
m : ι → M
i : ι
h : m i = 0
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) m : N) (0 : N)

Tactic:
f.toMultilinearMap.map_coord_zero i h

Premises used: AlternatingMap.toMultilinearMap, MultilinearMap.map_coord_zero
-- 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
inst_5 : DecidableEq ι
m : ι → M
i : ι
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) m i 0) : N) (0 : N)

Tactic:
f.toMultilinearMap.map_update_zero m i

Premises used: AlternatingMap.toMultilinearMap, MultilinearMap.map_update_zero
-- 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
inst_5 : Nonempty ι
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) 0 : N) (0 : N)

Tactic:
f.toMultilinearMap.map_zero

Premises used: MultilinearMap.map_zero, AlternatingMap.toMultilinearMap
-- 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
v : ι → M
hv : ¬Injective v
⊢ ¬∀ ⦃a₁ a₂ : ι⦄, v a₁ = v a₂ → a₁ = a₂

Tactic:
rw [Function.Injective] at hv

Premises used: Function.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_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
hv : ¬∀ ⦃a₁ a₂ : ι⦄, v a₁ = v a₂ → a₁ = a₂
⊢ ∃ (a₁ : ι) (a₂ : ι), v a₁ = v a₂ ∧ a₁ ≠ a₂

Tactic:
push Not at hv

Premises used: Not
-- 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
v : ι → M
hv : ∃ (a₁ : ι) (a₂ : ι), v a₁ = v a₂ ∧ a₁ ≠ a₂
rcases : ∀ (i₁ i₂ : ι) (heq : v i₁ = v i₂) (hne : i₁ ≠ i₂), Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) v : N) (0 : N)
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) v : N) (0 : N)

Tactic:
rcases hv with ⟨i₁, i₂, heq, hne⟩
-- 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
v : ι → M
i₁ i₂ : ι
heq : v i₁ = v i₂
hne : i₁ ≠ i₂
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) v : N) (0 : N)

Tactic:
f.map_eq_zero_of_eq v heq hne

Premises used: AlternatingMap.map_eq_zero_of_eq
-- 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
v : ι → M
i₁ i₂ : ι
heq : v i₁ = v i₂
hne : i₁ ≠ i₂
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) v : N) (0 : N)

Tactic:
exact f.map_eq_zero_of_eq v heq hne

Premises used: AlternatingMap.map_eq_zero_of_eq
-- 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
f_1 f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v_1 : ι → M
v' : ι → M'
S : Type u_10
inst_11 : Monoid S
inst_12 : DistribMulAction S N
inst_13 : SMulCommClass R S N
c : S
f : M [⋀^ι]→ₗ[R] N
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ (c • (↑f : MultilinearMap R (fun (x : ι) ↦ M) N)).toFun (M₁ := fun (x : ι) ↦ M) v = 0

Tactic:
simp [f.map_eq_zero_of_eq v h hij]

Premises used: AlternatingMap.map_eq_zero_of_eq
-- 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
S : Type u_10
inst_5 : Monoid S
inst_6 : DistribMulAction S N
inst_7 : SMulCommClass R S N
c : S
m : ι → M
⊢ (c • f : (a : ι → M) → N) m = HSMul.hSMul (β := N) c ((f : (a : ι → M) → N) 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_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
S : Type u_10
inst_5 : Monoid S
inst_6 : DistribMulAction S N
inst_7 : SMulCommClass R S N
c : S
⊢ (↑(c • f) : MultilinearMap R (fun (x : ι) ↦ M) N) = c • (↑f : MultilinearMap R (fun (x : ι) ↦ 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_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
S : Type u_10
inst_5 : Monoid S
inst_6 : DistribMulAction S N
inst_7 : SMulCommClass R S N
c : S
f : M [⋀^ι]→ₗ[R] N
⊢ (⇑(c • f) : (a : ι → M) → N) = HSMul.hSMul (β := (a : ι → M) → N) c (⇑f : (a : ι → 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_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
f f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
S : Type u_10
inst_11 : Monoid S
inst_12 : DistribMulAction S N
inst_13 : SMulCommClass R S N
inst_14 : DistribMulAction.{u_10, u_3} Sᵐᵒᵖ N
inst_15 : IsCentralScalar S N
⊢ IsCentralScalar S (M [⋀^ι]→ₗ[R] N)

Tactic:
⟨fun _ _ => ext fun _ => op_smul_eq_smul _ _⟩

Premises used: AlternatingMap.toMultilinearMap, IsCentralScalar.mk, AlternatingMap.ext, DFunLike.coe, IsCentralScalar.op_smul_eq_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_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
g : M [⋀^ι]→ₗ[R] P
⊢ (↑(f.prod g) : MultilinearMap R (fun (x : ι) ↦ M) (N × P)) =
    (↑f : MultilinearMap R (fun (x : ι) ↦ M) N).prod (M₁ := fun (x : ι) ↦ M) (↑g : MultilinearMap R (fun (x : ι) ↦ M) P)

Tactic:
rfl

Premises used: MultilinearMap.prod, 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
ι : Type u_7
ι' : Type u_10
N : ι' → Type u_11
inst_3 : (i : ι') → AddCommMonoid (N i)
inst_4 : (i : ι') → Module.{u_1, u_11} R (N i)
f : (i : ι') → AlternatingMap.{u_1, u_2, u_11, u_7} R M (N i) ι
⊢ (↑(pi (N := N) f) : MultilinearMap R (fun (x : ι) ↦ M) ((i : ι') → N i)) =
    MultilinearMap.pi (M₁ := fun (x : ι) ↦ M) (M' := N) fun (a : ι') ↦
      (↑(f a) : MultilinearMap R (fun (x : ι) ↦ M) (N a))

Tactic:
rfl

Premises used: MultilinearMap.pi, rfl
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
Goal:
R_1 : Type u_1
inst : Semiring R_1
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R_1 M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R_1 N
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R_1 P
M' : Type u_5
inst_7 : AddCommGroup M'
inst_8 : Module R_1 M'
N' : Type u_6
inst_9 : AddCommGroup N'
inst_10 : Module R_1 N'
ι_1 : Type u_7
ι' : Type u_8
ι'' : Type u_9
f_1 f' : M [⋀^ι_1]→ₗ[R_1] N
g g₂ : M [⋀^ι_1]→ₗ[R_1] N'
g' : M' [⋀^ι_1]→ₗ[R_1] N'
v_1 : ι_1 → M
v' : ι_1 → M'
R : Type u_10
M₁ : Type u_11
M₂ : Type u_12
ι : Type u_13
inst_11 : CommSemiring R
inst_12 : AddCommMonoid M₁
inst_13 : AddCommMonoid M₂
inst_14 : Module R M₁
inst_15 : Module R M₂
f : M₁ [⋀^ι]→ₗ[R] R
z : M₂
v : ι → M₁
i j : ι
h : v i = v j
hne : i ≠ j
⊢ MultilinearMap.toFun (M₁ := fun (x : ι) ↦ M₁)
      ((↑f : MultilinearMap R (fun (x : ι) ↦ M₁) R).smulRight (M₁ := fun (x : ι) ↦ M₁) z) v =
    0

Tactic:
simp [f.map_eq_zero_of_eq v h hne]

Premises used: AlternatingMap.map_eq_zero_of_eq
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
Goal:
R : Type u_10
M₁ : Type u_11
M₂ : Type u_12
ι : Type u_13
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
f : M₁ [⋀^ι]→ₗ[R] R
z : M₂
⊢ Eq (α := MultilinearMap.{u_10, u_13, u_11, u_12} R (fun (x : ι) ↦ M₁) M₂)
    (↑(f.smulRight z) : MultilinearMap R (fun (x : ι) ↦ M₁) M₂)
    ((↑f : MultilinearMap R (fun (x : ι) ↦ M₁) R).smulRight (M₁ := fun (x : ι) ↦ M₁) z)

Tactic:
rfl

Premises used: MultilinearMap.smulRight, LinearMap.compMultilinearMap, 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
f f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v_1 : ι → M
v' : ι → M'
a b : M [⋀^ι]→ₗ[R] N
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ ((↑a : MultilinearMap R (fun (x : ι) ↦ M) N) + (↑b : MultilinearMap R (fun (x : ι) ↦ M) N)).toFun (M₁ := fun (x : ι) ↦
      M) v =
    0

Tactic:
simp [a.map_eq_zero_of_eq v h hij, b.map_eq_zero_of_eq v h hij]

Premises used: AlternatingMap.map_eq_zero_of_eq
-- 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 f' : M [⋀^ι]→ₗ[R] N
v : ι → M
⊢ (f + f' : (a : ι → M) → N) v =
    HAdd.hAdd (α := N) (β := N) ((f : (a : ι → M) → N) v : N) ((f' : (a : ι → M) → N) v : 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_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
f f' : M [⋀^ι]→ₗ[R] N
⊢ (↑(f + f') : MultilinearMap R (fun (x : ι) ↦ M) N) =
    (↑f : MultilinearMap R (fun (x : ι) ↦ M) N) + (↑f' : MultilinearMap R (fun (x : ι) ↦ 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_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
f f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
x : ι → M
x_1 x_2 : ι
h : x x_1 = x x_2
h_1 : x_1 ≠ x_2
⊢ Eq.{u_3 + 1} (α := N) (MultilinearMap.toFun.{u_1, u_7, u_2, u_3} (R := R) (M₁ := fun (x : ι) ↦ M) 0 x) 0

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
ι : Type u_7
v : ι → M
⊢ Eq.{u_3 + 1} (α := N) ((0 : (a : ι → M) → N) v : N) (0 : 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_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
⊢ Eq (α := MultilinearMap.{u_1, u_7, u_2, u_3} R (fun (x : ι) ↦ M) N) (↑0 : MultilinearMap R (fun (x : ι) ↦ M) N) 0

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_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
⊢ Eq (α := M [⋀^ι]→ₗ[R] N) { toMultilinearMap := 0, map_eq_zero_of_eq' := ⋯ } 0

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_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
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 : ι
h : v i = v j
hij : i ≠ j
⊢ (-(↑f : MultilinearMap R (fun (x : ι) ↦ M) N')).toFun (M₁ := fun (x : ι) ↦ M) v = 0

Tactic:
simp [f.map_eq_zero_of_eq v h hij]

Premises used: AlternatingMap.map_eq_zero_of_eq
-- 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'
m : ι → M
⊢ Eq.{u_6 + 1} (α := N') ((-g : (a : ι → M) → N') m : N') (-(g : (a : ι → M) → N') 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
g : M [⋀^ι]→ₗ[R] N'
⊢ (↑(-g) : MultilinearMap R (fun (x : ι) ↦ M) N') = -(↑g : MultilinearMap R (fun (x : ι) ↦ 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_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
f_1 f' : M [⋀^ι]→ₗ[R] N
g_1 g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v_1 : ι → M
v' : ι → M'
f g : M [⋀^ι]→ₗ[R] N'
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ ((↑f : MultilinearMap R (fun (x : ι) ↦ M) N') - (↑g : MultilinearMap R (fun (x : ι) ↦ M) N')).toFun (M₁ :=
      fun (x : ι) ↦ M) v =
    0

Tactic:
simp [f.map_eq_zero_of_eq v h hij, g.map_eq_zero_of_eq v h hij]

Premises used: AlternatingMap.map_eq_zero_of_eq
-- 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 g₂ : M [⋀^ι]→ₗ[R] N'
m : ι → M
⊢ (g - g₂ : (a : ι → M) → N') m =
    HSub.hSub (α := N') (β := N') ((g : (a : ι → M) → N') m : N') ((g₂ : (a : ι → M) → N') 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
g g₂ : M [⋀^ι]→ₗ[R] N'
⊢ (↑(g - g₂) : MultilinearMap R (fun (x : ι) ↦ M) N') =
    (↑g : MultilinearMap R (fun (x : ι) ↦ M) N') - (↑g₂ : MultilinearMap R (fun (x : ι) ↦ 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_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
f f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
S : Type u_10
inst_11 : Semiring S
inst_12 : Module S N
inst_13 : SMulCommClass R S N
inst_14 : IsTorsionFree S N
⊢ IsTorsionFree S (M [⋀^ι]→ₗ[R] N)

Tactic:
coe_injective.moduleIsTorsionFree _ coeFn_smul

Premises used: AlternatingMap.coe_injective, AlternatingMap.coeFn_smul, Function.Injective.moduleIsTorsionFree
-- 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
S : Type u_10
N₂ : Type u_11
inst_11 : AddCommMonoid N₂
inst_12 : Module R N₂
g : N →ₗ[R] N₂
f : M [⋀^ι]→ₗ[R] N
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ (g.compMultilinearMap (M₁ := fun (x : ι) ↦ M) (↑f : MultilinearMap R (fun (x : ι) ↦ M) N)).toFun (M₁ := fun (x : ι) ↦
      M) v =
    0

Tactic:
simp [f.map_eq_zero_of_eq v h hij]

Premises used: AlternatingMap.map_eq_zero_of_eq