mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: case monomial
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
i : ℤ
n : ℕ
r : R
⊢ eval (↑i) (map f ((monomial n) r)) = f (eval (↑i) ((monomial n) r))

Tactic:
simp only [map_intCast, eval_monomial, map_monomial, map_pow, map_mul]

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ R[ X] = ⊤

Tactic:
by
  refine top_unique fun p _hp => ?_
  set S := adjoin R ({X} : Set R[X])
  rw [← sum_monomial_eq p]; simp only [← smul_X_eq_monomial]
  exact S.sum_mem fun n _hn => S.smul_mem (S.pow_mem (subset_adjoin rfl) _) _

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
r : R
hr : r ∈ nonZeroDivisors R
⊢ p.comp (C r * X) = 0 ↔ p = 0

Tactic:
ext_iff

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
r : R
hr : r ∈ nonZeroDivisors R
⊢ (∀ (n : ℕ), (p.comp (C r * X)).coeff n = coeff 0 n) ↔ ∀ (n : ℕ), p.coeff n = coeff 0 n
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: case hf
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : (map φ f).degree = 0
⊢ φ f.leadingCoeff ≠ 0

Tactic:
intro h

Goal state after:
case hf
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hf : IsUnit f.leadingCoeff
H : IsUnit (map φ f)
dz : (map φ f).degree = 0
h : φ f.leadingCoeff = 0
⊢ False
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: case mp
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
⊢ x + y = single a n → ∃ a_2 b, a_2 + b = n ∧ single a a_2 = x ∧ single a b = y

Tactic:
intro h

Goal state after:
case mp
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : x + y = single a n
⊢ ∃ a_1 b, a_1 + b = n ∧ single a a_1 = x ∧ single a b = y
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
S : Type v
T : Type w
A : Type z
A' : Type u_1
B : Type u_2
a b : R
n : ℕ
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
p q r : R[X]
inst✝ : Nontrivial A
⊢ ⊥ ≠ ⊤

Tactic:
rw [Ne, SetLike.ext_iff, not_forall]
      refine ⟨X, ?_⟩
      simp only [Algebra.mem_bot, not_exists, Set.mem_range, iff_true, Algebra.mem_top,
        algebraMap_apply]
      intro x
      rw [ext_iff, not_forall]
      refine ⟨1, ?_⟩
      simp

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: case mpr
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : Zero α
inst✝¹ : LE α
inst✝ : Std.Refl fun x1 x2 ↦ x1 ≤ x2
f : ι ↪ κ
g₁ g₂ : ι →₀ α
⊢ g₁ ≤ g₂ → embDomain f g₁ ≤ embDomain f g₂

Tactic:
intro h

Goal state after:
case mpr
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : Zero α
inst✝¹ : LE α
inst✝ : Std.Refl fun x1 x2 ↦ x1 ≤ x2
f : ι ↪ κ
g₁ g₂ : ι →₀ α
h : g₁ ≤ g₂
⊢ embDomain f g₁ ≤ embDomain f g₂
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : Preorder α
inst✝ : IsOrderedAddMonoid α
f : ι → κ
g : ι →₀ α
hg : 0 ≤ g
⊢ 0 ≤ mapDomain f g

Tactic:
simpa using mapDomain_mono hg

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : Preorder α
inst✝ : IsOrderedAddMonoid α
f : ι → κ
g : ι →₀ α
hg : g ≤ 0
⊢ mapDomain f g ≤ 0

Tactic:
simpa using mapDomain_mono hg

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
t : R
⊢ (algEquivAevalXAddC t).symm = algEquivAevalXAddC (-t)

Tactic:
simp [algEquivAevalXAddC, sub_eq_add_neg]

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: case refine_1
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
j : ι
hj : (fun x1 x2 ↦ x1 < x2) j i
⊢ a₁✝ j = Function.update a₂ i a j

Tactic:
rw [h j hj]
        dsimp only at hj
        rw [Function.update_of_ne hj.ne a]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
r : R
⊢ eval₂ f (f r) p = 0 → p.IsRoot r

Tactic:
intro h

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ⇑f
r : R
h : eval₂ f (f r) p = 0
⊢ p.IsRoot r
Module: Mathlib.Data.DFinsupp.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → AddCommMonoid (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝¹ : (i : ι) → Sub (α i)
inst✝ : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
⊢ ⇑(f - g) = ⇑f - ⇑g

Tactic:
by
  ext i
  exact tsub_apply f g i

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
⊢ coeff m (C a * p) = a * coeff m p

Tactic:
mul_def,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
⊢ coeff m ((C a).coeff.sum fun m a ↦ p.coeff.sum fun n b ↦ (monomial (m + n)) (a * b)) = a * coeff m p
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
⊢ (∀ (i : σ →₀ ℕ), r ∣ coeff i φ) → C r ∣ φ

Tactic:
intro h

Goal state after:
case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
h : ∀ (i : σ →₀ ℕ), r ∣ coeff i φ
⊢ C r ∣ φ
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
n : σ
inst✝ : CommSemiring R
⊢ IsRegular (X n)

Tactic:
by
  suffices IsLeftRegular (X n : MvPolynomial σ R) from
    ⟨this, this.right_of_commute <| Commute.all _⟩
  intro P Q (hPQ : (X n) * P = (X n) * Q)
  ext i
  rw [← coeff_X_mul i n P, hPQ, coeff_X_mul i n Q]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f : MvPolynomial σ R
d : ℕ
h : 0 < d
⊢ degreeOf n f < d ↔ ∀ m ∈ f.support, m n < d

Tactic:
degreeOf_eq_sup,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f : MvPolynomial σ R
d : ℕ
h : 0 < d
⊢ (f.support.sup fun m ↦ m n) < d ↔ ∀ m ∈ f.support, m n < d
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f : MvPolynomial σ R
d : ℕ
⊢ degreeOf n f ≤ d ↔ ∀ m ∈ f.support, m n ≤ d

Tactic:
degreeOf_eq_sup,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f : MvPolynomial σ R
d : ℕ
⊢ (f.support.sup fun m ↦ m n) ≤ d ↔ ∀ m ∈ f.support, m n ≤ d
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
s : σ →₀ ℕ
h : s ∈ p.support
si : 0 < s i
⊢ s i ≤ degreeOf i p

Tactic:
degreeOf_eq_sup,

Goal state after:
case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
s : σ →₀ ℕ
h : s ∈ p.support
si : 0 < s i
⊢ s i ≤ p.support.sup fun m ↦ m i
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ 0 i = 0

Tactic:
simp only [coe_zero, Pi.zero_apply]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
x : σ
f g : MvPolynomial σ R
k : ℕ
h : 0 < k
hf : ∀ m ∈ f.support, k ≤ m x → coeff m f = coeff m g
hg : ∀ m ∈ g.support, k ≤ m x → coeff m f = coeff m g
⊢ degreeOf x (f - g) < k

Tactic:
degreeOf_lt_iff h

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommRing R
x : σ
f g : MvPolynomial σ R
k : ℕ
h : 0 < k
hf : ∀ m ∈ f.support, k ≤ m x → coeff m f = coeff m g
hg : ∀ m ∈ g.support, k ≤ m x → coeff m f = coeff m g
⊢ ∀ m ∈ (f - g).support, m x < k
Module: Mathlib.Algebra.BigOperators.Finsupp.Fin

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
⊢ ∑ i_1, f i_1 ((cons i σ) i_1) = f 0 i + σ.sum (Fin.tail f)

Tactic:
sum_fintype _ _ (fun _ => by apply h)

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
n : ℕ
σ : Fin n →₀ M
i : M
f : Fin (n + 1) → M → N
h : ∀ (x : Fin (n + 1)), f x 0 = 0
⊢ ∑ i_1, f i_1 ((cons i σ) i_1) = f 0 i + ∑ i, Fin.tail f i (σ i)
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
i : σ
⊢ degreeOf (f i) ((rename f) p) = degreeOf i p

Tactic:
by
  classical
  simp only [degreeOf, degrees_rename_of_injective h, Multiset.count_map_eq_count' f p.degrees h]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree = 0 → p = C (coeff 0 p)

Tactic:
intro h

Goal state after:
case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
⊢ p = C (coeff 0 p)
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p = C (coeff 0 p) → p.totalDegree = 0

Tactic:
intro h

Goal state after:
case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p = C (coeff 0 p)
⊢ p.totalDegree = 0
Module: Mathlib.Algebra.Polynomial.Degree.Monomial

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : #p.support ≤ 1
⊢ C p.leadingCoeff * X ^ p.natDegree = p

Tactic:
rw [C_mul_X_pow_eq_monomial, monomial_natDegree_leadingCoeff_eq_self h]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).trailingDegree ≤ ↑p.natTrailingDegree + ↑q.natTrailingDegree

Tactic:
←
    ENat.natCast_add

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).trailingDegree ≤ ↑(p.natTrailingDegree + q.natTrailingDegree)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree ≠ 0
⊢ (map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0

Tactic:
simp_all [natDegree, WithBot.unbotD_eq_unbotD_iff]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial (Option σ) R
h : f ≠ 0
⊢ (((optionEquivLeft R σ) f).support.sup fun x ↦ x) = degreeOf none f

Tactic:
degreeOf_eq_sup,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial (Option σ) R
h : f ≠ 0
⊢ (((optionEquivLeft R σ) f).support.sup fun x ↦ x) = f.support.sup fun m ↦ m none
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
p q : K[X]
h : q ≠ 0
h₁ : q.leadingCoeff⁻¹ ≠ 0
⊢ (p * C q.leadingCoeff⁻¹).degree = p.degree

Tactic:
rw [degree_mul_C h₁]

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

Goal state before:
pp: case mp
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ eval₂ i (⅟x) (reflect N f) = 0 → eval₂ i (⅟x) (reflect N f) * x ^ N = 0

Tactic:
intro h

Goal state after:
case mp
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
h : eval₂ i (⅟x) (reflect N f) = 0
⊢ eval₂ i (⅟x) (reflect N f) * x ^ N = 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ eval₂ i (⅟x) (reflect N f) * x ^ N = 0 → eval₂ i (⅟x) (reflect N f) = 0

Tactic:
intro h

Goal state after:
case mpr
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
h : eval₂ i (⅟x) (reflect N f) * x ^ N = 0
⊢ eval₂ i (⅟x) (reflect N f) = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
⊢ m ∈ (((finSuccEquiv R n) f).coeff i).support → cons i m ∈ f.support

Tactic:
intro h

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
h : m ∈ (((finSuccEquiv R n) f).coeff i).support
⊢ cons i m ∈ f.support
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
⊢ cons i m ∈ f.support → m ∈ (((finSuccEquiv R n) f).coeff i).support

Tactic:
intro h

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
h : cons i m ∈ f.support
⊢ m ∈ (((finSuccEquiv R n) f).coeff i).support
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ coeff m f ≠ 0 ∧ m 0 = i → ∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m

Tactic:
intro h

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : coeff m f ≠ 0 ∧ m 0 = i
⊢ ∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α : Type ?u.39} {β : Type ?u.41} (f : α → β), (fun x ↦ x) ∘ f = f
h₁ : ∀ {α : Type ?u.55} {β : Type ?u.57} (f : α → β), (f ∘ fun x ↦ x) = f
⊢ (((finSuccEquiv R n) f).support.sup fun x ↦ x) = degreeOf 0 f

Tactic:
degreeOf_eq_sup,

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
h₀ : ∀ {α : Type ?u.39} {β : Type ?u.41} (f : α → β), (fun x ↦ x) ∘ f = f
h₁ : ∀ {α : Type ?u.55} {β : Type ?u.57} (f : α → β), (f ∘ fun x ↦ x) = f
⊢ (((finSuccEquiv R n) f).support.sup fun x ↦ x) = f.support.sup fun m ↦ m 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
⊢ degreeOf j (((finSuccEquiv R n) p).coeff i) ≤ degreeOf j.succ p

Tactic:
degreeOf_eq_sup,

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
⊢ ((((finSuccEquiv R n) p).coeff i).support.sup fun m ↦ m j) ≤ degreeOf j.succ p
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
⊢ ((((finSuccEquiv R n) p).coeff i).support.sup fun m ↦ m j) ≤ degreeOf j.succ p

Tactic:
degreeOf_eq_sup,

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
⊢ ((((finSuccEquiv R n) p).coeff i).support.sup fun m ↦ m j) ≤ p.support.sup fun m ↦ m j.succ
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
⊢ #f.support = n + 1 → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin (n + 1)), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i

Tactic:
intro h

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
⊢ ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin (n + 1)), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0) →
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)

Tactic:
intro h

Goal state after:
case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
⊢ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)) →
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

Tactic:
intro h

Goal state after:
case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)
⊢ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case inr.mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
h✝ : Nontrivial R
a b : R[X]
ha : a.Monic
hb : b.Monic
hm : (a * b).Monic
hnd : (a * b).natDegree = 2
hdb : b.natDegree = 1
hda : a.natDegree + b.natDegree = 2
⊢ ∃ c₁ c₂, (a * b).coeff 0 = c₁ * c₂ ∧ (a * b).coeff 1 = c₁ + c₂

Tactic:
hdb

Goal state after:
case inr.mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
h✝ : Nontrivial R
a b : R[X]
ha : a.Monic
hb : b.Monic
hm : (a * b).Monic
hnd : (a * b).natDegree = 2
hdb : b.natDegree = 1
hda : a.natDegree + 1 = 2
⊢ ∃ c₁ c₂, (a * b).coeff 0 = c₁ * c₂ ∧ (a * b).coeff 1 = c₁ + c₂
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case hnc
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ¬(Multiset.map natDegree (Multiset.map (fun x ↦ X - C x) t)).sum = 0

Tactic:
simp_rw [Multiset.sum_eq_zero_iff, Multiset.mem_map]

Goal state after:
case hnc
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ¬∀ (x : ℕ), (∃ a, (∃ a_1 ∈ t, X - C a_1 = a) ∧ a.natDegree = x) → x = 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
⊢ (Polynomial.map f P).coeff P.natDegree ≠ 0

Tactic:
rw [coeff_map, Monic.coeff_natDegree hmo, map_one]

Goal state after:
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
⊢ 1 ≠ 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
⊢ ¬IsUnit (X ^ n - 1)

Tactic:
intro h

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
h : IsUnit (X ^ n - 1)
⊢ False
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
x : R
⊢ (∀ (n : ℕ), (C x).coeff n ∈ P) → x ∈ P

Tactic:
intro h

Goal state after:
case mpr
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
x : R
h : ∀ (n : ℕ), (C x).coeff n ∈ P
⊢ x ∈ P
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommRing R
P : Ideal R
⊢ P.IsPrime → (map C P).IsPrime

Tactic:
intro h

Goal state after:
case mpr
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ (map C P).IsPrime
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := ⋯
n : ℕ := ⋯
⊢ ∀ c ∈ (antidiagonal ((m, n).1 + (m, n).2)).erase (m, n), f.coeff c.1 * g.coeff c.2 ∈ P

Tactic:
rintro ⟨i, j⟩ hij

Goal state after:
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (i, j) ∈ (antidiagonal ((m, n).1 + (m, n).2)).erase (m, n)
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
⊢ C r ≠ 0

Tactic:
intro h

Goal state after:
R : Type u
inst✝ : CommRing R
r : R
hr : (Ideal.span {r}).IsPrime
this : r ≠ 0
h : C r = 0
⊢ False
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
hp0 : p ≠ 0
⊢ 0 ≠ 1

Tactic:
intro h

Goal state after:
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h✝ : N < k
hp0 : p ≠ 0
h : 0 = 1
⊢ False
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd x)) →
          (∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd y)) →
            ∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd (x + y))

Tactic:
rintro m₁ m₂ _ _ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
      exact
        ⟨P₁ * P₂, by
          rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single,
            one_mul]; rfl⟩

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case of.refine_3
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
⊢ ∀ (x y : M),
    x ∈ closure S →
      y ∈ closure S →
        (∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd x)) →
          (∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd y)) →
            ∃ a, ((FreeAlgebra.lift R) fun s ↦ of' R M ↑s) a = (of R M) (Multiplicative.ofAdd (x + y))

Tactic:
rintro m₁ m₂ _ _ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
      exact
        ⟨P₁ * P₂, by
          rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single,
            one_mul]; rfl⟩

Goal state after: