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

Goal state before:
pp: case e'_3
R : Type u
ι : Type w
inst✝ : CommSemiring R
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : l.Nodup
h : ∀ p ∈ { val := l, nodup := hl }, (f p).natDegree ≤ n
⊢ ∏ i ∈ { val := l, nodup := hl }, (f i).coeff n = (Multiset.map (fun p ↦ p.coeff n) (Multiset.map f l)).prod

pp: R : Type u
ι : Type w
inst✝ : CommSemiring R
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : l.Nodup
h : ∀ p ∈ { val := l, nodup := hl }, (f p).natDegree ≤ n
⊢ ∀ p ∈ Multiset.map f l, p.natDegree ≤ n

Tactic:
·

Goal state after:
case e'_3
R : Type u
ι : Type w
inst✝ : CommSemiring R
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : l.Nodup
h : ∀ p ∈ { val := l, nodup := hl }, (f p).natDegree ≤ n
⊢ ∏ i ∈ { val := l, nodup := hl }, (f i).coeff n = (Multiset.map (fun p ↦ p.coeff n) (Multiset.map f l)).prod
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
inst✝ : CommSemiring R
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : l.Nodup
h : ∀ p ∈ { val := l, nodup := hl }, (f p).natDegree ≤ n
⊢ ∀ p ∈ Multiset.map f l, p.natDegree ≤ n

Tactic:
·

Goal state after:
R : Type u
ι : Type w
inst✝ : CommSemiring R
f : ι → R[X]
n : ℕ
l : Multiset ι
hl : l.Nodup
h : ∀ p ∈ { val := l, nodup := hl }, (f p).natDegree ≤ n
⊢ ∀ p ∈ Multiset.map f l, p.natDegree ≤ n
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h :
  ∀ (f_1 g_1 : R[X]),
    f_1.Monic → g_1.Monic → f_1 * g_1 = f * g → ¬(0 < g_1.natDegree ∧ g_1.natDegree + g_1.natDegree ≤ (f * g).natDegree)
⊢ f.natDegree = 0 ∨ g.natDegree = 0

Tactic:
·

Goal state after:
case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h :
  ∀ (f_1 g_1 : R[X]),
    f_1.Monic → g_1.Monic → f_1 * g_1 = f * g → ¬(0 < g_1.natDegree ∧ g_1.natDegree + g_1.natDegree ≤ (f * g).natDegree)
⊢ f.natDegree = 0 ∨ g.natDegree = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ k i < Function.extend Fin.castSucc k (fun x ↦ f.natDegree) j

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ k i < Function.extend Fin.castSucc k (fun x ↦ f.natDegree) j
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ (prod 0).coeff 0 = (Multiset.map (fun f ↦ f.coeff 0) 0).prod

pp: case refine_2
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ht : t.prod.coeff 0 = (Multiset.map (fun f ↦ f.coeff 0) t).prod
⊢ (a ::ₘ t).prod.coeff 0 = (Multiset.map (fun f ↦ f.coeff 0) (a ::ₘ t)).prod

Tactic:
·

Goal state after:
case refine_1
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ (prod 0).coeff 0 = (Multiset.map (fun f ↦ f.coeff 0) 0).prod
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mpr.inl
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : f.natDegree ≠ 0 ∧ g.natDegree ≠ 0
hl : f.natDegree ≤ g.natDegree
⊢ ∃ f_1 g_1,
    f_1.Monic ∧
      g_1.Monic ∧ f_1 * g_1 = f * g ∧ g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree

pp: case mpr.inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : f.natDegree ≠ 0 ∧ g.natDegree ≠ 0
hl : g.natDegree ≤ f.natDegree
⊢ ∃ f_1 g_1,
    f_1.Monic ∧
      g_1.Monic ∧ f_1 * g_1 = f * g ∧ g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree

Tactic:
·

Goal state after:
case mpr.inl
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : f.natDegree ≠ 0 ∧ g.natDegree ≠ 0
hl : f.natDegree ≤ g.natDegree
⊢ ∃ f_1 g_1,
    f_1.Monic ∧
      g_1.Monic ∧ f_1 * g_1 = f * g ∧ g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mpr.inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : f.natDegree ≠ 0 ∧ g.natDegree ≠ 0
hl : g.natDegree ≤ f.natDegree
⊢ ∃ f_1 g_1,
    f_1.Monic ∧
      g_1.Monic ∧ f_1 * g_1 = f * g ∧ g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree

Tactic:
·

Goal state after:
case mpr.inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : R[X]
hf : f.Monic
hg : g.Monic
hp : (f * g).Monic
h : f.natDegree ≠ 0 ∧ g.natDegree ≠ 0
hl : g.natDegree ≤ f.natDegree
⊢ ∃ f_1 g_1,
    f_1.Monic ∧
      g_1.Monic ∧ f_1 * g_1 = f * g ∧ g_1.natDegree ≠ 0 ∧ g_1.natDegree + g_1.natDegree ≤ f.natDegree + g.natDegree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)) →
    ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p

pp: case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p) →
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)

Tactic:
·

Goal state after:
case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)) →
    ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝ : CommRing R
t : Multiset R
⊢ (Multiset.map (fun i ↦ (X - C i).nextCoeff) t).sum = -t.sum

pp: case h
R : Type u
inst✝ : CommRing R
t : Multiset R
⊢ ∀ i ∈ t, (X - C i).Monic

Tactic:
·

Goal state after:
R : Type u
inst✝ : CommRing R
t : Multiset R
⊢ (Multiset.map (fun i ↦ (X - C i).nextCoeff) t).sum = -t.sum
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p) →
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)

Tactic:
·

Goal state after:
case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p) →
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
t : Multiset R
⊢ ∀ i ∈ t, (X - C i).Monic

Tactic:
·

Goal state after:
case h
R : Type u
inst✝ : CommRing R
t : Multiset R
⊢ ∀ i ∈ t, (X - C i).Monic
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case inl
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Subsingleton R
⊢ ¬Irreducible p ↔ ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂

pp: case inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ ¬Irreducible p ↔ ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂

Tactic:
·

Goal state after:
case inl
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Subsingleton R
⊢ ¬Irreducible p ↔ ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ (¬∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (2 / 2)) ↔
    ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂

pp: case inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ p ≠ 1

Tactic:
·

Goal state after:
case inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ (¬∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (2 / 2)) ↔
    ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case inr.mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ (∃ f g, f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)) →
    ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂

pp: case inr.mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ (∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂) →
    ∃ f g, f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)

Tactic:
·

Goal state after:
case inr.mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ (∃ f g, f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)) →
    ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case hnc
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ¬(Multiset.map (fun x ↦ X - C x) t).prod.natDegree = 0

pp: R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ (Multiset.map (fun x ↦ X - C x) t).prod.coeff (t.card - 1) =
    (Multiset.map (fun x ↦ X - C x) t).prod.coeff ((Multiset.map (fun x ↦ X - C x) t).prod.natDegree - 1)

Tactic:
·

Goal state after:
case hnc
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ¬(Multiset.map (fun x ↦ X - C x) t).prod.natDegree = 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case inr.mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ (∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂) →
    ∃ f g, f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)

Tactic:
·

Goal state after:
case inr.mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ (∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂) →
    ∃ f g, f.Monic ∧ g.Monic ∧ f * g = p ∧ g.natDegree ∈ Ioc 0 (2 / 2)
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case inr.mpr.refine_1
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
c₁ c₂ : R
hmul : p.coeff 0 = c₁ * c₂
hadd : p.coeff 1 = c₁ + c₂
⊢ (X + C c₁) * (X + C c₂) = p

pp: case inr.mpr.refine_2
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
c₁ c₂ : R
hmul : p.coeff 0 = c₁ * c₂
hadd : p.coeff 1 = c₁ + c₂
⊢ (X + C c₂).natDegree ∈ Ioc 0 (2 / 2)

Tactic:
·

Goal state after:
case inr.mpr.refine_1
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
c₁ c₂ : R
hmul : p.coeff 0 = c₁ * c₂
hadd : p.coeff 1 = c₁ + c₂
⊢ (X + C c₁) * (X + C c₂) = p
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case hnc.h
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ∀ f ∈ Multiset.map (fun x ↦ X - C x) t, f.Monic

pp: case hnc
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ¬(Multiset.map natDegree (Multiset.map (fun x ↦ X - C x) t)).sum = 0

Tactic:
·

Goal state after:
case hnc.h
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ∀ f ∈ Multiset.map (fun x ↦ X - C x) t, f.Monic
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
⊢ ∑ i ∈ range 0, x ^ i * y ^ (0 - 1 - i) = ∑ i ∈ range 0, y ^ i * x ^ (0 - 1 - i)

pp: case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
⊢ ∑ i ∈ range (n✝ + 1), x ^ i * y ^ (n✝ + 1 - 1 - i) = ∑ i ∈ range (n✝ + 1), y ^ i * x ^ (n✝ + 1 - 1 - i)

Tactic:
·

Goal state after:
case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
⊢ ∑ i ∈ range 0, x ^ i * y ^ (0 - 1 - i) = ∑ i ∈ range 0, y ^ i * x ^ (0 - 1 - i)
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ x i ≠ 0

pp: case neg.h₀
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ ∀ b ∈ univ, b ≠ i → (C (x b) * X ^ k b).coeff (k i) = 0

pp: case neg.h₁
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ i ∉ univ → (C (x i) * X ^ k i).coeff (k i) = 0

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ x i ≠ 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg.h₀
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ ∀ b ∈ univ, b ≠ i → (C (x b) * X ^ k b).coeff (k i) = 0

pp: case neg.h₁
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ i ∉ univ → (C (x i) * X ^ k i).coeff (k i) = 0

Tactic:
·

Goal state after:
case neg.h₀
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ ∀ b ∈ univ, b ≠ i → (C (x b) * X ^ k b).coeff (k i) = 0
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case e_a.e_a
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ t.card = (Multiset.map natDegree (Multiset.map (fun x ↦ X - C x) t)).sum

Tactic:
·

Goal state after:
case e_a.e_a
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ t.card = (Multiset.map natDegree (Multiset.map (fun x ↦ X - C x) t)).sum
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case e_a.e_a.h
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ∀ f ∈ Multiset.map (fun x ↦ X - C x) t, f.Monic

Tactic:
·

Goal state after:
case e_a.e_a.h
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ∀ f ∈ Multiset.map (fun x ↦ X - C x) t, f.Monic
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case inr.mpr.refine_2
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
c₁ c₂ : R
hmul : p.coeff 0 = c₁ * c₂
hadd : p.coeff 1 = c₁ + c₂
⊢ (X + C c₂).natDegree ∈ Ioc 0 (2 / 2)

Tactic:
·

Goal state after:
case inr.mpr.refine_2
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
c₁ c₂ : R
hmul : p.coeff 0 = c₁ * c₂
hadd : p.coeff 1 = c₁ + c₂
⊢ (X + C c₂).natDegree ∈ Ioc 0 (2 / 2)
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
k : ℕ
hk : ∑ i ∈ range k, (-1) ^ i = if Even k then 0 else 1
h : Even k
⊢ (-1) ^ k + 0 = 1

pp: case neg
R : Type u_1
inst✝ : Ring R
k : ℕ
hk : ∑ i ∈ range k, (-1) ^ i = if Even k then 0 else 1
h : ¬Even k
⊢ (-1) ^ k + 1 = 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
k : ℕ
hk : ∑ i ∈ range k, (-1) ^ i = if Even k then 0 else 1
h : Even k
⊢ (-1) ^ k + 0 = 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ p ≠ 1

Tactic:
·

Goal state after:
case inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ p ≠ 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ p ≠ 1

Tactic:
rintro rfl
    simp [natDegree_one] at hnd

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
k : ℕ
hk : ∑ i ∈ range k, (-1) ^ i = if Even k then 0 else 1
h : ¬Even k
⊢ (-1) ^ k + 1 = 0

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
k : ℕ
hk : ∑ i ∈ range k, (-1) ^ i = if Even k then 0 else 1
h : ¬Even k
⊢ (-1) ^ k + 1 = 0
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case a
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
⊢ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).degree ≤ s.sup fun i ↦ (f i).degree

pp: case a
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
⊢ (s.sup fun i ↦ (f i).degree) ≤ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).degree

Tactic:
·

Goal state after:
case a
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
⊢ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).degree ≤ s.sup fun i ↦ (f i).degree
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case a
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
⊢ (s.sup fun i ↦ (f i).degree) ≤ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).degree

Tactic:
·

Goal state after:
case a
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
⊢ (s.sup fun i ↦ (f i).degree) ≤ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).degree
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : IsUnit (X ^ 0 - 1)
⊢ False

pp: case inr
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
h : IsUnit (X ^ n - 1)
hn : n ≠ 0
⊢ False

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
h : IsUnit (X ^ 0 - 1)
⊢ False
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg.h₁
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ i ∉ univ → (C (x i) * X ^ k i).coeff (k i) = 0

Tactic:
·

Goal state after:
case neg.h₁
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ i ∉ univ → (C (x i) * X ^ k i).coeff (k i) = 0
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case pos
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
i : ι
hi : i ∈ s
hf : f i = 0
⊢ (f i).degree ≤ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).degree

pp: case neg
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
i : ι
hi : i ∈ s
hf : ¬f i = 0
⊢ (f i).degree ≤ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).degree

Tactic:
·

Goal state after:
case pos
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
i : ι
hi : i ∈ s
hf : f i = 0
⊢ (f i).degree ≤ (∑ i ∈ s, v i • map (algebraMap R A) (f i)).degree
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r

pp: case neg
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : ¬p = 0
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : b = 0
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r

pp: case neg
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : ¬b = 0
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : b = 0
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r