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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = f.mirror
⊢ g ∣ f.mirror

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
⊢ (ofFn n) ((toFn n) p) = p

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = -f.mirror
⊢ g ∣ f.mirror

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : n < m
r : R
⊢ ((monomial m) r).homogenize n = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
⊢ (fun₀ | 0 => m) 1 = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : m ≤ n
⊢ (X ^ m).homogenize n = MvPolynomial.X 0 ^ m * MvPolynomial.X 1 ^ (n - m)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n : ℕ
hn : n ≠ 0
⊢ 1 ≤ n

Tactic:
Nat.one_le_iff_ne_zero

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
hn : n ≠ 0
⊢ n ≠ 0
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n : ℕ
hn : n ≠ 0
⊢ X.homogenize n = MvPolynomial.X 0 * MvPolynomial.X 1 ^ (n - 1)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
c : R
n : ℕ
⊢ (C c).homogenize n = MvPolynomial.C c * MvPolynomial.X 1 ^ n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
⊢ Irreducible f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n : ℕ
⊢ homogenize 1 n = MvPolynomial.X 1 ^ n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
⊢ (fun₀ | 0 => m 0 | 1 => m 1) = m

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
h : p.homogenize n = 0
i : ℕ
H : i ≤ p.natDegree
⊢ p.coeff i = MvPolynomial.coeff (fun₀ | 0 => i | 1 => n - i) (p.homogenize n)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
h : p.homogenize n = 0
⊢ p = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ p = 0 → p.homogenize n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
h : R b a
⊢ destutter' R b (a :: l) = b :: destutter' R a l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
h : ¬R b a
⊢ destutter' R b (a :: l) = destutter' R b l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
⊢ destutter' R a [b] = if R a b then [a, b] else [a]

Tactic:
by

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

Goal state before:
pp: 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 (p.homogenize n) = eval₂ f (g 0) p

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
g : Fin 2 → A
hg : g 1 = 1
⊢ (MvPolynomial.aeval g) (p.homogenize n) = (aeval (g 0)) p

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: case pos
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
h✝ : R a b
⊢ a :: destutter' R b l <+ a :: b :: l

pp: case neg
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
h✝ : ¬R a b
⊢ destutter' R a l <+ a :: b :: l

Tactic:
· exact Sublist.cons_cons a (hl b)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ (MvPolynomial.aeval ![X, 1]) (p.homogenize n) = p

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n : ℕ
p : R[X]
⊢ (p.homogenize n).IsHomogeneous n

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
⊢ destutter' R a l <+ a :: l

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n : ℕ
q : MvPolynomial (Fin 2) R
hq : q.IsHomogeneous n
m : Fin 2 →₀ ℕ
hm : m ∈ q.support
⊢ MvPolynomial.coeff m q ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
n : ℕ
q : MvPolynomial (Fin 2) R
hq : q.IsHomogeneous n
hpq : (MvPolynomial.aeval ![X, 1]) q = p
⊢ p.homogenize n = q

Tactic:
by

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

Goal state before:
pp: case hq
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
m n : ℕ
hm : p.natDegree ≤ m
hn : q.natDegree ≤ n
⊢ (p.homogenize m * q.homogenize n).IsHomogeneous (m + n)

pp: case hpq
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
m n : ℕ
hm : p.natDegree ≤ m
hn : q.natDegree ≤ n
⊢ (MvPolynomial.aeval ![X, 1]) (p.homogenize m * q.homogenize n) = p * q

Tactic:
· apply_rules [MvPolynomial.IsHomogeneous.mul, isHomogeneous_homogenize]

Goal state after:
case hpq
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
m n : ℕ
hm : p.natDegree ≤ m
hn : q.natDegree ≤ n
⊢ (MvPolynomial.aeval ![X, 1]) (p.homogenize m * q.homogenize n) = p * q
Module: Mathlib.Algebra.Polynomial.Homogenize

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
m n : ℕ
hm : p.natDegree ≤ m
hn : q.natDegree ≤ n
⊢ (p * q).homogenize (m + n) = p.homogenize m * q.homogenize n

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
p : ι → R[X]
n : ι → ℕ
h : ∀ i ∈ s, (p i).natDegree ≤ n i
⊢ (∏ i ∈ s, p i).homogenize (∑ i ∈ s, n i) = ∏ i ∈ s, (p i).homogenize (n i)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p r : R[X]
⊢ p = 0 ∨ r = 0 ∨ p ≠ 0 ∧ r ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
l : List α
a : α
⊢ IsChain R (destutter' R a l)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p ∣ q
⊢ p.homogenize p.natDegree ∣ q.homogenize q.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
l : List α
a b : α
hab : R a b
⊢ IsChain R (a :: destutter' R b l)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
h : IsChain R (a :: l)
⊢ destutter' R a l = a :: l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
h : destutter' R a l = a :: l
⊢ IsChain R (a :: l)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
⊢ destutter R [] = [] ↔ IsChain R []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
inst✝¹ : DecidableRel R
R₂ : β → β → Prop
inst✝ : DecidableRel R₂
f : α → β
hl : ∀ (a : α), a ∈ [] → ∀ (b : α), b ∈ [] → (R a b ↔ R₂ (f a) (f b))
⊢ map f (destutter R []) = destutter R₂ (map f [])

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
inst✝¹ : DecidableRel R
R₂ : β → β → Prop
inst✝ : DecidableRel R₂
f : α → β
a : α
hl : ∀ (a_1 : α), a_1 ∈ [a] → ∀ (b : α), b ∈ [a] → (R a_1 b ↔ R₂ (f a_1) (f b))
⊢ map f (destutter R [a]) = destutter R₂ (map f [a])

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
inst✝¹ : DecidableRel R
R₂ : β → β → Prop
inst✝ : DecidableRel R₂
f : α → β
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → (R a_1 b_1 ↔ R₂ (f a_1) (f b_1))
⊢ a ∈ a :: b :: l

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
inst✝¹ : DecidableRel R
R₂ : β → β → Prop
inst✝ : DecidableRel R₂
f : α → β
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → (R a_1 b_1 ↔ R₂ (f a_1) (f b_1))
⊢ b ∈ a :: b :: l

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
f g : R[X]
hg : g.Monic
n : ℕ
⊢ ∃ q r, (∀ (i : Fin n), (r i).degree < g.degree) ∧ f = q * g ^ n + ∑ i, r i * g ^ ↑i

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
q₁ q₂ : R[X]
r₁ r₂ : Fin 0 → R[X]
hr₁ : ∀ (i : Fin 0), (r₁ i).degree < g.degree
hr₂ : ∀ (i : Fin 0), (r₂ i).degree < g.degree
hf : q₁ * g ^ 0 + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ 0 + ∑ i, r₂ i * g ^ ↑i
⊢ q₁ = q₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
inst✝¹ : DecidableRel R
R₂ : β → β → Prop
inst✝ : DecidableRel R₂
f : α → β
a b : α
l : List α
hl : ∀ (a_1 : α), a_1 ∈ a :: b :: l → ∀ (b_1 : α), b_1 ∈ a :: b :: l → (R a_1 b_1 ↔ R₂ (f a_1) (f b_1))
⊢ map f (destutter R (a :: b :: l)) = destutter R₂ (map f (a :: b :: l))

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

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

Tactic:
by

Goal state after:
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
⊢ (destutter' R b (c :: l)).length ≤ (destutter' R a (c :: l)).length

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
⊢ (destutter' R b []).length ≤ (destutter' R a [b]).length

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
i : Fin 2
⊢ (p.toTupleMvPolynomial i).IsHomogeneous p.natDegree

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
⊢ (MvPolynomial.aeval ![X, 1]) (p.toTupleMvPolynomial 0) = p * (MvPolynomial.aeval ![X, 1]) (p.toTupleMvPolynomial 1)

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝ : Field R
p : R[X]
x : R
⊢ eval x p =
    (MvPolynomial.eval ![x, 1]) (p.toTupleMvPolynomial 0) / (MvPolynomial.eval ![x, 1]) (p.toTupleMvPolynomial 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a b : α
inst✝ : IsEquiv α Rᶜ
c : α
cs : List α
⊢ (destutter' R b (c :: cs)).length ≤ (destutter' R a (b :: c :: cs)).length

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : R[X]
s : Fin 2 →₀ ℕ
hs : s ∈ (p.homogenize p.natDegree).support
⊢ s 0 + s 1 = p.natDegree

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a : α
inst✝ : IsEquiv α Rᶜ
⊢ (destutter R []).length ≤ (destutter R [a]).length

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
inst✝ : IsEquiv α Rᶜ
x✝¹ : [] <+ []
x✝ : IsChain R []
⊢ [].length ≤ (destutter R []).length

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
inst✝ : IsEquiv α Rᶜ
l₁ : List α
a : α
hl : [] <+ l₁
hl₁ : IsChain R [a]
⊢ [a].length ≤ (destutter R (a :: l₁)).length

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
n : ℕ
hn : n ∈ p.support
⊢ (fun₀ | 0 => n | 1 => p.natDegree - n) 0 = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
inst✝ : IsEquiv α Rᶜ
l₁ : List α
b : α
l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : IsChain R (a :: l₁)
⊢ (a :: l₁).length ≤ (destutter R (a :: b :: l₂)).length

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
inst✝ : IsEquiv α Rᶜ
b : α
l₁ l₂ : List α
a : α
hl : l₁ <+ l₂
hl₁ : IsChain R (a :: b :: l₁)
⊢ (a :: b :: l₁).length ≤ (destutter R (a :: b :: l₂)).length

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
h : Pairwise r []
⊢ destutter (fun x1 x2 ↦ x1 ≠ x2) [] = [].dedup

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x : α
h : Pairwise r [x]
⊢ destutter (fun x1 x2 ↦ x1 ≠ x2) [x] = [x].dedup

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
M : Type u_2
inst✝ : AddCommMonoid M
p : R[X]
f : R → M
⊢ ((p.homogenize p.natDegree).coeff.sum fun x c ↦ f c) = p.sum fun x c ↦ f c

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
p : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
⊢ p.smeval x = p.sum (smul_pow x)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
r : R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
⊢ (C r).smeval x = r • x ^ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
r : R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
n : ℕ
⊢ ((monomial n) r).smeval x = r • x ^ n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
p : R[X]
⊢ eval r p = p.smeval r

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x y : α
xs : List α
hxy : x ≠ y
h : (r x y ∧ ∀ (a : α), a ∈ xs → r x a) ∧ (∀ (a' : α), a' ∈ xs → r y a') ∧ Pairwise r xs
this : ¬x ∈ xs
⊢ ¬x ∈ y :: xs

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
rs₁ : Fin n → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₁ r₁ i).degree < g.degree
rs₂ : Fin n → R[X]
r₂ : R[X]
hr₂ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₂ r₂ i).degree < g.degree
hf : (r₁ + g * q₁) * g ^ n + ∑ x, rs₁ x * g ^ ↑x = (r₂ + g * q₂) * g ^ n + ∑ x, rs₂ x * g ^ ↑x
i : Fin n
⊢ (rs₁ i).degree < g.degree

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Module R S
inst✝ : IsScalarTower R S S
p : R[X]
x : S
⊢ eval₂ RingHom.smulOneHom x p = p.smeval x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
⊢ smeval 0 x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Destutter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : Std.Antisymm r
x y : α
xs : List α
h : Pairwise r (x :: y :: xs)
⊢ destutter (fun x1 x2 ↦ x1 ≠ x2) (x :: y :: xs) = (x :: y :: xs).dedup

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
⊢ smeval 1 x = 1 • x ^ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
rs₁ : Fin n → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₁ r₁ i).degree < g.degree
rs₂ : Fin n → R[X]
r₂ : R[X]
hr₂ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₂ r₂ i).degree < g.degree
hf : (r₁ + g * q₁) * g ^ n + ∑ x, rs₁ x * g ^ ↑x = (r₂ + g * q₂) * g ^ n + ∑ x, rs₂ x * g ^ ↑x
i : Fin n
⊢ (rs₂ i).degree < g.degree

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
⊢ X.smeval x = x ^ 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
n : ℕ
⊢ (X ^ n).smeval x = x ^ n

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
rs₁ : Fin n → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₁ r₁ i).degree < g.degree
rs₂ : Fin n → R[X]
r₂ : R[X]
hr₂ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₂ r₂ i).degree < g.degree
hf : (r₁ + g * q₁) * g ^ n + ∑ x, rs₁ x * g ^ ↑x = (r₂ + g * q₂) * g ^ n + ∑ x, rs₂ x * g ^ ↑x
hqr : r₁ + g * q₁ = r₂ + g * q₂
hrs : rs₁ = rs₂
⊢ r₁.degree < g.degree

Tactic:
by

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

Goal state before:
pp: 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
⊢ (p + q).smeval x = p.smeval x + q.smeval x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
rs₁ : Fin n → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₁ r₁ i).degree < g.degree
rs₂ : Fin n → R[X]
r₂ : R[X]
hr₂ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₂ r₂ i).degree < g.degree
hf : (r₁ + g * q₁) * g ^ n + ∑ x, rs₁ x * g ^ ↑x = (r₂ + g * q₂) * g ^ n + ∑ x, rs₂ x * g ^ ↑x
hqr : r₁ + g * q₁ = r₂ + g * q₂
hrs : rs₁ = rs₂
hq₁ : (r₁ + g * q₁) /ₘ g = q₁
hrr₁ : (r₁ + g * q₁) %ₘ g = r₁
⊢ r₂.degree < g.degree

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
n : ℕ
⊢ (↑n).smeval x = n • x ^ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
q₁ q₂ : R[X]
r₁ r₂ : Fin n → R[X]
hr₁ : ∀ (i : Fin n), (r₁ i).degree < g.degree
hr₂ : ∀ (i : Fin n), (r₂ i).degree < g.degree
hf : q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i
⊢ q₁ = q₂ ∧ r₁ = r₂

Tactic:
by

Goal state after: