mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: case refine_1
R✝ : Type u_1
inst✝¹⁸ : CommSemiring R✝
S✝ : Type u_2
inst✝¹⁷ : CommSemiring S✝
inst✝¹⁶ : Algebra R✝ S✝
P✝ : Type u_3
inst✝¹⁵ : CommSemiring P✝
p✝ : Ideal R✝
inst✝¹⁴ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝¹³ : CommSemiring Rₚ✝
inst✝¹² : Algebra R✝ Rₚ✝
inst✝¹¹ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁰ : IsLocalRing Rₚ✝
Sₚ : Type u_5
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra S✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ✝ Sₚ
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
n : ℕ
⊢ ∀ a ∈ p ^ n, (ofId R (Rₚ ⧸ maximalIdeal Rₚ ^ n)) a = 0

Tactic:
simp_rw [ofId_apply, ← RingHom.mem_ker, ← SetLike.le_def]

Goal state after:
case refine_1
R✝ : Type u_1
inst✝¹⁸ : CommSemiring R✝
S✝ : Type u_2
inst✝¹⁷ : CommSemiring S✝
inst✝¹⁶ : Algebra R✝ S✝
P✝ : Type u_3
inst✝¹⁵ : CommSemiring P✝
p✝ : Ideal R✝
inst✝¹⁴ : p✝.IsPrime
Rₚ✝ : Type u_4
inst✝¹³ : CommSemiring Rₚ✝
inst✝¹² : Algebra R✝ Rₚ✝
inst✝¹¹ : IsLocalization.AtPrime Rₚ✝ p✝
inst✝¹⁰ : IsLocalRing Rₚ✝
Sₚ : Type u_5
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra S✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ✝ Sₚ
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
n : ℕ
⊢ p ^ n ≤ RingHom.ker (algebraMap R (Rₚ ⧸ maximalIdeal Rₚ ^ n))
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : EssFiniteType R S
f g : S →ₐ[R] T
H : ∀ s ∈ finset R S, f s = g s
this : f.comp (IsScalarTower.toAlgHom R ?m.97 S) = g.comp (IsScalarTower.toAlgHom R ?m.97 S)
⊢ f.comp (algebraMap (↥(subalgebra R S)) S) = g.comp (algebraMap (↥(subalgebra R S)) S)

Tactic:
ext; exact AlgHom.congr_fun this _

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

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ A.adjugate i j = (A.updateRow j (Pi.single i 1)).det

Tactic:
adjugate_def,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ of (fun i ↦ Aᵀ.cramer (Pi.single i 1)) i j = (A.updateRow j (Pi.single i 1)).det
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
n : ℤ
h : ∀ (s : ℤ), ¬f.coeff s = 0 → ↑s = ⊥
⊢ f.coeff n = 0

Tactic:
WithBot.coe_ne_bot,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
n : ℤ
h : ∀ (s : ℤ), ¬f.coeff s = 0 → False
⊢ f.coeff n = 0
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ ∑ σ, ↑↑(sign σ) * ∏ i_1, A.updateRow i (Pi.single j 1) (σ i_1) i_1 =
    ∑ σ, ↑↑(sign σ) * ∏ i_1, A.updateCol j (Pi.single i 1) (σ i_1) i_1

Tactic:
apply Finset.sum_congr rfl

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ ∀ x ∈ univ,
    ↑↑(sign x) * ∏ i_1, A.updateRow i (Pi.single j 1) (x i_1) i_1 =
      ↑↑(sign x) * ∏ i_1, A.updateCol j (Pi.single i 1) (x i_1) i_1
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℤ
⊢ (T n).degree = ↑n

Tactic:
by
  rw [← one_mul (T n), ← map_one C]
  exact degree_C_mul_T n 1 (one_ne_zero : (1 : R) ≠ 0)

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

Goal state before:
pp: n : Type u_3
R : Type u_6
inst✝² : Fintype n
ι : Type u_8
inst✝¹ : Unique ι
inst✝ : NonUnitalNonAssocSemiring R
a b : n → R
⊢ (replicateCol ι a * replicateRow ι b).trace = a ⬝ᵥ b

Tactic:
apply Finset.sum_congr rfl

Goal state after:
n : Type u_3
R : Type u_6
inst✝² : Fintype n
ι : Type u_8
inst✝¹ : Unique ι
inst✝ : NonUnitalNonAssocSemiring R
a b : n → R
⊢ ∀ x ∈ Finset.univ, (replicateCol ι a * replicateRow ι b).diag x = a x * b x
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ A.adjugate =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
      -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
      A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]

Tactic:
by
  ext i j
  rw [adjugate_fin_succ_eq_det_submatrix, det_fin_two]
  fin_cases i <;> fin_cases j <;> simp [Fin.succAbove, Fin.lt_def] <;> ring

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

Goal state before:
pp: α : Type u_3
l : Type u_9
m : Type u_10
n : Type u_11
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq l
a : ℕ
B : Matrix m n α
⊢ (reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (blockDiagonal fun i ↦ ↑a •> B) =
    (reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (blockDiagonal fun x ↦ a •> B)

Tactic:
congr! 2
    ext
    simp [(Nat.cast_commute a _).eq]

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

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ (A * B).adjugate = B.adjugate * A.adjugate

Tactic:
let g : Matrix n n α → Matrix n n α[X] := fun M =>
    M.map Polynomial.C + (Polynomial.X : α[X]) • (1 : Matrix n n α[X])

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M ↦ M.map ⇑C + X • 1
⊢ (A * B).adjugate = B.adjugate * A.adjugate
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: case e_a.e_a.e_a
m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝¹ : Invertible A
inst✝ : Invertible (C + C * V * ⅟A * U * C)
⊢ ⅟(C + C * V * ⅟A * U * C) * (C * (V * (⅟A * A)) + C * (V * (⅟A * (U * (C * V))))) = V

Tactic:
Matrix.invOf_mul_eq_iff_eq_mul_left

Goal state after:
case e_a.e_a.e_a
m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝¹ : Invertible A
inst✝ : Invertible (C + C * V * ⅟A * U * C)
⊢ C * (V * (⅟A * A)) + C * (V * (⅟A * (U * (C * V)))) = (C + C * V * ⅟A * U * C) * V
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
⊢ ((⅟(diagonal v)).diag * v) i = 1 i

Tactic:
let : Invertible (diagonal v).det := detInvertibleOfInvertible _

Goal state after:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
⊢ ((⅟(diagonal v)).diag * v) i = 1 i
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
⊢ (v * (⅟(diagonal v)).diag) i = 1 i

Tactic:
let : Invertible (diagonal v).det := detInvertibleOfInvertible _

Goal state after:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (diagonal v).det := (diagonal v).detInvertibleOfInvertible
⊢ (v * (⅟(diagonal v)).diag) i = 1 i
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case inr
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H : ¬∀ (i : Unit) (j : Fin r), of (fun i j ↦ M (inr i) (inl j)) i j = 0 i j
⊢ ∃ i, M (inl i) (inr ()) ≠ 0 ∨ M (inr ()) (inl i) ≠ 0

Tactic:
contrapose! H
      rintro ⟨⟩ j
      exact (H j).2

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
e : n ≃ m
M : Matrix n n R
⊢ ((reindex e e) M).charpoly = M.charpoly

Tactic:
by
  unfold Matrix.charpoly
  rw [charmatrix_reindex, Matrix.det_reindex_self]

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
α : Type u_5
b : n → α
inst✝ : LinearOrder α
h : M.BlockTriangular b
⊢ M.charpoly = ∏ a ∈ image b univ, (M.toSquareBlock b a).charpoly

Tactic:
by
  simp only [Matrix.charpoly, h.charmatrix.det, charmatrix_toSquareBlock]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
C : Matrix n m α
D : Matrix n n α
inst✝² : Invertible A
inst✝¹ : Invertible D
inst✝ : Invertible (fromBlocks A 0 C D)
⊢ ⅟(fromBlocks A 0 C D) = fromBlocks (⅟A) 0 (-(⅟D * C * ⅟A)) ⅟D

Tactic:
let := fromBlocksZero₁₂Invertible A C D
  convert! (rfl : ⅟(fromBlocks A 0 C D) = _)

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✝¹ : DecidableEq n
inst✝ : Fintype n
a₁✝ a₂✝ : A
b₁✝ b₂✝ : Matrix n n R
⊢ (TensorProduct.lift (toFunBilinear n R A)) ((a₁✝ * a₂✝) ⊗ₜ[R] (b₁✝ * b₂✝)) =
    (TensorProduct.lift (toFunBilinear n R A)) (a₁✝ ⊗ₜ[R] b₁✝) *
      (TensorProduct.lift (toFunBilinear n R A)) (a₂✝ ⊗ₜ[R] b₂✝)

Tactic:
lift.tmul,

Goal state after:
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✝¹ : DecidableEq n
inst✝ : Fintype n
a₁✝ a₂✝ : A
b₁✝ b₂✝ : Matrix n n R
⊢ ((toFunBilinear n R A) (a₁✝ * a₂✝)) (b₁✝ * b₂✝) = ((toFunBilinear n R A) a₁✝) b₁✝ * ((toFunBilinear n R A) a₂✝) b₂✝
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✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ (TensorProduct.lift (toFunBilinear n R A)) (1 ⊗ₜ[R] 1) = 1

Tactic:
lift.tmul,

Goal state after:
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✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ ((toFunBilinear n R A) 1) 1 = 1
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: 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
⊢ invFun n R A (M.map ⇑(algebraMap R A)) = 1 ⊗ₜ[R] M

Tactic:
dsimp [invFun]
  simp only [Algebra.algebraMap_eq_smul_one, smul_tmul, ← tmul_sum]
  congr
  conv_rhs => rw [matrix_eq_sum_single M]
  convert! Finset.sum_product (β := Matrix n n R) ..; simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝² : Invertible D
inst✝¹ : Invertible (A - B * ⅟D * C)
inst✝ : Invertible (fromBlocks A B C D)
⊢ ⅟(fromBlocks A B C D) =
    fromBlocks (⅟(A - B * ⅟D * C)) (-(⅟(A - B * ⅟D * C) * B * ⅟D)) (-(⅟D * C * ⅟(A - B * ⅟D * C)))
      (⅟D + ⅟D * C * ⅟(A - B * ⅟D * C) * B * ⅟D)

Tactic:
let := fromBlocks₂₂Invertible A B C D
  convert! (rfl : ⅟(fromBlocks A B C D) = _)

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Subalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
⊢ (↑I).FG

Tactic:
by
  obtain ⟨T, T', hT, hT', one_mem⟩ := mem_span_mul_finite_of_mem_mul (I.mul_inv ▸ one_le.mp le_rfl)
  refine ⟨T, span_eq_of_le _ hT ?_⟩
  rw [← one_mul I, ← mul_one (span R (T : Set A))]
  conv_rhs => rw [← I.inv_mul, ← mul_assoc]
  grw [← span_le.mpr hT', Units.val_mul, Units.val_one, span_mul_span, one_le.2 one_mem]

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
c : n ≃ n
hc : c ∈ univ.erase (Equiv.refl n)
⊢ C ↑↑(Equiv.Perm.sign c) * ∏ i, M.charmatrix (c i) i ∈ degreeLT R (Fintype.card n - 1)

Tactic:
C_mul'

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
c : n ≃ n
hc : c ∈ univ.erase (Equiv.refl n)
⊢ ↑↑(Equiv.Perm.sign c) • ∏ i, M.charmatrix (c i) i ∈ degreeLT R (Fintype.card n - 1)
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
⊢ ⊥.spanFinrank = 0

Tactic:
by simp [spanFinrank]

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
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ (∏ i, (X - C (M i i))).natDegree = Fintype.card n

Tactic:
natDegree_prod'

Goal state after:
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
⊢ ∑ i, (X - C (M i i)).natDegree = Fintype.card n

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
⊢ ∏ i, (X - C (M i i)).leadingCoeff ≠ 0
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
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∑ i, (X - C (M i i)).natDegree = Fintype.card n

Tactic:
natDegree_X_sub_C

Goal state after:
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 = Fintype.card n
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
inst✝ : Nonempty n
M : Matrix n n R
⊢ M.trace = -M.charpoly.coeff (Fintype.card n - 1)

Tactic:
by
  rw [charpoly_coeff_eq_prod_coeff_of_le _ le_rfl, Fintype.card,
    prod_X_sub_C_coeff_card_pred univ (fun i : n => M i i) Fintype.card_pos, neg_neg, trace]
  simp_rw [diag_apply]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Vandermonde

Goal state before:
pp: m n k : ℕ
⊢ ∑ x ∈ antidiagonal k, ((X + 1) ^ m).coeff x.1 * ((X + 1) ^ n).coeff x.2 =
    ∑ ij ∈ antidiagonal k, m.choose ij.1 * n.choose ij.2

Tactic:
Finset.sum_congr rfl

Goal state after:
m n k : ℕ
⊢ (antidiagonal k).sum ?m.136 = ∑ ij ∈ antidiagonal k, m.choose ij.1 * n.choose ij.2

m n k : ℕ
⊢ ∀ x ∈ antidiagonal k, ((X + 1) ^ m).coeff x.1 * ((X + 1) ^ n).coeff x.2 = ?m.136 x

m n k : ℕ
⊢ ℕ × ℕ → ℕ
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case h₁
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
n : ℕ
⊢ n + k ∉ f.support → ((monomial (n + k - k)) (↑((n + k).choose k) * f.coeff (n + k))).coeff n = 0

Tactic:
· intro h
    simp only [notMem_support_iff.mp h, monomial_zero_right, mul_zero, coeff_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k l : ℕ
⊢ hasseDeriv k ∘ₗ hasseDeriv l = (k + l).choose k • hasseDeriv (k + l)

Tactic:
ext i : 2

Goal state after:
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
⊢ ((hasseDeriv k ∘ₗ hasseDeriv l) ∘ₗ monomial i) 1 = (((k + l).choose k • hasseDeriv (k + l)) ∘ₗ monomial i) 1
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ max (if {x ∈ p.support | ↑(x.choose n) * p.coeff x = 0} = ∅ then 0 else max 0 0)
      (Finset.fold max 0 (fun x ↦ x - n) ({i ∈ p.support | ¬↑(i.choose n) * p.coeff i = 0})) ≤
    p.natDegree - n

Tactic:
simp only [ite_self, max_eq_right, zero_le, Finset.fold_max_le, true_and, and_imp,
        tsub_le_iff_right, mem_support_iff, Ne, Finset.mem_filter]

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ ∀ (x : ℕ), ¬p.coeff x = 0 → ¬↑(x.choose n) * p.coeff x = 0 → x ≤ p.natDegree - n + n
Module: Mathlib.Algebra.Polynomial.Taylor

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
r : R
⊢ ((taylor r) p).natDegree = p.natDegree

Tactic:
by
  refine map_natDegree_eq_natDegree _ ?_
  nontriviality R
  intro n c c0
  simp [taylor_monomial, natDegree_C_mul_of_mul_ne_zero, natDegree_pow_X_add_C, c0]

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
n : ℕ
⊢ ∑ i ∈ Finset.antidiagonal n, p.coeff i.1 * q.coeff i.2 * r ^ (p.natDegree + q.natDegree - n) =
    ∑ x ∈ Finset.antidiagonal n, (p.scaleRoots r).coeff x.1 * (q.scaleRoots r).coeff x.2

Tactic:
apply Finset.sum_congr rfl

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
n : ℕ
⊢ ∀ x ∈ Finset.antidiagonal n,
    p.coeff x.1 * q.coeff x.2 * r ^ (p.natDegree + q.natDegree - n) =
      (p.scaleRoots r).coeff x.1 * (q.scaleRoots r).coeff x.2
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
f : R[X]
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
hf : (map (algebraMap R A) f).Splits
e : A →ₐ[R] B
⊢ (map (↑e) (map (algebraMap R A) f)).Splits

Tactic:
apply hf.map

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
hm : f.Monic
x : R
⊢ eval x f = (Multiset.map (fun x_1 ↦ x - x_1) f.roots).prod

Tactic:
simp [hf.eval_eq_prod_roots, hm]

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
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : (X - C a) * f ≠ 0
this : X - C a ∣ (X - C a) * f ∨ X - C a ∣ g
h : ((X - C a) * (f * g)).Splits
hn : (X - C a).natDegree + (f * g).natDegree = n + 1
ha : eval a ((X - C a) * (f * g)) = 0
⊢ ((X - C a) * f).Splits ∧ g.Splits

Tactic:
natDegree_X_sub_C,

Goal state after:
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
g : R[X]
hg₀ : g ≠ 0
a : R
f : R[X]
hf₀ : (X - C a) * f ≠ 0
this : X - C a ∣ (X - C a) * f ∨ X - C a ∣ g
h : ((X - C a) * (f * g)).Splits
hn : 1 + (f * g).natDegree = n + 1
ha : eval a ((X - C a) * (f * g)) = 0
⊢ ((X - C a) * f).Splits ∧ g.Splits
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
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Algebra S B
inst✝² : IsScalarTower R S B
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
isIntegral : Algebra.IsIntegral R S
x y : S
⊢ mk' A ((algebraMap S B) (x + y)) ⋯ = mk' A ((algebraMap S B) x) ⋯ + mk' A ((algebraMap S B) y) ⋯

Tactic:
by simp_rw [← mk'_add, map_add]

Goal state after:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : n = p.natDegree
⊢ p.coeff p.natDegree * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - p.natDegree) ∈
    Set.range ⇑(algebraMap R Rₘ)

Tactic:
Polynomial.coeff_natDegree,

Goal state after:
case pos
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
Rₘ : Type u_3
inst✝² : CommRing Rₘ
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
p : Rₘ[X]
hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range
n : ℕ
h₁ : n ∈ p.support
h₂ : n = p.natDegree
⊢ p.leadingCoeff * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - p.natDegree) ∈
    Set.range ⇑(algebraMap R Rₘ)
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
a b : R
hg : (C a * X + C b).natDegree = 1
hf : (f.comp (C a * X + C b)).Splits
ha : a ≠ 0
this : f = (f.comp (C a * X + C b)).comp (C a⁻¹ * (X - C b))
⊢ (X - C b).natDegree ≤ 1

Tactic:
natDegree_X_sub_C

Goal state after:
R : Type u_1
inst✝ : Field R
f : R[X]
a b : R
hg : (C a * X + C b).natDegree = 1
hf : (f.comp (C a * X + C b)).Splits
ha : a ≠ 0
this : f = (f.comp (C a * X + C b)).comp (C a⁻¹ * (X - C b))
⊢ 1 ≤ 1
Module: Mathlib.Algebra.Polynomial.Splits

Goal state before:
pp: R : Type u_1
inst✝ : Field R
f : R[X]
x : R
h₁ : f.natDegree = 2
h₂ : eval x f = 0
⊢ 2 - (X - C x).natDegree = 1

Tactic:
natDegree_X_sub_C

Goal state after:
R : Type u_1
inst✝ : Field R
f : R[X]
x : R
h₁ : f.natDegree = 2
h₂ : eval x f = 0
⊢ 2 - 1 = 1
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case inr.refine_2
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
Rₘ : Type u_3
inst✝⁴ : CommRing Rₘ
inst✝³ : Algebra R Rₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : Algebra Rₘ S
inst✝ : IsScalarTower R Rₘ S
x : S
nontriv : Nontrivial Rₘ
p : Rₘ[X]
hp₁ : p.Monic
hp₂ : eval₂ (algebraMap Rₘ S) x p = 0
⊢ (p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff))).Monic

Tactic:
rwa [Polynomial.monic_scaleRoots_iff]

Goal state after:
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
S : Type u_2
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Algebra.IsIntegral R S
P : Ideal R
inst✝¹ : P.IsPrime
I : Ideal S
inst✝ : I.IsPrime
hIP : comap (algebraMap R S) I ≤ P
⊢ RingHom.ker (Quotient.mk (comap (algebraMap R S) I)) ≤ P

Tactic:
simp [hIP]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
⊢ False

Tactic:
have x_prime : x.asIdeal.IsPrime := by infer_instance

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
x_prime : x.asIdeal.IsPrime
⊢ False