mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix n n R
s : R
hA : A.IsHadamard
hcard : IsRegular ↑(Fintype.card n)
hcol : ∀ (j : n), ∑ i, A i j = s
hvcol : 1 ᵥ* A = s • 1
hconjcol : Aᴴ *ᵥ 1 = star s • 1
⊢ Fintype.card n • (1 ᵥ* 1 ⬝ᵥ 1) = ↑(Fintype.card n) ^ 2

Tactic:
]

Goal state after:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix n n R
s : R
hA : A.IsHadamard
hcard : IsRegular ↑(Fintype.card n)
hcol : ∀ (j : n), ∑ i, A i j = s
hvcol : 1 ᵥ* A = s • 1
hconjcol : Aᴴ *ᵥ 1 = star s • 1
⊢ Fintype.card n • (1 ᵥ* 1 ⬝ᵥ 1) = ↑(Fintype.card n) ^ 2
Module: Mathlib.LinearAlgebra.Matrix.Gershgorin

Goal state before:
pp: K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h✝ : A.det = 0
this : ∃ k, 0 ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.univ.erase k, ‖A k j‖)
a : n
h : ‖A a a‖ ≤ ∑ j ∈ Finset.univ.erase a, ‖A a j‖
⊢ ‖A a a‖ ≤ ∑ j ∈ Finset.univ.erase a, ‖A a j‖

Tactic:
]

Goal state after:
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h✝ : A.det = 0
this : ∃ k, 0 ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.univ.erase k, ‖A k j‖)
a : n
h : ‖A a a‖ ≤ ∑ j ∈ Finset.univ.erase a, ‖A a j‖
⊢ ‖A a a‖ ≤ ∑ j ∈ Finset.univ.erase a, ‖A a j‖
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix n n R
s : R
hA : A.IsHadamard
hcard : IsRegular ↑(Fintype.card n)
hcol : ∀ (j : n), ∑ i, A i j = s
hvcol : 1 ᵥ* A = s • 1
hconjcol : Aᴴ *ᵥ 1 = star s • 1
hleft : 1 ᵥ* (A * Aᴴ) ⬝ᵥ 1 = ↑(Fintype.card n) ^ 2
⊢ s • 1 ⬝ᵥ star s • 1 = ↑(Fintype.card n) * (s * star s)

Tactic:
]

Goal state after:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix n n R
s : R
hA : A.IsHadamard
hcard : IsRegular ↑(Fintype.card n)
hcol : ∀ (j : n), ∑ i, A i j = s
hvcol : 1 ᵥ* A = s • 1
hconjcol : Aᴴ *ᵥ 1 = star s • 1
hleft : 1 ᵥ* (A * Aᴴ) ⬝ᵥ 1 = ↑(Fintype.card n) ^ 2
⊢ s • 1 ⬝ᵥ star s • 1 = ↑(Fintype.card n) * (s * star s)
Module: Mathlib.LinearAlgebra.Matrix.Gershgorin

Goal state before:
pp: K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : A.det = 0
⊢ ⊥ ≠ (Matrix.toLin' A).ker

Tactic:
]

Goal state after:
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : A.det = 0
⊢ ⊥ ≠ (Matrix.toLin' A).ker
Module: Mathlib.LinearAlgebra.Matrix.Gershgorin

Goal state before:
pp: K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : A.det = 0
⊢ A.det = 0

Tactic:
]

Goal state after:
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : A.det = 0
⊢ A.det = 0
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
⊢ ↑(Fintype.card n) • 1 = ↑(Fintype.card n) • 1

Tactic:
]

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

Goal state before:
pp: K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ i ∈ Finset.univ.erase k, ‖A i k‖ < ‖A k k‖
⊢ A.transpose.det ≠ 0

Tactic:
]

Goal state after:
K : Type u_1
n : Type u_2
inst✝² : NormedField K
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n K
h : ∀ (k : n), ∑ i ∈ Finset.univ.erase k, ‖A i k‖ < ‖A k k‖
⊢ A.transpose.det ≠ 0
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
this : A.det * star A.det = ↑(Fintype.card n) ^ Fintype.card n
⊢ A.det * star A.det = ↑(Fintype.card n) ^ Fintype.card n

Tactic:
]

Goal state after:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
this : A.det * star A.det = ↑(Fintype.card n) ^ Fintype.card n
⊢ A.det * star A.det = ↑(Fintype.card n) ^ Fintype.card n
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
⊢ ↑(Fintype.card n) ^ Fintype.card n = ↑(Fintype.card n) ^ Fintype.card n

Tactic:
]

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

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : StarRing R
A : Matrix n n R
inst✝ : IsReduced R
hA : A.IsHadamard
hcard : ↑(Fintype.card n) ≠ 0
h : A.det = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
h_nonneg : ∀ (i j : n), 0 ≤ A i j
k : ℕ
hk_pos : k > 0
hk_all : ∀ (i j : n), 0 < (A ^ k) i j
⊢ ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j

Tactic:
]

Goal state after:
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
h_nonneg : ∀ (i j : n), 0 ≤ A i j
k : ℕ
hk_pos : k > 0
hk_all : ∀ (i j : n), 0 < (A ^ k) i j
⊢ ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
hcard : IsRegular ↑(Fintype.card n)
⊢ IsRegular (↑(Fintype.card n) ^ Fintype.card n)

Tactic:
]

Goal state after:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : StarRing R
A : Matrix n n R
hA : A.IsHadamard
hcard : IsRegular ↑(Fintype.card n)
⊢ IsRegular (↑(Fintype.card n) ^ Fintype.card n)
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: case inl
α : Type u_1
n : Type u_4
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i : n
⊢ A i i = A i i

Tactic:
]

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

Goal state before:
pp: case inr
α : Type u_1
n : Type u_4
inst✝¹ : Zero α
inst✝ : DecidableEq n
A : Matrix n n α
h : A.IsDiag
i j : n
hij : i ≠ j
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case step
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A✝ : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → 0 < ↑A 0 0 → 0 ≤ ↑A 0 1 → |↑A 0 1| < |↑A 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A✝)
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 ≠ 0
ih : C (reduce (reduceStep A)) → C (reduceStep A)
hA : C (reduce (reduceStep A))
⊢ C A

Tactic:
]

Goal state after:
case step
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A✝ : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → 0 < ↑A 0 0 → 0 ≤ ↑A 0 1 → |↑A 0 1| < |↑A 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A✝)
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 ≠ 0
ih : C (reduce (reduceStep A)) → C (reduceStep A)
hA : C (reduce (reduceStep A))
⊢ C A
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: case pos
α : Type u_1
n : Type u_4
inst✝ : Zero α
A : Matrix n n α
h : A.IsDiag
i j : n
g : i = j
⊢ A j j = A j j

Tactic:
]

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

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : StarRing R
A : Matrix n n R
hentry : ∀ (i j : n), A i j ∈ unitary R
hmul : A * Aᴴ = ↑(Fintype.card n) • 1
hcard : IsRegular ↑(Fintype.card n)
this : A.det * star A.det = ↑(Fintype.card n) ^ Fintype.card n
⊢ IsRegular (A.det * star A.det)

Tactic:
]

Goal state after:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : StarRing R
A : Matrix n n R
hentry : ∀ (i j : n), A i j ∈ unitary R
hmul : A * Aᴴ = ↑(Fintype.card n) • 1
hcard : IsRegular ↑(Fintype.card n)
this : A.det * star A.det = ↑(Fintype.card n) ^ Fintype.card n
⊢ IsRegular (A.det * star A.det)
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA_nonneg : ∀ (i j : n), 0 ≤ A i j
h : Aᵀ.IsIrreducible
i j : n
⊢ 0 ≤ Aᵀ i j

Tactic:
simpa [Matrix.transpose_apply] using hA_nonneg j i

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA_nonneg : ¬∀ (i j : n), 0 ≤ A i j
⊢ ¬((∀ (i j : n), 0 ≤ Aᵀ i j) ∧ IsSStronglyConnected n)

Tactic:
]

Goal state after:
n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA_nonneg : ¬∀ (i j : n), 0 ≤ A i j
⊢ ¬((∀ (i j : n), 0 ≤ Aᵀ i j) ∧ IsSStronglyConnected n)
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : StarRing R
A : Matrix n n R
hentry : ∀ (i j : n), A i j ∈ unitary R
hmul : A * Aᴴ = ↑(Fintype.card n) • 1
hcard : IsRegular ↑(Fintype.card n)
this : A.det * star A.det = ↑(Fintype.card n) ^ Fintype.card n
⊢ IsRegular (↑(Fintype.card n) ^ Fintype.card n)

Tactic:
]

Goal state after:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : StarRing R
A : Matrix n n R
hentry : ∀ (i j : n), A i j ∈ unitary R
hmul : A * Aᴴ = ↑(Fintype.card n) • 1
hcard : IsRegular ↑(Fintype.card n)
this : A.det * star A.det = ↑(Fintype.card n) ^ Fintype.card n
⊢ IsRegular (↑(Fintype.card n) ^ Fintype.card n)
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA_nonneg : ¬∀ (i j : n), 0 ≤ A i j
this : ¬Aᵀ.IsIrreducible
⊢ ¬((∀ (i j : n), 0 ≤ A i j) ∧ IsSStronglyConnected n)

Tactic:
]

Goal state after:
n : Type u_1
R : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrder R
A : Matrix n n R
hA_nonneg : ¬∀ (i j : n), 0 ≤ A i j
this : ¬Aᵀ.IsIrreducible
⊢ ¬((∀ (i j : n), 0 ≤ A i j) ∧ IsSStronglyConnected n)
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: ⊢ ∀ (x : SL(2, ℤ)), x ∈ closure {S, T}

Tactic:
]

Goal state after:
⊢ ∀ (x : SL(2, ℤ)), x ∈ closure {S, T}
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: case h0
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : ↑A 1 0 = 0
a4 : 0 < ↑A 0 0
a✝ : 0 ≤ ↑A 0 1
a6 : |↑A 0 1| < |↑A 1 1|
⊢ 1 ∈ closure {S, T}

Tactic:
]

Goal state after:
case h0
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : ↑A 1 0 = 0
a4 : 0 < ↑A 0 0
a✝ : 0 ≤ ↑A 0 1
a6 : |↑A 0 1| < |↑A 1 1|
⊢ 1 ∈ closure {S, T}
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : StarRing R
A : Matrix n n R
hentry : ∀ (i j : n), A i j ∈ unitary R
hmul : A * Aᴴ = ↑(Fintype.card n) • 1
hcard : IsRegular ↑(Fintype.card n)
hdet : IsRegular (A.det * star A.det)
hreg : IsLeftRegular A
⊢ ↑(Fintype.card n) • A = ↑(Fintype.card n) • A

Tactic:
]

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

Goal state before:
pp: α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
h : (Matrix.fromBlocks A 0 C D).IsSymm
ha : A.IsDiag
hd : D.IsDiag
⊢ (Matrix.fromBlocks A 0 0ᵀ D).IsDiag

Tactic:
]

Goal state after:
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
h : (Matrix.fromBlocks A 0 C D).IsSymm
ha : A.IsDiag
hd : D.IsDiag
⊢ (Matrix.fromBlocks A 0 0ᵀ D).IsDiag
Module: Mathlib.LinearAlgebra.Matrix.Module

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : Fintype ι
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
N₁ N₂ : Matrix ι ι R
v : ι → M
i : ι
⊢ ∑ y, ∑ x, N₁ i y • N₂ y x • v x = ∑ x, ∑ x_1, N₁ i x • N₂ x x_1 • v x_1

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
r : R
v : ι → M
i' : ι
⊢ single i j r i' j • v j = Pi.single i (r • v j) i'

pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
r : R
v : ι → M
i' j' : ι
hj : j' ≠ j
⊢ single i j r i' j' • v j' = 0

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
r : R
v : ι → M
i' : ι
⊢ single i j r i' j • v j = Pi.single i (r • v j) i'

ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : Ring R
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
r : R
v : ι → M
i' j' : ι
hj : j' ≠ j
⊢ single i j r i' j' • v j' = 0
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℤ
hA : A.IsHadamard
hcard : 2 < Fintype.card n
hpm : ∀ (i j : n), A i j = 1 ∨ A i j = -1
r s t : n
hrs : r ≠ s
hrt : r ≠ t
hst : s ≠ t
horth : ∀ ⦃i k : n⦄, i ≠ k → ∑ j, A i j * A k j = 0
hexpand : ∀ (j : n), (1 + A s j * A r j) * (1 + A t j * A r j) = 1 + A s j * A r j + A t j * A r j + A s j * A t j
hdvd : ∀ (j : n), 4 ∣ (1 + A s j * A r j) * (1 + A t j * A r j)
hsum : ∑ j, (1 + A s j * A r j) * (1 + A t j * A r j) = ↑(Fintype.card n)
⊢ ↑4 ∣ ∑ j, (1 + A s j * A r j) * (1 + A t j * A r j)

Tactic:
]

Goal state after:
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℤ
hA : A.IsHadamard
hcard : 2 < Fintype.card n
hpm : ∀ (i j : n), A i j = 1 ∨ A i j = -1
r s t : n
hrs : r ≠ s
hrt : r ≠ t
hst : s ≠ t
horth : ∀ ⦃i k : n⦄, i ≠ k → ∑ j, A i j * A k j = 0
hexpand : ∀ (j : n), (1 + A s j * A r j) * (1 + A t j * A r j) = 1 + A s j * A r j + A t j * A r j + A s j * A t j
hdvd : ∀ (j : n), 4 ∣ (1 + A s j * A r j) * (1 + A t j * A r j)
hsum : ∑ j, (1 + A s j * A r j) * (1 + A t j * A r j) = ↑(Fintype.card n)
⊢ ↑4 ∣ ∑ j, (1 + A s j * A r j) * (1 + A t j * A r j)
Module: Mathlib.LinearAlgebra.Matrix.Swap

Goal state before:
pp: R : Type u_1
n : Type u_2
m : Type u_3
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
a : m
g : Matrix n m R
⊢ g i a = g i a

Tactic:
]

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

Goal state before:
pp: R : Type u_1
n : Type u_2
m : Type u_3
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
a : m
g : Matrix m n R
⊢ g a i = g a i

Tactic:
]

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
⊢ Equiv.Perm.permMatrix R (Equiv.symm (Equiv.swap i j)) * Equiv.Perm.permMatrix R (Equiv.symm (Equiv.swap i j)) = 1

Tactic:
]

Goal state after:
R : Type u_1
n : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
⊢ Equiv.Perm.permMatrix R (Equiv.symm (Equiv.swap i j)) * Equiv.Perm.permMatrix R (Equiv.symm (Equiv.swap i j)) = 1
Module: Mathlib.LinearAlgebra.Matrix.Permanent

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
⊢ (diagonal fun x ↦ 1).permanent = 1

Tactic:
]

Goal state after:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
⊢ (diagonal fun x ↦ 1).permanent = 1
Module: Mathlib.LinearAlgebra.Matrix.Permanent

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
σ : Perm n
M : Matrix n n R
⊢ M.permanent = M.permanent

Tactic:
]

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

Goal state before:
pp: case e_f
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
c : R
x✝ : Perm n
⊢ ∏ x, c * M (x✝ x) x = (∏ i, M (x✝ i) i) * c ^ Fintype.card n

Tactic:
]

Goal state after:
case e_f
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
c : R
x✝ : Perm n
⊢ ∏ x, c * M (x✝ x) x = (∏ i, M (x✝ i) i) * c ^ Fintype.card n
Module: Mathlib.LinearAlgebra.Matrix.Permanent

Goal state before:
pp: case e_f
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
p : Perm n
⊢ c * u (p j) * (univ.erase j).prod ?m.57 = c * u (p j) * ∏ i ∈ univ.erase j, M.updateCol j u (p i) i

pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
p : Perm n
⊢ n → R

pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
p : Perm n
i : n
hi : i ∈ univ.erase j
⊢ M.updateCol j (c • u) (p i) i = ?m.57 i

Tactic:
]

Goal state after:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
p : Perm n
i : n
hi : i ∈ univ.erase j
⊢ M.updateCol j (c • u) (p i) i = M.updateCol j u (p i) i
Module: Mathlib.LinearAlgebra.Matrix.Permanent

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
⊢ c * (M.updateRow j u).permanent = c * (M.updateRow j u).permanent

Tactic:
]

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

Goal state before:
pp: n : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix n n R
⊢ A.det ≠ 0 ↔ A.det ≠ 0

Tactic:
]

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

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : Module R N
inst✝² : Finite ι
inst✝¹ : ∀ (i : ι), Finite (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    (f.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)) = g.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
this✝ : (i : ι) → Fintype (κ i)
this : DecidableEq ι
⊢ (f fun i ↦ (fun i ↦ ∑ i_1, Pi.single i_1 (x i i_1)) i) = g fun i ↦ (fun i ↦ ∑ i_1, Pi.single i_1 (x i i_1)) i

Tactic:
]

Goal state after:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : Module R N
inst✝² : Finite ι
inst✝¹ : ∀ (i : ι), Finite (κ i)
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ (j : κ i) → M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    (f.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)) = g.compLinearMap fun i ↦ LinearMap.single R (M i) (p i)
x : (i : ι) → (j : κ i) → M i j
i : Fintype ι
this✝ : (i : ι) → Fintype (κ i)
this : DecidableEq ι
⊢ (f fun i ↦ (fun i ↦ ∑ i_1, Pi.single i_1 (x i i_1)) i) = g fun i ↦ (fun i ↦ ∑ i_1, Pi.single i_1 (x i i_1)) i
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
ind : LinearIndependent R A.col
a b : R
bal : A.IsDetpBalanced a b
P : ℕ → Prop := fun r ↦ ∀ (f g : Fin r → n), (A.submatrix f g).IsDetpBalanced a b
r : ℕ
x✝¹ : r < Fintype.card n
x✝ : 0 ≤ r
ih : P (r + 1)
f g : Fin r → n
hg : ¬Function.Surjective g
j₀ : n
h₀ : ∀ (x : Fin r), ¬g x = j₀
D : Matrix (Fin r) (Fin r) R := A.submatrix f g
Aj : Fin r → Matrix (Fin r) (Fin r) R := fun j ↦ A.submatrix f (Function.update g j j₀)
v : R → R → n →₀ R :=
  fun a b ↦
    ∑ j, Finsupp.single (g j) (a * detp (-1) (Aj j) + b * detp 1 (Aj j)) +
      Finsupp.single j₀ (a * detp 1 D + b * detp (-1) D)
i : n
Ai : Matrix (Option (Fin r)) (Option (Fin r)) R := A.submatrix (fun t ↦ Option.rec i f t) fun t ↦ Option.rec j₀ g t
s : ℤˣ
⊢ ∑ k, Ai none (some k) * detp (-s) (Ai.submatrix some (Function.update some k none)) +
      Ai none none * detp s (Ai.submatrix some some) =
    ∑ x, A.col (g x) i * detp (-s) (Aj x) + A.col j₀ i * detp s D

Tactic:
]

Goal state after:
R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
ind : LinearIndependent R A.col
a b : R
bal : A.IsDetpBalanced a b
P : ℕ → Prop := fun r ↦ ∀ (f g : Fin r → n), (A.submatrix f g).IsDetpBalanced a b
r : ℕ
x✝¹ : r < Fintype.card n
x✝ : 0 ≤ r
ih : P (r + 1)
f g : Fin r → n
hg : ¬Function.Surjective g
j₀ : n
h₀ : ∀ (x : Fin r), ¬g x = j₀
D : Matrix (Fin r) (Fin r) R := A.submatrix f g
Aj : Fin r → Matrix (Fin r) (Fin r) R := fun j ↦ A.submatrix f (Function.update g j j₀)
v : R → R → n →₀ R :=
  fun a b ↦
    ∑ j, Finsupp.single (g j) (a * detp (-1) (Aj j) + b * detp 1 (Aj j)) +
      Finsupp.single j₀ (a * detp 1 D + b * detp (-1) D)
i : n
Ai : Matrix (Option (Fin r)) (Option (Fin r)) R := A.submatrix (fun t ↦ Option.rec i f t) fun t ↦ Option.rec j₀ g t
s : ℤˣ
⊢ ∑ k, Ai none (some k) * detp (-s) (Ai.submatrix some (Function.update some k none)) +
      Ai none none * detp s (Ai.submatrix some some) =
    ∑ x, A.col (g x) i * detp (-s) (Aj x) + A.col j₀ i * detp s D
Module: Mathlib.LinearAlgebra.Multilinear.Pi

Goal state before:
pp: case inr
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁴ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝³ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝² : (p : (i : ι) → κ i) → Module R (N p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
hpq : p ≠ q
⊢ (piFamily f) (fun i ↦ Pi.single (p i) (m i)) q = 0

Tactic:
]

Goal state after:
case inr
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁴ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝³ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝² : (p : (i : ι) → κ i) → Module R (N p)
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
q : (i : ι) → κ i
hpq : p ≠ q
⊢ (piFamily f) (fun i ↦ Pi.single (p i) (m i)) q = 0
Module: Mathlib.LinearAlgebra.Matrix.Nonsingular

Goal state before:
pp: R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
h : IsLeftRegular A
⊢ IsLeftRegular A

Tactic:
]

Goal state after:
R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
h : IsLeftRegular A
⊢ IsLeftRegular A