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

Goal state before:
pp: case succ.succ.refine_1
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ f.eraseLead.natDegree < (C f.leadingCoeff * X ^ f.natDegree).natDegree

pp: case succ.succ.refine_2
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ (C f.leadingCoeff * X ^ f.natDegree).natDegree ≤ N

pp: case succ.succ.refine_3
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ motive f.eraseLead

pp: case succ.succ.refine_4
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ motive (C f.leadingCoeff * X ^ f.natDegree)

Tactic:
·

Goal state after:
case succ.succ.refine_1
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ f.eraseLead.natDegree < (C f.leadingCoeff * X ^ f.natDegree).natDegree
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case refine_3
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
⊢ ∀ (f g : R[X]),
    f.natDegree < g.natDegree →
      g.natDegree ≤ N →
        eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f →
          eval₂ i (⅟x) (reflect N g) * x ^ N = eval₂ i x g →
            eval₂ i (⅟x) (reflect N (f + g)) * x ^ N = eval₂ i x (f + g)

Tactic:
·

Goal state after:
case refine_3
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
⊢ ∀ (f g : R[X]),
    f.natDegree < g.natDegree →
      g.natDegree ≤ N →
        eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f →
          eval₂ i (⅟x) (reflect N g) * x ^ N = eval₂ i x g →
            eval₂ i (⅟x) (reflect N (f + g)) * x ^ N = eval₂ i x (f + g)
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case succ.succ.refine_1.refine_1
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ 2 ≤ #f.support

pp: case succ.succ.refine_1.refine_2
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ f.natDegree = (C f.leadingCoeff * X ^ f.natDegree).natDegree

Tactic:
·

Goal state after:
case succ.succ.refine_1.refine_1
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ 2 ≤ #f.support
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case succ.succ.refine_1.refine_2
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ f.natDegree = (C f.leadingCoeff * X ^ f.natDegree).natDegree

Tactic:
·

Goal state after:
case succ.succ.refine_1.refine_2
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ f.natDegree = (C f.leadingCoeff * X ^ f.natDegree).natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case pos
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
hp0 : p = 0
⊢ Irreducible (p * C p.leadingCoeff⁻¹) ↔ Irreducible p

pp: case neg
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
hp0 : ¬p = 0
⊢ Irreducible (p * C p.leadingCoeff⁻¹) ↔ Irreducible p

Tactic:
·

Goal state after:
case pos
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
hp0 : p = 0
⊢ Irreducible (p * C p.leadingCoeff⁻¹) ↔ Irreducible p
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
c : p = 0
⊢ ((optionEquivLeft R σ) p).natDegree = degreeOf none p

pp: case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
c : ¬p = 0
⊢ ((optionEquivLeft R σ) p).natDegree = degreeOf none p

Tactic:
·

Goal state after:
case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
c : p = 0
⊢ ((optionEquivLeft R σ) p).natDegree = degreeOf none p
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
c : ¬p = 0
⊢ ((optionEquivLeft R σ) p).natDegree = degreeOf none p

Tactic:
·

Goal state after:
case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
c : ¬p = 0
⊢ ((optionEquivLeft R σ) p).natDegree = degreeOf none p
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

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

Tactic:
have h₁ : (leadingCoeff q)⁻¹ ≠ 0 := inv_ne_zero (mt leadingCoeff_eq_zero.1 h)
  rw [degree_mul_C h₁]

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

Goal state before:
pp: case pos
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ((optionEquivLeft R S₁) p).coeff i = 0
⊢ (((optionEquivLeft R S₁) p).coeff i).totalDegree + i ≤ p.totalDegree

pp: case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
⊢ (((optionEquivLeft R S₁) p).coeff i).totalDegree + i ≤ p.totalDegree

Tactic:
·

Goal state after:
case pos
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ((optionEquivLeft R S₁) p).coeff i = 0
⊢ (((optionEquivLeft R S₁) p).coeff i).totalDegree + i ≤ p.totalDegree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case pos
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
hp : p = 0
⊢ (p * C p.leadingCoeff⁻¹).degree = p.degree

pp: case neg
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
hp : ¬p = 0
⊢ (p * C p.leadingCoeff⁻¹).degree = p.degree

Tactic:
·

Goal state after:
case pos
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
hp : p = 0
⊢ (p * C p.leadingCoeff⁻¹).degree = p.degree
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case succ.succ.refine_2
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ (C f.leadingCoeff * X ^ f.natDegree).natDegree ≤ N

pp: case succ.succ.refine_3
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ motive f.eraseLead

pp: case succ.succ.refine_4
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ motive (C f.leadingCoeff * X ^ f.natDegree)

Tactic:
·

Goal state after:
case succ.succ.refine_2
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ (C f.leadingCoeff * X ^ f.natDegree).natDegree ≤ N
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

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:
·

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
⊢ eval₂ i (⅟x) (reflect N f) = 0 → eval₂ i (⅟x) (reflect N f) * x ^ N = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case succ.succ.refine_3
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ motive f.eraseLead

pp: case succ.succ.refine_4
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ motive (C f.leadingCoeff * X ^ f.natDegree)

Tactic:
·

Goal state after:
case succ.succ.refine_3
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ motive f.eraseLead
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case succ.succ.refine_4
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ motive (C f.leadingCoeff * X ^ f.natDegree)

Tactic:
·

Goal state after:
case succ.succ.refine_4
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ motive (C f.leadingCoeff * X ^ f.natDegree)
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:
·

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
⊢ 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 neg.refine_1
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ (i + σ.sum fun x e ↦ e) ≤ (embDomain Embedding.some σ + Finsupp.single none i).sum fun x e ↦ e

pp: case neg.refine_2
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ embDomain Embedding.some σ + Finsupp.single none i ∈ p.support

Tactic:
·

Goal state after:
case neg.refine_1
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ (i + σ.sum fun x e ↦ e) ≤ (embDomain Embedding.some σ + Finsupp.single none i).sum fun x e ↦ e
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case neg.refine_2
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ embDomain Embedding.some σ + Finsupp.single none i ∈ p.support

Tactic:
·

Goal state after:
case neg.refine_2
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ embDomain Embedding.some σ + Finsupp.single none i ∈ p.support
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case pos
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ((optionEquivLeft R S₁) p).coeff i = 0
⊢ (((optionEquivLeft R S₁) p).coeff i).totalDegree ≤ p.totalDegree

pp: case neg
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
⊢ (((optionEquivLeft R S₁) p).coeff i).totalDegree ≤ p.totalDegree

Tactic:
·

Goal state after:
case pos
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ((optionEquivLeft R S₁) p).coeff i = 0
⊢ (((optionEquivLeft R S₁) p).coeff i).totalDegree ≤ p.totalDegree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R
⊢ (p.comp (X + C r)).Monic

Tactic:
by
  nontriviality R
  refine hp.comp (monic_X_add_C _) fun ha ↦ ?_
  rw [natDegree_X_add_C] at ha
  exact one_ne_zero ha

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : q = 0
⊢ (p * q).degree = (q * p).degree

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ (p * q).degree = (q * p).degree

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : q = 0
⊢ (p * q).degree = (q * p).degree
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
⊢ p.degree + q.degree = q.degree + p.degree

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

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.degree + q.degree = q.degree + p.degree
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
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
·

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 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

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]),
    f.natDegree < g.natDegree →
      g.natDegree ≤ p.natDegree →
        (φ f).natDegree = fu f.natDegree →
          (φ g).natDegree = fu g.natDegree → (φ (f + g)).natDegree = fu (f + g).natDegree

Tactic:
·

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.MvPolynomial.Equiv

Goal state before:
pp: case neg.refine_1
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ (σ.sum fun x e ↦ e) ≤ (embDomain Embedding.some σ + Finsupp.single none i).sum fun x e ↦ e

pp: case neg.refine_2
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ embDomain Embedding.some σ + Finsupp.single none i ∈ p.support

Tactic:
·

Goal state after:
case neg.refine_1
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ (σ.sum fun x e ↦ e) ≤ (embDomain Embedding.some σ + Finsupp.single none i).sum fun x e ↦ e
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case neg.refine_2
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ embDomain Embedding.some σ + Finsupp.single none i ∈ p.support

Tactic:
·

Goal state after:
case neg.refine_2
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hpi : ¬((optionEquivLeft R S₁) p).coeff i = 0
σ : S₁ →₀ ℕ
hσ : σ ∈ (((optionEquivLeft R S₁) p).coeff i).support
⊢ embDomain Embedding.some σ + Finsupp.single none i ∈ p.support
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : q = 0
⊢ (p * q).natDegree = (q * p).natDegree

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ (p * q).natDegree = (q * p).natDegree

Tactic:
·

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : q = 0
⊢ (p * q).natDegree = (q * p).natDegree
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f = 0
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree

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

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f = 0
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case neg.a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.natDegree ≤ f.reverse.natDegree + f.natTrailingDegree

pp: case a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.reverse.natDegree + f.natTrailingDegree ≤ f.natDegree

Tactic:
·

Goal state after:
case neg.a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.natDegree ≤ f.reverse.natDegree + f.natTrailingDegree
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case hC
R : Type u
inst✝ : CommSemiring R
n : ℕ
i : R
⊢ ((↑(finSuccEquiv R n)).comp C) i =
    ((eval₂Hom (Polynomial.C.comp C) fun i ↦ Fin.cases Polynomial.X (fun k ↦ Polynomial.C (X k)) i).comp C) i

pp: case hX
R : Type u
inst✝ : CommSemiring R
n : ℕ
i : Fin (n + 1)
n✝ : ℕ
⊢ (↑(finSuccEquiv R n) (X i)).coeff n✝ =
    ((eval₂Hom (Polynomial.C.comp C) fun i ↦ Fin.cases Polynomial.X (fun k ↦ Polynomial.C (X k)) i) (X i)).coeff n✝

Tactic:
·

Goal state after:
case hC
R : Type u
inst✝ : CommSemiring R
n : ℕ
i : R
⊢ ((↑(finSuccEquiv R n)).comp C) i =
    ((eval₂Hom (Polynomial.C.comp C) fun i ↦ Fin.cases Polynomial.X (fun k ↦ Polynomial.C (X k)) i).comp C) i
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.reverse.natDegree + f.natTrailingDegree ≤ f.natDegree

Tactic:
·

Goal state after:
case a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.reverse.natDegree + f.natTrailingDegree ≤ f.natDegree