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' : MultilinearMap R M₁ M₂
k n : ℕ
f : MultilinearMap R (fun x ↦ M') M₂
s : Finset (Fin n)
hk : #s = k
z : M'
⊢ ∀ [inst : DecidableEq (Fin k)] (m : Fin k → M') (i : Fin k) (x y : M'),
    (f fun j ↦ if h : j ∈ s then update m i (x + y) ((s.orderIsoOfFin hk).symm ⟨j, h⟩) else z) =
      (f fun j ↦ if h : j ∈ s then update m i x ((s.orderIsoOfFin hk).symm ⟨j, h⟩) else z) +
        f fun j ↦ if h : j ∈ s then update m i y ((s.orderIsoOfFin hk).symm ⟨j, h⟩) else z

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₂
k n : ℕ
f : MultilinearMap R (fun x ↦ M') M₂
s : Finset (Fin n)
hk : #s = k
z : M'
⊢ ∀ [inst : DecidableEq (Fin k)] (m : Fin k → M') (i : Fin k) (c : R) (x : M'),
    (f fun j ↦ if h : j ∈ s then update m i (c • x) ((s.orderIsoOfFin hk).symm ⟨j, h⟩) else z) =
      c • f fun j ↦ if h : j ∈ s then update m i x ((s.orderIsoOfFin hk).symm ⟨j, h⟩) else z

Tactic:
by

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

Goal state before:
pp: R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.succ
x y : M 0
⊢ f (Fin.cons (x + y) m) = f (Fin.cons x m) + f (Fin.cons y m)

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'
S : Type u_12
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
σ : ι ≃ ι'
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
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.succ
c : R
x : M 0
⊢ f (Fin.cons (c • x) m) = c • f (Fin.cons x m)

Tactic:
by

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

Goal state before:
pp: R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.castSucc
x y : M (last n)
⊢ f (snoc m (x + y)) = f (snoc m x) + f (snoc m 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
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'
S : Type u_12
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
σ : ι ≃ ι'
m : M [⋀^ι']→ₗ[R] N
⊢ domDomCongr σ (domDomCongr σ.symm m) = m

Tactic:
by

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

Goal state before:
pp: R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.castSucc
c : R
x : M (last n)
⊢ f (snoc m (c • x)) = c • f (snoc m x)

Tactic:
by

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

Goal state before:
pp: R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
p : Fin (n + 1)
m : (i : Fin n) → M (p.succAbove i)
x y : M p
⊢ f (p.insertNth (x + y) m) = f (p.insertNth x m) + f (p.insertNth y m)

Tactic:
by

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

Goal state before:
pp: R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
p : Fin (n + 1)
m : (i : Fin n) → M (p.succAbove i)
c : R
x : M p
⊢ f (p.insertNth (c • x) m) = c • f (p.insertNth x m)

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✝⁴ : (i : ι) → AddCommMonoid (M₁' i)
inst✝³ : (i : ι) → Module R (M₁' i)
inst✝² : (i : ι) → AddCommMonoid (M₁'' i)
inst✝¹ : (i : ι) → Module R (M₁'' i)
g : MultilinearMap R M₁' M₂
f : (i : ι) → M₁ i →ₗ[R] M₁' i
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ (g fun i_1 ↦ (f i_1) (update m i (x + y) i_1)) =
    (g fun i_1 ↦ (f i_1) (update m i x i_1)) + g fun i_1 ↦ (f i_1) (update m i y i_1)

Tactic:
by

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

Goal state before:
pp: ι : Type u_7
K : Type u_12
M : Type u_13
N : Type u_14
inst✝⁶ : Ring K
inst✝⁵ : IsDomain K
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : IsTorsionFree K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
h : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
hz : g i ≠ 0
this✝ : DecidableEq ι := Classical.decEq ι
this : f (update v i (g i • v i)) = 0
⊢ f v = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
⊢ ∀ (i : Perm n), i ∈ ofSign s ↔ (Equiv.inv (Perm n)) i ∈ ofSign s

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✝⁴ : (i : ι) → AddCommMonoid (M₁' i)
inst✝³ : (i : ι) → Module R (M₁' i)
inst✝² : (i : ι) → AddCommMonoid (M₁'' i)
inst✝¹ : (i : ι) → Module R (M₁'' i)
g : MultilinearMap R M₁' M₂
f : (i : ι) → M₁ i →ₗ[R] M₁' i
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ (g fun i_1 ↦ (f i_1) (update m i (c • x) i_1)) = c • g fun i_1 ↦ (f i_1) (update m i x i_1)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
σ : Perm n
x✝ : σ ∈ ofSign s
⊢ ∀ (i : n), i ∈ univ ↔ σ i ∈ univ

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
σ : Perm n
x✝ : σ ∈ ofSign s
⊢ ∀ i ∈ univ, Aᵀ i (σ i) = A (σ i) (((Equiv.inv (Perm n)) σ) (σ i))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
s : ℤˣ
inst✝ : Nonempty n
⊢ detp s 0 = 0

Tactic:
by

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

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
inst✝¹ : (i : ι) → AddCommMonoid (M₁' i)
inst✝ : (i : ι) → Module R (M₁' i)
f : (i : ι) → M₁ i →ₗ[R] M₁' i
hf : ∀ (i : ι), Surjective ⇑(f i)
g₁ g₂ : MultilinearMap R M₁' M₂
h : (fun g ↦ g.compLinearMap f) g₁ = (fun g ↦ g.compLinearMap f) g₂
x : (i : ι) → M₁' i
⊢ g₁ x = g₂ x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
d : n → R
⊢ detp 1 (diagonal d) = ∏ i, d i

Tactic:
by

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

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
inst✝¹ : (i : ι) → AddCommMonoid (M₁' i)
inst✝ : (i : ι) → Module R (M₁' i)
g : MultilinearMap R M₁' M₂
f : (i : ι) → M₁ i ≃ₗ[R] M₁' i
⊢ (g.compLinearMap fun i ↦ ↑(f i)) = 0 ↔ g = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
⊢ detp 1 1 = 1

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✝⁵ : (i : ι) → AddCommMonoid (M₁' i)
inst✝⁴ : (i : ι) → Module R (M₁' i)
inst✝³ : (i : ι) → AddCommMonoid (M₁'' i)
inst✝² : (i : ι) → Module R (M₁'' i)
β : ι → Type u_1
N : (i : ι) → β i → Type u_2
inst✝¹ : (i : ι) → (b : β i) → AddCommMonoid (N i b)
inst✝ : (i : ι) → (b : β i) → Module R (N i b)
g : MultilinearMap R M₁ M₂
f : (i : ι) → MultilinearMap R (N i) (M₁ i)
hDecEqSigma : DecidableEq ((i : ι) × β i)
⊢ ∀ (m : (i : (i : ι) × β i) → N i.fst i.snd) (i : (i : ι) × β i) (x y : N i.fst i.snd),
    (g fun i_1 ↦ (f i_1) (Sigma.curry (update m i (x + y)) i_1)) =
      (g fun i_1 ↦ (f i_1) (Sigma.curry (update m i x) i_1)) + g fun i_1 ↦ (f i_1) (Sigma.curry (update m i y) i_1)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
d : n → R
σ : Perm n
hσ : σ ∈ ofSign (-1)
⊢ σ ≠ 1

Tactic:
by

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

Goal state before:
pp: ι : Type u_7
K : Type u_12
M : Type u_13
N : Type u_14
inst✝⁶ : Ring K
inst✝⁵ : IsDomain K
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : IsTorsionFree K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h : ¬LinearIndependent K v
⊢ f v = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
d : n → R
⊢ detp (-1) (diagonal d) = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
⊢ detp (-1) 1 = 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_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : MultilinearMap R (fun x ↦ M) N'
v : ι → M
i j : ι
i_ne_j : i ≠ j
hv : v i = v j
σ : Perm ι
x✝ : σ ∈ Finset.univ
⊢ (Perm.sign σ • domDomCongr σ m) v + (Perm.sign (swap i j * σ) • domDomCongr (swap i j * σ) m) 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_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : MultilinearMap R (fun x ↦ M) N'
v : ι → M
i j : ι
i_ne_j : i ≠ j
hv : v i = v j
⊢ (∑ σ, Perm.sign σ • domDomCongr σ m) v = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
A : Matrix n n R
inst✝ : IsEmpty n
⊢ detp 1 A = 1

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✝⁵ : (i : ι) → AddCommMonoid (M₁' i)
inst✝⁴ : (i : ι) → Module R (M₁' i)
inst✝³ : (i : ι) → AddCommMonoid (M₁'' i)
inst✝² : (i : ι) → Module R (M₁'' i)
β : ι → Type u_1
N : (i : ι) → β i → Type u_2
inst✝¹ : (i : ι) → (b : β i) → AddCommMonoid (N i b)
inst✝ : (i : ι) → (b : β i) → Module R (N i b)
g : MultilinearMap R M₁ M₂
f : (i : ι) → MultilinearMap R (N i) (M₁ i)
hDecEqSigma : DecidableEq ((i : ι) × β i)
⊢ ∀ (m : (i : (i : ι) × β i) → N i.fst i.snd) (i : (i : ι) × β i) (c : R) (x : N i.fst i.snd),
    (g fun i_1 ↦ (f i_1) (Sigma.curry (update m i (c • x)) i_1)) =
      c • g fun i_1 ↦ (f i_1) (Sigma.curry (update m i x) i_1)

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
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ (let __src := ∑ σ, Perm.sign σ • domDomCongr σ 0;
    { toFun := ⇑(∑ σ, Perm.sign σ • domDomCongr σ 0), map_update_add' := ⋯, map_update_smul' := ⋯,
      map_eq_zero_of_eq' := ⋯ }) =
    0

Tactic:
by

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

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
t : Finset ι
⊢ ∀ (m' : (i : ι) → M₁ i), f (∅.piecewise (m + m') m') = ∑ s ∈ ∅.powerset, f (s.piecewise m m')

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
A : Matrix n n R
inst✝ : IsEmpty n
⊢ detp (-1) A = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
f g : m ≃ n
⊢ ∀ (i : Perm m), i ∈ ofSign s ↔ (f.equivCongr g) i ∈ ofSign (s * sign (f.symm.trans g))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
f g : m ≃ n
x✝¹ : Perm m
x✝ : x✝¹ ∈ ofSign s
⊢ ∀ (i : m), i ∈ univ ↔ f i ∈ univ

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
f g : m ≃ n
x✝³ : Perm m
x✝² : x✝³ ∈ ofSign s
x✝¹ : m
x✝ : x✝¹ ∈ univ
⊢ A.submatrix (⇑f) (⇑g) x✝¹ (x✝³ x✝¹) = A (f x✝¹) (((f.equivCongr g) x✝³) (f x✝¹))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
e : m ≃ n
⊢ detp s (A.submatrix ⇑e ⇑e) = detp s A

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
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : MultilinearMap R (fun x ↦ M) N'
⊢ (let __src := ∑ σ, Perm.sign σ • domDomCongr σ (a + b);
    { toFun := ⇑(∑ σ, Perm.sign σ • domDomCongr σ (a + b)), map_update_add' := ⋯, map_update_smul' := ⋯,
      map_eq_zero_of_eq' := ⋯ }) =
    (let __src := ∑ σ, Perm.sign σ • domDomCongr σ a;
      { toFun := ⇑(∑ σ, Perm.sign σ • domDomCongr σ a), map_update_add' := ⋯, map_update_smul' := ⋯,
        map_eq_zero_of_eq' := ⋯ }) +
      let __src := ∑ σ, Perm.sign σ • domDomCongr σ b;
      { toFun := ⇑(∑ σ, Perm.sign σ • domDomCongr σ b), map_update_add' := ⋯, map_update_smul' := ⋯,
        map_eq_zero_of_eq' := ⋯ }

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
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : MultilinearMap R (fun x ↦ M) N'
v : ι → M
⊢ (alternatization m) v = ∑ σ, Perm.sign σ • (domDomCongr σ m) v

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
c : R
⊢ detp s (c • A) = c ^ Fintype.card n * detp s A

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
s : ℤˣ
A : Matrix n n R
S : Type u_4
inst✝ : CommSemiring S
f : R →+* S
⊢ detp s (A.map ⇑f) = f (detp s A)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
eq : detp 1 A = detp (-1) A
⊢ A.IsDetpBalanced a b

Tactic:
by

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

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
t✝ : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)
⊢ update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'

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
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
a : M [⋀^ι]→ₗ[R] N'
⊢ MultilinearMap.alternatization ↑a = (Fintype.card ι).factorial • a

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
A : Matrix n n R
a b c : R
inst✝ : IsCancelAdd R
hab : A.IsDetpBalanced a b
hbc : A.IsDetpBalanced b c
⊢ A.IsDetpBalanced a c

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
N'₂ : Type u_10
inst✝³ : AddCommGroup N'₂
inst✝² : Module R N'₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
g : N' →ₗ[R] N'₂
f : MultilinearMap R (fun x ↦ M) N'
⊢ MultilinearMap.alternatization (g.compMultilinearMap f) = g.compAlternatingMap (MultilinearMap.alternatization f)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
s t : ℤˣ
⊢ a * detp s A + b * detp t A = b * detp s A + a * detp t A

Tactic:
by

Goal state after: