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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
⊢ ∏ i ∈ s, m.leadingCoeff (P i) = 1

pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
⊢ ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
⊢ ∏ i ∈ s, m.leadingCoeff (P i) = 1

σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
⊢ ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
i : ι
hi : i ∈ s
⊢ IsRegular 1

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
i : ι
hi : i ∈ s
⊢ IsRegular 1
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
⊢ (↑n.primeFactorsList).Nodup ↔ n.primeFactorsList.Nodup

Tactic:
]

Goal state after:
n : ℕ
h0 : n ≠ 0
⊢ (↑n.primeFactorsList).Nodup ↔ n.primeFactorsList.Nodup
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case inr
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
⊢ n.factorization p ≤ 1

Tactic:
]

Goal state after:
case inr
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
⊢ n.factorization p ≤ 1
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case pos
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
this : emultiplicity p n ≤ 1 ∨ IsUnit p
⊢ multiplicity p n ≤ 1

Tactic:
]

Goal state after:
case pos
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
this : emultiplicity p n ≤ 1 ∨ IsUnit p
⊢ multiplicity p n ≤ 1
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case neg
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : ¬Prime p
⊢ 0 ≤ 1

Tactic:
]

Goal state after:
case neg
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : ¬Prime p
⊢ 0 ≤ 1
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), n.factorization p ≤ 1
⊢ ∀ (a : ℕ), List.count a n.primeFactorsList ≤ 1

Tactic:
]

Goal state after:
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), n.factorization p ≤ 1
⊢ ∀ (a : ℕ), List.count a n.primeFactorsList ≤ 1
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), n.factorization p ≤ 1
a : ℕ
⊢ n.factorization a ≤ 1

Tactic:
]

Goal state after:
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), n.factorization p ≤ 1
a : ℕ
⊢ n.factorization a ≤ 1
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: 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
⊢ #({r ∈ piFinset (tail S) | (eval r) pₖ ≠ 0}.biUnion fun a ↦
        filter ((fun x ↦ (eval x) p = 0) ∘ ⇑(consEquiv fun i ↦ R).toEmbedding) (image (fun a_1 ↦ (a_1, a)) (S 0))) =
    #({xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}.biUnion fun xₜ ↦
        image (fun x₀ ↦ (x₀, xₜ)) ({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0}))

Tactic:
]

Goal state after:
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
⊢ #({r ∈ piFinset (tail S) | (eval r) pₖ ≠ 0}.biUnion fun a ↦
        filter ((fun x ↦ (eval x) p = 0) ∘ ⇑(consEquiv fun i ↦ R).toEmbedding) (image (fun a_1 ↦ (a_1, a)) (S 0))) =
    #({xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}.biUnion fun xₜ ↦
        image (fun x₀ ↦ (x₀, xₜ)) ({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0}))
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : n.factorization p = 0 ↔ m.factorization p = 0
⊢ n.factorization p = m.factorization p

Tactic:
]

Goal state after:
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : n.factorization p = 0 ↔ m.factorization p = 0
⊢ n.factorization p = m.factorization p
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case neg
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : ¬Prime p
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
this : 2 ≤ k
⊢ n ^ 2 ∣ n ^ k

Tactic:
]

Goal state after:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
this : 2 ≤ k
⊢ n ^ 2 ∣ n ^ k
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
⊢ (Squarefree n ∧ ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n) → Prime n

Tactic:
]

Goal state after:
n : ℕ
⊢ (Squarefree n ∧ ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n) → Prime n
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: p k : ℕ
hp : Prime p
hk : 0 < k
h : Squarefree p ∧ k = 1
⊢ Prime (p ^ k)

Tactic:
]

Goal state after:
p k : ℕ
hp : Prime p
hk : 0 < k
h : Squarefree p ∧ k = 1
⊢ Prime (p ^ k)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ m.degree p = m.degree q ∧ m.leadingCoeff p = m.leadingCoeff q ∨ m.leadingCoeff p = 0 ∧ m.leadingCoeff q = 0 ↔
    m.leadingCoeff p = m.leadingCoeff q ∧ m.degree p = m.degree q

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial σ R
⊢ m.degree p = m.degree q ∧ m.leadingCoeff p = m.leadingCoeff q ∨ m.leadingCoeff p = 0 ∧ m.leadingCoeff q = 0 ↔
    m.leadingCoeff p = m.leadingCoeff q ∧ m.degree p = m.degree q
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: p k : ℕ
hp : Prime p
hk : 0 < k
h : Squarefree p ∧ k = 1
⊢ Prime p

Tactic:
]

Goal state after:
p k : ℕ
hp : Prime p
hk : 0 < k
h : Squarefree p ∧ k = 1
⊢ Prime p
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case none
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
H : ∀ (x : ℕ), Prime x → ¬x * x ∣ n / k
⊢ ∀ (x : ℕ), Prime x → ¬x * x ∣ n

Tactic:
]

Goal state after:
case none
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
H : ∀ (x : ℕ), Prime x → ¬x * x ∣ n / k
⊢ ∀ (x : ℕ), Prime x → ¬x * x ∣ n
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
⊢ n.MinSqFacProp
    (if h : n < k * k then none
    else
      have this := ⋯;
      if k ∣ n then
        let n' := n / k;
        have this := ⋯;
        if k ∣ n' then some k else n'.minSqFacAux (k + 2)
      else n.minSqFacAux (k + 2))

Tactic:
]

Goal state after:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
⊢ n.MinSqFacProp
    (if h : n < k * k then none
    else
      have this := ⋯;
      if k ∣ n then
        let n' := n / k;
        have this := ⋯;
        if k ∣ n' then some k else n'.minSqFacAux (k + 2)
      else n.minSqFacAux (k + 2))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
⊢ ∀ (y : MvPolynomial σ R), f * y = 0 → y = 0

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
⊢ ∀ (y : MvPolynomial σ R), f * y = 0 → y = 0
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : n'.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : Prime m
d : (2 * i + 3).succ ∣ n'
ml : k < m
me : k.succ = m
⊢ False

Tactic:
]

Goal state after:
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : n'.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : Prime m
d : (2 * i + 3).succ ∣ n'
ml : k < m
me : k.succ = m
⊢ False
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: 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ₜ : Fin n → R
hxₜ : xₜ ∈ {xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}
pₓ : Polynomial R := Polynomial.map (eval xₜ) p'
hpₓ : pₓ = Polynomial.map (eval xₜ) p'
⊢ p'.natDegree = p'.natDegree

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this✝ : n'.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : Prime m
ml : k < m
me : k.succ = m
d : 2 * (i + 2) ∣ n'
this : 2 * i + 3 ≤ 2
⊢ False

Tactic:
]

Goal state after:
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this✝ : n'.sqrt - k < n.sqrt + 2 - k
m : ℕ
m2 : Prime m
ml : k < m
me : k.succ = m
d : 2 * (i + 2) ∣ n'
this : 2 * i + 3 ≤ 2
⊢ False
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp (some d)
⊢ Prime d

Tactic:
]

Goal state after:
n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp (some d)
⊢ Prime d
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp (some d)
⊢ d * d ∣ n

Tactic:
]

Goal state after:
n d : ℕ
h : n.minSqFac = some d
this : n.MinSqFacProp (some d)
⊢ d * d ∣ n
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n d : ℕ
h : n.minSqFac = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : n.MinSqFacProp (some d)
⊢ d ≤ m

Tactic:
]

Goal state after:
n d : ℕ
h : n.minSqFac = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : n.MinSqFacProp (some d)
⊢ d ≤ m
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
h0 : f ≠ 0 ∧ g ≠ 0
hf : ∀ (x : MvPolynomial σ R), f * x = 0 → x = 0
⊢ f * g ≠ 0

Tactic:
]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h0 : f ≠ 0 ∧ g ≠ 0
hf : ∀ (x : MvPolynomial σ R), f * x = 0 → x = 0
⊢ f * g ≠ 0
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case mp.some
n : ℕ
H : Squarefree n
d : ℕ
this : n.MinSqFacProp (some d)
e : n.minSqFac = some d
⊢ some d = none

Tactic:
]

Goal state after:
case mp.some
n : ℕ
H : Squarefree n
d : ℕ
this : n.MinSqFacProp (some d)
e : n.minSqFac = some d
⊢ some d = none
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case mpr
n : ℕ
this : n.MinSqFacProp none
H : n.minSqFac = none
⊢ Squarefree n

Tactic:
]

Goal state after:
case mpr
n : ℕ
this : n.MinSqFacProp none
H : n.minSqFac = none
⊢ Squarefree n
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: ⊢ (primeFactorsList 2).Nodup

pp: ⊢ 2 ≠ 0

Tactic:
]

Goal state after:
⊢ (primeFactorsList 2).Nodup

⊢ 2 ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff g ∈ R⁰
⊢ m.withBotDegree g + m.withBotDegree f = m.withBotDegree g + m.withBotDegree f

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
⊢ ∀ (a : ℕ),
    a ∈ {d ∈ n.divisors | Squarefree d}.val ↔
      a ∈ Multiset.map (fun x ↦ x.val.prod) (normalizedFactors n).toFinset.powerset.val

pp: n : ℕ
h0 : n ≠ 0
⊢ ∀ x ∈ (normalizedFactors n).toFinset.powerset.val,
    ∀ y ∈ (normalizedFactors n).toFinset.powerset.val, x.val.prod = y.val.prod → x = y

Tactic:
]

Goal state after:
n : ℕ
h0 : n ≠ 0
⊢ ∀ (a : ℕ),
    a ∈ {d ∈ n.divisors | Squarefree d}.val ↔
      a ∈ Multiset.map (fun x ↦ x.val.prod) (normalizedFactors n).toFinset.powerset.val

n : ℕ
h0 : n ≠ 0
⊢ ∀ x ∈ (normalizedFactors n).toFinset.powerset.val,
    ∀ y ∈ (normalizedFactors n).toFinset.powerset.val, x.val.prod = y.val.prod → x = y
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: 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ₜ : Fin n → R
hxₜ : xₜ ∈ {xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}
pₓ : Polynomial R := Polynomial.map (eval xₜ) p'
hpₓ : pₓ = Polynomial.map (eval xₜ) p'
hpₓdeg : pₓ.natDegree = k
h : pₓ = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
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
inst✝ : NoZeroDivisors R
a✝ : Nontrivial R
hf : m.leadingCoeff f ∈ R⁰
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

Tactic:
]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
f g : MvPolynomial σ R
inst✝ : NoZeroDivisors R
a✝ : Nontrivial R
hf : m.leadingCoeff f ∈ R⁰
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case h
a : ℕ
hsq : Squarefree a
b : ℕ
h0✝ : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ (normalizedFactors a).toFinset ⊆ (normalizedFactors (a * b)).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a

Tactic:
]

Goal state after:
case h
a : ℕ
hsq : Squarefree a
b : ℕ
h0✝ : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ (normalizedFactors a).toFinset ⊆ (normalizedFactors (a * b)).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case h
a : ℕ
hsq : (normalizedFactors a).Nodup
b : ℕ
h0✝ : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ (normalizedFactors a).toFinset ⊆ (normalizedFactors (a * b)).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a

Tactic:
]

Goal state after:
case h
a : ℕ
hsq : (normalizedFactors a).Nodup
b : ℕ
h0✝ : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ (normalizedFactors a).toFinset ⊆ (normalizedFactors (a * b)).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case h
a : ℕ
hsq : (normalizedFactors a).Nodup
b : ℕ
h0✝ : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ normalizedFactors a ⊆ normalizedFactors a + normalizedFactors b ∧ Associated (normalizedFactors a).prod a

Tactic:
]

Goal state after:
case h
a : ℕ
hsq : (normalizedFactors a).Nodup
b : ℕ
h0✝ : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ normalizedFactors a ⊆ normalizedFactors a + normalizedFactors b ∧ Associated (normalizedFactors a).prod a
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case mpr
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
⊢ (s.val.prod ∣ n ∧ n ≠ 0) ∧ Squarefree s.val.prod

Tactic:
]

Goal state after:
case mpr
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
⊢ (s.val.prod ∣ n ∧ n ≠ 0) ∧ Squarefree s.val.prod
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
⊢ 0 ∉ s.val

Tactic:
]

Goal state after:
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
⊢ 0 ∉ s.val
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case mpr
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
⊢ (s.val.prod ∣ (normalizedFactors n).prod ∧ n ≠ 0) ∧ Squarefree s.val.prod

Tactic:
]

Goal state after:
case mpr
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
⊢ (s.val.prod ∣ (normalizedFactors n).prod ∧ n ≠ 0) ∧ Squarefree s.val.prod
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: 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ₜ : Fin n → R
hxₜ : xₜ ∈ {xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}
pₓ : Polynomial R := Polynomial.map (eval xₜ) p'
hpₓ : pₓ = Polynomial.map (eval xₜ) p'
hpₓdeg : pₓ.natDegree = k
hpₓ₀ : pₓ ≠ 0
⊢ pₖ ≠ 0

Tactic:
]

Goal state after:
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ₜ : Fin n → R
hxₜ : xₜ ∈ {xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}
pₓ : Polynomial R := Polynomial.map (eval xₜ) p'
hpₓ : pₓ = Polynomial.map (eval xₜ) p'
hpₓdeg : pₓ.natDegree = k
hpₓ₀ : pₓ ≠ 0
⊢ pₖ ≠ 0
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case mpr
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
h : normalizedFactors s.val.prod = s.val
⊢ Squarefree s.val.prod

Tactic:
]

Goal state after:
case mpr
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
h : normalizedFactors s.val.prod = s.val
⊢ Squarefree s.val.prod
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case mpr
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
h : normalizedFactors s.val.prod = s.val
⊢ s.val.Nodup

Tactic:
]

Goal state after:
case mpr
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
h : normalizedFactors s.val.prod = s.val
⊢ s.val.Nodup
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
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 i ↦ ∑ i_1, ↑(i i_1) / ↑(#(S i_1.succ)) + ↑(degreeOf 0 p) / ↑(#(S 0))) ≤
    p.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#(S i))

Tactic:
]

Goal state after:
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 i ↦ ∑ i_1, ↑(i i_1) / ↑(#(S i_1.succ)) + ↑(degreeOf 0 p) / ↑(#(S 0))) ≤
    p.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#(S i))
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ∈ (normalizedFactors n).toFinset.powerset.val
y : Finset ℕ
hy : y ∈ (normalizedFactors n).toFinset.powerset.val
h : x.val.prod = y.val.prod
⊢ Multiset.Rel (fun x1 x2 ↦ Associated x1 x2) x.val y.val

Tactic:
]

Goal state after:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ∈ (normalizedFactors n).toFinset.powerset.val
y : Finset ℕ
hy : y ∈ (normalizedFactors n).toFinset.powerset.val
h : x.val.prod = y.val.prod
⊢ Multiset.Rel (fun x1 x2 ↦ Associated x1 x2) x.val y.val
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
⊢ Multiset.Rel (fun x1 x2 ↦ Associated x1 x2) x.val y.val

Tactic:
]

Goal state after:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
⊢ Multiset.Rel (fun x1 x2 ↦ Associated x1 x2) x.val y.val
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
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
i : Fin n →₀ ℕ
hi : i ∈ pₖ.support
⊢ ↑(degreeOf 0 p) / ↑(#(S 0)) + ∑ i_1, ↑(i i_1) / ↑(#(S i_1.succ)) ≤
    ↑((Finsupp.cons p'.natDegree i) 0) / ↑(#(S 0)) + ∑ i_1, ↑((Finsupp.cons p'.natDegree i) i_1.succ) / ↑(#(S i_1.succ))

Tactic:
]

Goal state after:
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
i : Fin n →₀ ℕ
hi : i ∈ pₖ.support
⊢ ↑(degreeOf 0 p) / ↑(#(S 0)) + ∑ i_1, ↑(i i_1) / ↑(#(S i_1.succ)) ≤
    ↑((Finsupp.cons p'.natDegree i) 0) / ↑(#(S 0)) + ∑ i_1, ↑((Finsupp.cons p'.natDegree i) i_1.succ) / ↑(#(S i_1.succ))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toWithBotSyn (m.withBotDegree f) < m.toWithBotSyn (m.withBotDegree g)
⊢ m.withBotDegree g = m.withBotDegree g

Tactic:
]

Goal state after: