mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
hd : d = 0
⊢ coeff d f = coeff d (C (coeff 0 f))

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ coeff d f = coeff d (C (coeff 0 f))

Tactic:
·

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
hd : d = 0
⊢ coeff d f = coeff d (C (coeff 0 f))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ coeff d f = coeff d (C (coeff 0 f))

Tactic:
·

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ coeff d f = coeff d (C (coeff 0 f))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∈ f.support
⊢ m.toSyn b ≤ m.toSyn (m.degree f) ∨ m.toSyn b ≤ m.toSyn (m.degree g)

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∉ f.support
⊢ m.toSyn b ≤ m.toSyn (m.degree f) ∨ m.toSyn b ≤ m.toSyn (m.degree g)

Tactic:
·

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∈ f.support
⊢ m.toSyn b ≤ m.toSyn (m.degree f) ∨ m.toSyn b ≤ m.toSyn (m.degree g)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∉ f.support
⊢ m.toSyn b ≤ m.toSyn (m.degree f) ∨ m.toSyn b ≤ m.toSyn (m.degree g)

Tactic:
·

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∉ f.support
⊢ m.toSyn b ≤ m.toSyn (m.degree f) ∨ m.toSyn b ≤ m.toSyn (m.degree g)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree (f + g)) ≤ m.toSyn (m.degree f)

pp: case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree f) ≤ m.toSyn (m.degree (f + g))

Tactic:
·

Goal state after:
case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree (f + g)) ≤ m.toSyn (m.degree f)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree f) ≤ m.toSyn (m.degree (f + g))

Tactic:
·

Goal state after:
case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree f) ≤ m.toSyn (m.degree (f + g))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree (f + g)) = max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' : ¬m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree (f + g)) = max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))

Tactic:
·

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree (f + g)) = max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' : ¬m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree (f + g)) = max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))

Tactic:
·

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.degree f ≠ m.degree g
h' : ¬m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree (f + g)) = max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : m.toSyn (m.degree f) < m.toSyn d
⊢ coeff d f * coeff e g = 0

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : ¬m.toSyn (m.degree f) < m.toSyn d
⊢ coeff d f * coeff e g = 0

Tactic:
·

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : m.toSyn (m.degree f) < m.toSyn d
⊢ coeff d f * coeff e g = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : ¬m.toSyn (m.degree f) < m.toSyn d
⊢ coeff d f * coeff e g = 0

Tactic:
·

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : ¬m.toSyn (m.degree f) < m.toSyn d
⊢ coeff d f * coeff e g = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case h₀
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha : m.toSyn (m.degree f) ≤ m.toSyn a
hb : m.toSyn (m.degree g) ≤ m.toSyn b
⊢ ∀ b_1 ∈ Finset.antidiagonal (a + b), b_1 ≠ (a, b) → coeff b_1.1 f * coeff b_1.2 g = 0

pp: case h₁
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha : m.toSyn (m.degree f) ≤ m.toSyn a
hb : m.toSyn (m.degree g) ≤ m.toSyn b
⊢ (a, b) ∉ Finset.antidiagonal (a + b) → coeff (a, b).1 f * coeff (a, b).2 g = 0

Tactic:
·

Goal state after:
case h₀
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha : m.toSyn (m.degree f) ≤ m.toSyn a
hb : m.toSyn (m.degree g) ≤ m.toSyn b
⊢ ∀ b_1 ∈ Finset.antidiagonal (a + b), b_1 ≠ (a, b) → coeff b_1.1 f * coeff b_1.2 g = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha : m.toSyn (m.degree f) ≤ m.toSyn a
hb : m.toSyn (m.degree g) ≤ m.toSyn b
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf : m.toSyn (m.degree f) < m.toSyn c
⊢ coeff (c, d).1 f * coeff (c, d).2 g = 0

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha : m.toSyn (m.degree f) ≤ m.toSyn a
hb : m.toSyn (m.degree g) ≤ m.toSyn b
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf : ¬m.toSyn (m.degree f) < m.toSyn c
⊢ coeff (c, d).1 f * coeff (c, d).2 g = 0

Tactic:
·

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha : m.toSyn (m.degree f) ≤ m.toSyn a
hb : m.toSyn (m.degree g) ≤ m.toSyn b
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf : m.toSyn (m.degree f) < m.toSyn c
⊢ coeff (c, d).1 f * coeff (c, d).2 g = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat

Goal state before:
pp: case zero
b : ℕ
h : DvdNotUnit 0 b
⊢ (if 0 = 0 then ⊤ else ↑0) < if b = 0 then ⊤ else ↑b

pp: case succ
b a : ℕ
h : DvdNotUnit (a + 1) b
⊢ (if a + 1 = 0 then ⊤ else ↑(a + 1)) < if b = 0 then ⊤ else ↑b

Tactic:
·

Goal state after:
case zero
b : ℕ
h : DvdNotUnit 0 b
⊢ (if 0 = 0 then ⊤ else ↑0) < if b = 0 then ⊤ else ↑b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat

Goal state before:
pp: case succ.zero
a : ℕ
h : DvdNotUnit (a + 1) 0
⊢ (if a + 1 = 0 then ⊤ else ↑(a + 1)) < if 0 = 0 then ⊤ else ↑0

pp: case succ.succ
a n✝ : ℕ
h : DvdNotUnit (a + 1) (n✝ + 1)
⊢ (if a + 1 = 0 then ⊤ else ↑(a + 1)) < if n✝ + 1 = 0 then ⊤ else ↑(n✝ + 1)

Tactic:
·

Goal state after:
case succ.zero
a : ℕ
h : DvdNotUnit (a + 1) 0
⊢ (if a + 1 = 0 then ⊤ else ↑(a + 1)) < if 0 = 0 then ⊤ else ↑0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat

Goal state before:
pp: n : ℕ
⊢ Associated (normalizedFactors (n + 1)).prod (↑(n + 1).primeFactorsList).prod

pp: n : ℕ
⊢ ∀ x ∈ ↑(n + 1).primeFactorsList, Irreducible x

Tactic:
·

Goal state after:
n : ℕ
⊢ Associated (normalizedFactors (n + 1)).prod (↑(n + 1).primeFactorsList).prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat

Goal state before:
pp: n : ℕ
⊢ ∀ x ∈ ↑(n + 1).primeFactorsList, Irreducible x

Tactic:
·

Goal state after:
n : ℕ
⊢ ∀ x ∈ ↑(n + 1).primeFactorsList, Irreducible x
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha : m.toSyn (m.degree f) ≤ m.toSyn a
hb : m.toSyn (m.degree g) ≤ m.toSyn b
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf : ¬m.toSyn (m.degree f) < m.toSyn c
⊢ coeff (c, d).1 f * coeff (c, d).2 g = 0

Tactic:
·

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha : m.toSyn (m.degree f) ≤ m.toSyn a
hb : m.toSyn (m.degree g) ≤ m.toSyn b
c d : σ →₀ ℕ
h : (c, d) ≠ (a, b)
hcd : c + d = a + b
hf : ¬m.toSyn (m.degree f) < m.toSyn c
⊢ coeff (c, d).1 f * coeff (c, d).2 g = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case h₁
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha : m.toSyn (m.degree f) ≤ m.toSyn a
hb : m.toSyn (m.degree g) ≤ m.toSyn b
⊢ (a, b) ∉ Finset.antidiagonal (a + b) → coeff (a, b).1 f * coeff (a, b).2 g = 0

Tactic:
·

Goal state after:
case h₁
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
a b : σ →₀ ℕ
ha : m.toSyn (m.degree f) ≤ m.toSyn a
hb : m.toSyn (m.degree g) ≤ m.toSyn b
⊢ (a, b) ∉ Finset.antidiagonal (a + b) → coeff (a, b).1 f * coeff (a, b).2 g = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
hg : g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
hg : ¬g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
·

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
hg : g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
hg : ¬g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
·

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
hg : ¬g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : m.leadingCoeff g ∈ R⁰
hf : f = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : m.leadingCoeff g ∈ R⁰
hf : ¬f = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
·

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : m.leadingCoeff g ∈ R⁰
hf : f = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : m.leadingCoeff g ∈ R⁰
hf : ¬f = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
·

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : m.leadingCoeff g ∈ R⁰
hf : ¬f = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : IsRegular (m.leadingCoeff f)
hg : g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : IsRegular (m.leadingCoeff f)
hg : ¬g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
·

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : IsRegular (m.leadingCoeff f)
hg : g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : IsRegular (m.leadingCoeff f)
hg : ¬g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
·

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : IsRegular (m.leadingCoeff f)
hg : ¬g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : IsRegular (m.leadingCoeff g)
hf : f = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : IsRegular (m.leadingCoeff g)
hf : ¬f = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
·

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : IsRegular (m.leadingCoeff g)
hf : f = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : IsRegular (m.leadingCoeff g)
hf : ¬f = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
·

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : IsRegular (m.leadingCoeff g)
hf : ¬f = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : MvPolynomial σ R
h : f = 0 ∨ g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : MvPolynomial σ R
h : f ≠ 0 ∧ g ≠ 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
·

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : MvPolynomial σ R
h : f = 0 ∨ g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
⊢ m.degree (f ^ n) = n • m.degree f

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : ¬f = 0
⊢ m.degree (f ^ n) = n • m.degree f

Tactic:
·

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
⊢ m.degree (f ^ n) = n • m.degree f
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: case calc_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
⊢ ↑(#({x ∈ piFinset fun i ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ = 0})) / ∏ i, ↑(#(S i)) +
      ↑(#({x ∈ piFinset fun i ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ ≠ 0})) / ∏ i, ↑(#(S i)) ≤
    (pₖ.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#(S i.succ))) + ↑(degreeOf 0 p) / ↑(#(S 0))

pp: case calc_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
⊢ (pₖ.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#(S i.succ))) + ↑(degreeOf 0 p) / ↑(#(S 0)) ≤
    p.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#(S i))

Tactic:
·

Goal state after:
case calc_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
⊢ ↑(#({x ∈ piFinset fun i ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ = 0})) / ∏ i, ↑(#(S i)) +
      ↑(#({x ∈ piFinset fun i ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ ≠ 0})) / ∏ i, ↑(#(S i)) ≤
    (pₖ.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#(S i.succ))) + ↑(degreeOf 0 p) / ↑(#(S 0))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
hn : n = 0
⊢ m.degree (0 ^ n) = 0

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
hn : ¬n = 0
⊢ m.degree (0 ^ n) = 0

Tactic:
·

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
hn : n = 0
⊢ m.degree (0 ^ n) = 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
hn : ¬n = 0
⊢ m.degree (0 ^ n) = 0

Tactic:
·

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
hn : ¬n = 0
⊢ m.degree (0 ^ n) = 0
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: case h₁
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
⊢ ↑(#({x ∈ piFinset fun i ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ = 0})) / ∏ i, ↑(#(S i)) ≤
    pₖ.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#(S i.succ))

pp: case h₂
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
⊢ ↑(#({x ∈ piFinset fun i ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ ≠ 0})) / ∏ i, ↑(#(S i)) ≤
    ↑(degreeOf 0 p) / ↑(#(S 0))

Tactic:
·

Goal state after:
case h₁
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
⊢ ↑(#({x ∈ piFinset fun i ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ = 0})) / ∏ i, ↑(#(S i)) ≤
    pₖ.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#(S i.succ))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : r ∈ R⁰
f : MvPolynomial σ R
hf : f = 0
⊢ m.degree (r • f) = m.degree f

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : r ∈ R⁰
f : MvPolynomial σ R
hf : ¬f = 0
⊢ m.degree (r • f) = m.degree f

Tactic:
·

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
hr : r ∈ R⁰
f : MvPolynomial σ R
hf : f = 0
⊢ m.degree (r • f) = m.degree f