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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : P.natDegree + 1 ≤ k + 1
⊢ P.degree.succ ≤ k + 1

Tactic:
lia

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
⊢ P.degree.succ - 1 - (k + 1) < P.degree.succ

Tactic:
lia

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
⊢ dk ≠ P.natDegree

Tactic:
lia

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

Goal state before:
pp: case e_a
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
⊢ P.degree.succ - 1 - (k + 1) = dk

Tactic:
lia

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
hkn : k < n
⊢ P.eraseLead.natDegree < dk

Tactic:
lia

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
hkn : n ≤ k
⊢ P.eraseLead.degree.succ - 1 - (k - n) < P.eraseLead.degree.succ

Tactic:
lia

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

Goal state before:
pp: case e_a
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
hkn : n ≤ k
⊢ dk = P.eraseLead.degree.succ - 1 - (k - n)

Tactic:
lia

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
hkn : n ≤ k
⊢ k - n < P.eraseLead.degree.succ

Tactic:
lia

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
P : R[X]
x : R
hx : x ≠ 0
⊢ (C x * P).coeffList = List.map (fun x_1 ↦ x * x_1) P.coeffList

Tactic:
by
  by_cases hp : P = 0
  · simp [hp]
  · simp [coeffList, Polynomial.degree_C hx]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
x : R
⊢ evalEvalRingHom x = eval₂RingHom (evalRingHom x)

Tactic:
ext <;> simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
x y : S
⊢ eval₂RingHom (eval₂RingHom f x) y = (evalEvalRingHom x y).comp (mapRingHom (mapRingHom f))

Tactic:
ext <;> simp

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ (evalRingHom (C X)).comp (eval₂RingHom (mapRingHom (algebraMap R R[X][Y])) (C Y)) = RingHom.id R[X][Y]

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.CardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : Fintype Fq
card_pos : 0 < Fintype.card Fq
pow_pos : ∀ (n : ℕ), 0 < ↑(Fintype.card Fq) ^ n
this : DecidableEq Fq := Classical.decEq Fq
p q : Fq[X]
hp : ¬p = 0
hq : ¬q = 0
hpq : ¬p + q = 0
⊢ 1 ≤ ↑(Fintype.card Fq)

Tactic:
lia

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ (MvPolynomial.aeval ![C X, Y]).comp (aevalAeval (MvPolynomial.X 0) (MvPolynomial.X 1)) = AlgHom.id R R[X][Y]

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ≠ 0
hp : p.IsMonicOfDegree n
⊢ n - 1 < n

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semiring R
p q : R[X]
n : ℕ
hp : p.natDegree ≤ n ∧ p.coeff n = 1
hq : q.natDegree ≤ n ∧ q.coeff n = 1
a✝ : Nontrivial R
hm : n ≤ n
⊢ p.coeff n = q.coeff n

Tactic:
rw [hp.2, hq.2]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 1
n : ℕ
hn : n > 0
⊢ 1 ≤ n

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
n : ℕ
hn : 1 < n
⊢ 2 ≤ n

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Order.Module.HahnEmbedding

Goal state before:
pp: K : Type u_1
inst✝¹² : DivisionRing K
inst✝¹¹ : LinearOrder K
inst✝¹⁰ : IsOrderedRing K
inst✝⁹ : Archimedean K
M : Type u_2
inst✝⁸ : AddCommGroup M
inst✝⁷ : LinearOrder M
inst✝⁶ : IsOrderedAddMonoid M
inst✝⁵ : Module K M
inst✝⁴ : IsOrderedModule K M
R : Type u_3
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : Module K R
seed : Seed K M R
inst✝ : IsOrderedAddMonoid R
c : Set (Partial seed)
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
hnonempty : c.Nonempty
⊢ BddAbove c

Tactic:
exact ⟨sSup hnonempty hc.directedOn, mem_upperBounds.mpr fun _ hf ↦ le_sSupFun hc.directedOn hf⟩

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b r : R[X]
m n : ℕ
hmn : n ≤ m
ha : a.IsMonicOfDegree m
hb : b.IsMonicOfDegree n
hr : r.natDegree < m
h : b ∣ a + r
q : R[X]
hq : a + r = q * b
⊢ m - n + n = m

Tactic:
lia

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

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

Tactic:
by_cases hp : p = 0
  · rw [hp, mirror_zero]
  · rw [mirror, natTrailingDegree_mul_X_pow ((mt reverse_eq_zero.mp) hp),
      natTrailingDegree_reverse, zero_add]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ (0 * mirror 0).natDegree = 2 * natDegree 0

Tactic:
zero_mul,

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ natDegree 0 = 2 * natDegree 0
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ (0 * mirror 0).natTrailingDegree = 2 * natTrailingDegree 0

Tactic:
zero_mul,

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ natTrailingDegree 0 = 2 * natTrailingDegree 0
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ (0 * q).mirror = mirror 0 * q.mirror

Tactic:
zero_mul,

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ mirror 0 = mirror 0 * q.mirror
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
a : R
⊢ (a • p).mirror = a • p.mirror

Tactic:
← C_mul',

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
a : R
⊢ (C a * p).mirror = a • p.mirror
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
a : R
⊢ (C a * p).mirror = a • p.mirror

Tactic:
← C_mul',

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
p : R[X]
inst✝ : NoZeroDivisors R
a : R
⊢ (C a * p).mirror = C a * p.mirror
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
h_deg : p.natDegree < n
i : ℕ
h : n ≤ i
⊢ p.natDegree < i

Tactic:
lia

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

Goal state before:
pp: case monomial
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
⊢ MvPolynomial.coeff m (((monomial k) c).homogenize n) = if m 0 + m 1 = n then ((monomial k) c).coeff (m 0) else 0

Tactic:
rcases le_or_gt k n with hkn | hnk
    · rw [homogenize_monomial hkn, coeff_monomial, MvPolynomial.coeff_monomial]
      have : (fun₀ | 0 => m 0 | 1 => m 1) = m := by ext i; fin_cases i <;> simp
      aesop
    · aesop (add simp homogenize_monomial_of_lt) (add simp coeff_monomial)

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

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p r : R[X]
hp₀ : p ≠ 0
hr₀ : r ≠ 0
⊢ p.homogenize p.natDegree ∣ (p * r).homogenize (p * r).natDegree

Tactic:
natDegree_mul hp₀ hr₀,

Goal state after:
case inr.inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p r : R[X]
hp₀ : p ≠ 0
hr₀ : r ≠ 0
⊢ p.homogenize p.natDegree ∣ (p * r).homogenize (p.natDegree + r.natDegree)
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : R b c
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length

Tactic:
have hac : ¬Rᶜ a c := (mt (_root_.trans hba)) (not_not.2 hbc)

Goal state after:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
i : IsTrans α Rᶜ
a c : α
l : List α
hba : ¬R b a
hbc : R b c
hac : ¬Rᶜ a c
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case e'_2.e'_5
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
x : ℕ
hx : x ∈ range q
⊢ (q.choose (x + 1) * q.descFactorial (q - (x + 1))) • (0 * eval r ((X - C r) ^ (q - (q - (x + 1)) - 1))) *
      eval r ((⇑derivative)^[x + 1] p') =
    0

Tactic:
zero_mul,

Goal state after:
case e'_2.e'_5
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
x : ℕ
hx : x ∈ range q
⊢ (q.choose (x + 1) * q.descFactorial (q - (x + 1))) • 0 * eval r ((⇑derivative)^[x + 1] p') = 0
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hePn0 : P.eraseLead ≠ 0
⊢ P.eraseLead.natDegree + 1 = P.natDegree

Tactic:
exact natDegree_eraseLead_add_one hc.ne

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
⊢ ((X - C η) * P).nextCoeff < 0

Tactic:
rw [hQ, sub_neg]

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
⊢ P.coeff d < η * P.coeff (d + 1)
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
hη : 0 < η
hP₀ : 0 < P.leadingCoeff
hc : P.nextCoeff < 0
d : ℕ
hd : P.natDegree = d + 1
hndxP : ((X - C η) * P).natDegree = P.natDegree + 1
hndxeP : ((X - C η) * P.eraseLead).natDegree = P.natDegree
hQ : ((X - C η) * P).nextCoeff = P.coeff d - η * P.coeff (d + 1)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
this : ((X - C η) * P).eraseLead.eraseLead = ((X - C η) * P.eraseLead).eraseLead
⊢ 0 < ((X - C η) * P.eraseLead).natDegree

Tactic:
lia

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
k : ℕ
hk : q ≤ k
⊢ ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (if hk : q ≤ k then ⋯.choose else 0)

Tactic:
dif_pos hk

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
k : ℕ
hk : q ≤ k
⊢ ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) ⋯.choose
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
d : ℕ
c : R
hc : c ≠ 0
hη : 0 < η
h₁ : ((X - C η) * (monomial d) c).nextCoeff = -(η * c)
h₂ : ((X - C η) * (monomial d) c).eraseLead ≠ 0
⊢ ((monomial d) c).signVariations + 1 ≤ ((X - C η) * (monomial d) c).signVariations

Tactic:
have h₃ : SignType.sign c ≠ SignType.sign (-(η * c)) := by
    simp [hη, hc, Left.sign_neg, sign_mul]

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
d : ℕ
c : R
hc : c ≠ 0
hη : 0 < η
h₁ : ((X - C η) * (monomial d) c).nextCoeff = -(η * c)
h₂ : ((X - C η) * (monomial d) c).eraseLead ≠ 0
h₃ : SignType.sign c ≠ SignType.sign (-(η * c))
⊢ ((monomial d) c).signVariations + 1 ≤ ((X - C η) * (monomial d) c).signVariations
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : AddZeroClass R
x y : R
⊢ QuadraticAlgebra.C (x + y) = QuadraticAlgebra.C x + QuadraticAlgebra.C y

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : NegZeroClass R
x : R
⊢ QuadraticAlgebra.C (-x) = -QuadraticAlgebra.C x

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝¹ : Monoid S
inst✝ : MulAction S R
x✝ : QuadraticAlgebra R a b
⊢ 1 • x✝ = x✝

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : Monoid S
inst✝¹ : AddMonoid R
inst✝ : DistribMulAction S R
x✝ : S
⊢ x✝ • 0 = 0

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : Monoid S
inst✝¹ : AddMonoid R
inst✝ : DistribMulAction S R
x✝² : S
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ x✝² • (x✝¹ + x✝) = x✝² • x✝¹ + x✝² • x✝

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommSemiring R
⊢ ω * ω = { re := a, im := b }

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommSemiring R
⊢ ω * ω = a • 1 + b • ω

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommSemiring R
x y : R
⊢ ω * { re := x, im := y } = { re := a * y, im := x + b * y }

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommSemiring R
n x y : R
⊢ ω * (algebraMap R (QuadraticAlgebra R a b)) n * { re := x, im := y } = { re := a * n * y, im := n * x + n * b * y }

Tactic:
ext <;> simp

Goal state after:
case im
R : Type u_2
a b : R
inst✝ : CommSemiring R
n x y : R
⊢ n * x + b * n * y = n * x + n * b * y
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommSemiring R
x y : R
⊢ { re := x, im := y } = (algebraMap R (QuadraticAlgebra R a b)) x + y • ω

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x✝ y : QuadraticAlgebra R a b
inst✝² : Semiring S
inst✝¹ : AddCommMonoid R
inst✝ : Module S R
x : QuadraticAlgebra R a b
⊢ 0 • x = 0

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoidWithOne R
⊢ QuadraticAlgebra.C ↑0 = 0

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : AddCommMonoidWithOne R
n : ℕ
⊢ QuadraticAlgebra.C ↑(n + 1) = QuadraticAlgebra.C ↑n + 1

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonUnitalNonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ 0 * x✝ = 0

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonUnitalNonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ x✝ * 0 = 0

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : QuadraticAlgebra R a b
⊢ QuadraticAlgebra.C r * x = r • x

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : NonUnitalNonAssocSemiring R
x y : R
⊢ QuadraticAlgebra.C (x * y) = QuadraticAlgebra.C x * QuadraticAlgebra.C y

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ 1 * x✝ = x✝

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : NonAssocSemiring R
x✝ : QuadraticAlgebra R a b
⊢ x✝ * 1 = x✝

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : NonAssocSemiring R
n : ℕ
x y : R
⊢ ↑n * { re := x, im := y } = { re := ↑n * x, im := ↑n * y }

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
x y : R
⊢ { re := x, im := y } * star { re := x, im := y } =
    (algebraMap R (QuadraticAlgebra R a b)) x * (algebraMap R (QuadraticAlgebra R a b)) x +
        (algebraMap R (QuadraticAlgebra R a b)) b * (algebraMap R (QuadraticAlgebra R a b)) x *
          (algebraMap R (QuadraticAlgebra R a b)) y -
      (algebraMap R (QuadraticAlgebra R a b)) a * (algebraMap R (QuadraticAlgebra R a b)) y *
        (algebraMap R (QuadraticAlgebra R a b)) y

Tactic:
ext <;> simp

Goal state after:
case re
R : Type u_2
a b : R
inst✝ : CommRing R
x y : R
⊢ x * (x + b * y) + -(a * y * y) = x * x + b * x * y - a * y * y

case im
R : Type u_2
a b : R
inst✝ : CommRing R
x y : R
⊢ -(x * y) + y * (x + b * y) + -(b * y * y) = 0
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : CommSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ x✝² * x✝¹ * x✝ = x✝² * (x✝¹ * x✝)

Tactic:
ext <;> simp

Goal state after:
case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : CommSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝².re * x✝¹.re + a * x✝².im * x✝¹.im) * x✝.re +
      a * (x✝².re * x✝¹.im + x✝².im * x✝¹.re + b * x✝².im * x✝¹.im) * x✝.im =
    x✝².re * (x✝¹.re * x✝.re + a * x✝¹.im * x✝.im) + a * x✝².im * (x✝¹.re * x✝.im + x✝¹.im * x✝.re + b * x✝¹.im * x✝.im)

case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : CommSemiring R
x✝² x✝¹ x✝ : QuadraticAlgebra R a b
⊢ (x✝².re * x✝¹.re + a * x✝².im * x✝¹.im) * x✝.im + (x✝².re * x✝¹.im + x✝².im * x✝¹.re + b * x✝².im * x✝¹.im) * x✝.re +
      b * (x✝².re * x✝¹.im + x✝².im * x✝¹.re + b * x✝².im * x✝¹.im) * x✝.im =
    x✝².re * (x✝¹.re * x✝.im + x✝¹.im * x✝.re + b * x✝¹.im * x✝.im) + x✝².im * (x✝¹.re * x✝.re + a * x✝¹.im * x✝.im) +
      b * x✝².im * (x✝¹.re * x✝.im + x✝¹.im * x✝.re + b * x✝¹.im * x✝.im)
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : CommSemiring R
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
ext <;> simp

Goal state after:
case re
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : CommSemiring R
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ x✝¹.re * x✝.re + a * x✝¹.im * x✝.im = x✝.re * x✝¹.re + a * x✝.im * x✝¹.im

case im
R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝ : CommSemiring R
x✝¹ x✝ : QuadraticAlgebra R a b
⊢ x✝¹.re * x✝.im + x✝¹.im * x✝.re + b * x✝¹.im * x✝.im = x✝.re * x✝¹.im + x✝.im * x✝¹.re + b * x✝.im * x✝¹.im
Module: Mathlib.Algebra.QuadraticAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
a b r : R
x y : QuadraticAlgebra R a b
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
⊢ QuadraticAlgebra.C ((algebraMap S R) 1) = 1

Tactic:
ext <;> simp

Goal state after: