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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ (X ^ k).coeff k * r ^ (n - k) * ↑(n.choose k) = r ^ (n - k) * ↑(n.choose k)

pp: case h₀
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ ∀ b ∈ range (n + 1), b ≠ k → (X ^ b).coeff k * r ^ (n - b) * ↑(n.choose b) = 0

pp: case h₁
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ k ∉ range (n + 1) → (X ^ k).coeff k * r ^ (n - k) * ↑(n.choose k) = 0

Tactic:
coeff_X_pow_self,

Goal state after:
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ 1 * r ^ (n - k) * ↑(n.choose k) = r ^ (n - k) * ↑(n.choose k)

case h₀
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ ∀ b ∈ range (n + 1), b ≠ k → (X ^ b).coeff k * r ^ (n - b) * ↑(n.choose b) = 0

case h₁
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ k ∉ range (n + 1) → (X ^ k).coeff k * r ^ (n - k) * ↑(n.choose k) = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff + q.leadingCoeff ≠ 0
hlt : p.degree < q.degree
⊢ max p.degree q.degree ≤ (p + q).degree

Tactic:
by
      rw [degree_add_eq_right_of_degree_lt hlt, max_eq_right_of_lt hlt]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ p.degree + q.degree ≤ ↑(p.natDegree + q.natDegree)

Tactic:
rw [Nat.cast_add]

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ p.degree + q.degree ≤ ↑p.natDegree + ↑q.natDegree
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case hb
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hpq : leadingCoeff D p * leadingCoeff D q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ ∀ {a b : B}, a ∈ Set.range D → b ∈ Set.range D → a + b ∈ Set.range D

Tactic:
· exact (AddHom.srange ⟨D, hadd⟩).add_mem

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ (X ^ n).coeff n + (C r).coeff n = 1

Tactic:
coeff_X_pow_self,

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ 1 + (C r).coeff n = 1
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder B
inst✝⁴ : OrderBot B
p q : R[A]
D : A → B
inst✝³ : AddZeroClass A
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hbot : ⊥ + ⊥ = ⊥
hp : Monic D p
hq : Monic D q
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
cases subsingleton_or_nontrivial R
  · simp_rw [Subsingleton.eq_zero p, Subsingleton.eq_zero q, mul_zero, supDegree_zero, hbot]
  exact hq.supDegree_mul_of_ne_zero_left hD hadd hp.ne_zero

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

Goal state before:
pp: 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)
⊢ IsUnit f

Tactic:
by
  have dz := degree_eq_zero_of_isUnit H
  rw [degree_map_eq_of_leadingCoeff_ne_zero] at dz
  · rw [eq_C_of_degree_eq_zero dz]
    refine IsUnit.map C ?_
    convert! hf
    change coeff f 0 = coeff f (natDegree f)
    rw [(degree_eq_iff_natDegree_eq _).1 dz]
    · rfl
    rintro rfl
    simp at H
  · intro h
    have u : IsUnit (φ f.leadingCoeff) := IsUnit.map φ hf
    rw [h] at u
    simp at u

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
s : Finset ι
hf : f.support ⊆ s
⊢ f ≤ g ↔ ∀ i ∈ s, f i ≤ g i

Tactic:
refine ⟨fun h s _ ↦ h s, fun h s ↦ ?_⟩
  by_cases H : s ∈ f.support
  · exact h s (hf H)
  · exact notMem_support_iff.1 H ▸ zero_le

Goal state after:
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✝³ : CommSemiring A'
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p✝ q✝ : R[X]
x : A
p q : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
⊢ R[X] ≃ₐ[R] R[X]

Tactic:
refine AlgEquiv.ofAlgHom (aeval p) (aeval q) ?_ ?_

Goal state after:
case refine_1
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✝³ : CommSemiring A'
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p✝ q✝ : R[X]
x : A
p q : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
⊢ (aeval p).comp (aeval q) = AlgHom.id R R[X]

case refine_2
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✝³ : CommSemiring A'
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
p✝ q✝ : R[X]
x : A
p q : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
⊢ (aeval q).comp (aeval p) = AlgHom.id R R[X]
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : Unique ι
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (β i)
x y : Colex ((i : ι) → β i)
⊢ x ≤ y ↔ x default ≤ y default

Tactic:
by
  simp_rw [le_iff_lt_or_eq, Pi.Colex.lt_iff_of_unique, ← ofColex_inj, funext_iff, Unique.forall_iff,
    ofColex_apply]

Goal state after:
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ (- -f).neLocus (-g) = f.neLocus (-g)

Tactic:
neg_neg

Goal state after:
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ f.neLocus (-g) = f.neLocus (-g)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case single_add
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive (MvPolynomial.C a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
⊢ ∀ (a_1 : σ) (b : ℕ) (f : σ →₀ ℕ),
    a_1 ∉ f.support → b ≠ 0 → motive ((monomial f) a) → motive ((monomial (Finsupp.single a_1 b + f)) a)

Tactic:
intro n

Goal state after:
case single_add
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive (MvPolynomial.C a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
n : σ
⊢ ∀ (b : ℕ) (f : σ →₀ ℕ),
    n ∉ f.support → b ≠ 0 → motive ((monomial f) a) → motive ((monomial (Finsupp.single n b + f)) a)
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case single_add
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive (MvPolynomial.C a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e : ℕ
⊢ ∀ (f : σ →₀ ℕ), n ∉ f.support → e ≠ 0 → motive ((monomial f) a) → motive ((monomial (Finsupp.single n e + f)) a)

Tactic:
p

Goal state after:
case single_add
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive (MvPolynomial.C a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e : ℕ
p : σ →₀ ℕ
⊢ n ∉ p.support → e ≠ 0 → motive ((monomial p) a) → motive ((monomial (Finsupp.single n e + p)) a)
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
r : R
⊢ k (f r) = eval₂ k (⇑k ∘ g) (C (f r))

Tactic:
eval₂_C

Goal state after:
case C
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
r : R
⊢ k (f r) = k (f r)
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case C
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p : MvPolynomial S₂ R
r : R
⊢ C (f r) = eval₂ C (⇑(map f) ∘ g) (C (f r))

Tactic:
eval₂_C

Goal state after:
case C
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p : MvPolynomial S₂ R
r : R
⊢ C (f r) = C (f r)
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ (p * q).degrees ≤ p.degrees + q.degrees

Tactic:
classical
  simp_rw [degrees_def]
  exact supDegree_mul_le (map_add _)

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

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial (↥s₁) R
s₂ : Finset σ
q₂ : MvPolynomial (↥s₂) R
⊢ ∃ s q₁_1 q₂_1,
    (rename Subtype.val) q₁ = (rename Subtype.val) q₁_1 ∧ (rename Subtype.val) q₂ = (rename Subtype.val) q₂_1

Tactic:
use s₁ ∪ s₂

Goal state after:
case h
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial (↥s₁) R
s₂ : Finset σ
q₂ : MvPolynomial (↥s₂) R
⊢ ∃ q₁_1 q₂_1, (rename Subtype.val) q₁ = (rename Subtype.val) q₁_1 ∧ (rename Subtype.val) q₂ = (rename Subtype.val) q₂_1
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x : MvPolynomial R ℤ
n : ℤ
⊢ eval₂ c (⇑f ∘ X) (C n) = ↑n

Tactic:
eval₂_C

Goal state after:
S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x : MvPolynomial R ℤ
n : ℤ
⊢ c n = ↑n
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case a
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
⊢ Algebra.adjoin R (range f) ≤ (aeval f).range

Tactic:
rw [Algebra.adjoin_le_iff]
    rintro x ⟨i, rfl⟩
    use X i, by aesop

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : DecidableEq σ
i : σ
⊢ i ∈ p.vars ↔ i ∈ p.support.biUnion Finsupp.support

Tactic:
mem_vars_iff_mem_support,

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : DecidableEq σ
i : σ
⊢ (∃ d ∈ p.support, i ∈ d.support) ↔ i ∈ p.support.biUnion Finsupp.support
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ eraseLead 0 = 0

Tactic:
simp only [eraseLead, erase_zero]

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

Goal state before:
pp: case insert.inr.inl
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
H : (f x).degree = (s.sum f).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)

pp: case insert.inr.inr
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
H : (s.sum f).degree < (f x).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)

Tactic:
· rcases s.eq_empty_or_nonempty with (rfl | hs)
      · simp
      obtain ⟨y, hy, hy'⟩ := Finset.exists_mem_eq_sup s hs fun i => degree (f i)
      rw [IH, hy'] at H
      by_cases hx0 : f x = 0
      · simp [hx0, IH]
      have hy0 : f y ≠ 0 := by
        contrapose! H
        simpa [H, degree_eq_bot] using hx0
      refine absurd H (h ?_ ?_ fun H => hx ?_)
      · simp [hx0]
      · simp [hy, hy0]
      · exact H.symm ▸ hy

Goal state after:
case insert.inr.inr
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
H : (s.sum f).degree < (f x).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
i : ℕ
r : R
hr : ¬r = 0
⊢ erase (if r = 0 then 0 else i) ((monomial i) r) = 0

Tactic:
if_neg hr,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
i : ℕ
r : R
hr : ¬r = 0
⊢ erase i ((monomial i) r) = 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : eval₂ f z (C (p.coeff 0)) = 0
inj : ∀ (x : R), f x = 0 → x = 0
hlt : p.natDegree ≤ 0
A : p = C (p.coeff 0)
⊢ False

Tactic:
eval₂_C

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : f (p.coeff 0) = 0
inj : ∀ (x : R), f x = 0 → x = 0
hlt : p.natDegree ≤ 0
A : p = C (p.coeff 0)
⊢ False
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ p.comp q = 0 ↔ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

Tactic:
by
  refine ⟨fun h ↦ ?_, Or.rec (fun h ↦ by simp [h]) fun h ↦ by rw [h.2, comp_C, h.1, C_0]⟩
  have key : p.natDegree = 0 ∨ q.natDegree = 0 := by
    rw [← mul_eq_zero, ← natDegree_comp, h, natDegree_zero]
  obtain key | key := Or.imp eq_C_of_natDegree_eq_zero eq_C_of_natDegree_eq_zero key
  · rw [key, C_comp] at h
    exact Or.inl (key.trans h)
  · rw [key, comp_C, C_eq_zero] at h
    exact Or.inr ⟨h, key⟩

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

Goal state before:
pp: case refine_2
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
⊢ ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → eval₂ i (⅟x) (reflect N (C r * X ^ n)) * x ^ N = eval₂ i x (C r * X ^ n)

Tactic:
intro n

Goal state after:
case refine_2
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
n : ℕ
⊢ ∀ (r : R), r ≠ 0 → n ≤ N → eval₂ i (⅟x) (reflect N (C r * X ^ n)) * x ^ N = eval₂ i x (C r * X ^ n)
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ ∀ (m : ℕ), ↑f.natDegree < ↑m → f.reverse.coeff m = 0

Tactic:
intro n

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
⊢ ↑f.natDegree < ↑n → f.reverse.coeff n = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
⊢ ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ p.natDegree → (φ (C r * X ^ n)).natDegree = fu (C r * X ^ n).natDegree

Tactic:
intro n

Goal state after:
case refine_1
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
n : ℕ
⊢ ∀ (r : R), r ≠ 0 → n ≤ p.natDegree → (φ (C r * X ^ n)).natDegree = fu (C r * X ^ n).natDegree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
ih : (p ^ n).nextCoeff = n • p.nextCoeff
⊢ (p ^ n * p).nextCoeff = (n + 1) • p.nextCoeff

Tactic:
(hp.pow n).nextCoeff_mul hp,

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
ih : (p ^ n).nextCoeff = n • p.nextCoeff
⊢ (p ^ n).nextCoeff + p.nextCoeff = (n + 1) • p.nextCoeff
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case refine_1
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ (∀ i ∈ 0, (f i).Monic) → (Multiset.map f 0).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) 0).sum

Tactic:
simp only [Multiset.notMem_zero, forall_prop_of_true, forall_prop_of_false, Multiset.map_zero,
      Multiset.prod_zero, Multiset.sum_zero, not_false_iff, forall_true_iff]
    rw [← C_1]
    rw [nextCoeff_C_eq_zero]

Goal state after:
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) →₀ ℕ
h : coeff m f ≠ 0 ∧ m 0 = i
⊢ ∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m

Tactic:
use tail m

Goal state after:
case h
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
⊢ ¬coeff (cons i m.tail) f = 0 ∧ cons i m.tail = m
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
⊢ - -1 = 1

Tactic:
neg_neg

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
⊢ 1 = 1
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
a✝ : Nontrivial R
x : ι
hx : x ∈ s
⊢ (f x).leadingCoeff ≠ 0

Tactic:
simp [h x hx]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : ¬p = 0
this : ↑p.natDegree < ↑p.natDegree
⊢ False

Tactic:
lt_self_iff_false

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
p : R[X]
hs : s.Nonempty
hp : p ∈ Submodule.span R s
h : ∀ p' ∈ s, p'.degree < p.degree
hp_zero : ¬p = 0
this : False
⊢ False
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.refine_4
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : f ∈ map C I
⊢ ∀ (a x : R[X]), x ∈ Submodule.span R[X] (⇑C '' ↑I) → (∀ (n : ℕ), x.coeff n ∈ I) → ∀ (n : ℕ), (a • x).coeff n ∈ I

Tactic:
· intro f g _ hg n
      rw [smul_eq_mul, coeff_mul]
      exact I.sum_mem fun c _ => I.mul_mem_left (f.coeff c.fst) (hg c.snd)

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.MulOpposite

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set Aᵐᵒᵖ
⊢ (Algebra.adjoin R s).unop = Algebra.adjoin R (MulOpposite.op ⁻¹' s)

Tactic:
apply toSubsemiring_injective
  simp_rw [Algebra.adjoin, unop_toSubsemiring, Subsemiring.unop_closure, Set.preimage_union]
  congr with x
  simp

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

Goal state before:
pp: case h
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
⊢ p ∈ Ideal.span ↑s

Tactic:
rcases le_or_gt k N with h | h

Goal state after:
case h.inl
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 : k ≤ N
⊢ p ∈ Ideal.span ↑s

case h.inr
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
⊢ p ∈ Ideal.span ↑s
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
⊢ adjoin R (of' R M '' ⋃ f ∈ S, ↑f.coeff.support) = ⊤

Tactic:
by
  suffices of' R M '' ⋃ f ∈ S, (f.coeff.support : Set M) = ⋃ f ∈ S, of' R M '' f.coeff.support by
    rw [this]
    exact support_gen_of_gen hS
  simp only [Set.image_iUnion]

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_1.smul
R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝³ : AddCommMonoid M
x✝² : Module R M
x✝¹ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x✝ : ↥N
a : ↥A
x : ↥N
hx✝ : x ∈ span (↥A) ({n} ∪ Set.range nj)
hx : (↑↥A i) x ∈ M'
⊢ (↑↥A i) (a • x) ∈ M'

Tactic:
map_smul

Goal state after:
case refine_1.smul
R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝³ : AddCommMonoid M
x✝² : Module R M
x✝¹ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x✝ : ↥N
a : ↥A
x : ↥N
hx✝ : x ∈ span (↥A) ({n} ∪ Set.range nj)
hx : (↑↥A i) x ∈ M'
⊢ a • (↑↥A i) x ∈ M'
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.coeff.support
⊢ ∑ i ∈ d.support, d i ≤ F.totalDegree

Tactic:
rw [MvPolynomial.totalDegree]

Goal state after:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.coeff.support
⊢ ∑ i ∈ d.support, d i ≤ F.support.sup fun s ↦ s.sum fun x e ↦ e