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

Goal state before:
pp: case succ.h₀.succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1 + 1)) (Fin (n + 1 + 1)) R
i : Fin (n + 1).succ
a✝ : i ∈ univ
hi : i ≠ 0
⊢ ∀ (i_1 : Fin (n + 1)), submatrix 1 Fin.succ i.succAbove i_1 0 = 0

Tactic:
intro j

Goal state after:
case succ.h₀.succ
R : Type u
inst✝ : CommRing R
n : ℕ
IH : ∀ (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R), eval 0 (derivative (1 + X • M.map ⇑C).det) = M.trace
M : Matrix (Fin (n + 1 + 1)) (Fin (n + 1 + 1)) R
i : Fin (n + 1).succ
a✝ : i ∈ univ
hi : i ≠ 0
j : Fin (n + 1)
⊢ submatrix 1 Fin.succ i.succAbove j 0 = 0
Module: Mathlib.Data.Nat.Factorial.Cast

Goal state before:
pp: case zero
S : Type u_1
inst✝ : Ring S
⊢ ↑((0 - 1) * descFactorial 0 1) = ↑0 * (↑0 - 1)

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
n : ℕ
hl : (monomial n) 0 ∈ lifts f
⊢ map f 0 = (monomial n) 0 ∧ degree 0 = ((monomial n) 0).degree

Tactic:
simp

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

Goal state before:
pp: case pos
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
mp : m = k
m0 : m = 0
⊢ 1 - (M ^ k) j j = (1 - M ^ k) j j

Tactic:
simp

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

Goal state before:
pp: case neg
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
mp : m = k
m0 : ¬m = 0
⊢ 1 - 0 = (1 - 0) j j

Tactic:
simp

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

Goal state before:
pp: case pos
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
mp : ¬m = k
h✝ : m = 0
⊢ 0 - (M ^ k) j j = (0 - M ^ k) j j

Tactic:
simp

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

Goal state before:
pp: case neg
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
K : Type u_1
k : ℕ
inst✝ : CommRing K
M : Matrix n n K
m : ℕ
i j : n
hij : i = j
mp : ¬m = k
h✝ : ¬m = 0
⊢ 0 - 0 = (0 - 0) j j

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
hR : Subsingleton S
hlifts : 1 ∈ lifts f
hp : Monic 1
⊢ natDegree 1 = natDegree 1

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
hR : Subsingleton S
hlifts : 1 ∈ lifts f
hp : Monic 1
⊢ Monic 1

Tactic:
simp

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
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ ((scalar n) X - C.mapMatrix A⁻¹).det = C (A⁻¹ * A).det * ((scalar n) X - C.mapMatrix A⁻¹).det

Tactic:
simp

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
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C (A⁻¹.det * A.det) * ((scalar n) X - C.mapMatrix A⁻¹).det =
    C A⁻¹.det * C A.det * ((scalar n) X - C.mapMatrix A⁻¹).det

Tactic:
simp

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
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C A⁻¹.det * (C.mapMatrix A * ((scalar n) X - C.mapMatrix A⁻¹)).det =
    C A⁻¹.det * (C.mapMatrix A * (scalar n) X - 1).det

Tactic:
rw [mul_sub, ← map_mul]

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C A⁻¹.det * (C.mapMatrix A * (scalar n) X - C.mapMatrix (A * A⁻¹)).det =
    C A⁻¹.det * (C.mapMatrix A * (scalar n) X - 1).det
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
A : Matrix n n R
h : IsUnit A
this : Invertible A
⊢ C A⁻¹.det * (C.mapMatrix A * (scalar n) X - C.mapMatrix (A * A⁻¹)).det =
    C A⁻¹.det * (C.mapMatrix A * (scalar n) X - 1).det

Tactic:
simp

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

Goal state before:
pp: case inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
h✝ : IsEmpty n
⊢ IsNilpotent M.trace

Tactic:
simp

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
hM : IsNilpotent M
a✝ : Nontrivial R
p : R[X] := M.charpolyRev
hp : p - 1 = X * (p /ₘ X)
this : IsNilpotent (p /ₘ X)
⊢ max M.charpoly.natDegree (X ^ Fintype.card n).natDegree ≤ M.charpoly.natDegree

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ (lsum fun i ↦ monomial (i - k) ∘ₗ DistribSMul.toLinearMap R R (i.choose k)) f =
    f.sum fun i r ↦ (monomial (i - k)) (↑(i.choose k) * r)

Tactic:
simp

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
hM : IsNilpotent M
a✝ : Nontrivial R
p : R[X] := M.charpolyRev
hp : p - 1 = X * (p /ₘ X)
this : IsNilpotent (p /ₘ X)
aux : (M.charpoly - X ^ Fintype.card n).natDegree ≤ M.charpoly.natDegree
⊢ IsNilpotent (reflect M.charpoly.natDegree M.charpoly - reflect M.charpoly.natDegree (X ^ Fintype.card n))

Tactic:
← reverse,

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
hM : IsNilpotent M
a✝ : Nontrivial R
p : R[X] := M.charpolyRev
hp : p - 1 = X * (p /ₘ X)
this : IsNilpotent (p /ₘ X)
aux : (M.charpoly - X ^ Fintype.card n).natDegree ≤ M.charpoly.natDegree
⊢ IsNilpotent (M.charpoly.reverse - reflect M.charpoly.natDegree (X ^ Fintype.card n))
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ (if n + k - k = n then ↑((n + k).choose k) * f.coeff (n + k) else 0) = ↑((n + k).choose k) * f.coeff (n + k)

Tactic:
simp

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
⊢ (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)

Tactic:
rw [choose_eq_zero_of_lt hikl, mul_zero]

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
⊢ (i - l).choose k * i.choose l = 0
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r✝ : R
f✝ : R[X]
r c : R
f : R[X]
⊢ (c • f).comp (X + C r) = (RingHom.id R) c • f.comp (X + C r)

Tactic:
by simp only [smul_eq_C_mul, C_mul_comp, RingHom.id_apply]

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

Goal state before:
pp: case h
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ max 0 (max 0 0) = max 0 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
s : R
n✝ : ℕ
⊢ (scaleRoots 0 s).coeff n✝ = coeff 0 n✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r c : R
n✝ : ℕ
⊢ ((C c).scaleRoots r).coeff n✝ = (C c).coeff n✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n✝ : ℕ
⊢ (p.scaleRoots 1).coeff n✝ = p.coeff n✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
n✝ : ℕ
⊢ (scaleRoots 1 r).coeff n✝ = coeff 1 n✝

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
r s : R
a✝ : Nontrivial R
⊢ ((X + C r).scaleRoots s).coeff 0 = (X + C (r * s)).coeff 0

Tactic:
simp

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

Goal state before:
pp: case succ.zero
R : Type u_1
inst✝ : Semiring R
r s : R
a✝ : Nontrivial R
⊢ ((X + C r).scaleRoots s).coeff (0 + 1) = (X + C (r * s)).coeff (0 + 1)

Tactic:
simp

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

Goal state before:
pp: case succ.succ
R : Type u_1
inst✝ : Semiring R
r s : R
a✝ : Nontrivial R
i : ℕ
⊢ ((X + C r).scaleRoots s).coeff (i + 1 + 1) = (X + C (r * s)).coeff (i + 1 + 1)

Tactic:
simp

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

Goal state before:
pp: S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
i : ℕ
_hi : i ∈ p.support
hi' : i ∉ (p.scaleRoots s).support
⊢ f (p.coeff i * s ^ (p.natDegree - i)) * (f s * a) ^ i = 0

Tactic:
by
        let : coeff p i * s ^ (p.natDegree - i) = 0 := by simpa using hi'
        simp [this]

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

Goal state before:
pp: S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
⊢ eval₂ f (f s * a) (p.scaleRoots s) = f s ^ p.natDegree * eval₂ f a p

Tactic:
by
  calc
    _ = (scaleRoots p s).support.sum fun i =>
          f (coeff p i * s ^ (p.natDegree - i)) * (f s * a) ^ i := by
      simp [eval₂_eq_sum, sum_def]
    _ = p.support.sum fun i => f (coeff p i * s ^ (p.natDegree - i)) * (f s * a) ^ i :=
      (Finset.sum_subset (support_scaleRoots_le p s) fun i _hi hi' => by
        let : coeff p i * s ^ (p.natDegree - i) = 0 := by simpa using hi'
        simp [this])
    _ = p.support.sum fun i : ℕ => f (p.coeff i) * f s ^ (p.natDegree - i + i) * a ^ i :=
      (Finset.sum_congr rfl fun i _hi => by
        simp_rw [f.map_mul, f.map_pow, pow_add, hsa.mul_pow, mul_assoc])
    _ = p.support.sum fun i : ℕ => f s ^ p.natDegree * (f (p.coeff i) * a ^ i) :=
      Finset.sum_congr rfl fun i hi => by
        rw [mul_assoc, ← map_pow, (hf _ _).left_comm, map_pow, tsub_add_cancel_of_le]
        exact le_natDegree_of_ne_zero (Polynomial.mem_support_iff.mp hi)
    _ = f s ^ p.natDegree * eval₂ f a p := by simp [← Finset.mul_sum, eval₂_eq_sum, sum_def]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
a✝ : Nontrivial R
hp : ¬p = 0
⊢ p.integralNormalization.coeff p.natDegree ≠ 0

Tactic:
by simp [integralNormalization_coeff_natDegree, *]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p q : R[X]
r : R
inst✝ : NoZeroDivisors R
⊢ (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Tactic:
by
  by_cases hp : p = 0; · simp [hp]
  by_cases hq : q = 0; · simp [hq]
  apply mul_scaleRoots'
  simp only [ne_eq, mul_eq_zero, leadingCoeff_eq_zero, hp, hq, or_self, not_false_eq_true]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r : R
hp : p.leadingCoeff ^ 0 ≠ 0
⊢ (p ^ 0).scaleRoots r = p.scaleRoots r ^ 0

Tactic:
simp

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

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝ : CommSemiring R
r : R
h✝ : Nontrivial R
hp : Splits 0
⊢ (Polynomial.scaleRoots 0 r).Splits

Tactic:
simp

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

Goal state before:
pp: case inr.inr.empty
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
hp : p.Splits
r : R
h✝ : Nontrivial R
hp0 : p ≠ 0
⊢ ((Multiset.map (fun x ↦ X + C x) 0).prod.scaleRoots r).Splits

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Ring R
r s : R
a✝ : Nontrivial R
⊢ ((X - C r).scaleRoots s).coeff 0 = (X - C (r * s)).coeff 0

Tactic:
simp

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

Goal state before:
pp: case succ.zero
R : Type u_1
inst✝ : Ring R
r s : R
a✝ : Nontrivial R
⊢ ((X - C r).scaleRoots s).coeff (0 + 1) = (X - C (r * s)).coeff (0 + 1)

Tactic:
simp

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

Goal state before:
pp: case succ.succ
R : Type u_1
inst✝ : Ring R
r s : R
a✝ : Nontrivial R
i : ℕ
⊢ ((X - C r).scaleRoots s).coeff (i + 1 + 1) = (X - C (r * s)).coeff (i + 1 + 1)

Tactic:
simp

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

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝ : CommRing R
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
⊢ rootMultiplicity (r * a) (scaleRoots 0 r) = rootMultiplicity a 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
n : ℕ
⊢ ↑((p.toSubring T hp).coeff n) = p.coeff n

Tactic:
simp

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semiring R
b : R
hf : (C 0 * X + C b).natDegree ≤ 1
h : Invertible (C 0 * X + C b).leadingCoeff
⊢ (C 0 * X + C b).Splits

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
H : (p.toSubring T hp).coeff p.natDegree = 1
⊢ ↑1 = 1

Tactic:
OneMemClass.coe_one

Goal state after:
R : Type u_1
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
H : (p.toSubring T hp).coeff p.natDegree = 1
⊢ 1 = 1
Module: Mathlib.RingTheory.Polynomial.Subring

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
T : Subring R
i : ℕ
⊢ ↑((toSubring 0 T ⋯).coeff i) = ↑(coeff 0 i)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
T : Subring R
⊢ toSubring 0 T ⋯ = 0

Tactic:
ext i
  simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
T : Subring R
i : ℕ
⊢ (if i = 0 then 1 else 0) = if i = 0 then ↑1 else 0

Tactic:
OneMemClass.coe_one

Goal state after:
R : Type u_1
inst✝ : Ring R
T : Subring R
i : ℕ
⊢ (if i = 0 then 1 else 0) = if i = 0 then 1 else 0
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case inr.inr.hp
R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ (X - C a).leadingCoeff ^ rootMultiplicity a p ≠ 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : R[X]
r a : R
hr : IsLeftRegular r
h✝ : Nontrivial R
hp : p ≠ 0
q : R[X]
e : p = (X - C a) ^ rootMultiplicity a p * q
hq : ¬X - C a ∣ q
hq0 : q ≠ 0
⊢ (X - C a).leadingCoeff ^ rootMultiplicity a p ≠ 0

Tactic:
simp

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
hf : f.Splits
h : Irreducible f
a✝ : Nontrivial R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) 0).prod
⊢ (C f.leadingCoeff * (Multiset.map (fun x ↦ X + C x) 0).prod).natDegree ≤ 1

Tactic:
simp

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
hf : f.Splits
a✝ : Nontrivial R
a : R
m : Multiset R
hm : f = C f.leadingCoeff * ((X + C a) * (Multiset.map (fun x ↦ X + C x) m).prod)
ha : a ∈ a ::ₘ m
h : (Irreducible (X + C a) ∧ ∀ m_1 ∈ (Multiset.map (fun x ↦ X + C x) m).toList, IsUnit m_1) ∧ IsUnit (C f.leadingCoeff)
this : m = 0
⊢ (C f.leadingCoeff).natDegree + ((X + C a) * (Multiset.map (fun x ↦ X + C x) 0).prod).natDegree ≤ 1

Tactic:
simp

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
hf : f.Splits
hg✝ : g.natDegree ≤ 1
h : Invertible g.leadingCoeff
hg : g.natDegree < 1
⊢ (f.comp (C (g.coeff 0))).Splits

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
N : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
x✝¹ : M
x✝ : B
a✝ : M
⊢ (((AlgebraTensorModule.curry
              (((Algebra.TensorProduct.lift ((IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]).comp includeLeft)
                        (mapAlgHom M includeRight) ⋯).comp
                    rTensorEquivAlgEquiv.invFun).toLinearMap ∘ₗ
                lsingle x✝¹))
            1)
          x✝).coeff
      a✝ =
    (((AlgebraTensorModule.curry ((AlgHom.id A (A ⊗[R] B)[M]).toLinearMap ∘ₗ lsingle x✝¹)) 1) x✝).coeff a✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
x✝¹ : M
x✝ : B
⊢ (((AlgHom.restrictScalars R
                (rTensorEquivAlgEquiv.invFun.comp
                  (Algebra.TensorProduct.lift ((IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]).comp includeLeft)
                    (mapAlgHom M includeRight) ⋯))).comp
            includeRight).toLinearMap ∘ₗ
        lsingle x✝¹)
      x✝ =
    (((AlgHom.restrictScalars R (AlgHom.id A (A ⊗[R] B[M]))).comp includeRight).toLinearMap ∘ₗ lsingle x✝¹) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : R[X]
hf : f.Splits
⊢ (comp 1 (-X)).Splits

Tactic:
simp

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Ring R
f : R[X]
hf : f.Splits
a : R
⊢ ((C a).comp (-X)).Splits

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝ : CommSemiring R
m : M
r₁ : R
n : N
r₂ : R
a✝ : M × N
⊢ ((tensorEquiv R) (single m r₁ ⊗ₜ[R] single n r₂)).coeff a✝ = (single (m, n) (r₁ * r₂)).coeff a✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
hf : f.Splits
hf0 : f.degree ≠ 0
hf₀ : ¬f.leadingCoeff = 0
a : R
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) (a ::ₘ m)).prod
ha : a ∈ a ::ₘ m
⊢ eval a (C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) (a ::ₘ m)).prod) = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf✝ : f.Splits
hf0 : ¬f.leadingCoeff = 0
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
hf : f.roots = m
⊢ f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) f.roots).prod

Tactic:
hf

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf✝ : f.Splits
hf0 : ¬f.leadingCoeff = 0
m : Multiset R
hm : f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
hf : f.roots = m
⊢ f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
f : R[X]
S : Type u_4
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : R →+* S
hi : Function.Injective ⇑i
hf : (map i f).Splits
j : (a : S) → a ∈ (map i f).roots → R
hj : ∀ (a : S) (a_1 : a ∈ (map i f).roots), i (j a a_1) = a
⊢ f.Splits

Tactic:
rw [splits_iff_exists_multiset]

Goal state after:
R : Type u_1
inst✝² : CommRing R
f : R[X]
S : Type u_4
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : R →+* S
hi : Function.Injective ⇑i
hf : (map i f).Splits
j : (a : S) → a ∈ (map i f).roots → R
hj : ∀ (a : S) (a_1 : a ∈ (map i f).roots), i (j a a_1) = a
⊢ ∃ m, f = C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) m).prod
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.Splits
x : R
hr : f.roots = {x}
⊢ C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) {x}).prod =
    C (C f.leadingCoeff * (Multiset.map (fun x ↦ X - C x) {x}).prod).leadingCoeff * (X - C x)

Tactic:
simp

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

Goal state before:
pp: case mem.inl
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R[X]
φ : R →+* S
r : R
hφ : map φ (C r) ≠ 0
⊢ (map φ (C r)).roots = Multiset.map (⇑φ) (C r).roots

Tactic:
simp

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

Goal state before:
pp: case mem.inr
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R[X]
φ : R →+* S
a : R
hφ : map φ (X + C a) ≠ 0
⊢ (map φ (X + C a)).roots = Multiset.map (⇑φ) (X + C a).roots

Tactic:
simp

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

Goal state before:
pp: case one
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : IsDomain S
f : R[X]
φ : R →+* S
hφ : map φ 1 ≠ 0
⊢ (map φ 1).roots = Multiset.map (⇑φ) (roots 1)

Tactic:
simp

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

Goal state before:
pp: case right
R : Type u_1
A : Type u_2
S : Type u_4
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R S
f : A ≃ₐ[R] S
y : S
hy : y ∈ integralClosure R S
⊢ ↑f (f.symm y) = y

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih : ∀ {f g : R[X]}, f ≠ 0 → g ≠ 0 → ∀ (p : R[X]), f * g = p → p.Splits → p.natDegree = n → f.Splits ∧ g.Splits
f g : R[X]
hf₀ : f ≠ 0
hg₀ : g ≠ 0
p : R[X]
hp : f * g = p
h : p.Splits
hn : p.natDegree = n + 1
⊢ n + 1 ≠ Zero.zero

Tactic:
simp

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

Goal state before:
pp: case a.e'_3.a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
this : g = (Multiset.map (fun x ↦ X - C x) g.roots).prod
x : R
hx : x ∈ s
x✝¹ : R
a✝ : x✝¹ ∈ g.roots
x✝ : R
⊢ x - x✝ = (eval x ∘ fun x ↦ X - C x) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
s : Multiset R
g : R[X]
hg : g.Monic
hg' : g.Splits
⊢ (Multiset.map ((fun ij ↦ ij.1 - ij.2) ∘ Prod.swap) (s ×ˢ g.roots)).prod =
    (Multiset.map (fun ij ↦ -1 * (ij.1 - ij.2)) (s ×ˢ g.roots)).prod

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra A B
inst✝⁷ : IsIntegralClosure A R B
A' : Type u_4
inst✝⁶ : CommRing A'
inst✝⁵ : Algebra A' B
inst✝⁴ : IsIntegralClosure A' R B
inst✝³ : Algebra R A
inst✝² : Algebra R A'
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R A' B
x : A'
⊢ (algebraMap A' B) (((lift R A' B).comp (lift R A B)) x) = (algebraMap A' B) ((AlgHom.id R A') x)

Tactic:
simp

Goal state after: