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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.coeff f.natTrailingDegree = f.coeff f.natTrailingDegree

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
h0 : p * r ≠ 0
hl : p.natDegree + r.natDegree < p.natDegree
⊢ False

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R[X]
h0 : p * r ≠ 0
hl : p.natDegree + r.natDegree < p.natDegree
⊢ False
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f = 0 ∨ f ≠ 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f = 0 ∨ f ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case monomial
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ r * coeff m ((Polynomial.X ^ j 0 * Polynomial.C (∏ x, X x ^ j x.succ)).coeff i) = if j = cons i m then r else 0

Tactic:
← mul_boole,

Goal state after:
case monomial
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ r * coeff m ((Polynomial.X ^ j 0 * Polynomial.C (∏ x, X x ^ j x.succ)).coeff i) = r * if j = cons i m then 1 else 0
Module: Mathlib.Algebra.Polynomial.Reverse

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

Tactic:
]

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

Goal state before:
pp: case monomial
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ r * coeff m (if i = j 0 then ∏ x, X x ^ j x.succ else 0) = r * if j = cons i m then 1 else 0

Tactic:
]

Goal state after:
case monomial
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ r * coeff m (if i = j 0 then ∏ x, X x ^ j x.succ else 0) = r * if j = cons i m then 1 else 0
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.reverse * q.reverse).coeff 1 = p.reverse.coeff 1 + q.reverse.coeff 1

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

Tactic:
]

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

R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
a✝ : Nontrivial R
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f g : R[X]
fg : f.leadingCoeff * g.leadingCoeff ≠ 0
⊢ reflect f.natDegree f * reflect g.natDegree g = reflect f.natDegree f * reflect g.natDegree g

Tactic:
]

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

Goal state before:
pp: case zero
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
g0 : g = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
hjmi : j ≠ j
⊢ False

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
hjmi : j ≠ j
⊢ False
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ p.trailingCoeff * q.trailingCoeff = p.trailingCoeff * q.trailingCoeff

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.coeff ((revAt f.natDegree) 1) = if f.natDegree = 0 then 0 else f.coeff (f.natDegree - 1)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.coeff ((revAt f.natDegree) 1) = if f.natDegree = 0 then 0 else f.coeff (f.natDegree - 1)
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
⊢ n • p.nextCoeff + p.nextCoeff = n • p.nextCoeff + p.nextCoeff

Tactic:
]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f.natDegree = 0
⊢ f.coeff (f.natDegree - 1) = f.coeff (f.natDegree - 1)

pp: case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f.natDegree = 0
⊢ 1 ≤ f.natDegree

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f.natDegree = 0
⊢ 1 ≤ f.natDegree
Module: Mathlib.Algebra.Polynomial.Reverse

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

Tactic:
]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : (p * X ^ n).reverse = p.reverse
⊢ p.reverse = p.reverse

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ p.reverse = p.reverse

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
t : R
⊢ C t * X ^ p.natDegree + p.reverse = C t * X ^ p.natDegree + p.reverse

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
⊢ 0 = 0

pp: R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
⊢ f p.leadingCoeff ≠ 0

Tactic:
]

Goal state after:
R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
⊢ f p.leadingCoeff ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
  let __src := Polynomial.mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
⊢ (aeval (Fin.cons y s)) (X 0) = ((Polynomial.aeval y).comp (φ.comp ↑(finSuccEquiv R n))) (X 0) ∧
    ∀ (i : Fin n),
      (aeval (Fin.cons y s)) (X i.succ) = ((Polynomial.aeval y).comp (φ.comp ↑(finSuccEquiv R n))) (X i.succ)

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
  let __src := Polynomial.mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
⊢ (aeval (Fin.cons y s)) (X 0) = ((Polynomial.aeval y).comp (φ.comp ↑(finSuccEquiv R n))) (X 0) ∧
    ∀ (i : Fin n),
      (aeval (Fin.cons y s)) (X i.succ) = ((Polynomial.aeval y).comp (φ.comp ↑(finSuccEquiv R n))) (X i.succ)
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
⊢ 1 ≠ 0

Tactic:
]

Goal state after:
R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
⊢ 1 ≠ 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : R[X]
N : ℕ
⊢ -reflect N f = -reflect N f

Tactic:
]

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

Goal state before:
pp: case refine_2
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
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
⊢ (φ f + φ g).natDegree = fu g.natDegree

Tactic:
]

Goal state after:
case refine_2
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
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
⊢ (φ f + φ g).natDegree = fu g.natDegree
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f g : R[X]
N : ℕ
⊢ reflect N f + -reflect N g = reflect N f + -reflect N g

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
hdeg : p.degree = 0
hndeg : p.natDegree = 0
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : R[X]
⊢ -reflect f.natDegree f = -reflect f.natDegree f

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
r : R
⊢ n = n

Tactic:
]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
⊢ ¬((finSuccEquiv R n) f).coeff i = 0

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
⊢ ¬((finSuccEquiv R n) f).coeff i = 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
a✝ : Nontrivial R
q : R[X]
h : p * q = 1
this : p.natDegree = 0 ∧ q.natDegree = 0
⊢ p = 1

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
hm : p.Monic
hpu : IsUnit p
a✝ : Nontrivial R
q : R[X]
h : p * q = 1
this : p.natDegree = 0 ∧ q.natDegree = 0
⊢ p = 1
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case pos
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
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
FG : k ≤ f.natDegree
⊢ fu g.natDegree = fu g.natDegree

pp: case pos
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
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
FG : k ≤ f.natDegree
⊢ (φ f).natDegree < (φ g).natDegree

Tactic:
]

Goal state after:
case pos
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
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
FG : k ≤ f.natDegree
⊢ (φ f).natDegree < (φ g).natDegree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
u : R[X]ˣ
hq : (p * ↑u).Monic
⊢ p = p

Tactic:
]

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

Goal state before:
pp: case cons
S : Type u_1
inst✝ : Semiring S
n : WithBot ℕ
hd : S[X]
tl : List S[X]
ih : (∀ p ∈ tl, p.degree ≤ n) → tl.sum.degree ≤ n
hhd : hd.degree ≤ n
htl : ∀ a ∈ tl, a.degree ≤ n
⊢ (hd + tl.sum).degree ≤ n

Tactic:
]

Goal state after:
case cons
S : Type u_1
inst✝ : Semiring S
n : WithBot ℕ
hd : S[X]
tl : List S[X]
ih : (∀ p ∈ tl, p.degree ≤ n) → tl.sum.degree ≤ n
hhd : hd.degree ≤ n
htl : ∀ a ∈ tl, a.degree ≤ n
⊢ (hd + tl.sum).degree ≤ n
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case e'_3
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
hf'_sup : (((finSuccEquiv R n) f).coeff i).support.Nonempty
σ : Fin n →₀ ℕ
hσ1 : σ ∈ (((finSuccEquiv R n) f).coeff i).support
hσ2 : ((((finSuccEquiv R n) f).coeff i).support.sup fun s ↦ s.sum fun x e ↦ e) = σ.sum fun x e ↦ e
σ' : Fin (n + 1) →₀ ℕ := cons i σ
⊢ (i + σ.sum fun x e ↦ e) = i + σ.sum fun x e ↦ e

Tactic:
]

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
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case convert_4
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
hf'_sup : (((finSuccEquiv R n) f).coeff i).support.Nonempty
σ : Fin n →₀ ℕ
hσ1 : σ ∈ (((finSuccEquiv R n) f).coeff i).support
hσ2 : ((((finSuccEquiv R n) f).coeff i).support.sup fun s ↦ s.sum fun x e ↦ e) = σ.sum fun x e ↦ e
σ' : Fin (n + 1) →₀ ℕ := cons i σ
⊢ σ ∈ (((finSuccEquiv R n) f).coeff i).support

Tactic:
]

Goal state after:
case convert_4
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
hf'_sup : (((finSuccEquiv R n) f).coeff i).support.Nonempty
σ : Fin n →₀ ℕ
hσ1 : σ ∈ (((finSuccEquiv R n) f).coeff i).support
hσ2 : ((((finSuccEquiv R n) f).coeff i).support.sup fun s ↦ s.sum fun x e ↦ e) = σ.sum fun x e ↦ e
σ' : Fin (n + 1) →₀ ℕ := cons i σ
⊢ σ ∈ (((finSuccEquiv R n) f).coeff i).support
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case pos
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
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
FG : k ≤ f.natDegree
⊢ fu f.natDegree < fu g.natDegree

Tactic:
]

Goal state after:
case pos
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
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
FG : k ≤ f.natDegree
⊢ fu f.natDegree < fu g.natDegree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
p : R[X]
hp : p.Monic
hp' : p.natDegree = n
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
h : ¬p = 0
⊢ ↑p.natDegree ≤ (List.map natDegree l).maximum

Tactic:
]

Goal state after:
case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
h : ¬p = 0
⊢ ↑p.natDegree ≤ (List.map natDegree l).maximum
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
h : ¬p = 0
⊢ ∃ a ∈ l, a.natDegree = ↑p.natDegree

Tactic:
]

Goal state after:
case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
h : ¬p = 0
⊢ ∃ a ∈ l, a.natDegree = ↑p.natDegree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.Monic
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (f a * (Multiset.map f t).prod).Monic

Tactic:
]

Goal state after:
case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.Monic
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (f a * (Multiset.map f t).prod).Monic
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ (∃ a ∈ (((finSuccEquiv R n) f).coeff i).support, cons i a = m) ↔ coeff m f ≠ 0 ∧ m 0 = i

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ (∃ a ∈ (((finSuccEquiv R n) f).coeff i).support, cons i a = m) ↔ coeff m f ≠ 0 ∧ m 0 = i
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
⊢ (if h : Function.HasFiniteMulSupport f then ∏ i ∈ Set.Finite.toFinset h, f i else 1).Monic

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
⊢ (if h : Function.HasFiniteMulSupport f then ∏ i ∈ Set.Finite.toFinset h, f i else 1).Monic
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]
⊢ (C 1).nextCoeff = 0

Tactic:
]

Goal state after:
case refine_1
R : Type u
ι : Type y
inst✝ : CommSemiring R
t : Multiset ι
f : ι → R[X]
⊢ (C 1).nextCoeff = 0
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]
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: 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 m f = 0 ∧ m = m

Tactic:
]

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 m f = 0 ∧ m = 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
⊢ f ≠ 0

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
⊢ f ≠ 0
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case cons
S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p ↦ p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ (hd * tl.prod).coeff (n + n * tl.length) = hd.coeff n * tl.prod.coeff (n * tl.length)

Tactic:
]

Goal state after:
case cons
S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p ↦ p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ (hd * tl.prod).coeff (n + n * tl.length) = hd.coeff n * tl.prod.coeff (n * tl.length)
Module: Mathlib.Algebra.Polynomial.Monic

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

pp: case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ ∀ i ∈ t, (f i).Monic

pp: case refine_2.hp
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (f a).Monic

pp: case refine_2.hq
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (Multiset.map f t).prod.Monic

Tactic:
]

Goal state after:
case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ ∀ i ∈ t, (f i).Monic

case refine_2.hp
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (f a).Monic

case refine_2.hq
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (Multiset.map f t).prod.Monic
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} (f : α → β), (fun x ↦ x) ∘ f = f
h₁ : ∀ {α : Type ?u.55} {β : Type ?u.57} (f : α → β), (f ∘ fun x ↦ x) = f
⊢ (f.support.sup fun m ↦ m 0) = f.support.sup fun m ↦ m 0

Tactic:
]

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

Goal state before:
pp: S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p ↦ p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ (List.map natDegree tl).sum ≤ (List.map natDegree tl).length * n

Tactic:
]

Goal state after:
S : Type u_1
inst✝ : Semiring S
n : ℕ
hd : S[X]
tl : List S[X]
IH : (∀ p ∈ tl, p.natDegree ≤ n) → tl.prod.coeff (tl.length * n) = (List.map (fun p ↦ p.coeff n) tl).prod
hl : ∀ p ∈ hd :: tl, p.natDegree ≤ n
hl' : ∀ p ∈ tl, p.natDegree ≤ n
⊢ (List.map natDegree tl).sum ≤ (List.map natDegree tl).length * n