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
N₂ : Type u_11
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
g : N →ₗ[R] N₂
f : M [⋀^ι]→ₗ[R] N
⊢ Eq (α := (a : ι → M) → N₂) (⇑(g.compAlternatingMap f) : (a : ι → M) → N₂)
    (Function.comp (β := N) (⇑g : (a : N) → 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
N₂ : Type u_11
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
g : N →ₗ[R] N₂
f : M [⋀^ι]→ₗ[R] N
m : ι → M
⊢ Eq.{u_11 + 1} (α := N₂) ((g.compAlternatingMap f : (a : ι → M) → N₂) m : N₂)
    ((g : (a : N) → N₂) ((f : (a : ι → M) → N) m : N) : 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
N₂ : Type u_11
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
g : N →ₗ[R] N₂
⊢ Eq (α := M [⋀^ι]→ₗ[R] N₂) (g.compAlternatingMap 0) 0

Tactic:
AlternatingMap.ext fun _ => map_zero g

Premises used: map_zero, 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
N₂ : Type u_11
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
f : M [⋀^ι]→ₗ[R] N
⊢ Eq (α := M [⋀^ι]→ₗ[R] N₂) (compAlternatingMap 0 f) 0

Tactic:
rfl

Premises used: LinearMap.compAlternatingMap, 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
ι : Type u_7
N₂ : Type u_11
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
g : N →ₗ[R] N₂
f₁ f₂ : M [⋀^ι]→ₗ[R] N
⊢ g.compAlternatingMap (f₁ + f₂) = g.compAlternatingMap f₁ + g.compAlternatingMap f₂

Tactic:
AlternatingMap.ext fun _ => map_add g _ _

Premises used: map_add, AlternatingMap.toMultilinearMap, AlternatingMap.ext, 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
N₂ : Type u_11
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
g₁ g₂ : N →ₗ[R] N₂
f : M [⋀^ι]→ₗ[R] N
⊢ (g₁ + g₂).compAlternatingMap f = g₁.compAlternatingMap f + g₂.compAlternatingMap f

Tactic:
rfl

Premises used: LinearMap.compAlternatingMap, 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
ι : Type u_7
S : Type u_10
N₂ : Type u_11
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
inst_7 : Monoid S
inst_8 : DistribMulAction S N
inst_9 : DistribMulAction S N₂
inst_10 : SMulCommClass R S N
inst_11 : SMulCommClass R S N₂
inst_12 : CompatibleSMul N N₂ S R
g : N →ₗ[R] N₂
s : S
f : M [⋀^ι]→ₗ[R] N
⊢ g.compAlternatingMap (s • f) = s • g.compAlternatingMap f

Tactic:
AlternatingMap.ext fun _ => g.map_smul_of_tower _ _

Premises used: AlternatingMap.toMultilinearMap, LinearMap.map_smul_of_tower, AlternatingMap.ext, 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
S : Type u_10
N₂ : Type u_11
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
inst_7 : Monoid S
inst_8 : DistribMulAction S N₂
inst_9 : SMulCommClass R S N₂
g : N →ₗ[R] N₂
s : S
f : M [⋀^ι]→ₗ[R] N
⊢ (s • g).compAlternatingMap f = s • g.compAlternatingMap f

Tactic:
rfl

Premises used: LinearMap.compAlternatingMap, LinearMap.compMultilinearMap, rfl
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
Goal:
R : Type u_12
M₁ : Type u_13
M₂ : Type u_14
ι : Type u_15
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 (α := M₁ [⋀^ι]→ₗ[R] M₂) (f.smulRight z) (compAlternatingMap (smulRight id z) f)

Tactic:
rfl

Premises used: AlternatingMap.smulRight, MultilinearMap.smulRight, LinearMap.compAlternatingMap, 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
p : Submodule R N
h : ∀ (v : ι → M), Membership.mem (α := N) p ((f : (a : ι → M) → N) v : N)
⊢ p.subtype.compAlternatingMap (f.codRestrict p h) = f

Tactic:
AlternatingMap.ext fun _ => rfl

Premises used: AlternatingMap.ext, 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
N₂ : Type u_11
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₂
g : N →ₗ[R] N₂
f : M [⋀^ι]→ₗ[R] N
p : Submodule R N₂
h : ∀ (c : N), Membership.mem (α := N₂) p ((g : (a : N) → N₂) c : N₂)
⊢ (codRestrict p g h).compAlternatingMap f = (g.compAlternatingMap f).codRestrict p ⋯

Tactic:
AlternatingMap.ext fun _ => rfl

Premises used: AlternatingMap.ext, 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
M₂ : Type u_10
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
f : M [⋀^ι]→ₗ[R] N
g : M₂ →ₗ[R] M
⊢ Eq (α := (a : ι → M₂) → N) (⇑(f.compLinearMap g) : (a : ι → M₂) → N)
    (Function.comp (β := ι → M) (⇑f : (a : ι → M) → N) fun (x : ι → M₂) ↦ (⇑g : (a : M₂) → M) ∘ x)

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
M₂ : Type u_10
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
f : M [⋀^ι]→ₗ[R] N
g : M₂ →ₗ[R] M
v : ι → M₂
⊢ Eq.{u_3 + 1} (α := N) ((f.compLinearMap g : (a : ι → M₂) → N) v : N)
    ((f : (a : ι → M) → N) fun (i : ι) ↦ (g : (a : M₂) → M) (v i) : 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
M₂ : Type u_10
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
M₃ : Type u_11
inst_7 : AddCommMonoid M₃
inst_8 : Module R M₃
f : M [⋀^ι]→ₗ[R] N
g₁ : M₂ →ₗ[R] M
g₂ : M₃ →ₗ[R] M₂
⊢ (f.compLinearMap g₁).compLinearMap g₂ = f.compLinearMap (g₁ ∘ₗ g₂)

Tactic:
rfl

Premises used: MultilinearMap.compLinearMap, AlternatingMap.compLinearMap, 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
M₂ : Type u_10
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
g : M₂ →ₗ[R] M
H : ∀ (x : ι → M₂), Eq.{u_3 + 1} (α := N) ((compLinearMap 0 g : (a : ι → M₂) → N) x : N) ((0 : (a : ι → M₂) → N) x : N)
⊢ Eq (α := M₂ [⋀^ι]→ₗ[R] N) (compLinearMap 0 g) 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
ι : Type u_7
M₂ : Type u_10
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
g : M₂ →ₗ[R] M
x : ι → M₂
⊢ Eq.{u_3 + 1} (α := N) ((compLinearMap 0 g : (a : ι → M₂) → N) x : N) ((0 : (a : ι → M₂) → N) x : N)

Tactic:
simp only [compLinearMap_apply, zero_apply]

Premises used: AlternatingMap.zero_apply, AlternatingMap.compLinearMap_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_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
M₂ : Type u_10
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
f₁ f₂ : M [⋀^ι]→ₗ[R] N
g : M₂ →ₗ[R] M
H :
  ∀ (x : ι → M₂),
    Eq.{u_3 + 1} (α := N) (((f₁ + f₂).compLinearMap g : (a : ι → M₂) → N) x : N)
      ((f₁.compLinearMap g + f₂.compLinearMap g : (a : ι → M₂) → N) x : N)
⊢ (f₁ + f₂).compLinearMap g = f₁.compLinearMap g + f₂.compLinearMap g

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
ι : Type u_7
M₂ : Type u_10
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
f₁ f₂ : M [⋀^ι]→ₗ[R] N
g : M₂ →ₗ[R] M
x : ι → M₂
⊢ Eq.{u_3 + 1} (α := N) (((f₁ + f₂).compLinearMap g : (a : ι → M₂) → N) x : N)
    ((f₁.compLinearMap g + f₂.compLinearMap g : (a : ι → M₂) → N) x : N)

Tactic:
simp only [compLinearMap_apply, add_apply]

Premises used: AlternatingMap.add_apply, AlternatingMap.compLinearMap_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_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
M₂ : Type u_10
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : M [⋀^ι]→ₗ[R] N
H : ∀ (x : ι → M₂), Eq.{u_3 + 1} (α := N) ((f.compLinearMap 0 : (a : ι → M₂) → N) x : N) ((0 : (a : ι → M₂) → N) x : N)
⊢ Eq (α := M₂ [⋀^ι]→ₗ[R] N) (f.compLinearMap 0) 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
ι : Type u_7
M₂ : Type u_10
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : M [⋀^ι]→ₗ[R] N
x : ι → M₂
H :
  Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) fun (i : ι) ↦ (0 : (a : M₂) → M) (x i) : N)
    ((0 : (a : ι → M₂) → N) x : N)
H₁ : Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) fun (i : ι) ↦ 0 : N) ((0 : (a : ι → M₂) → N) x : N)
H₂ : Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) 0 : N) ((0 : (a : ι → M₂) → N) x : N)
H₃ : Eq.{u_3 + 1} (α := N) (0 : N) ((0 : (a : ι → M₂) → N) x : N)
⊢ Eq.{u_3 + 1} (α := N) ((f.compLinearMap 0 : (a : ι → M₂) → N) x : N) ((0 : (a : ι → M₂) → N) x : N)

Tactic:
simp_rw [compLinearMap_apply, LinearMap.zero_apply, ← Pi.zero_def, map_zero, zero_apply]

Premises used: LinearMap.zero_apply, AlternatingMap.zero_apply, Pi.zero_def, AlternatingMap.map_zero, AlternatingMap.compLinearMap_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_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
⊢ f.compLinearMap LinearMap.id = f

Tactic:
ext fun _ => rfl

Premises used: AlternatingMap.ext, 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
M₂ : Type u_10
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
f : M₂ →ₗ[R] M
hf : Function.Surjective.{u_10 + 1, u_2 + 1} (α := M₂) (β := M) (⇑f : (a : M₂) → M)
g₁ g₂ : M [⋀^ι]→ₗ[R] N
h :
  Eq (α := M₂ [⋀^ι]→ₗ[R] N) ((fun (g : M [⋀^ι]→ₗ[R] N) ↦ g.compLinearMap f) g₁)
    ((fun (g : M [⋀^ι]→ₗ[R] N) ↦ g.compLinearMap f) g₂)
x : ι → M
⊢ Eq.{u_3 + 1} (α := N) ((g₁ : (a : ι → M) → N) x : N) ((g₂ : (a : ι → M) → N) x : N)

Tactic:
simpa [Function.surjInv_eq hf] using AlternatingMap.ext_iff.mp h (Function.surjInv hf ∘ x)

Premises used: Function.comp, Function.surjInv, Function.surjInv_eq, AlternatingMap.ext_iff, Iff.mp
-- 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
M₂ : Type u_10
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
f : M₂ →ₗ[R] M
hf : Function.Surjective.{u_10 + 1, u_2 + 1} (α := M₂) (β := M) (⇑f : (a : M₂) → M)
g₁ g₂ : M [⋀^ι]→ₗ[R] N
⊢ g₁.compLinearMap f = g₂.compLinearMap f ↔ g₁ = g₂

Tactic:
(compLinearMap_injective _ hf).eq_iff

Premises used: Function.Injective.eq_iff, AlternatingMap.compLinearMap_injective
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
Goal:
N : Type u_3
inst : AddCommMonoid N
ι : Type u_7
R : Type u_12
inst_1 : CommSemiring R
inst_2 : Module R N
inst_3 : Finite ι
f g : R [⋀^ι]→ₗ[R] N
h : Eq.{u_3 + 1} (α := N) ((f : (a : ι → R) → N) fun (x : ι) ↦ 1 : N) ((g : (a : ι → R) → N) fun (x : ι) ↦ 1 : N)
⊢ f = g

Tactic:
coe_multilinearMap_injective <| MultilinearMap.ext_ring h

Premises used: MultilinearMap.ext_ring, AlternatingMap.coe_multilinearMap_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
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) (domLCongr R N ι S (LinearEquiv.refl R M))
    (LinearEquiv.refl S (M [⋀^ι]→ₗ[R] N))

Tactic:
LinearEquiv.ext fun _ => AlternatingMap.ext fun _ => rfl

Premises used: LinearEquiv.ext, AlternatingMap.ext, 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
M₂ : Type u_10
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
S : Type u_12
inst_7 : Semiring S
inst_8 : Module S N
inst_9 : SMulCommClass R S N
e : M ≃ₗ[R] M₂
⊢ Eq (α := M₂ [⋀^ι]→ₗ[R] N ≃ₗ[S] M [⋀^ι]→ₗ[R] N) (LinearEquiv.symm (domLCongr R N ι S e)) (domLCongr R N ι S e.symm)

Tactic:
rfl

Premises used: LinearEquiv.symm, AlternatingMap.compLinearMap, rfl, AlternatingMap.domLCongr
-- 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
M₂ : Type u_10
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
M₃ : Type u_11
inst_7 : AddCommMonoid M₃
inst_8 : Module R M₃
S : Type u_12
inst_9 : Semiring S
inst_10 : Module S N
inst_11 : SMulCommClass R S N
e : M ≃ₗ[R] M₂
f : M₂ ≃ₗ[R] M₃
⊢ Eq (α := M [⋀^ι]→ₗ[R] N ≃ₗ[S] M₃ [⋀^ι]→ₗ[R] N) (domLCongr R N ι S e ≪≫ₗ domLCongr R N ι S f)
    (domLCongr R N ι S (e ≪≫ₗ f))

Tactic:
rfl

Premises used: MultilinearMap.compLinearMap, LinearEquiv.trans, AlternatingMap.compLinearMap, rfl, AlternatingMap.domLCongr
-- 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
M₂ : Type u_10
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
f : M [⋀^ι]→ₗ[R] N
g : M₂ ≃ₗ[R] M
⊢ f.compLinearMap (↑g : M₂ →ₗ[R] M) = 0 ↔ f = 0

Tactic:
(domLCongr R N ι ℕ g.symm).map_eq_zero_iff

Premises used: LinearEquiv.symm, LinearEquiv.map_eq_zero_iff, Nat, AlternatingMap.compLinearMap, AlternatingMap.domLCongr
-- 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
α : Type u_12
inst_5 : DecidableEq ι
t : Finset α
i : ι
g : α → M
m : ι → M
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) m i (∑ a ∈ t, g a)) : N)
    (∑ a ∈ t, (f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) m i (g a)) : N)

Tactic:
f.toMultilinearMap.map_update_sum t i g m

Premises used: AlternatingMap.toMultilinearMap, MultilinearMap.map_update_sum
-- 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 ι
inst_6 : Fintype ι
m m' : ι → M
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) (m + m') : N)
    (∑ s : Finset ι, (f : (a : ι → M) → N) (s.piecewise (π := fun (a : ι) ↦ M) m m') : N)

Tactic:
f.toMultilinearMap.map_add_univ m m'

Premises used: AlternatingMap.toMultilinearMap, MultilinearMap.map_add_univ
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
Goal:
ι : Type u_7
R : Type u_12
inst : CommSemiring R
M : Type u_13
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_14
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Fintype ι
f : M [⋀^ι]→ₗ[R] N
c : ι → R
m : ι → M
⊢ ((f : (a : ι → M) → N) fun (i : ι) ↦ c i • m i) =
    HSMul.hSMul.{u_12, u_14, u_14} (α := R) (β := N) (∏ i : ι, c i) ((f : (a : ι → M) → N) m : N)

Tactic:
f.toMultilinearMap.map_smul_univ c m

Premises used: AlternatingMap.toMultilinearMap, MultilinearMap.map_smul_univ
-- 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 j : ι
hij : i ≠ j
rw : v j = update (β := fun (a : ι) ↦ M) v i (v j) j
rw₁ rw₂ : v j = v j
⊢ update (β := fun (a : ι) ↦ M) v i (v j) i = update (β := fun (a : ι) ↦ M) v i (v j) j

Tactic:
rw [Function.update_self, Function.update_of_ne hij.symm]

Premises used: Ne.symm, Function.update_self, Function.update_of_ne
-- 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 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
rw₂ rw₃ : 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

Tactic:
rw [Function.update_self, Function.update_of_ne hij, Function.update_self]

Premises used: Function.update_self, Function.update_of_ne
-- 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 j : ι
hij : i ≠ j
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
⊢ HAdd.hAdd (α := N) (β := N) ((f : (a : ι → M) → N) (v ∘ (⇑(Equiv.swap i j) : (a : ι) → ι)) : N)
      ((f : (a : ι → M) → N) v : N) =
    0

Tactic:
rw [Equiv.comp_swap_eq_update]

Premises used: Equiv.comp_swap_eq_update
-- 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 j : ι
hij : i ≠ j
⊢ Eq.{u_3 + 1} (α := N)
    ((f : (a : ι → M) → N)
        (update (β := fun (a : ι) ↦ M) (update (β := fun (a : ι) ↦ M) v i (v i + v j)) j (v i + v j)) :
      N)
    (0 : N)

Tactic:
f.map_update_update v hij (v i + v j)

Premises used: AlternatingMap.map_update_update, HAdd.hAdd
-- 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 j : ι
hij : i ≠ j
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))
⊢ 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:
convert! f.map_update_update v hij (v i + v j)

Premises used: AlternatingMap.map_update_update, HAdd.hAdd
-- 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 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) =
    (f : (a : ι → M) → N) (update (β := fun (a : ι) ↦ M) (update (β := fun (a : ι) ↦ M) v i (v i + v j)) j (v i + v j))

Tactic:
simp [f.map_update_self _ hij, f.map_update_self _ hij.symm,
    Function.update_comm hij (v i + v j) (v _) v, Function.update_comm hij.symm (v i) (v i) v]

Premises used: Ne.symm, Function.update_comm, 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
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst_5 : DecidableEq ι
i j : ι
hij : i ≠ j
rw :
  HAdd.hAdd (α := N) (β := N) ((f : (a : ι → M) → N) (v ∘ (⇑(Equiv.swap i j) : (a : ι) → ι)) : N)
      ((f : (a : ι → M) → N) v : N) =
    0
⊢ HAdd.hAdd (α := N) (β := N) ((f : (a : ι → M) → N) v : N)
      ((f : (a : ι → M) → N) (v ∘ (⇑(Equiv.swap i j) : (a : ι) → ι)) : N) =
    0

Tactic:
rw [add_comm]

Premises used: add_comm
-- 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 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

Tactic:
f.map_swap_add v hij

Premises used: AlternatingMap.map_swap_add
-- 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 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

Tactic:
exact f.map_swap_add v hij

Premises used: AlternatingMap.map_swap_add
-- 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 ι
i j : ι
hij : i ≠ j
⊢ Eq.{u_6 + 1} (α := N') ((g : (a : ι → M) → N') (v ∘ (⇑(Equiv.swap i j) : (a : ι) → ι)) : N')
    (-(g : (a : ι → M) → N') v : N')

Tactic:
eq_neg_of_add_eq_zero_left <| g.map_swap_add v hij

Premises used: eq_neg_of_add_eq_zero_left, AlternatingMap.map_swap_add