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
s : ℤˣ
A : Matrix n n R
σ : Perm n
x✝ : σ ∈ ofSign s
⊢ ∀ (i : n), i ∈ univ ↔ σ i ∈ univ

Tactic:
simp

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:
simp

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
⊢ ∏ k, diagonal d k (1 k) = ∏ i, d i

Tactic:
simp

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
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := ⋯
h : g i • v i = -∑ x ∈ s.erase i, g x • v x
⊢ ∀ x ∈ s.erase i, f (update v i (g x • v x)) = 0

Tactic:
intro j

Goal state after:
ι : 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
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
h : g i • v i = -∑ x ∈ s.erase i, g x • v x
j : ι
⊢ j ∈ s.erase i → f (update v i (g j • v j)) = 0
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
⊢ ∏ k, A k (default k) = 1

Tactic:
simp

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
⊢ 1 ∈ ofSign 1

Tactic:
simp

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

Tactic:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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''
x✝ : ι → M''
⊢ ((↑e).compAlternatingMap (x✝² + x✝¹)) x✝ = ((↑e).compAlternatingMap x✝² + (↑e).compAlternatingMap x✝¹) x✝

Tactic:
simp

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:
simp

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''
x✝ : ι → M''
⊢ ((↑e).compAlternatingMap (x✝² • x✝¹)) x✝ = ((RingHom.id R') x✝² • (↑e).compAlternatingMap x✝¹) x✝

Tactic:
simp

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''
x✝ : ι → M''
⊢ ((fun f ↦ (↑e.symm).compAlternatingMap f) ((fun f ↦ (↑e).compAlternatingMap f) x✝¹)) x✝ = x✝¹ x✝

Tactic:
simp

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₂''
x✝ : ι → M''
⊢ ((fun f ↦ (↑e).compAlternatingMap f) ((fun f ↦ (↑e.symm).compAlternatingMap f) x✝¹)) x✝ = x✝¹ x✝

Tactic:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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

Goal state before:
pp: case e_s
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
⊢ sign (swap none (some i)) * s = -s

Tactic:
simp

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
Ai_card : ∀ (i : ι), #(A i) = 1
r : (i : ι) → α i
hr : r ∈ piFinset A
i : ι
⊢ ∀ j ∈ A i, g i j = g i (r i)

Tactic:
intro j

Goal state after:
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
Ai_card : ∀ (i : ι), #(A i) = 1
r : (i : ι) → α i
hr : r ∈ piFinset A
i : ι
j : α i
⊢ j ∈ A i → g i j = g i (r i)
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x : ↑(colimitCocone F).pt
⊢ (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) zero) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) zero)

Tactic:
simp

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

Goal state before:
pp: case one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x : ↑(colimitCocone F).pt
⊢ (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) one) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) one)

Tactic:
simp

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

Goal state before:
pp: case zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x : ↑(colimitCocone F).pt
⊢ (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) zero) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) zero)

Tactic:
simp

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

Goal state before:
pp: case one
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x : ↑(colimitCocone F).pt
⊢ (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) one) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) one)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_1
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
hσ : σ ∈ ofSign 1
⊢ 1 • ∏ i, M (σ⁻¹ (σ i)) (σ i) = ∏ k, M k (σ k)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_2
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
hσ : σ ∈ ofSign (-1)
⊢ -1 • ∏ i, M (σ⁻¹ (σ i)) (σ i) = -∏ k, M k (σ k)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFiltered C
⊢ ∀ {X : C}, X ∈ ∅ → Nonempty (X ⟶ Classical.choice ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_2
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
⊢ 1 ∉ univ → ↑↑(sign 1) * ∏ i, diagonal d (1 i) i = 0

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_3
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
⊢ ↑↑(sign 1) * ∏ i, diagonal d (1 i) i = ∏ i, d i

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M N : Matrix n n R
σ : Perm n
x✝ : σ ∈ univ
τ : Perm n
⊢ ∏ i, M (τ (σ⁻¹ i)) (σ (σ⁻¹ i)) = ∏ j, M ((τ * σ⁻¹) j) j

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case e_a
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
⊢ ∀ (x : n), Mᵀ (σ x) x = M (σ⁻¹ (σ x)) (σ x)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X ↦
    Finset.univ.biUnion fun Y ↦ Finset.image (fun f ↦ ⟨F.obj X, ⟨F.obj Y, ⟨⋯, ⟨⋯, F.map f⟩⟩⟩⟩) Finset.univ
Z : C
f : {X : C} → X ∈ O → (X ⟶ Z)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f_1 ≫ f mY = f mX
⊢ ∀ ⦃X Y : J⦄ (f_1 : X ⟶ Y), F.map f_1 ≫ f ⋯ = f ⋯ ≫ ((Functor.const J).obj Z).map f_1

Tactic:
intro j

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X ↦
    Finset.univ.biUnion fun Y ↦ Finset.image (fun f ↦ ⟨F.obj X, ⟨F.obj Y, ⟨⋯, ⟨⋯, F.map f⟩⟩⟩⟩) Finset.univ
Z : C
f : {X : C} → X ∈ O → (X ⟶ Z)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f_1 ≫ f mY = f mX
j : J
⊢ ∀ ⦃Y : J⦄ (f_1 : j ⟶ Y), F.map f_1 ≫ f ⋯ = f ⋯ ≫ ((Functor.const J).obj Z).map f_1
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X ↦
    Finset.univ.biUnion fun Y ↦ Finset.image (fun f ↦ ⟨F.obj X, ⟨F.obj Y, ⟨⋯, ⟨⋯, F.map f⟩⟩⟩⟩) Finset.univ
Z : C
f : {X : C} → X ∈ O → (X ⟶ Z)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f_1 ≫ f mY = f mX
j j' : J
g : j ⟶ j'
⊢ ⟨F.obj j', ⟨⋯, ⟨⋯, F.map g⟩⟩⟩ ≍ ⟨F.obj j', ⟨⋯, ⟨⋯, F.map g⟩⟩⟩

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type u_3
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
x✝ : n
⊢ e₂ x✝ = (e₁.trans (e₁.symm.trans e₂)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
e e' : m ≃ n
M : Matrix m m R
i✝ j✝ : n
⊢ (reindex e e') M i✝ j✝ = (reindex e' e') ((reindex (e.trans e'.symm) (Equiv.refl m)) M) i✝ j✝

Tactic:
simp

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
⊢ detp s A =
    A none none * detp s (A.submatrix some some) +
      ∑ k, A none (some k) * detp (-s) (A.submatrix some (Function.update some k none))

Tactic:
by
  simp_rw [← A.mul_adjp_apply_eq s none, mul_apply,
    Fintype.sum_option, adjp_none_none, adjp_some_none]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
c : R
⊢ (diagonal fun x ↦ c).det * A.det = c ^ Fintype.card n * A.det

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsFilteredOrEmpty C
ι : Type u_1
inst✝ : Finite ι
k₁ k₂ : C
j : PEmpty.{u_1 + 1} → C
f : (i : PEmpty.{u_1 + 1}) → j i ⟶ k₁
g : (i : PEmpty.{u_1 + 1}) → j i ⟶ k₂
⊢ ∀ (i : PEmpty.{u_1 + 1}), f i ≫ leftToMax k₁ k₂ = g i ≫ rightToMax k₁ k₂

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case insert
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
c : n → R
a : R
k : n
s✝ : Finset n
hk : k ∉ s✝
h_ind : j ∉ s✝ → (M.updateRow j (a • M j + ∑ k ∈ s✝, c k • M k)).det = a • M.det
hj : j ∉ insert k s✝
h : k ≠ j
⊢ (M.updateRow j (a • M j + ∑ k ∈ insert k s✝, c k • M k)).det = a • M.det

Tactic:
rw [Finset.sum_insert hk, add_comm ((c k) • M k), ← add_assoc, det_updateRow_add,
        det_updateRow_smul, det_updateRow_eq_zero h, mul_zero, add_zero, h_ind]

Goal state after:
case insert
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
c : n → R
a : R
k : n
s✝ : Finset n
hk : k ∉ s✝
h_ind : j ∉ s✝ → (M.updateRow j (a • M j + ∑ k ∈ s✝, c k • M k)).det = a • M.det
hj : j ∉ insert k s✝
h : k ≠ j
⊢ j ∉ s✝
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsFilteredOrEmpty C
I : Type u_1
inst✝ : Finite I
i : C
j : I → C
f : (x : I) → i ⟶ j x
this : IsFiltered C
val✝ : Fintype I
x : I
⊢ i ∈ insert i (Finset.image j Finset.univ)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsFilteredOrEmpty C
I : Type u_1
inst✝ : Finite I
i : C
j : I → C
f : (x : I) → i ⟶ j x
this : IsFiltered C
val✝ : Fintype I
x : I
⊢ j x ∈ insert i (Finset.image j Finset.univ)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofiltered C
⊢ ∀ {X : C}, X ∈ ∅ → Nonempty (Classical.choice ⋯ ⟶ X)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X ↦
    Finset.univ.biUnion fun Y ↦ Finset.image (fun f ↦ ⟨F.obj X, ⟨F.obj Y, ⟨⋯, ⟨⋯, F.map f⟩⟩⟩⟩) Finset.univ
Z : C
f : {X : C} → X ∈ O → (Z ⟶ X)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f mX ≫ f_1 = f mY
⊢ ∀ ⦃X Y : J⦄ (f_1 : X ⟶ Y), ((Functor.const J).obj Z).map f_1 ≫ f ⋯ = f ⋯ ≫ F.map f_1

Tactic:
intro j

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsCofiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X ↦
    Finset.univ.biUnion fun Y ↦ Finset.image (fun f ↦ ⟨F.obj X, ⟨F.obj Y, ⟨⋯, ⟨⋯, F.map f⟩⟩⟩⟩) Finset.univ
Z : C
f : {X : C} → X ∈ O → (Z ⟶ X)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f mX ≫ f_1 = f mY
j : J
⊢ ∀ ⦃Y : J⦄ (f_1 : j ⟶ Y), ((Functor.const J).obj Z).map f_1 ≫ f ⋯ = f ⋯ ≫ F.map f_1