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

Goal state before:
pp: n : Type u_1
p : Type u_2
𝕜 : Type u_3
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : Fintype n
inst✝ : Fintype p
M : Matrix p p 𝕜
e : p ≃ n
L₀ L₀' : List (TransvectionStruct n 𝕜)
D₀ : n → 𝕜
h₀ : (List.map toMatrix L₀).prod * (reindexAlgEquiv 𝕜 𝕜 e) M * (List.map toMatrix L₀').prod = diagonal D₀
this : M = (reindexAlgEquiv 𝕜 𝕜 e.symm) ((reindexAlgEquiv 𝕜 𝕜 e) M)
⊢ (reindexAlgEquiv 𝕜 𝕜 e.symm) (diagonal D₀) = diagonal (D₀ ∘ ⇑e)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: case hX
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : (Matrix n n R)[X]
r : R
⊢ ((aeval r).mapMatrix.comp ↑matPolyEquiv.symm) X = (eval₂AlgHom (AlgHom.id R (Matrix n n R)) ((scalar n) r) ⋯) X

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝² : Field 𝕜
r : ℕ
IH :
  ∀ (n : Type) [inst : Fintype n] [inst_1 : DecidableEq n] (M : Matrix n n 𝕜),
    Fintype.card n = r → ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = r + 1
⊢ r + 1 = Fintype.card (Fin r) + Fintype.card Unit

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝² : Field 𝕜
r : ℕ
IH :
  ∀ (n : Type) [inst : Fintype n] [inst_1 : DecidableEq n] (M : Matrix n n 𝕜),
    Fintype.card n = r → ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = r + 1
e : n ≃ Fin r ⊕ Unit
N : Matrix (Fin r) (Fin r) 𝕜
⊢ Fintype.card (Fin r) = r

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
m : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
x✝ : Matrix m m (Matrix n n R[X])
i✝ j✝ : m × n
⊢ ((evalRingHom 0).mapMatrix.comp ↑(compRingEquiv m n R[X])) x✝ i✝ j✝ =
    ((compRingEquiv m n R).toRingHom.comp (evalRingHom 0).mapMatrix.mapMatrix) x✝ i✝ j✝

Tactic:
simp

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

Goal state before:
pp: n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n 𝕜
⊢ Fintype.card n = Fintype.card (Fin (Fintype.card n))

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n R
B : Matrix n m R
M : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks ((scalar m) X) (A.map ⇑C) (B.map ⇑C) 1
N : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks (-1) 0 (B.map ⇑C) (-(scalar n) X)
hMN : M * N = fromBlocks (-(scalar m) X + (A * B).map ⇑C) (-X • A.map ⇑C) 0 (-(scalar n) X)
hNM : N * M = fromBlocks (-(scalar m) X) (-A.map ⇑C) 0 ((B * A).map ⇑C - (scalar n) X)
⊢ (-1) ^ Fintype.card m * ((scalar m) X - (A * B).map ⇑C).det * (-(scalar n) X).det =
    (-1) ^ (Fintype.card m + Fintype.card n) * (X ^ Fintype.card n * ((scalar m) X - (A * B).map ⇑C).det)

Tactic:
simp

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n R
B : Matrix n m R
M : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks ((scalar m) X) (A.map ⇑C) (B.map ⇑C) 1
N : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks (-1) 0 (B.map ⇑C) (-(scalar n) X)
hMN : M * N = fromBlocks (-(scalar m) X + (A * B).map ⇑C) (-X • A.map ⇑C) 0 (-(scalar n) X)
hNM : N * M = fromBlocks (-(scalar m) X) (-A.map ⇑C) 0 ((B * A).map ⇑C - (scalar n) X)
⊢ (-1) ^ Fintype.card m * ((diagonal fun x ↦ X) - A.map ⇑C * B.map ⇑C).det * (-X) ^ Fintype.card n =
    (-1) ^ (Fintype.card m + Fintype.card n) * (X ^ Fintype.card n * ((diagonal fun x ↦ X) - A.map ⇑C * B.map ⇑C).det)
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring S
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Module S A
inst✝ : IsScalarTower R S A
i✝³ j✝³ : m
x✝³ : A
i✝² j✝² : n
x✝² : B
i✝¹ j✝¹ : m
x✝¹ : A
i✝ j✝ : n
x✝ : B
⊢ ((AlgebraTensorModule.curry
              (((AlgebraTensorModule.curry
                        ((LinearMap.mul R (Matrix m m A ⊗[R] Matrix n n B)).compr₂
                          (↑R ↑(kroneckerTMulLinearEquiv m m n n R S A B))) ∘ₗ
                      singleLinearMap R i✝³ j✝³)
                    x✝³ ∘ₗ
                  singleLinearMap R i✝² j✝²)
                x✝²) ∘ₗ
            singleLinearMap R i✝¹ j✝¹)
          x✝¹ ∘ₗ
        singleLinearMap R i✝ j✝)
      x✝ =
    ((AlgebraTensorModule.curry
              (((AlgebraTensorModule.curry
                        ((LinearMap.mul R (Matrix (m × n) (m × n) (A ⊗[R] B)) ∘ₗ
                              ↑R ↑(kroneckerTMulLinearEquiv m m n n R S A B)).compl₂
                          (↑R ↑(kroneckerTMulLinearEquiv m m n n R S A B))) ∘ₗ
                      singleLinearMap R i✝³ j✝³)
                    x✝³ ∘ₗ
                  singleLinearMap R i✝² j✝²)
                x✝²) ∘ₗ
            singleLinearMap R i✝¹ j✝¹)
          x✝¹ ∘ₗ
        singleLinearMap R i✝ j✝)
      x✝

Tactic:
simp [single_kroneckerTMul_single, mul_kroneckerTMul_mul]

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

Goal state before:
pp: n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P : Matrix n n 𝕜 → Prop
M : Matrix n n 𝕜
hMdet : M.det ≠ 0
hdiag : ∀ (D : n → 𝕜), (diagonal D).det ≠ 0 → P (diagonal D)
htransvec : ∀ (t : TransvectionStruct n 𝕜), P t.toMatrix
hmul : ∀ (A B : Matrix n n 𝕜), A.det ≠ 0 → B.det ≠ 0 → P A → P B → P (A * B)
Q : Matrix n n 𝕜 → Prop := fun N ↦ N.det ≠ 0 ∧ P N
t : TransvectionStruct n 𝕜
⊢ t.toMatrix.det ≠ 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n R
B : Matrix n m R
M : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks ((scalar m) X) (A.map ⇑C) (B.map ⇑C) 1
N : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks (-1) 0 (B.map ⇑C) (-(scalar n) X)
hMN : M * N = fromBlocks (-(scalar m) X + (A * B).map ⇑C) (-X • A.map ⇑C) 0 (-(scalar n) X)
hNM : N * M = fromBlocks (-(scalar m) X) (-A.map ⇑C) 0 ((B * A).map ⇑C - (scalar n) X)
hdet_MN :
  (M * N).det = (-1) ^ (Fintype.card m + Fintype.card n) * (X ^ Fintype.card n * ((scalar m) X - (A * B).map ⇑C).det)
⊢ (-(scalar m) X).det * ((-1) ^ Fintype.card n * ((scalar n) X - (B * A).map ⇑C).det) =
    (-1) ^ (Fintype.card m + Fintype.card n) * (X ^ Fintype.card m * ((scalar n) X - (B * A).map ⇑C).det)

Tactic:
simp

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n R
B : Matrix n m R
M : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks ((scalar m) X) (A.map ⇑C) (B.map ⇑C) 1
N : Matrix (m ⊕ n) (m ⊕ n) R[X] := fromBlocks (-1) 0 (B.map ⇑C) (-(scalar n) X)
hMN : M * N = fromBlocks (-(scalar m) X + (A * B).map ⇑C) (-X • A.map ⇑C) 0 (-(scalar n) X)
hNM : N * M = fromBlocks (-(scalar m) X) (-A.map ⇑C) 0 ((B * A).map ⇑C - (scalar n) X)
hdet_MN :
  (M * N).det = (-1) ^ (Fintype.card m + Fintype.card n) * (X ^ Fintype.card n * ((scalar m) X - (A * B).map ⇑C).det)
⊢ (-X) ^ Fintype.card m * ((-1) ^ Fintype.card n * ((diagonal fun x ↦ X) - B.map ⇑C * A.map ⇑C).det) =
    (-1) ^ (Fintype.card m + Fintype.card n) * (X ^ Fintype.card m * ((diagonal fun x ↦ X) - B.map ⇑C * A.map ⇑C).det)
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: case e'_3.a.a
n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
x✝¹ : n
a✝¹ : x✝¹ ∈ Finset.univ
x✝ : n
a✝ : x✝ ∈ Finset.univ
⊢ single x✝¹ x✝ (M x✝¹ x✝) = M (x✝¹, x✝).1 (x✝¹, x✝).2 • single (x✝¹, x✝).1 (x✝¹, x✝).2 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: case e'_3
n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n A
⊢ ∑ i, ∑ j, single i j (M i j) = ∑ x, ∑ y, M (x, y).1 (x, y).2 • (single (x, y).1 (x, y).2 1).map ⇑(algebraMap R A)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: case zero
n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ invFun n R A ((toFunAlgHom n R A) 0) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: case tmul
n : Type u_3
R : Type u_5
A : Type u_7
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a : A
m : Matrix n n R
⊢ invFun n R A ((toFunAlgHom n R A) (a ⊗ₜ[R] m)) = a ⊗ₜ[R] m

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : Semiring A
inst✝¹⁵ : Semiring B
inst✝¹⁴ : Algebra R A
inst✝¹³ : Algebra R B
inst✝¹² : Fintype n
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra S A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : StarRing R
inst✝³ : StarAddMonoid A
inst✝² : StarAddMonoid B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
x : Matrix m m A ⊗[R] Matrix n n B
⊢ (kroneckerTMulAlgEquiv m n R S A B) (star 0) = star ((kroneckerTMulAlgEquiv m n R S A B) 0)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Semiring B
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq n
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : StarRing R
x : Matrix m m R ⊗[R] Matrix n n R
⊢ (kroneckerAlgEquiv m n R) (star 0) = star ((kroneckerAlgEquiv m n R) 0)

Tactic:
simp

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

Goal state before:
pp: case inl
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
u v : n → R
h✝ : IsEmpty n
⊢ (vecMulVec u v).charpoly = X ^ Fintype.card n - (u ⬝ᵥ v) • X ^ (Fintype.card n - 1)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : (Matrix n n R)ˣ
N : Matrix n n R
⊢ ((↑M)⁻¹ * ↑M * N).charpoly = N.charpoly

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
⊢ (x + y) ^ 0 = x ^ 0 + ↑0 * x ^ (0 - 1) * y + 0 * y ^ 2

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R✝
m n : ℕ
R : Type u_1
inst✝ : CommSemiring R
x y : R
⊢ (x + y) ^ 1 = x ^ 1 + ↑1 * x ^ (1 - 1) * y + 0 * y ^ 2

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a✝ b : R
m n : ℕ
inst✝ : CommRing R
x y : R
e : ℕ
a : R
⊢ { k // a * (x + y) ^ e = a * (x ^ e + ↑e * x ^ (e - 1) * y + k * y ^ 2) }

Tactic:
exists (powAddExpansion x y e).val
  congr
  apply (powAddExpansion _ _ _).property

Goal state after:
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
x y : R
⊢ x ^ 0 - y ^ 0 = 0 * (x - y)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Identities

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst✝ : CommRing R
x y : R
⊢ x ^ 1 - y ^ 1 = 1 * (x - y)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
x : R
hx : IsUnit x
H : IsNilpotent x
⊢ Commute x (-x)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: R : Type u_1
r : R
inst✝ : Semiring R
n k : ℕ
⊢ (monomial n) r ^ k = 0 ↔ r ^ k = 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : IsNilpotent (X * P)
⊢ X ∈ nonZeroDivisorsLeft R[X]

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : R[X]
⊢ IsNilpotent 0 → ∀ (i : ℕ), IsNilpotent (coeff 0 i)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: case empty
R : Type u_1
inst✝ : Semiring R
ι : Type u_3
f : ι → R
hnp : ∀ i ∈ ∅, IsNilpotent (f i)
h_comm : ∀ (i j : ι), i ∈ ∅ → j ∈ ∅ → Commute (f i) (f j)
⊢ IsNilpotent (∑ i ∈ ∅, f i)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: case refine_3.zero
R : Type u_1
inst✝ : CommRing R
P p : R[X]
x✝ : p ≠ 0
hnp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpX : IsNilpotent (p * X)
⊢ IsNilpotent ((p * X).coeff 0)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
ι : Type u_3
f : ι → R
j : ι
s : Finset ι
hj : j ∉ s
ih : (∀ i ∈ s, IsNilpotent (f i)) → (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i ∈ s, f i)
hnp : ∀ i ∈ insert j s, IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
i : ι
hi : i ∈ s
⊢ j ∈ insert j s

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Basic

Goal state before:
pp: case insert.hx
R : Type u_1
inst✝ : Semiring R
ι : Type u_3
f : ι → R
j : ι
s : Finset ι
hj : j ∉ s
ih : (∀ i ∈ s, IsNilpotent (f i)) → (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i ∈ s, f i)
hnp : ∀ i ∈ insert j s, IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
⊢ j ∈ insert j s

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ span R ↑p = p

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
⊢ ∀ (i : ℕ), (C r + X * P).coeff (i + 1) = P.coeff i

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Nilpotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : R[X]
this : P = C (eval 0 P) + X * (P /ₘ X)
| IsUnit (C (eval 0 P) + X * (P /ₘ X))

Tactic:
simp

Goal state after:
R : Type u_1
inst✝ : CommRing R
P : R[X]
this : P = C (eval 0 P) + X * (P /ₘ X)
| IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
hb : Submodule.span R (Set.range b) = ⊤
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ ↥I
hbM' : ∀ (x : M), (Ideal.finsuppTotal ι M I b) (bM' x) = f x
A : Matrix ι ι R := fun i j ↦ ↑((bM' (b j)) i)
⊢ ∀ (j : ι), ∑ i, ↑((bM' (b j)) i) • b i = f (b j)

Tactic:
intro j

Goal state after:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
hb : Submodule.span R (Set.range b) = ⊤
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ ↥I
hbM' : ∀ (x : M), (Ideal.finsuppTotal ι M I b) (bM' x) = f x
A : Matrix ι ι R := fun i j ↦ ↑((bM' (b j)) i)
j : ι
⊢ ∑ i, ↑((bM' (b j)) i) • b i = f (b j)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Goal state before:
pp: ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
hb : Submodule.span R (Set.range b) = ⊤
f : Module.End R M
⊢ LinearMap.range f ≤ ⊤ • ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h2 : ⨅ s, ⨅ (_ : span R s = p), s.encard ≠ ⊤
s : Set M
h : span R s = p
hs : s.Finite
⊢ (↑↑⟨hs.toFinset, ⋯⟩).encard ≤ s.encard

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : ⨅ s, #↑↑s < ℵ₀
⊢ span R ↑p = p

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ ↑(toNat (span R s).spanRank) ≤ (↑↑toENat.toRingHom).toFun (span R s).spanRank

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
s : Set M
hs₁ : #↑s = p.spanRank
hs₂ : span R s = p
this : p.spanRank = ↑p.spanFinrank
⊢ toENat ↑p.spanFinrank = ↑(toNat ↑p.spanFinrank)

Tactic:
simp

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

Goal state before:
pp: M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : Module.End R M
⊢ range f ≤ ⊤ • ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
s : Set M
hs₁ : s.encard = ↑p.spanFinrank
hs₂ : span R s = p
s_f : s.Finite
⊢ ∃ s, s.card = p.spanFinrank ∧ span R ↑s = p

Tactic:
refine ⟨s_f.toFinset, ⟨?_, by simpa using hs₂⟩⟩

Goal state after:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
s : Set M
hs₁ : s.encard = ↑p.spanFinrank
hs₂ : span R s = p
s_f : s.Finite
⊢ s_f.toFinset.card = p.spanFinrank
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : p.FG
s : Set M
hs₁ : s.encard = ↑p.spanFinrank
hs₂ : span R s = p
s_f : s.Finite
⊢ s_f.toFinset.card = p.spanFinrank

Tactic:
simpa [s_f.encard_eq_coe_toFinset_card, ENat.natCast_inj] using hs₁

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: case e'_1
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : Cardinal.{u}
⊢ p.spanRank = lift.{u, u} p.spanRank

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: case e'_2
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : Cardinal.{u}
x✝ : Set M
⊢ #↑x✝ = lift.{u, u} #↑x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ span R ∅ = ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ #↑↑⟨∅, ⋯⟩ = 0

Tactic:
simp

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

Goal state before:
pp: case pos
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ degree 1 = ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
hm : m ≠ 0
⊢ {m}.Finite

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
hm : m ≠ 0
⊢ {m}.ncard ≤ 1

Tactic:
simp

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

Goal state before:
pp: case h
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∏ x, 1 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : Ring S
f : R →+* S
x : R
⊢ eval₂ f (f x) (X - C x) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_4
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Ring T
f : R →+* S
x : S
g : S →+* T
p : R[X]
hp : p.Monic
hx : eval₂ f x p = 0
⊢ eval₂ (g.comp f) (g x) p = 0

Tactic:
by simp_rw [← hom_eval₂, eval₂_eq_eval_map] at hx ⊢; simp [hx]

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
σ : R →+* S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
L : Type v
inst✝² : AddCommMonoid L
inst✝¹ : Module S L
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] L
p : Submodule R M
hp : p.FG
⊢ Cardinal.lift.{u, v} (map f p).spanRank ≤ Cardinal.lift.{v, u} p.spanRank

Tactic:
exact p.lift_spanRank_map_le f

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ M.det = (-1 • eval ((scalar n) 0) (X - C M)).det

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u
inst✝ : CommRing R
M : Matrix (Fin 0) (Fin 0) R
⊢ eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : RankCondition R
ι : Type u_3
v : Basis ι R M
⊢ #↑(Set.range ⇑v) = ⊤.spanRank

Tactic:
rw [← v.span_eq, spanRank_span_of_linearIndepOn]
  exact v.linearIndependent.linearIndepOn_id

Goal state after: