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

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
⊢ f.coeff 1 = (X ^ 2 + C (f.coeff 1) * X + C (f.coeff 0)).coeff 1

pp: case inr.inr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
n : ℕ
hn : 1 < n
⊢ f.coeff n = (X ^ 2 + C (f.coeff 1) * X + C (f.coeff 0)).coeff n

Tactic:
· simp

Goal state after:
case inr.inr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
n : ℕ
hn : 1 < n
⊢ f.coeff n = (X ^ 2 + C (f.coeff 1) * X + C (f.coeff 0)).coeff n
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
a b : R
⊢ (X ^ 2 - C a * X + C b).IsMonicOfDegree 2

Tactic:
rw [sub_add]

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
a b : R
⊢ (X ^ 2 - (C a * X - C b)).IsMonicOfDegree 2
Module: Mathlib.Algebra.Polynomial.CoeffMem

Goal state before:
pp: case neg.refine_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
H'' : spanCoeffs(q) ^ deg(r) * spanCoeffs(r) ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
⊢ (p.leadingCoeff * if i = deg(p) - deg(q) then 1 else 0) ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Tactic:
split_ifs <;> simp only [mul_one, mul_zero]
      exacts [H₀ _, zero_mem _]

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

Goal state before:
pp: case neg
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : ¬q.Monic
⊢ coeff 0 i ∈ Mq ^ deg(p) * Mp

Tactic:
· simp

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

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

Tactic:
hp,

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p = 0
⊢ (mirror 0).natDegree = natDegree 0
Module: Mathlib.Algebra.Polynomial.Mirror

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

Tactic:
hp,

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p = 0
⊢ (mirror 0).natTrailingDegree = natTrailingDegree 0
Module: Mathlib.Algebra.Polynomial.Mirror

Goal state before:
pp: case h.refine_2
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ Finset.range (p.natDegree + 1)
hp : p.coeff n ≠ 0
⊢ p.mirror.coeff ((revAt (p.natDegree + p.natTrailingDegree)) n) ≠ 0

Tactic:
change p.mirror.coeff _ ≠ 0
      rwa [coeff_mirror, revAt_invol]

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
⊢ (p * p.mirror).natDegree = 2 * p.natDegree

Tactic:
hp,

Goal state after:
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
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
⊢ (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree

Tactic:
hp,

Goal state after:
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
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
⊢ (p * q).mirror = p.mirror * q.mirror

Tactic:
hp,

Goal state after:
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
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ (MvPolynomial.monomial fun₀ | 0 => (m, n - m).1 | 1 => (m, n - m).2) (((monomial m) r).coeff (m, n - m).1) =
    (MvPolynomial.monomial fun₀ | 0 => m | 1 => n - m) r

pp: case h₀
R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ ∀ b ∈ antidiagonal n,
    b ≠ (m, n - m) → (MvPolynomial.monomial fun₀ | 0 => b.1 | 1 => b.2) (((monomial m) r).coeff b.1) = 0

pp: case h₁
R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ (m, n - m) ∉ antidiagonal n →
    (MvPolynomial.monomial fun₀ | 0 => (m, n - m).1 | 1 => (m, n - m).2) (((monomial m) r).coeff (m, n - m).1) = 0

Tactic:
· simp

Goal state after:
case h₀
R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ ∀ b ∈ antidiagonal n,
    b ≠ (m, n - m) → (MvPolynomial.monomial fun₀ | 0 => b.1 | 1 => b.2) (((monomial m) r).coeff b.1) = 0

case h₁
R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
r : R
⊢ (m, n - m) ∉ antidiagonal n →
    (MvPolynomial.monomial fun₀ | 0 => (m, n - m).1 | 1 => (m, n - m).2) (((monomial m) r).coeff (m, n - m).1) = 0
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ MvPolynomial.eval₂ f g (homogenize 0 n) = eval₂ f (g 0) 0

pp: case C_mul_pow
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ ∀ (n_1 : ℕ) (r : R),
    r ≠ 0 → n_1 ≤ n → MvPolynomial.eval₂ f g ((C r * X ^ n_1).homogenize n) = eval₂ f (g 0) (C r * X ^ n_1)

pp: case add
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ ∀ (f_1 g_1 : R[X]),
    f_1.natDegree < g_1.natDegree →
      g_1.natDegree ≤ n →
        MvPolynomial.eval₂ f g (f_1.homogenize n) = eval₂ f (g 0) f_1 →
          MvPolynomial.eval₂ f g (g_1.homogenize n) = eval₂ f (g 0) g_1 →
            MvPolynomial.eval₂ f g ((f_1 + g_1).homogenize n) = eval₂ f (g 0) (f_1 + g_1)

pp: case df
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ p.natDegree ≤ n

Tactic:
· simp

Goal state after:
case C_mul_pow
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ ∀ (n_1 : ℕ) (r : R),
    r ≠ 0 → n_1 ≤ n → MvPolynomial.eval₂ f g ((C r * X ^ n_1).homogenize n) = eval₂ f (g 0) (C r * X ^ n_1)

case add
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ ∀ (f_1 g_1 : R[X]),
    f_1.natDegree < g_1.natDegree →
      g_1.natDegree ≤ n →
        MvPolynomial.eval₂ f g (f_1.homogenize n) = eval₂ f (g 0) f_1 →
          MvPolynomial.eval₂ f g (g_1.homogenize n) = eval₂ f (g 0) g_1 →
            MvPolynomial.eval₂ f g ((f_1 + g_1).homogenize n) = eval₂ f (g 0) (f_1 + g_1)

case df
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
f : R →+* S
g : Fin 2 → S
hg : g 1 = 1
⊢ p.natDegree ≤ n
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
a b : ℕ
⊢ ((MvPolynomial.monomial fun₀ | 0 => a | 1 => b) (p.coeff a)).IsHomogeneous (a + b)

Tactic:
apply MvPolynomial.isHomogeneous_monomial

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
a b : ℕ
⊢ (Finsupp.degree fun₀ | 0 => a | 1 => b) = a + b
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case pos
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
l : List α
hl : a ∈ destutter' R a l
h✝ : R a b
⊢ a ∈ a :: destutter' R b l

pp: case neg
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
l : List α
hl : a ∈ destutter' R a l
h✝ : ¬R a b
⊢ a ∈ destutter' R a l

Tactic:
· simp

Goal state after:
case neg
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
l : List α
hl : a ∈ destutter' R a l
h✝ : ¬R a b
⊢ a ∈ destutter' R a l
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
r : R[X]
⊢ homogenize 0 (natDegree 0) ∣ (0 * r).homogenize (0 * r).natDegree

pp: case inr.inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
⊢ p.homogenize p.natDegree ∣ (p * 0).homogenize (p * 0).natDegree

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

Goal state after:
case inr.inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
⊢ p.homogenize p.natDegree ∣ (p * 0).homogenize (p * 0).natDegree

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
Module: Mathlib.Algebra.Polynomial.Homogenize

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

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

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 * r).natDegree
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case succ.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i, r i * g ^ ↑i
⊢ q * g ^ n + ∑ i, r i * g ^ ↑i = (q %ₘ g + q /ₘ g * g) * g ^ n + ∑ i, Fin.snoc r (q %ₘ g) i.castSucc * g ^ ↑i.castSucc

Tactic:
mul_comm (q /ₘ g) g,

Goal state after:
case succ.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
q : R[X]
r : Fin n → R[X]
hr : ∀ (i : Fin n), (r i).degree < g.degree
hf : f = q * g ^ n + ∑ i, r i * g ^ ↑i
⊢ q * g ^ n + ∑ i, r i * g ^ ↑i =
    (q %ₘ g + g * (q /ₘ g)) * g ^ n + ∑ i, Fin.snoc r (q %ₘ g) i.castSucc * g ^ ↑i.castSucc
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: K : Type u_1
inst✝ : Semifield K
p : K[X]
n : ℕ
hn : p.natDegree ≤ n
x : Fin 2 → K
hx : x 1 ≠ 0
⊢ (MvPolynomial.eval x) (p.homogenize n) = eval (x 0 / x 1) p * x 1 ^ n

Tactic:
simp only [homogenize, Polynomial.eval_eq_sum_range' (Nat.lt_succ_iff.mpr hn),
    Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, Finset.sum_mul, MvPolynomial.eval_sum]
  refine Finset.sum_congr rfl fun k hk ↦ ?_
  rw [MvPolynomial.eval_monomial, Finsupp.update_eq_add_single, Finsupp.prod_add_index',
    Finsupp.prod_single_index, Finsupp.prod_single_index, pow_sub₀]
  · ring
  all_goals simp_all [pow_add]

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

Goal state before:
pp: case monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : NonAssocSemiring S
inst✝² : Module R S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
a : R
n : ℕ
⊢ ((monomial (n + 1)) a).smeval 0 = ((monomial (n + 1)) a).coeff 0 • 1

Tactic:
| succ n =>

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
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
k : ℕ
hk : k < q
h : ∀ (x : ℕ), (X - C r) ^ (q - (k - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (k - x) - 1)
⊢ eval r ((⇑derivative)^[k] (map (algebraMap R A) p)) = 0

Tactic:
hp,

Goal state after:
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'
k : ℕ
hk : k < q
h : ∀ (x : ℕ), (X - C r) ^ (q - (k - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (k - x) - 1)
⊢ eval r ((⇑derivative)^[k] ((X - C r) ^ q * p')) = 0
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
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)
⊢ eval r ((⇑derivative)^[q] (map (algebraMap R A) p)) = q ! • eval r p'

Tactic:
hp,

Goal state after:
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)
⊢ eval r ((⇑derivative)^[q] ((X - C r) ^ q * p')) = q ! • eval r p'
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case refine_1
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ↑(u ^ 2) + (↑(v ^ 2) + ↑(w ^ 2)) = 3

Tactic:
Int.units_sq,

Goal state after:
case refine_1
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ ↑1 + (↑1 + ↑1) = 3
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ C ↑v * (C ↑u * X ^ (m + n) + C ↑w * X ^ (n - m + k + n)) =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (p * p.mirror).toFinsupp.coeff) }

Tactic:
hp,

Goal state after:
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ C ↑v * (C ↑u * X ^ (m + n) + C ↑w * X ^ (n - m + k + n)) =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n))
            (trinomial k m n ↑u ↑v ↑w * (trinomial k m n ↑u ↑v ↑w).mirror).toFinsupp.coeff) }
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case right.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
r : A
p' : A[X]
hp : p' = 0
⊢ 0 = (q - 1)! • eval r p'

Tactic:
hp,

Goal state after:
case right.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
r : A
p' : A[X]
hp : p' = 0
⊢ 0 = (q - 1)! • eval r 0
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ n + n ∉ Set.Ioo (k + n) (n + n)

pp: case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ n + (n - m + k) ∈ Set.Ioo (k + n) (n + n)

pp: case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ n + k ∉ Set.Ioo (k + n) (n + n)

pp: case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ m + n ∈ Set.Ioo (k + n) (n + n)

pp: case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ m + (n - m + k) ∉ Set.Ioo (k + n) (n + n)

pp: case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ m + k ∉ Set.Ioo (k + n) (n + n)

pp: case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ k + n ∉ Set.Ioo (k + n) (n + n)

pp: case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ k + (n - m + k) ∉ Set.Ioo (k + n) (n + n)

pp: case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ k + k ∉ Set.Ioo (k + n) (n + n)

Tactic:
· simp

Goal state after:
case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ n + (n - m + k) ∈ Set.Ioo (k + n) (n + n)

case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ n + k ∉ Set.Ioo (k + n) (n + n)

case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ m + n ∈ Set.Ioo (k + n) (n + n)

case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ m + (n - m + k) ∉ Set.Ioo (k + n) (n + n)

case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ m + k ∉ Set.Ioo (k + n) (n + n)

case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ k + n ∉ Set.Ioo (k + n) (n + n)

case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ k + (n - m + k) ∉ Set.Ioo (k + n) (n + n)

case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ k + k ∉ Set.Ioo (k + n) (n + n)
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
⊢ (X - C η) * P - (monomial ((X - C η) * P).natDegree) P.leadingCoeff -
      (monomial P.natDegree) ((X - C η) * P).nextCoeff =
    (X - C η) * P.eraseLead - (monomial P.natDegree) P.eraseLead.leadingCoeff

Tactic:
hndxP

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)
hQ₁ : ((X - C η) * P).nextCoeff < 0
hndexP0 : ((X - C η) * P).eraseLead.natDegree = P.natDegree
⊢ (X - C η) * P - (monomial (P.natDegree + 1)) P.leadingCoeff - (monomial P.natDegree) ((X - C η) * P).nextCoeff =
    (X - C η) * P.eraseLead - (monomial P.natDegree) P.eraseLead.leadingCoeff
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
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
⊢ q - 1 + p'.natDegree = (map (algebraMap R A) p).natDegree

Tactic:
hp,

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
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
⊢ q - 1 + p'.natDegree = ((X - C r) ^ (q - 1) * p').natDegree
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case e'_3
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
d : ℕ
c : R
hc : c ≠ 0
hη : 0 < η
⊢ -(η * c) = (X - C η).coeff 0 * c

Tactic:
· simp

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

Goal state before:
pp: p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * p.mirror = q * q.mirror
hmul : p.leadingCoeff * p.trailingCoeff = q.leadingCoeff * q.trailingCoeff
⊢ q = p ∨ q = p.mirror

Tactic:
hp,

Goal state after:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * p.mirror = q * q.mirror
hmul :
  (trinomial k m n ↑u ↑v ↑w).leadingCoeff * (trinomial k m n ↑u ↑v ↑w).trailingCoeff = q.leadingCoeff * q.trailingCoeff
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * p.mirror = q * q.mirror
hmul : ↑w * ↑u = ↑z * ↑x
hadd : eval 1 p ^ 2 = eval 1 q ^ 2
⊢ q = p ∨ q = p.mirror

Tactic:
hp,

Goal state after:
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w x z : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
hq : q = trinomial k m' n ↑x ↑v ↑z
h : p * p.mirror = q * q.mirror
hmul : ↑w * ↑u = ↑z * ↑x
hadd : eval 1 (trinomial k m n ↑u ↑v ↑w) ^ 2 = eval 1 q ^ 2
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inl
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n ↑x ↑y ↑z
h1 : ↑y = ↑v
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
rw [h1] at hq

Goal state after:
case inl
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n ↑x ↑v ↑z
h1 : ↑y = ↑v
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inr
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n ↑x ↑y ↑z
h1 : ↑y = -↑v
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
rw [h1] at hq

Goal state after:
case inr
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x) (-↑v) ↑z
h1 : ↑y = -↑v
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror