mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ Aᵀ.IsDetpBalanced a b ↔ A.IsDetpBalanced a b

Tactic:
by

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

Goal state before:
pp: ι : Type u_7
ι₁ : Type u_10
inst✝⁵ : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R' N₁
inst✝ : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h : ∀ (v : ι → ι₁), Function.Injective v → (f fun i ↦ e (v i)) = g fun i ↦ e (v i)
⊢ f = 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
A : Matrix n n R
a b : R
e₁ e₂ : m ≃ n
h : A.IsDetpBalanced a b
⊢ (A.submatrix ⇑e₁ ⇑e₂).IsDetpBalanced a b

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
A : Matrix n n R
a b : R
e₁ e₂ : m ≃ n
h : (A.submatrix ⇑e₁ ⇑e₂).IsDetpBalanced a b
⊢ A.IsDetpBalanced a b

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
c : R
⊢ (c • A).IsDetpBalanced a b

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
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
N₂'' : Type u_14
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : AddCommMonoid M₂''
inst✝⁵ : AddCommMonoid N''
inst✝⁴ : AddCommMonoid N₂''
inst✝³ : Module R' M''
inst✝² : Module R' M₂''
inst✝¹ : Module R' N''
inst✝ : Module R' N₂''
e : N'' ≃ₗ[R'] N₂''
x✝¹ x✝ : M'' [⋀^ι]→ₗ[R'] N''
⊢ (↑e).compAlternatingMap (x✝¹ + x✝) = (↑e).compAlternatingMap x✝¹ + (↑e).compAlternatingMap x✝

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)
B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'
m'' : (a : ι) → M₁ a := update 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.Matrix.SemiringInverse

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

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
⊢ A.Nonsingular

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ᵀ.Nonsingular ↔ A.Nonsingular

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
A : Matrix n n R
e₁ e₂ : m ≃ n
⊢ (A.submatrix ⇑e₁ ⇑e₂).Nonsingular ↔ A.Nonsingular

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
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
s t : ℤˣ
⊢ ∀ (i : Perm n), i ∈ ofSign 1 ↔ (Equiv.mulRight (swap p q)) i ∈ ofSign (-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
A : Matrix n n R
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
s t : ℤˣ
x✝¹ : Perm n
x✝ : x✝¹ ∈ ofSign 1
⊢ ∀ (i : n), i ∈ univ ↔ (swap p q) 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
A : Matrix n n R
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
s t : ℤˣ
x✝¹ : Perm n
x✝ : x✝¹ ∈ ofSign 1
⊢ ∀ i ∈ univ, A i (x✝¹ i) = A ((swap p q) i) (((Equiv.mulRight (swap p q)) x✝¹) ((swap p q) 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_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
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
N₂'' : Type u_14
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : AddCommMonoid M₂''
inst✝⁵ : AddCommMonoid N''
inst✝⁴ : AddCommMonoid N₂''
inst✝³ : Module R' M''
inst✝² : Module R' M₂''
inst✝¹ : Module R' N''
inst✝ : Module R' N₂''
e : N'' ≃ₗ[R'] N₂''
x✝¹ : R'
x✝ : M'' [⋀^ι]→ₗ[R'] N''
⊢ (↑e).compAlternatingMap (x✝¹ • x✝) = (RingHom.id R') x✝¹ • (↑e).compAlternatingMap 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
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
N₂'' : Type u_14
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : AddCommMonoid M₂''
inst✝⁵ : AddCommMonoid N''
inst✝⁴ : AddCommMonoid N₂''
inst✝³ : Module R' M''
inst✝² : Module R' M₂''
inst✝¹ : Module R' N''
inst✝ : Module R' N₂''
e : N'' ≃ₗ[R'] N₂''
x✝ : M'' [⋀^ι]→ₗ[R'] N''
⊢ (fun f ↦ (↑e.symm).compAlternatingMap f) ((fun f ↦ (↑e).compAlternatingMap f) x✝) = 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
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
N₂'' : Type u_14
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : AddCommMonoid M₂''
inst✝⁵ : AddCommMonoid N''
inst✝⁴ : AddCommMonoid N₂''
inst✝³ : Module R' M''
inst✝² : Module R' M₂''
inst✝¹ : Module R' N''
inst✝ : Module R' N₂''
e : N'' ≃ₗ[R'] N₂''
x✝ : M'' [⋀^ι]→ₗ[R'] N₂''
⊢ (fun f ↦ (↑e).compAlternatingMap f) ((fun f ↦ (↑e.symm).compAlternatingMap f) x✝) = 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
A : Matrix n n R
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
s t : ℤˣ
⊢ detp s A = detp t 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
p q : n
hpq : p ≠ q
hcol : A.col p = A.col q
s t : ℤˣ
⊢ detp s A = detp t 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
p : n
hcol : A.col p = 0
⊢ detp s 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
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
le : Fintype.card n ≤ Fintype.card m
f g : m → n
hf : ¬Function.Injective f
p q : m
eq : f p = f q
ne : p ≠ q
⊢ (A.submatrix f g).row p = (A.submatrix f g).row q

Tactic:
by

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

Goal state before:
pp: m : Type u_2
n : Type u_3
m' : Type u_6
n' : Type u_7
R : Type u_11
A : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid A
inst✝ : Module R A
eₘ : m ≃ m'
eₙ : n ≃ n'
M : Matrix m n A
⊢ (reindexLinearEquiv R A eₘ eₙ) M = (reindex eₘ eₙ) M

Tactic:
by

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

Goal state before:
pp: m : Type u_2
m' : Type u_6
R : Type u_11
A : Type u_12
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
inst✝² : DecidableEq m
inst✝¹ : DecidableEq m'
inst✝ : One A
e : m ≃ m'
⊢ (reindexLinearEquiv R A e e) 1 = 1

Tactic:
by

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

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
m' : Type u_6
n' : Type u_7
o' : Type u_8
R : Type u_11
A : Type u_12
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : Fintype n
inst✝ : Fintype n'
eₘ : m ≃ m'
eₙ : n ≃ n'
eₒ : o ≃ o'
M : Matrix m n A
N : Matrix n o A
⊢ (reindexLinearEquiv R A eₘ eₙ) M * (reindexLinearEquiv R A eₙ eₒ) N = (reindexLinearEquiv R A eₘ eₒ) (M * N)

Tactic:
by

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
l' : Type u_5
m' : Type u_6
n' : Type u_7
o' : Type u_8
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : Fintype o
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : DecidableEq o
inst✝¹ : Semiring A
inst✝ : Algebra R A
e : m ≃ n
x✝ : R
⊢ (reindexRingEquiv A e).toFun ((algebraMap R (Matrix m m A)) x✝) = (algebraMap R (Matrix n n A)) x✝

Tactic:
by

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_11
A : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring A
inst✝ : Algebra R A
e : m ≃ n
M : Matrix m m A
⊢ (reindexAlgEquiv R A e) M = (reindex e e) M

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BrauerGroup.Defs

Goal state before:
pp: K : Type u
inst✝ : Field K
A : CSA K
B : CSA K
C : CSA K
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
iso1 : Matrix (Fin n) (Fin n) ↑A.toAlgCat ≃ₐ[K] Matrix (Fin m) (Fin m) ↑B.toAlgCat
p q : ℕ
hp : p ≠ 0
hq : q ≠ 0
iso2 : Matrix (Fin p) (Fin p) ↑B.toAlgCat ≃ₐ[K] Matrix (Fin q) (Fin q) ↑C.toAlgCat
⊢ p * n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BrauerGroup.Defs

Goal state before:
pp: K : Type u
inst✝ : Field K
A : CSA K
B : CSA K
C : CSA K
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
iso1 : Matrix (Fin n) (Fin n) ↑A.toAlgCat ≃ₐ[K] Matrix (Fin m) (Fin m) ↑B.toAlgCat
p q : ℕ
hp : p ≠ 0
hq : q ≠ 0
iso2 : Matrix (Fin p) (Fin p) ↑B.toAlgCat ≃ₐ[K] Matrix (Fin q) (Fin q) ↑C.toAlgCat
⊢ m * q ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BrauerGroup.Defs

Goal state before:
pp: K : Type u
inst✝ : Field K
A : CSA K
B : CSA K
C : CSA K
hAB : IsBrauerEquivalent A B
hBC : IsBrauerEquivalent B C
⊢ IsBrauerEquivalent A C

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
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
le : Fintype.card n ≤ Fintype.card m
f g : m → n
hf : Function.Injective f
hg : ¬Function.Injective g
p q : m
eq : g p = g q
ne : p ≠ q
⊢ (A.submatrix f g).col p = (A.submatrix f g).col q

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
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
le : Fintype.card n ≤ Fintype.card m
f g : m → n
⊢ (A.submatrix f g).IsDetpBalanced a b

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
x✝¹ x✝ : n
⊢ ∀ (i : Perm n), i ∈ {x ∈ ofSign s | x x✝ = x✝¹} ↔ (Equiv.inv (Perm n)) i ∈ {x ∈ ofSign s | x x✝¹ = 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
s : ℤˣ
A : Matrix n n R
x✝¹ x✝ : n
σ : Perm n
hσ : σ ∈ {x ∈ ofSign s | x x✝ = x✝¹}
⊢ ∀ (i : n), i ∈ {x✝}ᶜ ↔ σ i ∈ {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
s : ℤˣ
A : Matrix n n R
x✝¹ x✝ : n
σ : Perm n
hσ : σ ∈ {x ∈ ofSign s | x x✝ = x✝¹}
⊢ ∀ i ∈ {x✝}ᶜ, Aᵀ i (σ i) = A (σ i) (((Equiv.inv (Perm n)) σ) (σ 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₂
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)
B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'
m'' : (a : ι) → M₁ a := update m' i (m i)
C : update (t.piecewise (m + m') m') i (m i) = t.piecewise (m + m'') m''
s : Finset ι
hs : s ∈ t.powerset
⊢ (insert i s).piecewise m m' = s.piecewise m m''

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ Quot.mk (⇑(colimitSetoid F)) x * Quot.mk (⇑(colimitSetoid F)) y * Quot.mk (⇑(colimitSetoid F)) z =
    Quot.mk (⇑(colimitSetoid F)) x * (Quot.mk (⇑(colimitSetoid F)) y * Quot.mk (⇑(colimitSetoid F)) z)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ Quot.mk (⇑(colimitSetoid F)) x * (Quot.mk (⇑(colimitSetoid F)) y + Quot.mk (⇑(colimitSetoid F)) z) =
    Quot.mk (⇑(colimitSetoid F)) x * Quot.mk (⇑(colimitSetoid F)) y +
      Quot.mk (⇑(colimitSetoid F)) x * Quot.mk (⇑(colimitSetoid F)) z

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 m' : (i : ι) → M₁ i
t : Finset ι
⊢ f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ (Quot.mk (⇑(colimitSetoid F)) x + Quot.mk (⇑(colimitSetoid F)) y) * Quot.mk (⇑(colimitSetoid F)) z =
    Quot.mk (⇑(colimitSetoid F)) x * Quot.mk (⇑(colimitSetoid F)) z +
      Quot.mk (⇑(colimitSetoid F)) y * Quot.mk (⇑(colimitSetoid F)) z

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 ι
inst✝ : Fintype ι
m m' : (i : ι) → M₁ i
⊢ f (m + m') = ∑ s, f (s.piecewise m m')

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j : J
⊢ coconeFun F j 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j : J
⊢ ∀ (x y : ↑(F.1 j)), coconeFun F j (x * y) = coconeFun F j x * coconeFun F j y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j : J
⊢ coconeFun F j 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j : J
⊢ ∀ (x y : ↑(F.1 j)), coconeFun F j (x + y) = coconeFun F j x + coconeFun F j y

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 (Option n) (Option n) R
i : Option n
σ : Perm (Option n)
x✝ : sign σ = s ∧ σ none = i
⊢ sign (removeNone σ) = sign (swap none i) * s ∧ decomposeOption.symm (i, removeNone σ) = σ

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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∃ i, A i = ∅
i : ι
hi : A i = ∅
⊢ ∑ j ∈ A i, g i j = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ coconeMorphism F j' = coconeMorphism F j

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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∃ i, A i = ∅
i : ι
hi : ∑ j ∈ A i, g i j = 0
⊢ piFinset 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 (Option n) (Option n) R
i : Option n
σ : Perm (Option n)
⊢ (∃ a, sign a = sign (swap none i) * s ∧ decomposeOption.symm (i, a) = σ) → sign σ = s ∧ σ none = i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom (coconeMorphism F j')) ((ConcreteCategory.hom (F.map f)) x) =
    (ConcreteCategory.hom (coconeMorphism F j)) x

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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
Ai_singleton : ∀ (i : ι), #(A i) ≤ 1
i : ι
⊢ #(A i) ≠ 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₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
Ai_singleton : ∀ (i : ι), #(A i) ≤ 1
⊢ ∀ (i : ι), #(A 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 (Option n) (Option n) R
i : Option n
⊢ adjp s A i none = detp (sign (swap none i) * s) (A.submatrix some (⇑(swap none i) ∘ some))

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 (Option n) (Option n) R
⊢ adjp s A none none = detp s (A.submatrix some some)

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 : ℤˣ
i : n
A : Matrix (Option n) (Option n) R
⊢ adjp s A (some i) none = detp (-s) (A.submatrix some (Function.update some i none))

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 : ℤˣ
i : n
A : Matrix (Option n) (Option n) R
⊢ adjp s A none (some i) = detp (-s) (A.submatrix (Function.update some i none) some)

Tactic:
by

Goal state after: