mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝³ : Finite ι'
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
this✝ : Fintype ι' := Fintype.ofFinite ι'
I : Set (ι' → K) := ⋯.extend ⋯
b : Module.Basis (↑I) K (ι' → K) := Module.Basis.extend ⋯
b' : Module.Basis (↑I) L (ι' → L) := (Module.Basis.baseChange L b).map (piScalarRight K L L ι')
v' : ι → ↑I := fun i ↦ ⟨v i, ⋯⟩
hv' : ⇑b' ∘ v' = fun i ↦ ⇑(algebraMap K L) ∘ v i
i j : ι
hij : v' i = v' j
this : Injective v
⊢ i = j

Tactic:
;

Goal state after:
ι : Type u_1
ι' : Type u_2
inst✝³ : Finite ι'
K : Type u_3
L : Type u_4
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
this✝ : Fintype ι' := Fintype.ofFinite ι'
I : Set (ι' → K) := ⋯.extend ⋯
b : Module.Basis (↑I) K (ι' → K) := Module.Basis.extend ⋯
b' : Module.Basis (↑I) L (ι' → L) := (Module.Basis.baseChange L b).map (piScalarRight K L L ι')
v' : ι → ↑I := fun i ↦ ⟨v i, ⋯⟩
hv' : ⇑b' ∘ v' = fun i ↦ ⇑(algebraMap K L) ∘ v i
i j : ι
hij : v' i = v' j
this : Injective v
⊢ i = j
Module: Mathlib.LinearAlgebra.Matrix.AbsoluteValue

Goal state before:
pp: case h1
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : CommRing S
inst✝³ : LinearOrder S
inst✝² : IsStrictOrderedRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (i j : n), abv (A i j) ≤ x
σ : Perm n
a✝¹ : σ ∈ univ
i : n
a✝ : i ∈ univ
⊢ abv (A (σ i) i) ≤ x

Tactic:
;

Goal state after:
case h1
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : CommRing S
inst✝³ : LinearOrder S
inst✝² : IsStrictOrderedRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (i j : n), abv (A i j) ≤ x
σ : Perm n
a✝¹ : σ ∈ univ
i : n
a✝ : i ∈ univ
⊢ abv (A (σ i) i) ≤ x
Module: Mathlib.LinearAlgebra.Matrix.AbsoluteValue

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : CommRing S
inst✝³ : LinearOrder S
inst✝² : IsStrictOrderedRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
ι : Type u_4
s : Finset ι
A : ι → Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (k : ι) (i j : n), abv (A k i j) ≤ x
i j : n
k : ι
a✝ : k ∈ s
⊢ abv (A k i j) ≤ x

Tactic:
;

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : CommRing S
inst✝³ : LinearOrder S
inst✝² : IsStrictOrderedRing S
n : Type u_3
inst✝¹ : Fintype n
inst✝ : DecidableEq n
ι : Type u_4
s : Finset ι
A : ι → Matrix n n R
abv : AbsoluteValue R S
x : S
hx : ∀ (k : ι) (i j : n), abv (A k i j) ≤ x
i j : n
k : ι
a✝ : k ∈ s
⊢ abv (A k i j) ≤ x
Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v✝ : ι → ι' → R
h : LinearIndependent R v✝
this : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
v : ι' → R
hv : v ∈ (Pi.algebraMap ι' R K).ker
⊢ v = 0

Tactic:
;

Goal state after:
ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v✝ : ι → ι' → R
h : LinearIndependent R v✝
this : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
v : ι' → R
hv : v ∈ (Pi.algebraMap ι' R K).ker
⊢ v = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v✝ : ι → ι' → R
h : LinearIndependent R v✝
this : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
v : ι' → R
hv : v ∈ (Pi.algebraMap ι' R K).ker
i : ι'
⊢ v i = 0 i

Tactic:
;

Goal state after:
ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v✝ : ι → ι' → R
h : LinearIndependent R v✝
this : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
v : ι' → R
hv : v ∈ (Pi.algebraMap ι' R K).ker
i : ι'
⊢ v i = 0 i
Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v : ι → ι' → R
this✝¹ : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
h : LinearIndependent K (⇑(Pi.algebraMap ι' R K) ∘ v)
this✝ : Algebra K L := FractionRing.liftAlgebra R L
this : LinearIndependent S (⇑(Pi.algebraMap ι' R L) ∘ v)
x✝¹ : ι
x✝ : ι'
⊢ (⇑(Pi.algebraMap ι' R L) ∘ v) x✝¹ x✝ = (⇑(Pi.algebraMap ι' S L) ∘ ⇑(Pi.algebraMap ι' R S) ∘ v) x✝¹ x✝

Tactic:
;

Goal state after:
ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v : ι → ι' → R
this✝¹ : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
h : LinearIndependent K (⇑(Pi.algebraMap ι' R K) ∘ v)
this✝ : Algebra K L := FractionRing.liftAlgebra R L
this : LinearIndependent S (⇑(Pi.algebraMap ι' R L) ∘ v)
x✝¹ : ι
x✝ : ι'
⊢ (⇑(Pi.algebraMap ι' R L) ∘ v) x✝¹ x✝ = (⇑(Pi.algebraMap ι' S L) ∘ ⇑(Pi.algebraMap ι' R S) ∘ v) x✝¹ x✝
Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v : ι → ι' → R
this✝ : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
h : LinearIndependent K (⇑(Pi.algebraMap ι' R K) ∘ v)
this : Algebra K L := FractionRing.liftAlgebra R L
x✝¹ : ι
x✝ : ι'
⊢ (⇑(Pi.algebraMap ι' R L) ∘ v) x✝¹ x✝ = (⇑(Pi.algebraMap ι' K L) ∘ ⇑(Pi.algebraMap ι' R K) ∘ v) x✝¹ x✝

Tactic:
;

Goal state after:
ι : Type u_1
ι' : Type u_2
inst✝⁵ : Finite ι'
R : Type u_3
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : IsDomain S
v : ι → ι' → R
this✝ : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
h : LinearIndependent K (⇑(Pi.algebraMap ι' R K) ∘ v)
this : Algebra K L := FractionRing.liftAlgebra R L
x✝¹ : ι
x✝ : ι'
⊢ (⇑(Pi.algebraMap ι' R L) ∘ v) x✝¹ x✝ = (⇑(Pi.algebraMap ι' K L) ∘ ⇑(Pi.algebraMap ι' R K) ∘ v) x✝¹ x✝
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField

Goal state before:
pp: case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (M ^ Fintype.card K).charpoly = M.charpoly

Tactic:
;

Goal state after:
case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (M ^ Fintype.card K).charpoly = M.charpoly
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField

Goal state before:
pp: case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (M ^ p ^ k).charpoly ^ p ^ k = (⇑(frobenius K[X] p))^[k] M.charpoly

Tactic:
;

Goal state after:
case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (M ^ p ^ k).charpoly ^ p ^ k = (⇑(frobenius K[X] p))^[k] M.charpoly
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField

Goal state before:
pp: case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (M ^ Fintype.card K).charpoly ^ Fintype.card K = M.charpoly ^ p ^ k

Tactic:
;

Goal state after:
case inl
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
p : ℕ
hp✝ : CharP K p
k : ℕ
kpos : 0 < k
hp : Nat.Prime p
hk : Fintype.card K = p ^ k
this : Fact (Nat.Prime p)
⊢ (M ^ Fintype.card K).charpoly ^ Fintype.card K = M.charpoly ^ p ^ k
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
h : (M ^ Fintype.card (ZMod p)).trace = M.trace ^ Fintype.card (ZMod p)
⊢ (M ^ p).trace = M.trace ^ p

Tactic:
;

Goal state after:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
h : (M ^ Fintype.card (ZMod p)).trace = M.trace ^ Fintype.card (ZMod p)
⊢ (M ^ p).trace = M.trace ^ p
Module: Mathlib.LinearAlgebra.Matrix.Circulant

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝ : SubtractionMonoid n
v : n → α
i✝ j✝ : n
⊢ (circulant v)ᵀ i✝ j✝ = circulant (fun i ↦ v (-i)) i✝ j✝

Tactic:
;

Goal state after:
α : Type u_1
n : Type u_3
inst✝ : SubtractionMonoid n
v : n → α
i✝ j✝ : n
⊢ (circulant v)ᵀ i✝ j✝ = circulant (fun i ↦ v (-i)) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Circulant

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝¹ : Star α
inst✝ : SubtractionMonoid n
v : n → α
i✝ j✝ : n
⊢ (circulant v)ᴴ i✝ j✝ = circulant (star fun i ↦ v (-i)) i✝ j✝

Tactic:
;

Goal state after:
α : Type u_1
n : Type u_3
inst✝¹ : Star α
inst✝ : SubtractionMonoid n
v : n → α
i✝ j✝ : n
⊢ (circulant v)ᴴ i✝ j✝ = circulant (star fun i ↦ v (-i)) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case h
m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsEmpty m
A : Matrix m n R
f : Fin 0 → m
g✝ : Fin 0 → n
a✝¹ : Function.Injective f
a✝ : Function.Injective g✝
⊢ ↑1 = (A.submatrix f g✝).det

Tactic:
;

Goal state after:
case h
m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : IsEmpty m
A : Matrix m n R
f : Fin 0 → m
g✝ : Fin 0 → n
a✝¹ : Function.Injective f
a✝ : Function.Injective g✝
⊢ ↑1 = (A.submatrix f g✝).det
Module: Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular

Goal state before:
pp: case h
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
hB : Nonempty n → ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
f : Fin 0 → m ⊕ m'
g : Fin 0 → n
hf : Function.Injective f
hg : Function.Injective g
⊢ ↑1 = ((A.fromRows B).submatrix f g).det

Tactic:
;

Goal state after:
case h
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
hB : Nonempty n → ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
f : Fin 0 → m ⊕ m'
g : Fin 0 → n
hf : Function.Injective f
hg : Function.Injective g
⊢ ↑1 = ((A.fromRows B).submatrix f g).det
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LT m
inst✝ : LT n
i : m
c : n
hA : A.IsPivotedBy l
hc : l i = ↑c
⊢ A.IsLeadingEntry i c

Tactic:
by
  refine ⟨fun j hj => (hA.isPivotEntry i).1 j ?_, (hA.isPivotEntry i).2 c hc⟩
  rw [hc]
  exact_mod_cast hj

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

Goal state before:
pp: case mk
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
B : FixedDetMatrix n R m
val✝ : Matrix n n R
property✝ : val✝.det = m
h : ↑⟨val✝, property✝⟩ = ↑B
⊢ ⟨val✝, property✝⟩ = B

Tactic:
;

Goal state after:
case mk
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
B : FixedDetMatrix n R m
val✝ : Matrix n n R
property✝ : val✝.det = m
h : ↑⟨val✝, property✝⟩ = ↑B
⊢ ⟨val✝, property✝⟩ = B
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
b : FixedDetMatrix n R m
⊢ ⟨↑1 * ↑b, ⋯⟩ = b

Tactic:
;

Goal state after:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
b : FixedDetMatrix n R m
⊢ ⟨↑1 * ↑b, ⋯⟩ = b
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: A : FixedDetMatrix (Fin 2) ℤ 0
h₁ : ↑A 1 0 = 0
h₂ : 0 < ↑A 0 0
h₄ : |↑A 0 1| < |↑A 1 1|
⊢ |↑A 0 1| < 0

Tactic:
have := A_c_eq_zero h₁

Goal state after:
A : FixedDetMatrix (Fin 2) ℤ 0
h₁ : ↑A 1 0 = 0
h₂ : 0 < ↑A 0 0
h₄ : |↑A 0 1| < |↑A 1 1|
this : ↑A 0 0 * ↑A 1 1 = 0
⊢ |↑A 0 1| < 0
Module: Mathlib.LinearAlgebra.Matrix.Integer

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
i✝ : n
j✝ : m
⊢ Aᵀ.num i✝ j✝ = A.numᵀ i✝ j✝

Tactic:
;

Goal state after:
m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
i✝ : n
j✝ : m
⊢ Aᵀ.num i✝ j✝ = A.numᵀ i✝ j✝
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
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i j : n
h_pos : 0 < ∑ j_1, (A ^ m) i j_1 * A j_1 j
l : n
hl_mem : l ∈ Finset.univ
hl_pos : 0 < (A ^ m) i l * A l j
hAm_nonneg : 0 ≤ (A ^ m) i l
hA_nonneg' : 0 ≤ A l j
h : (A ^ m) i l ≤ 0
⊢ False

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
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i j : n
h_pos : 0 < ∑ j_1, (A ^ m) i j_1 * A j_1 j
l : n
hl_mem : l ∈ Finset.univ
hl_pos : 0 < (A ^ m) i l * A l j
hAm_nonneg : 0 ≤ (A ^ m) i l
hA_nonneg' : 0 ≤ A l j
h : (A ^ m) i l ≤ 0
⊢ False
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
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.univ.sup' ⋯ fun i ↦ ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ A i i - μ = (A i i * v i - μ * v i) * (v i)⁻¹

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
μ : K
hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ
h✝ : Nonempty n
v : n → K
h_eg : v ∈ (Module.End.genEigenspace (Matrix.toLin' A) μ) 1
h_nz✝ : v ≠ 0
i : n
h_i : (Finset.univ.sup' ⋯ fun i ↦ ‖v i‖) = ‖v i‖
h_nz : v i ≠ 0
h_le : ∀ (j : n), ‖v j * (v i)⁻¹‖ ≤ 1
⊢ A i i - μ = (A i i * v i - μ * v i) * (v i)⁻¹
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
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i j : n
h_pos : 0 < ∑ j_1, (A ^ m) i j_1 * A j_1 j
l : n
hl_mem : l ∈ Finset.univ
hl_pos : 0 < (A ^ m) i l * A l j
hAm_nonneg : 0 ≤ (A ^ m) i l
hA_nonneg' : 0 ≤ A l j
h_Am : 0 < (A ^ m) i l
h : A l j ≤ 0
⊢ False

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
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
m : ℕ
ih : ∀ (i j : n), 0 < (A ^ m) i j ↔ Nonempty { p // p.length = m }
i j : n
h_pos : 0 < ∑ j_1, (A ^ m) i j_1 * A j_1 j
l : n
hl_mem : l ∈ Finset.univ
hl_pos : 0 < (A ^ m) i l * A l j
hAm_nonneg : 0 ≤ (A ^ m) i l
hA_nonneg' : 0 ≤ A l j
h_Am : 0 < (A ^ m) i l
h : A l j ≤ 0
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: case refine_1
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix m m R
B : Matrix n n R
hA : A.IsHadamard
hB : B.IsHadamard
i : m
i' : n
j : m
j' : n
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B * (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)ᴴ) (i, i') (j, j') =
    (↑(Fintype.card (m × n)) • 1) (i, i') (j, j')

Tactic:
calc
      _ = ∑ x₁, ∑ x₂, A i x₁ * (B i' x₂ * Bᴴ x₂ j') * Aᴴ x₁ j := by
        simp [conjTranspose_kronecker', mul_apply, mul_assoc, ← Finset.sum_product']
      _ = if i' = j' then ∑ x, A i x * (Fintype.card n • Aᴴ) x j else 0 := by
        simp [← Finset.sum_mul, ← Finset.mul_sum, ← mul_apply, hB.mul_conjTranspose,
          one_apply, mul_assoc _ (Fintype.card n : R), -conjTranspose_apply]
      _ = _ := by
        simp only [← mul_apply, mul_smul_comm, hA.mul_conjTranspose]
        simp [one_apply, ← Nat.cast_mul, mul_comm, ← ite_and, and_comm]

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‖
⊢ ∀ (k : n), ∑ j ∈ Finset.univ.erase k, ‖A j k‖ < ‖A k k‖

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‖
⊢ ∀ (k : n), ∑ j ∈ Finset.univ.erase k, ‖A j k‖ < ‖A k k‖
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

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

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j
    · rw [diagonal_apply_eq, diag]
    · rw [diagonal_apply_ne _ hij, h hij]

Goal state after:
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ᵀ i j = A i j

pp: case neg
α : Type u_1
n : Type u_4
inst✝ : Zero α
A : Matrix n n α
h : A.IsDiag
i j : n
g : ¬i = j
⊢ Aᵀ i j = A i j

Tactic:
;

Goal state after:
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ᵀ i j = A i j

case neg
α : Type u_1
n : Type u_4
inst✝ : Zero α
A : Matrix n n α
h : A.IsDiag
i j : n
g : ¬i = j
⊢ Aᵀ i j = A i j
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
a : ∀ (i j : n), 0 ≤ A j i
⊢ ∃ x x_1, ∀ (x_2 : Path x x_1), x_2.length = 0

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
a : ∀ (i j : n), 0 ≤ A j i
⊢ ∃ x x_1, ∀ (x_2 : Path x x_1), x_2.length = 0
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.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
N : Matrix ι ι R
v : ι → M
x✝ : ι
⊢ (N • v) x✝ = (∑ j, fun i ↦ N i j • v j) x✝

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
N : Matrix ι ι R
v : ι → M
x✝ : ι
⊢ (N • v) x✝ = (∑ j, fun i ↦ N i j • v j) x✝
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
S : Type u_6
inst✝³ : Ring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
x✝³ : R
x✝² : Matrix ι ι S
x✝¹ : ι → M
x✝ : ι
⊢ ((x✝³ • x✝²) • x✝¹) x✝ = (x✝³ • x✝² • x✝¹) x✝

Tactic:
;

Goal state after:
ι : 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
S : Type u_6
inst✝³ : Ring S
inst✝² : SMul R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
x✝³ : R
x✝² : Matrix ι ι S
x✝¹ : ι → M
x✝ : ι
⊢ ((x✝³ • x✝²) • x✝¹) x✝ = (x✝³ • x✝² • x✝¹) x✝
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
f : M →ₗ[R] N
x✝² : Matrix ι ι R
x✝¹ : ι → M
x✝ : ι
⊢ (f.compLeft ι) (x✝² • x✝¹) x✝ = ((RingHom.id (Matrix ι ι R)) x✝² • (f.compLeft ι) x✝¹) x✝

Tactic:
;

Goal state after:
ι : 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
f : M →ₗ[R] N
x✝² : Matrix ι ι R
x✝¹ : ι → M
x✝ : ι
⊢ (f.compLeft ι) (x✝² • x✝¹) x✝ = ((RingHom.id (Matrix ι ι R)) x✝² • (f.compLeft ι) x✝¹) x✝
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
x✝¹ : ι → M
x✝ : ι
⊢ (mapMatrixModule ι id) x✝¹ x✝ = id x✝¹ x✝

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
x✝¹ : ι → M
x✝ : ι
⊢ (mapMatrixModule ι id) x✝¹ x✝ = id x✝¹ x✝
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
f : M →ₗ[R] N
g : N →ₗ[R] P
x✝¹ : ι → M
x✝ : ι
⊢ (mapMatrixModule ι (g ∘ₗ f)) x✝¹ x✝ = (mapMatrixModule ι g ∘ₗ mapMatrixModule ι f) x✝¹ x✝

Tactic:
;

Goal state after:
ι : 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
f : M →ₗ[R] N
g : N →ₗ[R] P
x✝¹ : ι → M
x✝ : ι
⊢ (mapMatrixModule ι (g ∘ₗ f)) x✝¹ x✝ = (mapMatrixModule ι g ∘ₗ mapMatrixModule ι f) x✝¹ x✝