mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f✝ f'✝ f f' : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ f (update m i (c • x)) + f' (update m i (c • x)) = c • (f (update m i x) + f' (update m i x))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
N' : Type u_6
inst✝¹ : AddCommGroup N'
inst✝ : 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'
f g : M [⋀^ι]→ₗ[R] N
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f f' : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
x✝³ : (i : ι) → M₁ i
x✝² : ι
x✝¹ x✝ : M₁ x✝²
⊢ 0 = 0 + 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_7
f : (ι → M) → N
h₁ :
  ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (x y : M), f (update m i (x + y)) = f (update m i x) + f (update m i y)
h₂ : ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (c : R) (x : M), f (update m i (c • x)) = c • f (update m i x)
h₃ :
  ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → { toFun := f, map_update_add' := ⋯, map_update_smul' := ⋯ }.toFun v = 0
⊢ ↑{ toFun := f, map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := h₃ } =
    { toFun := f, map_update_add' := h₁, map_update_smul' := h₂ }

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
hv : ¬Injective v
⊢ f v = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f f' : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
x✝² : (i : ι) → M₁ i
x✝¹ : ι
c : R
x✝ : M₁ x✝¹
⊢ 0 = c • 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝¹³ : Semiring R
M : Type u_2
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
N : Type u_3
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
P : Type u_4
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
M' : Type u_5
inst✝⁶ : AddCommGroup M'
inst✝⁵ : Module R M'
N' : Type u_6
inst✝⁴ : AddCommGroup N'
inst✝³ : 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✝² : Monoid S
inst✝¹ : DistribMulAction S N
inst✝ : SMulCommClass R S N
c : S
f : M [⋀^ι]→ₗ[R] N
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ (c • ↑f).toFun v = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R✝ : Type u_1
inst✝¹⁵ : Semiring R✝
M : Type u_2
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R✝ M
N : Type u_3
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R✝ N
P : Type u_4
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R✝ P
M' : Type u_5
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R✝ M'
N' : Type u_6
inst✝⁶ : AddCommGroup N'
inst✝⁵ : 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'
R : Type u_10
M₁ : Type u_11
M₂ : Type u_12
ι : Type u_13
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
f : M₁ [⋀^ι]→ₗ[R] R
z : M₂
v : ι → M₁
i j : ι
h : v i = v j
hne : i ≠ j
⊢ ((↑f).smulRight z).toFun v = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
N' : Type u_6
inst✝¹ : AddCommGroup N'
inst✝ : 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'
a b : M [⋀^ι]→ₗ[R] N
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ (↑a + ↑b).toFun v = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
N' : Type u_6
inst✝¹ : AddCommGroup N'
inst✝ : 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✝³ x✝² : ι
x✝¹ : x✝⁴ x✝³ = x✝⁴ x✝²
x✝ : x✝³ ≠ x✝²
⊢ MultilinearMap.toFun 0 x✝⁴ = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹³ : Semiring R
inst✝¹² : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝¹¹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : (i : Fin n.succ) → Module R (M i)
inst✝⁶ : (i : ι) → Module R (M₁ i)
inst✝⁵ : Module R M₂
inst✝⁴ : Module R M₃
inst✝³ : Module R M'
f✝ f' : MultilinearMap R M₁ M₂
inst✝² : DistribSMul S M₂
inst✝¹ : SMulCommClass R S M₂
c : S
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ c • f (update m i (x + y)) = c • f (update m i x) + c • f (update m i y)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
N' : Type u_6
inst✝¹ : AddCommGroup N'
inst✝ : 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'
f : M [⋀^ι]→ₗ[R] N'
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ (-↑f).toFun v = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
N' : Type u_6
inst✝¹ : AddCommGroup N'
inst✝ : 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'
f g : M [⋀^ι]→ₗ[R] N'
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
⊢ (↑f - ↑g).toFun v = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝¹² : Semiring R
M : Type u_2
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
N : Type u_3
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
P : Type u_4
inst✝⁷ : AddCommMonoid P
inst✝⁶ : Module R P
M' : Type u_5
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
S : Type u_10
N₂ : Type u_11
inst✝¹ : AddCommMonoid N₂
inst✝ : 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 ↑f).toFun v = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹³ : Semiring R
inst✝¹² : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝¹¹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : (i : Fin n.succ) → Module R (M i)
inst✝⁶ : (i : ι) → Module R (M₁ i)
inst✝⁵ : Module R M₂
inst✝⁴ : Module R M₃
inst✝³ : Module R M'
f✝ f' : MultilinearMap R M₁ M₂
inst✝² : DistribSMul S M₂
inst✝¹ : SMulCommClass R S M₂
c : S
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
l : (i : ι) → M₁ i
i : ι
x : R
d : M₁ i
⊢ c • f (update l i (x • d)) = x • c • f (update l i d)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_7
M₂ : Type u_10
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₂ →ₗ[R] M
⊢ compLinearMap 0 g = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_7
M₂ : Type u_10
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f₁ f₂ : M [⋀^ι]→ₗ[R] N
g : M₂ →ₗ[R] M
⊢ (f₁ + f₂).compLinearMap g = f₁.compLinearMap g + f₂.compLinearMap g

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f f' : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ f (update m i (x + y)) = f (update m i x) + f (update m i y)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
N : Type u_3
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
ι : Type u_7
M₂ : Type u_10
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Nonempty ι
f : M [⋀^ι]→ₗ[R] N
⊢ f.compLinearMap 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_7
M₂ : Type u_10
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₂ →ₗ[R] M
hf : Function.Surjective ⇑f
g₁ g₂ : M [⋀^ι]→ₗ[R] N
h : (fun g ↦ g.compLinearMap f) g₁ = (fun g ↦ g.compLinearMap f) g₂
x : ι → M
⊢ g₁ x = g₂ x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f f' : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ f (update m i (c • x)) = (RingHom.id R) c • f (update m i x)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ update v i (v j) i = update v i (v j) j

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
m : M
⊢ update (update v i m) j m i = update (update v i m) j m j

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f✝ f' f : MultilinearMap R M₁ M₂
g : MultilinearMap R M₁ M₃
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ (f (update m i (x + y)), g (update m i (x + y))) =
    (f (update m i x), g (update m i x)) + (f (update m i y), g (update m i y))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ f (v ∘ ⇑(Equiv.swap i j)) + f v = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f✝ f' f : MultilinearMap R M₁ M₂
g : MultilinearMap R M₁ M₃
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ (f (update m i (c • x)), g (update m i (c • x))) = c • (f (update m i x), g (update m i x))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : Semiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ f v + f (v ∘ ⇑(Equiv.swap i j)) = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f✝ f' : MultilinearMap R M₁ M₂
inst✝ : Subsingleton ι
i : ι
f : M₂ →ₗ[R] M₃
⊢ ∀ [inst : DecidableEq ι] (m : ι → M₂) (i_1 : ι) (x y : M₂),
    f (update m i_1 (x + y) i) = f (update m i_1 x i) + f (update m i_1 y i)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f✝ f' : MultilinearMap R M₁ M₂
inst✝ : Subsingleton ι
i : ι
f : M₂ →ₗ[R] M₃
⊢ ∀ [inst : DecidableEq ι] (m : ι → M₂) (i_1 : ι) (c : R) (x : M₂),
    f (update m i_1 (c • x) i) = c • f (update m i_1 x i)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
g : M [⋀^ι]→ₗ[R] N'
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → M
σ : Equiv.Perm ι
⊢ g (v ∘ ⇑σ) = Equiv.Perm.sign σ • g v

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f✝ f' : MultilinearMap R M₁ M₂
inst✝ : Subsingleton ι
i : ι
f : MultilinearMap R (fun x ↦ M₂) M₃
x y : M₂
⊢ (f fun x_1 ↦ x + y) = (f fun x_1 ↦ x) + f fun x ↦ y

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f✝ f' : MultilinearMap R M₁ M₂
inst✝ : Subsingleton ι
i : ι
f : MultilinearMap R (fun x ↦ M₂) M₃
c : R
x : M₂
⊢ (f fun x_1 ↦ c • x) = (RingHom.id R) c • f fun x_1 ↦ x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
g : M [⋀^ι]→ₗ[R] N'
v : ι → M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
σ : Equiv.Perm ι
⊢ g v = Equiv.Perm.sign σ • g (v ∘ ⇑σ)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : Semiring R
M : Type u_2
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
N : Type u_3
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
P : Type u_4
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M' : Type u_5
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
N' : Type u_6
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
M₂ : Type u_10
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type u_11
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f✝ f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v✝ : ι → M
v' : ι → M'
σ : ι ≃ ι'
f : M [⋀^ι]→ₗ[R] N
v : ι' → M
i j : ι'
hv : v i = v j
hij : i ≠ j
⊢ (v ∘ ⇑σ) (σ.symm i) = (v ∘ ⇑σ) (σ.symm j)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : Semiring R
M : Type u_2
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
N : Type u_3
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
P : Type u_4
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M' : Type u_5
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
N' : Type u_6
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
M₂ : Type u_10
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type u_11
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f✝ f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
σ : ι ≃ ι'
f : M [⋀^ι]→ₗ[R] N
⊢ domDomCongr σ.symm (domDomCongr σ f) = f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f✝ f' : MultilinearMap R M₁ M₂
inst✝ : Subsingleton ι
i : ι
f : MultilinearMap R (fun x ↦ M₂) M₃
⊢ (fun f ↦ { toFun := fun x ↦ f (x i), map_update_add' := ⋯, map_update_smul' := ⋯ })
      ((fun f ↦ { toFun := fun x ↦ f fun x_1 ↦ x, map_add' := ⋯, map_smul' := ⋯ }) f) =
    f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁴ : Semiring R
M : Type u_2
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
N : Type u_3
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
P : Type u_4
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M' : Type u_5
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
N' : Type u_6
inst✝⁵ : AddCommGroup N'
inst✝⁴ : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
M₂ : Type u_10
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type u_11
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
σ : ι ≃ ι'
m : M [⋀^ι']→ₗ[R] N
⊢ domDomCongr σ (domDomCongr σ.symm m) = m

Tactic:
by

Goal state after: