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

Goal state before:
pp: S : Type u_6
R : Type u_7
inst✝⁸ : CommRing R
p : Ideal R
inst✝⁷ : p.IsMaximal
Sₚ : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
⊢ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS) ≤ pS

Tactic:
intro x hx

Goal state after:
S : Type u_6
R : Type u_7
inst✝⁸ : CommRing R
p : Ideal R
inst✝⁷ : p.IsMaximal
Sₚ : Type u_9
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing Sₚ
inst✝³ : Algebra S Sₚ
inst✝² : Algebra R Sₚ
inst✝¹ : IsLocalization (algebraMapSubmonoid S p.primeCompl) Sₚ
inst✝ : IsScalarTower R S Sₚ
x : S
hx : x ∈ comap (algebraMap S Sₚ) (Ideal.map (algebraMap S Sₚ) pS)
⊢ x ∈ pS
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ ⨅ p, ⨅ (x : p.IsPrime), ⨅ (_ : I ≤ p), RingHom.ker (algebraMap R (Localization.AtPrime p)) ≤ I

Tactic:
intro x hx

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
hx : x ∈ ⨅ p, ⨅ (x : p.IsPrime), ⨅ (_ : I ≤ p), RingHom.ker (algebraMap R (Localization.AtPrime p))
⊢ x ∈ I
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
⊢ trunc (C r * T n) = if 0 ≤ n then (monomial n.toNat) r else 0

Tactic:
by
  apply (toFinsuppIso R).injective
  simp only [← single_eq_C_mul_T, trunc, AddMonoidHom.coe_comp, Function.comp_apply,
    RingHom.toAddMonoidHom_eq_coe, RingEquiv.toRingHom_eq_coe,
    AddMonoidHom.coe_coe, RingHom.coe_coe, RingEquiv.apply_symm_apply, toFinsuppIso_apply]
  split_ifs with hn
  · lift n to ℕ using hn
    simp [toFinsupp_monomial, -single_eq_C_mul_T]
  · ext a
    have : a ≠ n := by lia
    simp [-single_eq_C_mul_T, single_eq_of_ne this]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
f g : R[T;T⁻¹]
m : ℕ
fn : R[X]
hf : toLaurent fn = f * T ↑m
n : ℕ
gn : R[X]
hg : toLaurent gn = g * T ↑n
⊢ ∃ n f', toLaurent f' = (f + g) * T ↑n

Tactic:
refine ⟨m + n, fn * X ^ n + gn * X ^ m, ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝ : Semiring R
f g : R[T;T⁻¹]
m : ℕ
fn : R[X]
hf : toLaurent fn = f * T ↑m
n : ℕ
gn : R[X]
hg : toLaurent gn = g * T ↑n
⊢ toLaurent (fn * X ^ n + gn * X ^ m) = (f + g) * T ↑(m + n)
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 = (A.updateCol j (Pi.single i 1)).det

Tactic:
det_apply'

Goal state after:
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
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
e : n ≃ m
A : Matrix m m α
i j : n
this : (fun j ↦ Pi.single i 1 (e.symm j)) = Pi.single (e i) 1
⊢ (A.submatrix ⇑e ⇑e).adjugate i j = A.adjugate.submatrix (⇑e) (⇑e) i j

Tactic:
rw [adjugate_apply, submatrix_apply, adjugate_apply, ← det_submatrix_equiv_self e,
    updateRow_submatrix_equiv, this]

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

Goal state before:
pp: m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
⊢ ∑ σ, ↑↑(Equiv.Perm.sign σ) * ∏ i, (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (σ i) i =
    (fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
        (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j)).det

Tactic:
det_apply'

Goal state after:
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
⊢ ∑ σ, ↑↑(Equiv.Perm.sign σ) * ∏ i, (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (σ i) i =
    ∑ σ,
      ↑↑(Equiv.Perm.sign σ) *
        ∏ i,
          fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
            (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j) (σ i) i
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case neg
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
B : Matrix n n α
hA : ¬IsUnit A.det
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 ↦ x1 * x2) A⁻¹ B⁻¹

pp: case pos
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
B : Matrix n n α
hA : IsUnit A.det
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 ↦ x1 * x2) A⁻¹ B⁻¹

Tactic:
· cases isEmpty_or_nonempty n
    · subsingleton
    have hAB : ¬IsUnit (A ⊗ₖ B).det := by
      refine mt (fun hAB => ?_) hA
      rw [det_kronecker] at hAB
      exact (isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_left hAB)
    rw [nonsing_inv_apply_not_isUnit _ hA, zero_kronecker, nonsing_inv_apply_not_isUnit _ hAB]

Goal state after:
case pos
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
B : Matrix n n α
hA : IsUnit A.det
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B)⁻¹ = kroneckerMap (fun x1 x2 ↦ x1 * x2) A⁻¹ B⁻¹
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
⊢ (matPolyEquiv.symm p i j).coeff k = p.coeff k i j

Tactic:
have t : p = matPolyEquiv (matPolyEquiv.symm p) := by simp
  conv_rhs => rw [t]
  simp only [matPolyEquiv_coeff_apply]

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
⊢ (toFunLinear n R A) ((a₁✝ * a₂✝) ⊗ₜ[R] (b₁✝ * b₂✝)) =
    (toFunLinear n R A) (a₁✝ ⊗ₜ[R] b₁✝) * (toFunLinear n R A) (a₂✝ ⊗ₜ[R] b₂✝)

Tactic:
simp_rw [toFunLinear, lift.tmul, toFunBilinear_apply, Matrix.map_mul]

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
⊢ (a₁✝ * a₂✝) • (b₁✝.map ⇑(algebraMap R A) * b₂✝.map ⇑(algebraMap R A)) =
    a₁✝ • b₁✝.map ⇑(algebraMap R A) * a₂✝ • b₂✝.map ⇑(algebraMap R A)
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:
| tmul a m =>

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

Goal state before:
pp: case neg
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 α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : ¬IsUnit A
hD : ¬IsUnit D
this : ¬IsUnit (fromBlocks A B 0 D)
⊢ 0 = fromBlocks 0 (-0) 0 0

Tactic:
neg_zero,

Goal state after:
case neg
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 α
D : Matrix n n α
hAD : IsUnit A ↔ IsUnit D
hA : ¬IsUnit A
hD : ¬IsUnit D
this : ¬IsUnit (fromBlocks A B 0 D)
⊢ 0 = fromBlocks 0 0 0 0
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
x y : A ⊗[R] Matrix n n R
hx : invFun n R A ((toFunAlgHom n R A) x) = x
hy : invFun n R A ((toFunAlgHom n R A) y) = y
| x + y

Tactic:
rw [← hx, ← hy, ← invFun_add]

Goal state after:
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
x y : A ⊗[R] Matrix n n R
hx : invFun n R A ((toFunAlgHom n R A) x) = x
hy : invFun n R A ((toFunAlgHom n R A) y) = y
| invFun n R A ((toFunAlgHom n R A) x + (toFunAlgHom n R A) y)
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: case neg
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 α
hAD : IsUnit A ↔ IsUnit D
hA : ¬IsUnit A
hD : ¬IsUnit D
this : ¬IsUnit (fromBlocks A 0 C D)
⊢ 0 = fromBlocks 0 0 (-0) 0

Tactic:
neg_zero,

Goal state after:
case neg
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 α
hAD : IsUnit A ↔ IsUnit D
hA : ¬IsUnit A
hD : ¬IsUnit D
this : ¬IsUnit (fromBlocks A 0 C D)
⊢ 0 = fromBlocks 0 0 0 0
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
n : ℕ
z : R
hz : (x + y) ^ (n + 1) = x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2
⊢ (x + y) * (x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2) =
    x ^ (n + 2) + ↑(n + 2) * x ^ (n + 1) * y + (x * z + (↑n + 1) * x ^ n + z * y) * y ^ 2

Tactic:
push_cast
        ring!

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : MonoidWithZero R
e : R
idem : IsIdempotentElem e
n : ℕ
hn : e ^ (n + 1) = 0
⊢ e = 0

Tactic:
rw [← hn, idem.pow_succ_eq]

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

Goal state before:
pp: R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
m n : ℕ
hx : x ^ m = 0
hy : y ^ n = 0
⊢ m + n ≤ m + n - 1 + 1

Tactic:
rw [← Nat.sub_le_iff_le_add]

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

Goal state before:
pp: case mp
ι : 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 ι
A : Matrix ι ι R
f : Module.End R M
h : Represents b A f
i : ι
this : ((PiToModule.fromMatrix R b) A) (Pi.single i 1) = ((PiToModule.fromEnd R b) f) (Pi.single i 1)
⊢ ∑ i_1, A i_1 i • b i_1 = f (b i)

Tactic:
PiToModule.fromEnd_apply_single_one,

Goal state after:
case mp
ι : 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 ι
A : Matrix ι ι R
f : Module.End R M
h : Represents b A f
i : ι
this : ((PiToModule.fromMatrix R b) A) (Pi.single i 1) = f (b i)
⊢ ∑ i_1, A i_1 i • b i_1 = f (b i)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Goal state before:
pp: case mpr
ι : 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 ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), ∑ i, A i j • b i = f (b j)
i✝ : ι
⊢ ((PiToModule.fromMatrix R b) A) (Pi.single i✝ 1) = ((PiToModule.fromEnd R b) f) (Pi.single i✝ 1)

Tactic:
PiToModule.fromEnd_apply_single_one,

Goal state after:
case mpr
ι : 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 ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), ∑ i, A i j • b i = f (b j)
i✝ : ι
⊢ ((PiToModule.fromMatrix R b) A) (Pi.single i✝ 1) = f (b i✝)
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
⊢ map f p ≤ span S (⇑f '' p.generators)

Tactic:
by simp [span_generators]

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
hf : Function.Injective ⇑f
p : Submodule R M
⊢ Cardinal.toNat (Cardinal.lift.{u, v} (map f p).spanRank) = Cardinal.toNat p.spanRank

Tactic:
← Cardinal.toNat_lift.{v, u},

Goal state after:
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
hf : Function.Injective ⇑f
p : Submodule R M
⊢ Cardinal.toNat (Cardinal.lift.{u, v} (map f p).spanRank) = Cardinal.toNat (Cardinal.lift.{v, u} p.spanRank)
Module: Mathlib.Algebra.Module.SpanRank

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
T : Type v
inst✝ : Semiring T
f : R ≃+* T
I : Ideal R
⊢ Cardinal.toNat (Cardinal.lift.{u, v} (Submodule.spanRank (map f I))) = Cardinal.toNat (Submodule.spanRank I)

Tactic:
← Cardinal.toNat_lift.{v, u},

Goal state after:
R : Type u
inst✝¹ : Semiring R
T : Type v
inst✝ : Semiring T
f : R ≃+* T
I : Ideal R
⊢ Cardinal.toNat (Cardinal.lift.{u, v} (Submodule.spanRank (map f I))) =
    Cardinal.toNat (Cardinal.lift.{v, u} (Submodule.spanRank I))
Module: Mathlib.Algebra.Polynomial.Eval.Subring

Goal state before:
pp: case h
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
i : ℕ
_hi : i ∈ Finset.range (p.natDegree + 1)
c : R
hc : f c = p.coeff i
⊢ C (p.coeff i) * map f (X ^ i) = C (p.coeff i) * X ^ i

Tactic:
Polynomial.map_pow,

Goal state after:
case h
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
i : ℕ
_hi : i ∈ Finset.range (p.natDegree + 1)
c : R
hc : f c = p.coeff i
⊢ C (p.coeff i) * map f X ^ i = C (p.coeff i) * X ^ i
Module: Mathlib.Algebra.Polynomial.Lifts

Goal state before:
pp: R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
hp : p.Monic
g : ℕ → R := fun k ↦ Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := X ^ p.natDegree + ∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k
⊢ map f (X ^ p.natDegree) + ∑ x ∈ Finset.range p.natDegree, map f (C (g x)) * map f (X ^ x) = p

Tactic:
Polynomial.map_pow,

Goal state after:
R : Type u
inst✝² : Semiring R
S : Type v
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Nontrivial S
p : S[X]
hlifts : ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
hp : p.Monic
g : ℕ → R := fun k ↦ Exists.choose ⋯
hg : ∀ (k : ℕ), f (g k) = p.coeff k
q : R[X] := X ^ p.natDegree + ∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k
⊢ map f X ^ p.natDegree + ∑ x ∈ Finset.range p.natDegree, map f (C (g x)) * map f X ^ x = p
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
I : Ideal R
h : ∀ (i j : n), M i j ∈ I
k : ℕ
⊢ M.charpoly.coeff k ∈ I ^ (Fintype.card n - k)

Tactic:
by
  delta charpoly
  rw [Matrix.det_apply, finsetSum_coeff]
  apply sum_mem
  rintro c -
  rw [coeff_smul, Submodule.smul_mem_iff']
  have : ∑ x : n, 1 = Fintype.card n := by rw [Finset.sum_const, card_univ, smul_eq_mul, mul_one]
  rw [← this]
  apply coeff_prod_mem_ideal_pow_tsub
  rintro i - (_ | k)
  · rw [tsub_zero, pow_one, charmatrix_apply, coeff_sub, ← smul_one_eq_diagonal, smul_apply,
      smul_eq_mul, coeff_X_mul_zero, coeff_C_zero, zero_sub, neg_mem_iff]
    exact h (c i) i
  · rw [add_comm, tsub_self_add, pow_zero, Ideal.one_eq_top]
    exact Submodule.mem_top

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 * ((-1) ^ Fintype.card n * (1 - (scalar n) X * C.mapMatrix A).det) =
    (-1) ^ Fintype.card n * C A.det⁻¹ʳ * A.charpolyRev

Tactic:
simp [charpolyRev, smul_eq_diagonal_mul]; ac_rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
⊢ ∀ x ∈ antidiagonal k,
    (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
      (monomial (m + n - k)) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))

Tactic:
intro x hx

Goal state after:
R : Type u_1
inst✝ : Semiring R
k : ℕ
D : ℕ → R[X] →+ R[X] := fun k ↦ (hasseDeriv k).toAddMonoidHom
Φ : R[X] →+ R[X] →+ R[X] := mul
m : ℕ
r : R
n : ℕ
s : R
x : ℕ × ℕ
hx : x ∈ antidiagonal k
⊢ (monomial (m - x.1 + (n - x.2))) (↑(m.choose x.1) * r * (↑(n.choose x.2) * s)) =
    (monomial (m + n - k)) (↑(m.choose x.1) * ↑(n.choose x.2) * (r * s))
Module: Mathlib.RingTheory.Polynomial.ScaleRoots

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : p = 0
⊢ (p.scaleRoots s).degree = p.degree

pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ (p.scaleRoots s).degree = p.degree

Tactic:
· rw [hp, zero_scaleRoots]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ (p.scaleRoots s).degree = p.degree
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
k : ℕ
hk : k ≤ Fintype.card n
a✝ : Nontrivial R
hnd : M.charpoly.natDegree = Fintype.card n
hrev : M.charpoly.coeff (Fintype.card n - k) = M.charpoly.reverse.coeff k
⊢ M.charpoly.coeff (Fintype.card n - k) =
    (-1) ^ k * ∑ s ∈ powersetCard k univ, (M.submatrix Subtype.val Subtype.val).det

Tactic:
hrev,

Goal state after:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
k : ℕ
hk : k ≤ Fintype.card n
a✝ : Nontrivial R
hnd : M.charpoly.natDegree = Fintype.card n
hrev : M.charpoly.coeff (Fintype.card n - k) = M.charpoly.reverse.coeff k
⊢ M.charpoly.reverse.coeff k = (-1) ^ k * ∑ s ∈ powersetCard k univ, (M.submatrix Subtype.val Subtype.val).det
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
⊢ (p.toSubring T hp).coeff p.natDegree = 1 ↔ ↑((p.toSubring T hp).coeff p.natDegree) = 1

Tactic:
exact ⟨fun H => by rw [H, OneMemClass.coe_one], fun H => Subtype.coe_injective H⟩

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:
apply_ite Subtype.val,

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.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ ↑J
hrI : r ∉ ↑I
rbar_ne_zero : (Quotient.mk I) r ≠ 0
rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J
⊢ ∀ x ∈ comap f I, ((Quotient.mk I).comp f) x = 0

Tactic:
simp [Quotient.eq_zero_iff_mem]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
f : R →+* S
I J : Ideal S
inst✝ : I.IsPrime
hIJ : I ≤ J
r : S
p : R[X]
p_ne_zero : Polynomial.map (Quotient.mk (comap f I)) p ≠ 0
hpI : eval₂ f r p ∈ I
hrJ : r ∈ ↑J
hrI : r ∉ ↑I
rbar_ne_zero : (Quotient.mk I) r ≠ 0
rbar_mem_J : (Quotient.mk I) r ∈ map (Quotient.mk I) J
quotient_f : ∀ x ∈ comap f I, ((Quotient.mk I).comp f) x = 0
rbar_root :
  eval₂ (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) ((Quotient.mk I) r)
      (Polynomial.map (Quotient.mk (comap f I)) p) =
    0
i : ℕ
ne_zero : (Quotient.mk (comap f I)) (p.coeff i) ≠ 0
mem :
  (Quotient.mk (comap f I)) (p.coeff i) ∈
    comap (Quotient.lift (comap f I) ((Quotient.mk I).comp f) quotient_f) (map (Quotient.mk I) J)
⊢ p.coeff i ∈ ↑(comap f I) → (Quotient.mk (comap f I)) (p.coeff i) = 0

Tactic:
simp [Quotient.eq_zero_iff_mem]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
p : (↥R[s])[X]
hpm : p.Monic
hpt : eval₂ (algebraMap (↥R[s]) S) t p = 0
this : Polynomial.map (algebraMap (↥R[s]) S) p ∈ lifts φ.toRingHom
q : R[X][X]
hqp : Polynomial.map φ.toRingHom q = Polynomial.map (algebraMap (↥R[s]) S) p
hqd : q.degree = (Polynomial.map (algebraMap (↥R[s]) S) p).degree
hqm : q.Monic
⊢ eval₂ (algebraMap (↥R[s]) S) t p = 0

Tactic:
hpt

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
p : (↥R[s])[X]
hpm : p.Monic
hpt : eval₂ (algebraMap (↥R[s]) S) t p = 0
this : Polynomial.map (algebraMap (↥R[s]) S) p ∈ lifts φ.toRingHom
q : R[X][X]
hqp : Polynomial.map φ.toRingHom q = Polynomial.map (algebraMap (↥R[s]) S) p
hqd : q.degree = (Polynomial.map (algebraMap (↥R[s]) S) p).degree
hqm : q.Monic
⊢ 0 = 0
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case refine_1.refine_2.h₁
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ q.natDegree ∉ q.support →
    (if q.natDegree ≤ q.natDegree + N then (q.coeff q.natDegree).coeff ((revAt N) (q.natDegree + N - q.natDegree))
      else 0) =
      0

Tactic:
simp +contextual

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), x ∉ zeroLocus s

Tactic:
intro x hx

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : x ∈ zeroLocus s
⊢ False