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

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

Tactic:
refine ⟨?_, ?_, revAt_invol⟩

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

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ (toFn n) 0 = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
⊢ -p.reverse * X ^ (-p).natTrailingDegree = -(p.reverse * X ^ p.natTrailingDegree)

Tactic:
natTrailingDegree_neg,

Goal state after:
R : Type u_1
inst✝ : Ring R
p : R[X]
⊢ -p.reverse * X ^ p.natTrailingDegree = -(p.reverse * X ^ p.natTrailingDegree)
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ (ofFn n) 0 = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
v : Fin 0 → R
⊢ (ofFn 0) v = 0

Tactic:
simp

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

Goal state before:
pp: case isUnit_or_isUnit
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 ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
⊢ IsUnit g ∨ IsUnit h

Tactic:
rcases hk with (hk | hk | hk | hk)

Goal state after:
case isUnit_or_isUnit.inl
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
⊢ IsUnit g ∨ IsUnit h

case isUnit_or_isUnit.inr.inl
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
⊢ IsUnit g ∨ IsUnit h

case isUnit_or_isUnit.inr.inr.inl
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
⊢ IsUnit g ∨ IsUnit h

case isUnit_or_isUnit.inr.inr.inr
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
⊢ IsUnit g ∨ IsUnit h
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

Tactic:
simp

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

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

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
⊢ (fun₀ | 0 => m 0 | 1 => m 1) ((fun i ↦ i) ⟨0, ⋯⟩) = m ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp

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

Goal state before:
pp: case «1»
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
m : Fin 2 →₀ ℕ
k : ℕ
c : R
hkn : k ≤ n
⊢ (fun₀ | 0 => m 0 | 1 => m 1) ((fun i ↦ i) ⟨1, ⋯⟩) = m ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
a : α
⊢ IsChain R (destutter' R a [])

Tactic:
simp

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

Tactic:
simp

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
a : α
h : IsChain R [a]
⊢ destutter' R a [] = [a]

Tactic:
simp

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

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

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

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

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

Goal state after:
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 ^ n + ∑ i, Fin.snoc r (q %ₘ g) i.castSucc * g ^ ↑i.castSucc

Tactic:
simp

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

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

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

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

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

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

Goal state before:
pp: case empty
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ ∅, (g i).Monic
hgg : (↑∅).Pairwise fun i j ↦ IsCoprime (g i) (g j)
⊢ ∃ q r, (∀ i ∈ ∅, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ ∅, g i + ∑ i ∈ ∅, r i * ∏ k ∈ ∅.erase i, g k

Tactic:
simp

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

Goal state before:
pp: S : Type u_3
inst✝² : NonAssocRing S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
q : ℕ[X]
n : ℕ
⊢ ∑ n_1 ∈ q.support, q.coeff n_1 • (-↑n) ^ n_1 = ↑(∑ n_1 ∈ q.support, q.coeff n_1 • (-↑n) ^ n_1)

Tactic:
simp

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

Goal state before:
pp: 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
⊢ 0 < 1

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ (derivativeFinsupp p).support ⊆ range (p.natDegree + 1)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∀ i ∈ range (p.natDegree + 1), id 0 = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
⊢ ∀ i ∈ range n, id 0 = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ ∀ i ∈ range (n + 1), id 0 = 0

Tactic:
simp

Goal state after:
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 * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (k + k) (↑u * ↑w)) +
                  Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (k + (n - m + k)) (↑u * ↑v)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (k + n) (↑u * ↑u)) +
              (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + k) (↑v * ↑w)) +
                  Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + (n - m + k)) (↑v * ↑v)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + n) (↑v * ↑u))) +
            (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + k) (↑w * ↑w)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + (n - m + k)) (↑w * ↑v)) +
              Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + n) (↑w * ↑u)))) }

Tactic:
Finsupp.filter_single_of_neg,

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 * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (0 + Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (k + (n - m + k)) (↑u * ↑v)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (k + n) (↑u * ↑u)) +
              (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + k) (↑v * ↑w)) +
                  Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + (n - m + k)) (↑v * ↑v)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + n) (↑v * ↑u))) +
            (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + k) (↑w * ↑w)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + (n - m + k)) (↑w * ↑v)) +
              Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + n) (↑w * ↑u)))) }

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.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
i j : ι
s : Finset ι
hj : j ∉ s
ih : ∀ (hi : i ∉ s), ((↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)) → IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
⊢ i ∈ ↑(Finset.cons i (Finset.cons j s hj) hi)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
inst✝ : DecidableEq ι
g : ι → R[X]
i j : ι
s : Finset ι
hj : j ∉ s
ih : ∀ (hi : i ∉ s), ((↑(Finset.cons i s hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)) → IsCoprime (g i) (∏ i ∈ s, g i)
hi : i ∉ Finset.cons j s hj
hgg : (↑(Finset.cons i (Finset.cons j s hj) hi)).Pairwise fun i j ↦ IsCoprime (g i) (g j)
⊢ j ∈ ↑(Finset.cons i (Finset.cons j s hj) hi)

Tactic:
simp

Goal state after:
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 * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (0 + Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (k + (n - m + k)) (↑u * ↑v)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (k + n) (↑u * ↑u)) +
              (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + k) (↑v * ↑w)) +
                  Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + (n - m + k)) (↑v * ↑v)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + n) (↑v * ↑u))) +
            (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + k) (↑w * ↑w)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + (n - m + k)) (↑w * ↑v)) +
              Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + n) (↑w * ↑u)))) }

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:
Finsupp.filter_single_of_neg,

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 * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (0 + 0 + Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (k + n) (↑u * ↑u)) +
              (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + k) (↑v * ↑w)) +
                  Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + (n - m + k)) (↑v * ↑v)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + n) (↑v * ↑u))) +
            (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + k) (↑w * ↑w)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + (n - m + k)) (↑w * ↑v)) +
              Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + n) (↑w * ↑u)))) }

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.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 * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (0 + 0 + Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (k + n) (↑u * ↑u)) +
              (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + k) (↑v * ↑w)) +
                  Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + (n - m + k)) (↑v * ↑v)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + n) (↑v * ↑u))) +
            (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + k) (↑w * ↑w)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + (n - m + k)) (↑w * ↑v)) +
              Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + n) (↑w * ↑u)))) }

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:
Finsupp.filter_single_of_neg,

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 * (monomial (m + n)) ↑u + C ↑v * (monomial (n - m + k + n)) ↑w =
    {
      toFinsupp :=
        AddMonoidAlgebra.ofCoeff
          (0 + 0 + 0 +
              (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + k) (↑v * ↑w)) +
                  Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + (n - m + k)) (↑v * ↑v)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (m + n) (↑v * ↑u))) +
            (Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + k) (↑w * ↑w)) +
                Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + (n - m + k)) (↑w * ↑v)) +
              Finsupp.filter (fun x ↦ x ∈ Set.Ioo (k + n) (n + n)) (Finsupp.single (n + n) (↑w * ↑u)))) }

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)