mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x : α
xs : List α
h : (∀ (a' : α), a' ∈ x :: xs → r x a') ∧ Pairwise r (x :: xs)
⊢ (if x ≠ x then x :: (x :: xs).dedup else destutter (fun x1 x2 ↦ x1 ≠ x2) (x :: xs)) = (x :: x :: xs).dedup

pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x y : α
xs : List α
h : (∀ (a' : α), a' ∈ y :: xs → r x a') ∧ Pairwise r (y :: xs)
hxy : x ≠ y
⊢ (if x ≠ y then x :: (y :: xs).dedup else destutter (fun x1 x2 ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x : α
xs : List α
h : (∀ (a' : α), a' ∈ x :: xs → r x a') ∧ Pairwise r (x :: xs)
⊢ (if x ≠ x then x :: (x :: xs).dedup else destutter (fun x1 x2 ↦ x1 ≠ x2) (x :: xs)) = (x :: x :: xs).dedup
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x y : α
xs : List α
h : (∀ (a' : α), a' ∈ y :: xs → r x a') ∧ Pairwise r (y :: xs)
hxy : x ≠ y
⊢ (if x ≠ y then x :: (y :: xs).dedup else destutter (fun x1 x2 ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x y : α
xs : List α
h : (∀ (a' : α), a' ∈ y :: xs → r x a') ∧ Pairwise r (y :: xs)
hxy : x ≠ y
⊢ (if x ≠ y then x :: (y :: xs).dedup else destutter (fun x1 x2 ↦ x1 ≠ x2) (x :: xs)) = (x :: y :: xs).dedup
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : Semiring R
p q : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
x✝ : ℕ
⊢ smul_pow x x✝ 0 = 0

pp: case refine_2
R : Type u_1
inst✝³ : Semiring R
p q : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
x✝² : ℕ
x✝¹ x✝ : R
⊢ smul_pow x x✝² (x✝¹ + x✝) = smul_pow x x✝² x✝¹ + smul_pow x x✝² x✝

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝³ : Semiring R
p q : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
x✝ : ℕ
⊢ smul_pow x x✝ 0 = 0
Module: Mathlib.Algebra.Polynomial.Smeval

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : Semiring R
p q : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
x✝ : ℕ
⊢ smul_pow x x✝ 0 = 0

Tactic:
rw [smul_pow, zero_smul]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : Semiring R
p q : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
x✝² : ℕ
x✝¹ x✝ : R
⊢ smul_pow x x✝² (x✝¹ + x✝) = smul_pow x x✝² x✝¹ + smul_pow x x✝² x✝

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝³ : Semiring R
p q : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
x✝² : ℕ
x✝¹ x✝ : R
⊢ smul_pow x x✝² (x✝¹ + x✝) = smul_pow x x✝² x✝¹ + smul_pow x x✝² x✝
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons.refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
⊢ ∀ i_1 ∈ Finset.cons i s hi,
    (Function.update (fun j ↦ r j * a j %ₘ g j) i ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) i_1).degree < (g i_1).degree

pp: case cons.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
⊢ q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k =
    ((q + ∑ j ∈ s, r j * b j %ₘ g i) /ₘ g i + ∑ j ∈ s, (r j * b j /ₘ g i + r j * a j /ₘ g j)) *
        ∏ i ∈ Finset.cons i s hi, g i +
      ∑ i_1 ∈ Finset.cons i s hi,
        Function.update (fun j ↦ r j * a j %ₘ g j) i ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) i_1 *
          ∏ k ∈ (Finset.cons i s hi).erase i_1, g k

Tactic:
·

Goal state after:
case cons.refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
⊢ ∀ i_1 ∈ Finset.cons i s hi,
    (Function.update (fun j ↦ r j * a j %ₘ g j) i ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) i_1).degree < (g i_1).degree
Module: Mathlib.Algebra.Polynomial.SpecificDegree

Goal state before:
pp: case ha
K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ p.leadingCoeff⁻¹ ≠ 0

pp: case hp2
K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ 2 ≤ (p * C p.leadingCoeff⁻¹).natDegree

pp: case hp3
K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ (p * C p.leadingCoeff⁻¹).natDegree ≤ 3

Tactic:
·

Goal state after:
case ha
K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ p.leadingCoeff⁻¹ ≠ 0
Module: Mathlib.Algebra.Polynomial.SpecificDegree

Goal state before:
pp: case hp2
K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ 2 ≤ (p * C p.leadingCoeff⁻¹).natDegree

pp: case hp3
K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ (p * C p.leadingCoeff⁻¹).natDegree ≤ 3

Tactic:
·

Goal state after:
case hp2
K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ 2 ≤ (p * C p.leadingCoeff⁻¹).natDegree
Module: Mathlib.Algebra.Polynomial.SpecificDegree

Goal state before:
pp: case hp3
K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ (p * C p.leadingCoeff⁻¹).natDegree ≤ 3

Tactic:
·

Goal state after:
case hp3
K : Type u_1
inst✝ : Field K
p : K[X]
hp2 : 2 ≤ p.natDegree
hp3 : p.natDegree ≤ 3
hp0 : p ≠ 0
⊢ (p * C p.leadingCoeff⁻¹).natDegree ≤ 3
Module: Mathlib.Algebra.Polynomial.SpecificDegree

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : 2 ≤ p.natDegree
⊢ Irreducible p

pp: case neg
K : Type u_1
inst✝ : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : ¬2 ≤ p.natDegree
⊢ Irreducible p

Tactic:
·

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : 2 ≤ p.natDegree
⊢ Irreducible p
Module: Mathlib.Algebra.Polynomial.SpecificDegree

Goal state before:
pp: case neg
K : Type u_1
inst✝ : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : ¬2 ≤ p.natDegree
⊢ Irreducible p

Tactic:
·

Goal state after:
case neg
K : Type u_1
inst✝ : Field K
p : K[X]
hdeg : 1 ≤ p.natDegree ∧ p.natDegree ≤ 3
hnot : ∀ (x : K), ¬p.IsRoot x
hdeg2 : ¬2 ≤ p.natDegree
⊢ Irreducible p
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: case cons.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
⊢ q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k =
    ((q + ∑ j ∈ s, r j * b j %ₘ g i) /ₘ g i + ∑ j ∈ s, (r j * b j /ₘ g i + r j * a j /ₘ g j)) *
        ∏ i ∈ Finset.cons i s hi, g i +
      ∑ i_1 ∈ Finset.cons i s hi,
        Function.update (fun j ↦ r j * a j %ₘ g j) i ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) i_1 *
          ∏ k ∈ (Finset.cons i s hi).erase i_1, g k

Tactic:
·

Goal state after:
case cons.refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hjs : ∀ {j : ι}, j ∈ s → i ≠ j
a b : ι → R[X]
hab : ∀ j ∈ s, a j * g i + b j * g j = 1
⊢ q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k =
    ((q + ∑ j ∈ s, r j * b j %ₘ g i) /ₘ g i + ∑ j ∈ s, (r j * b j /ₘ g i + r j * a j /ₘ g j)) *
        ∏ i ∈ Finset.cons i s hi, g i +
      ∑ i_1 ∈ Finset.cons i s hi,
        Function.update (fun j ↦ r j * a j %ₘ g j) i ((q + ∑ j ∈ s, r j * b j %ₘ g i) %ₘ g i) i_1 *
          ∏ k ∈ (Finset.cons i s hi).erase i_1, g k
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semiring R
m n : ℕ
u v w : R
hmn : m < n
hw : w ≠ 0
i : ℕ
hkm : i < m
⊢ ↑i ≤ ↑n

pp: case inr.inl
R : Type u_1
inst✝ : Semiring R
k n : ℕ
u v w : R
hw : w ≠ 0
i : ℕ
hkm : k < i
hmn : i < n
⊢ ↑i ≤ ↑n

pp: case inr.inr
R : Type u_1
inst✝ : Semiring R
k m : ℕ
u v w : R
hkm : k < m
hw : w ≠ 0
i : ℕ
hmn : m < i
⊢ ↑i ≤ ↑i

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝ : Semiring R
m n : ℕ
u v w : R
hmn : m < n
hw : w ≠ 0
i : ℕ
hkm : i < m
⊢ ↑i ≤ ↑n
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝ : Semiring R
k n : ℕ
u v w : R
hw : w ≠ 0
i : ℕ
hkm : k < i
hmn : i < n
⊢ ↑i ≤ ↑n

pp: case inr.inr
R : Type u_1
inst✝ : Semiring R
k m : ℕ
u v w : R
hkm : k < m
hw : w ≠ 0
i : ℕ
hmn : m < i
⊢ ↑i ≤ ↑i

Tactic:
·

Goal state after:
case inr.inl
R : Type u_1
inst✝ : Semiring R
k n : ℕ
u v w : R
hw : w ≠ 0
i : ℕ
hkm : k < i
hmn : i < n
⊢ ↑i ≤ ↑n
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝ : Semiring R
k m : ℕ
u v w : R
hkm : k < m
hw : w ≠ 0
i : ℕ
hmn : m < i
⊢ ↑i ≤ ↑i

Tactic:
·

Goal state after:
case inr.inr
R : Type u_1
inst✝ : Semiring R
k m : ℕ
u v w : R
hkm : k < m
hw : w ≠ 0
i : ℕ
hmn : m < i
⊢ ↑i ≤ ↑i
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semiring R
m n : ℕ
u v w : R
hmn : m < n
hu : u ≠ 0
i : ℕ
hkm : i < m
⊢ ↑i ≤ ↑i

pp: case inr.inl
R : Type u_1
inst✝ : Semiring R
k n : ℕ
u v w : R
hu : u ≠ 0
i : ℕ
hkm : k < i
hmn : i < n
⊢ ↑k ≤ ↑i

pp: case inr.inr
R : Type u_1
inst✝ : Semiring R
k m : ℕ
u v w : R
hkm : k < m
hu : u ≠ 0
i : ℕ
hmn : m < i
⊢ ↑k ≤ ↑i

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝ : Semiring R
m n : ℕ
u v w : R
hmn : m < n
hu : u ≠ 0
i : ℕ
hkm : i < m
⊢ ↑i ≤ ↑i
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝ : Semiring R
k n : ℕ
u v w : R
hu : u ≠ 0
i : ℕ
hkm : k < i
hmn : i < n
⊢ ↑k ≤ ↑i

pp: case inr.inr
R : Type u_1
inst✝ : Semiring R
k m : ℕ
u v w : R
hkm : k < m
hu : u ≠ 0
i : ℕ
hmn : m < i
⊢ ↑k ≤ ↑i

Tactic:
·

Goal state after:
case inr.inl
R : Type u_1
inst✝ : Semiring R
k n : ℕ
u v w : R
hu : u ≠ 0
i : ℕ
hkm : k < i
hmn : i < n
⊢ ↑k ≤ ↑i
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝ : Semiring R
k m : ℕ
u v w : R
hkm : k < m
hu : u ≠ 0
i : ℕ
hmn : m < i
⊢ ↑k ≤ ↑i

Tactic:
·

Goal state after:
case inr.inr
R : Type u_1
inst✝ : Semiring R
k m : ℕ
u v w : R
hkm : k < m
hu : u ≠ 0
i : ℕ
hmn : m < i
⊢ ↑k ≤ ↑i
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inl
k m n : ℕ
hmn : m < n
u v w : ℤˣ
hkm : k < m
hk : k ∈ (trinomial k m n ↑u ↑v ↑w).support
⊢ IsUnit ((trinomial k m n ↑u ↑v ↑w).coeff k)

pp: case inr.inl
k✝ k n : ℕ
u v w : ℤˣ
hkm : k < k✝
hmn : k✝ < n
hk : k✝ ∈ (trinomial k k✝ n ↑u ↑v ↑w).support
⊢ IsUnit ((trinomial k k✝ n ↑u ↑v ↑w).coeff k✝)

pp: case inr.inr
k✝ k m : ℕ
hkm : k < m
u v w : ℤˣ
hmn : m < k✝
hk : k✝ ∈ (trinomial k m k✝ ↑u ↑v ↑w).support
⊢ IsUnit ((trinomial k m k✝ ↑u ↑v ↑w).coeff k✝)

Tactic:
·

Goal state after:
case inl
k m n : ℕ
hmn : m < n
u v w : ℤˣ
hkm : k < m
hk : k ∈ (trinomial k m n ↑u ↑v ↑w).support
⊢ IsUnit ((trinomial k m n ↑u ↑v ↑w).coeff k)
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inr.inl
k✝ k n : ℕ
u v w : ℤˣ
hkm : k < k✝
hmn : k✝ < n
hk : k✝ ∈ (trinomial k k✝ n ↑u ↑v ↑w).support
⊢ IsUnit ((trinomial k k✝ n ↑u ↑v ↑w).coeff k✝)

pp: case inr.inr
k✝ k m : ℕ
hkm : k < m
u v w : ℤˣ
hmn : m < k✝
hk : k✝ ∈ (trinomial k m k✝ ↑u ↑v ↑w).support
⊢ IsUnit ((trinomial k m k✝ ↑u ↑v ↑w).coeff k✝)

Tactic:
·

Goal state after:
case inr.inl
k✝ k n : ℕ
u v w : ℤˣ
hkm : k < k✝
hmn : k✝ < n
hk : k✝ ∈ (trinomial k k✝ n ↑u ↑v ↑w).support
⊢ IsUnit ((trinomial k k✝ n ↑u ↑v ↑w).coeff k✝)
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inr.inr
k✝ k m : ℕ
hkm : k < m
u v w : ℤˣ
hmn : m < k✝
hk : k✝ ∈ (trinomial k m k✝ ↑u ↑v ↑w).support
⊢ IsUnit ((trinomial k m k✝ ↑u ↑v ↑w).coeff k✝)

Tactic:
·

Goal state after:
case inr.inr
k✝ k m : ℕ
hkm : k < m
u v w : ℤˣ
hmn : m < k✝
hk : k✝ ∈ (trinomial k m k✝ ↑u ↑v ↑w).support
⊢ IsUnit ((trinomial k m k✝ ↑u ↑v ↑w).coeff k✝)
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : #{k, m, n} = 3 ∧ ∀ k_1 ∈ {k, m, n}, IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
hx : IsUnit ((x + y * if k = m then 1 else 0) + z * if k = n then 1 else 0)
hy : IsUnit ((x * if m = k then 1 else 0) + y + z * if m = n then 1 else 0)
hz : IsUnit (((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial

Tactic:
rw [if_neg hkm.ne, if_neg (hkm.trans hmn).ne] at hx

Goal state after:
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : ℤ
hp : #{k, m, n} = 3 ∧ ∀ k_1 ∈ {k, m, n}, IsUnit ((C x * X ^ k + C y * X ^ m + C z * X ^ n).coeff k_1)
hx : IsUnit (x + y * 0 + z * 0)
hy : IsUnit ((x * if m = k then 1 else 0) + y + z * if m = n then 1 else 0)
hz : IsUnit (((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z)
⊢ (C x * X ^ k + C y * X ^ m + C z * X ^ n).IsUnitTrinomial
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
d : ℕ
c : R
hcz : c = 0
⊢ ((monomial d) c).signVariations = 0

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
d : ℕ
c : R
hcz : ¬c = 0
⊢ ((monomial d) c).signVariations = 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
d : ℕ
c : R
hcz : c = 0
⊢ ((monomial d) c).signVariations = 0
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
d : ℕ
c : R
hcz : ¬c = 0
⊢ ((monomial d) c).signVariations = 0

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
d : ℕ
c : R
hcz : ¬c = 0
⊢ ((monomial d) c).signVariations = 0
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case refine_1
p : ℤ[X]
⊢ p.IsUnitTrinomial → (p.sum fun x x_1 ↦ x_1 ^ 2) = 3

pp: case refine_2
p : ℤ[X]
hp : (p.sum fun x x_1 ↦ x_1 ^ 2) = 3
⊢ p.IsUnitTrinomial

Tactic:
·

Goal state after:
case refine_1
p : ℤ[X]
⊢ p.IsUnitTrinomial → (p.sum fun x x_1 ↦ x_1 ^ 2) = 3
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : SignType.sign P.leadingCoeff = SignType.sign P.nextCoeff
hpz : P = 0
⊢ P.eraseLead.signVariations = P.signVariations

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : SignType.sign P.leadingCoeff = SignType.sign P.nextCoeff
hpz : ¬P = 0
⊢ P.eraseLead.signVariations = P.signVariations

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : SignType.sign P.leadingCoeff = SignType.sign P.nextCoeff
hpz : P = 0
⊢ P.eraseLead.signVariations = P.signVariations
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : SignType.sign P.leadingCoeff = SignType.sign P.nextCoeff
hpz : ¬P = 0
⊢ P.eraseLead.signVariations = P.signVariations

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : SignType.sign P.leadingCoeff = SignType.sign P.nextCoeff
hpz : ¬P = 0
⊢ P.eraseLead.signVariations = P.signVariations
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : P = 0
⊢ P.signVariations =
    P.eraseLead.signVariations + if SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff then 1 else 0

pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
⊢ P.signVariations =
    P.eraseLead.signVariations + if SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff then 1 else 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : P = 0
⊢ P.signVariations =
    P.eraseLead.signVariations + if SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff then 1 else 0
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case refine_2
p : ℤ[X]
hp : (p.sum fun x x_1 ↦ x_1 ^ 2) = 3
⊢ p.IsUnitTrinomial

Tactic:
·

Goal state after:
case refine_2
p : ℤ[X]
hp : (p.sum fun x x_1 ↦ x_1 ^ 2) = 3
⊢ p.IsUnitTrinomial
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 k : ℕ
hk : q ≤ k
p' : R[X]
p'_le : p'.natDegree ≤ p.natDegree - k
hp' : (⇑derivative)^[k] p = k ! • p'
⊢ ∃ gp, gp.natDegree ≤ p.natDegree - k ∧ ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) gp

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hk

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 : ℕ
p' : R[X]
k : ℕ
hk : q ≤ q + k
p'_le : p'.natDegree ≤ p.natDegree - (q + k)
hp' : (⇑derivative)^[q + k] p = (q + k)! • p'
⊢ ∃ gp, gp.natDegree ≤ p.natDegree - (q + k) ∧ ∀ (r : A), (aeval r) ((⇑derivative)^[q + k] p) = q ! • (aeval r) gp
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case neg.nil
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
h_eL : P.eraseLead.coeffList = []
⊢ (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0))
            (SignType.sign P.leadingCoeff ::
              (List.replicate (P.natDegree - P.eraseLead.degree.succ) (SignType.sign 0) ++
                List.map ⇑SignType.sign [])))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2) (List.filter (fun x ↦ decide (x ≠ 0)) (List.map ⇑SignType.sign []))).length -
        1 +
      if SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff then 1 else 0

pp: case neg.cons
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
c : R
cs : List R
h_eL : P.eraseLead.coeffList = c :: cs
⊢ (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0))
            (SignType.sign P.leadingCoeff ::
              (List.replicate (P.natDegree - P.eraseLead.degree.succ) (SignType.sign 0) ++
                List.map (⇑SignType.sign) (c :: cs))))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
            (List.filter (fun x ↦ decide (x ≠ 0)) (List.map (⇑SignType.sign) (c :: cs)))).length -
        1 +
      if SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff then 1 else 0

Tactic:
·

Goal state after:
case neg.nil
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
h_eL : P.eraseLead.coeffList = []
⊢ (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.filter (fun x ↦ decide (x ≠ 0))
            (SignType.sign P.leadingCoeff ::
              (List.replicate (P.natDegree - P.eraseLead.degree.succ) (SignType.sign 0) ++
                List.map ⇑SignType.sign [])))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2) (List.filter (fun x ↦ decide (x ≠ 0)) (List.map ⇑SignType.sign []))).length -
        1 +
      if SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff then 1 else 0
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
c : ℕ → R[X]
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
hc : ∀ (k : ℕ) (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
⊢ ((range (p.natDegree + 1)).sum c).natDegree ≤ p.natDegree - q

pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
c : ℕ → R[X]
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
hc : ∀ (k : ℕ) (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
⊢ ∀ (r : A),
    (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) (sumIDeriv p) = q ! • (aeval r) ((range (p.natDegree + 1)).sum c)

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
c : ℕ → R[X]
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - q
hc : ∀ (k : ℕ) (r : A), (X - C r) ^ q ∣ map (algebraMap R A) p → (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
⊢ ((range (p.natDegree + 1)).sum c).natDegree ≤ p.natDegree - q