mathlib-initiative/mathlib-tactics huggingface dataset:
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
D : A → B
inst✝ : Nonempty A
hD : Function.Injective D
a : A
r : R
⊢ leadingCoeff D (single a r) = r

Tactic:
leadingCoeff,

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
inst✝ : Nonempty A
hD : Function.Injective D
a : A
r : R
⊢ (single a r).coeff (Function.invFun D (supDegree D (single a r))) = r
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
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
⊢ leadingCoeff D (p + q) = leadingCoeff D p

Tactic:
leadingCoeff,

Goal state after:
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
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
⊢ (p + q).coeff (Function.invFun D (supDegree D (p + q))) = leadingCoeff D p
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 : R[A]
D : A → B
inst✝ : AddZeroClass A
hD : Function.Injective D
h : ¬p = 0
⊢ ¬leadingCoeff D p = 0

Tactic:
leadingCoeff,

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p : R[A]
D : A → B
inst✝ : AddZeroClass A
hD : Function.Injective D
h : ¬p = 0
⊢ ¬p.coeff (Function.invFun D (supDegree D p)) = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ (C a * p).leadingCoeff = a * p.leadingCoeff

Tactic:
leadingCoeff,

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ (C a * p).coeff (C a * p).natDegree = a * p.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree = ↑1
⊢ C (p.coeff 1) * X + C (p.coeff 0) = C p.leadingCoeff * X + C (p.coeff 0)

Tactic:
leadingCoeff,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree = ↑1
⊢ C (p.coeff 1) * X + C (p.coeff 0) = C (p.coeff p.natDegree) * X + C (p.coeff 0)
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ (p * C a).leadingCoeff = p.leadingCoeff * a

Tactic:
leadingCoeff,

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ (p * C a).coeff (p * C a).natDegree = p.leadingCoeff * a
Module: Mathlib.Algebra.Polynomial.Degree.SmallDegree

Goal state before:
pp: R : Type u
a b : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X + C b).degree = 1

Tactic:
rw [degree_add_eq_left_of_degree_lt <| degree_C_lt_degree_C_mul_X ha, degree_C_mul_X ha]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
⊢ (p ^ i * p).coeff ((i + 1) * p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff

Tactic:
Nat.succ_mul

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case inr.inr
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
hp✝ : p ≠ 0
hq✝ : q ≠ 0
ap : A
hp : supDegree D p = D ap
aq : A
hq : supDegree D q = D aq
⊢ (p * q).coeff (Function.invFun D (supDegree D p + supDegree D q)) = leadingCoeff D p * leadingCoeff D q

Tactic:
leadingCoeff,

Goal state after:
case inr.inr
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
hp✝ : p ≠ 0
hq✝ : q ≠ 0
ap : A
hp : supDegree D p = D ap
aq : A
hq : supDegree D q = D aq
⊢ (p * q).coeff (Function.invFun D (supDegree D p + supDegree D q)) =
    p.coeff (Function.invFun D (supDegree D p)) * q.coeff (Function.invFun D (supDegree D q))
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hf : p.leadingCoeff = 1
hfd : p.natDegree = 0
⊢ p = 1

Tactic:
leadingCoeff,

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hf : p.coeff p.natDegree = 1
hfd : p.natDegree = 0
⊢ p = 1
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 + C r).leadingCoeff = 1

Tactic:
leadingCoeff,

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

Goal state before:
pp: case inr
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
hq : Monic D q
hp : p ≠ 0
⊢ leadingCoeff D (p * q) = leadingCoeff D p

Tactic:
leadingCoeff,

Goal state after:
case inr
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
hq : Monic D q
hp : p ≠ 0
⊢ (p * q).coeff (Function.invFun D (supDegree D (p * q))) = leadingCoeff D p
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case inr
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
hp : Monic D p
hq : q ≠ 0
⊢ leadingCoeff D (p * q) = leadingCoeff D q

Tactic:
leadingCoeff,

Goal state after:
case inr
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
hp : Monic D p
hq : q ≠ 0
⊢ (p * q).coeff (Function.invFun D (supDegree D (p * q))) = leadingCoeff D q
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : f p.leadingCoeff = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ p = 0

Tactic:
leadingCoeff,

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : f (p.coeff p.natDegree) = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ p = 0
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
P : R[X]
⊢ P ∉ R[X]⁰ ↔ ∃ a, a ≠ 0 ∧ a • P = 0

Tactic:
refine ⟨fun hP ↦ ?_, fun ⟨a, ha, h⟩ h1 ↦ ha <| C_eq_zero.1 <| (h1.2 _) <| smul_eq_C_mul a ▸ h⟩
  by_contra! h
  obtain ⟨Q, hQ⟩ := notMem_nonZeroDivisors_iff_right.1 hP
  refine hQ.2 (eq_zero_of_mul_eq_zero_of_smul P (fun a ha ↦ ?_) Q (mul_comm P _ ▸ hQ.1))
  contrapose! ha
  exact h a ha

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : σ → R
p : MvPolynomial σ R
s : R
⊢ (eval x) (C s * p) = s * (eval x) p

Tactic:
(eval x).map_mul,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : σ → R
p : MvPolynomial σ R
s : R
⊢ (eval x) (C s) * (eval x) p = s * (eval x) p
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
r : R
⊢ (rename f) (C r) = C r

Tactic:
by
  unfold rename C monomial MvPolynomial; simp

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
c : R
⊢ c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = coeff n p

Tactic:
simp [coeffs, eq_comm, (Finset.mem_image)]

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

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
h✝ : Surjective ⇑(map f)
s : S₁
p : MvPolynomial σ R
h : (map f) p = C s
⊢ f (coeff 0 p) = s

Tactic:
simpa [coeff_map] using congr(coeff 0 $h)

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

Goal state before:
pp: case a
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
n : ℕ
x✝ : n + 2 ≠ 0
M : Submodule R S
⊢ n + 1 ≠ 0

Tactic:
exact n.succ_ne_zero

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

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
j : σ
hj : j ∈ x.support
hi : f j ≠ i
⊢ (if f j = i then x j else 0) = 0

Tactic:
if_neg hi

Goal state after:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) ((rename f) φ) ≠ 0
j : σ
hj : j ∈ x.support
hi : f j ≠ i
⊢ 0 = 0
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ (p + q).vars ⊆ p.vars ∪ q.vars

Tactic:
intro x hx
  simp only [vars_def, Finset.mem_union, Multiset.mem_toFinset] at hx ⊢
  simpa using Multiset.mem_of_le degrees_add_le hx

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
h : Disjoint p.vars q.vars
⊢ (p + q).vars = p.vars ∪ q.vars

Tactic:
refine (vars_add_subset p q).antisymm fun x hx => ?_
  simp only [vars_def, Multiset.disjoint_toFinset] at h hx ⊢
  rwa [degrees_add_of_disjoint h, Multiset.toFinset_union]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
r : R
⊢ max p.totalDegree (C r).totalDegree = p.totalDegree

Tactic:
by rw [totalDegree_C, Nat.max_zero]

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

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
t : Fin (n + 1) →₀ M
⊢ cons (t 0) t.tail = t

Tactic:
ext a
  by_cases c_a : a = 0
  · rw [c_a, cons_zero]
  · rw [← Fin.succ_pred a c_a, cons_succ, ← tail_apply]

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

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
x₀ y₀ : M
x y : Fin n →₀ M
h : cons x₀ x = cons y₀ y
this : (cons x₀ x) 0 = (cons y₀ y) 0
⊢ x₀ = y₀ ∧ x = y

Tactic:
simp only [cons_zero] at this

Goal state after:
n : ℕ
M : Type u_1
inst✝ : Zero M
x₀ y₀ : M
x y : Fin n →₀ M
h : cons x₀ x = cons y₀ y
this : x₀ = y₀
⊢ x₀ = y₀ ∧ x = y
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
⊢ degreeOf i (p + q) ≤ degreeOf i p

pp: case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
⊢ degreeOf i p ≤ degreeOf i (p + q)

Tactic:
· rw [← max_eq_left_of_lt h]
    exact degreeOf_add_le i p q

Goal state after:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h : degreeOf i q < degreeOf i p
⊢ degreeOf i p ≤ degreeOf i (p + q)
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
j : τ
h : j ∈ ((rename f) φ).vars
⊢ ∃ i ∈ φ.vars, f i = j

Tactic:
classical
  simpa only [exists_prop, Finset.mem_image] using vars_rename f φ h

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ f.eraseLead.leadingCoeff = f.nextCoeff

Tactic:
leadingCoeff,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
this : 0 < f.natDegree
⊢ f.eraseLead.coeff f.eraseLead.natDegree = f.nextCoeff
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
rw [← eraseLead_add_C_mul_X_pow g, mul_add, reflect_add, reflect_add, mul_add, hcg, hcg]

Goal state after:
case neg.Cg
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ #(C g.leadingCoeff * X ^ g.natDegree).support ≤ cg.succ

case neg.Og
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ (C g.leadingCoeff * X ^ g.natDegree).natDegree ≤ O

case neg.Cg
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ #g.eraseLead.support ≤ cg.succ

case neg.Og
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ g.eraseLead.natDegree ≤ O
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case neg.Cg
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ #g.eraseLead.support ≤ cg.succ

Tactic:
exact Nat.lt_succ_iff.mp (lt_of_lt_of_le (eraseLead_support_card_lt g0) Cg)

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

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
s : S₂
⊢ (sumRingEquiv R S₁ S₂) (X (Sum.inr s)) = C (X s)

Tactic:
by
  unfold sumRingEquiv C X MvPolynomial; simp [monomial]

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
qn : (-q).natDegree ≤ n
⊢ (p - q).natDegree ≤ n ↔ p.natDegree ≤ n

Tactic:
rw [sub_eq_add_neg, natDegree_add_le_iff_left _ _ qn]

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

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q : R[X]
hq : 0 < q.degree
⊢ ⊥ = ⊥ * q.degree

Tactic:
WithBot.bot_mul'

Goal state after:
case inl
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
q : R[X]
hq : 0 < q.degree
⊢ ⊥ = if q.degree = 0 then 0 else ⊥
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
simpa [hp.leadingCoeff, leadingCoeff_ne_zero]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ q.leadingCoeff * p.leadingCoeff ≠ 0

Tactic:
simpa [hp.leadingCoeff, leadingCoeff_ne_zero]

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

Goal state before:
pp: case a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
key : ¬f.reverse.leadingCoeff = 0
⊢ f.coeff (f.natDegree - f.reverse.natDegree) ≠ 0

Tactic:
leadingCoeff,

Goal state after:
case a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
key : ¬f.reverse.coeff f.reverse.natDegree = 0
⊢ f.coeff (f.natDegree - f.reverse.natDegree) ≠ 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse.leadingCoeff = f.trailingCoeff

Tactic:
leadingCoeff,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse.coeff f.reverse.natDegree = f.trailingCoeff
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
a✝ : Nontrivial R
⊢ (p * q).reverse.coeff 1 = p.reverse.coeff 1 + q.reverse.coeff 1

Tactic:
rw [reverse_mul] <;> simp [hp.leadingCoeff, hq.leadingCoeff, mul_coeff_one, add_comm]

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

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : MonicDegreeEq R n
a✝ : Nontrivial R
⊢ (↑p).leadingCoeff = 1

Tactic:
leadingCoeff,

Goal state after:
R : Type u
n : ℕ
inst✝ : Semiring R
p : MonicDegreeEq R n
a✝ : Nontrivial R
⊢ (↑p).coeff (↑p).natDegree = 1
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
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 : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
i : Fin (n + 1)
hi : ¬∃ i₀, i₀.castSucc = i
⊢ ¬n + 1 = 0

Tactic:
exact n.succ_ne_zero

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

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ degreeLE R ↑n ≤ Submodule.span R ↑(image (fun n ↦ X ^ n) (range (n + 1)))

Tactic:
intro p hp
    replace hp := mem_degreeLE.1 hp
    rw [← Polynomial.sum_monomial_eq p, Polynomial.sum]
    refine Submodule.sum_mem _ fun k hk => ?_
    have := WithBot.coe_le_coe.1 (Finset.sup_le_iff.1 hp k hk)
    rw [← C_mul_X_pow_eq_monomial, C_mul']
    refine
      Submodule.smul_mem _ _
        (Submodule.subset_span <|
          Finset.mem_coe.2 <|
            Finset.mem_image.2 ⟨_, Finset.mem_range.2 (Nat.lt_succ_of_le this), rfl⟩)

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
hRS : ⊤.FG
hSA : ⊤.FG
⊢ ⊤.FG

Tactic:
rcases hRS with ⟨s, hs⟩
  rcases hSA with ⟨t, ht⟩
  exact ⟨s.image (algebraMap S A) ∪ t, by
    rw [Finset.coe_union, Finset.coe_image,
        Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin,
        hs, Algebra.adjoin_top, ht, Subalgebra.restrictScalars_top,
        Subalgebra.restrictScalars_top
       ]
    ⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
⊢ x ∈ I.leadingCoeff ↔ ∃ p ∈ I, p.leadingCoeff = x

Tactic:
leadingCoeff,

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
⊢ x ∈ ⨆ n, I.leadingCoeffNth n ↔ ∃ p ∈ I, p.leadingCoeff = x
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial (↥s) R
hd : (algebraMap R (MvPolynomial σ R)) r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'
this : (algebraMap R (MvPolynomial (↥s) R)) r ∣ a' * b'
⊢ C r ∣ (rename Subtype.val) a' ∨ C r ∣ (rename Subtype.val) b'

Tactic:
← rename_C ((↑) : s → σ)

Goal state after:
R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial (↥s) R
hd : (algebraMap R (MvPolynomial σ R)) r ∣ (rename Subtype.val) a' * (rename Subtype.val) b'
this : (algebraMap R (MvPolynomial (↥s) R)) r ∣ a' * b'
⊢ (rename Subtype.val) (C r) ∣ (rename Subtype.val) a' ∨ (rename Subtype.val) (C r) ∣ (rename Subtype.val) b'
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : (g.comp f).FiniteType
⊢ g.FiniteType

Tactic:
algebraize [f, g, g.comp f]
  exact Algebra.FiniteType.of_restrictScalars_finiteType A B C

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: 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
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₁ = (of R M) (Multiplicative.ofAdd m₁)
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₂ = (of R M) (Multiplicative.ofAdd m₂)
⊢ (of R M) (Multiplicative.ofAdd m₁) * (of R M) (Multiplicative.ofAdd m₂) = (of R M) (Multiplicative.ofAdd (m₁ + m₂))

Tactic:
of_apply,

Goal state after:
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
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₁ = (of R M) (Multiplicative.ofAdd m₁)
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₂ = (of R M) (Multiplicative.ofAdd m₂)
⊢ single (Multiplicative.toAdd (Multiplicative.ofAdd m₁)) 1 * (of R M) (Multiplicative.ofAdd m₂) =
    (of R M) (Multiplicative.ofAdd (m₁ + m₂))
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: 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
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₁ = (of R M) (Multiplicative.ofAdd m₁)
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₂ = (of R M) (Multiplicative.ofAdd m₂)
⊢ single (Multiplicative.toAdd (Multiplicative.ofAdd m₁)) 1 * (of R M) (Multiplicative.ofAdd m₂) =
    (of R M) (Multiplicative.ofAdd (m₁ + m₂))

Tactic:
of_apply,

Goal state after:
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
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : MvPolynomial (↑S) R
hP₁ : (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₁ = (of R M) (Multiplicative.ofAdd m₁)
P₂ : MvPolynomial (↑S) R
hP₂ : (MvPolynomial.aeval fun s ↦ of' R M ↑s) P₂ = (of R M) (Multiplicative.ofAdd m₂)
⊢ single (Multiplicative.toAdd (Multiplicative.ofAdd m₁)) 1 *
      single (Multiplicative.toAdd (Multiplicative.ofAdd m₂)) 1 =
    (of R M) (Multiplicative.ofAdd (m₁ + m₂))