mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α ↪ β
y : β →₀ ℕ
z : α →₀ ℕ
h : y ≤ embDomain f z
w : β →₀ ℕ
hw : embDomain f z = y + w
x✝ : β
⊢ ¬y x✝ = 0 → y x✝ = 0 → ¬w x✝ = 0

Tactic:
grind

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝ : ∀ (i : ι), Std.Trichotomous s
wf : WellFounded r
a b : (i : ι) → β i
hab : ¬Pi.Lex r s a b
hba : ¬Pi.Lex r s b a
h✝ : ∃ a_1, a a_1 ≠ b a_1
i : ι := wf.min {i | a i ≠ b i} h✝
j : ι
hr : r j i
h : ¬a j = b j
⊢ j ∈ {i | a i ≠ b i}

Tactic:
grind

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝² : Preorder ι
inst✝¹ : DecidableEq ι
inst✝ : LT α
f : ι → α
i j : ι
h₁ : i ≤ j
h₂ : f i < f j
⊢ toColex (f ∘ ⇑(Equiv.swap i j)) < toColex f

Tactic:
Equiv.swap_comm

Goal state after:
ι : Type u_1
α : Type u_3
inst✝² : Preorder ι
inst✝¹ : DecidableEq ι
inst✝ : LT α
f : ι → α
i j : ι
h₁ : i ≤ j
h₂ : f i < f j
⊢ toColex (f ∘ ⇑(Equiv.swap j i)) < toColex f
Module: Mathlib.Data.DFinsupp.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁶ : (i : ι) → AddCommMonoid (α i)
inst✝⁵ : (i : ι) → PartialOrder (α i)
inst✝⁴ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝³ : (i : ι) → Sub (α i)
inst✝² : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
⊢ f.support \ g.support ⊆ (f - g).support

Tactic:
by
  simp +contextual [subset_iff]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
this : (P * Q).coeff (l + m) = P.coeff l * Q.leadingCoeff
⊢ P.coeff l * Q.leadingCoeff = 0

Tactic:
by rw [← this, hQ, coeff_zero]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Fintype σ
g : R →+* S₁
X : σ → S₁
f : MvPolynomial σ R
⊢ ∑ d ∈ f.support, g (coeff d f) * ∏ i ∈ d.support, X i ^ d i =
    ∑ x ∈ f.support, g (coeff x f) * x.prod fun a b ↦ X a ^ b

Tactic:
rfl

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
α : Type u_2
s : Finset α
f : α → σ →₀ ℕ
g : α → R
⊢ ∏ x ∈ s, C (g x) * (monomial (f x)) 1 = ∏ i ∈ s, (monomial (f i)) (g i)

Tactic:
C_mul_monomial,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
α : Type u_2
s : Finset α
f : α → σ →₀ ℕ
g : α → R
⊢ ∏ x ∈ s, (monomial (f x)) (g x * 1) = ∏ i ∈ s, (monomial (f i)) (g i)
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f₁ : R →+* S₁
g₁ : σ → S₁
p₁ : MvPolynomial σ R
⊢ (eval₂Hom f₁ g₁) p₁ = (eval₂Hom f₁ g₁) p₁

Tactic:
rfl

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

Goal state before:
pp: R : Type u
σ : Type u_1
a : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
h : Decidable (a = 0)
⊢ ((monomial s) a).support = if a = 0 then ∅ else {s}

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
p : MvPolynomial σ R
⊢ φ ((eval₂Hom f g) p) = (φ.comp (eval₂Hom f g)) p

Tactic:
rfl

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
d : σ →₀ ℕ
x : σ → ℕ
s : Finset σ
⊢ coeff d (∏ y ∈ s, X y ^ x y) = if d = Finsupp.indicator s fun i x_1 ↦ x i then 1 else 0

Tactic:
simp_rw [prod_X_pow x s, coeff_monomial, eq_comm]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (∃ d, coeff d p ≠ 0) ↔ ∃ d, coeff d p ≠ 0

Tactic:
rfl

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

Goal state before:
pp: case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
c' : (σ →₀ ℕ) → R := fun i ↦ if i ∈ φ.support then C i else 0
ψ : MvPolynomial σ R := ∑ i ∈ φ.support, (monomial i) (c' i)
i : σ →₀ ℕ
hi : i ∉ φ.support
⊢ coeff i φ = r * 0

Tactic:
rw [notMem_support_iff] at hi
        rwa [mul_zero]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
q : S₁ →+* S₂
g : σ → S₁
p : MvPolynomial σ S₁
⊢ q ((eval g) p) = (eval (⇑q ∘ g)) ((map q) p)

Tactic:
rw [← eval₂_eq_eval_map, ← eval₂_id, eval₂_comp_right, map_id]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
⊢ (p.support.sup fun s ↦ toMultiset s) = p.support.sup fun s ↦ toMultiset s

Tactic:
convert!
      rfl

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case refine_1
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
s : σ →₀ ℕ
hs : s ∈ p.support
h : ∀ (a : σ), ¬∃ d, coeff d p ≠ 0 ∧ a ∈ d.support
⊢ s.support = ∅

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case refine_2
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : ∀ b ∈ p.support, b = 0
i : σ
hi : i ∈ p.degrees
s : σ →₀ ℕ
hs1 : coeff s p ≠ 0
hs2 : i ∈ s.support
this : i ∈ ∅
⊢ False

Tactic:
grind

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

Goal state before:
pp: case mpr
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
i✝ : σ →₀ ℕ
hp : ∀ (i : σ →₀ ℕ), coeff i p ∈ M
i : σ →₀ ℕ
⊢ (if i✝ ≤ i then coeff (i - i✝) p * 1 else 0) ∈ M

Tactic:
split <;> simp [hp]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case add.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial (↥s) R
t : Finset σ
q : MvPolynomial (↥t) R
⊢ (rename Subtype.val) p + (rename Subtype.val) q =
    (rename (Subtype.val ∘ Subtype.map id ⋯)) p + (rename (Subtype.val ∘ Subtype.map id ⋯)) q

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case mul_X.refine_2
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial (↥s) R
⊢ (rename Subtype.val) p * X n = (rename (Subtype.val ∘ Subtype.map id ⋯)) p * X n

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₁ → R
hg : g 0 = 0
φ : MvPolynomial σ S₁
⊢ (∀ (m : σ →₀ ℕ), f (coeff m (ofCoeff (mapRange g hg φ.coeff))) = coeff m φ) ↔
    ∀ (d : σ →₀ ℕ), f (g (coeff d φ)) = coeff d φ

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case refine_2.monomial_add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
a : σ →₀ ℕ
s : S₁
p : MvPolynomial σ S₁
ha : a ∉ p.coeff.support
hs : s ≠ 0
hp : ↑p.coeffs ⊆ range ⇑f → p ∈ range ⇑(map f)
ih : ↑((monomial a) s).coeffs ⊆ range ⇑f → (monomial a) s ∈ range ⇑(map f)
hx : ↑((monomial a) s + p).coeffs ⊆ range ⇑f
⊢ (monomial a) s + p ∈ range ⇑(map f)

Tactic:
coeffs_add (disjoint_support_monomial ha hs)

Goal state after:
case refine_2.monomial_add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
a : σ →₀ ℕ
s : S₁
p : MvPolynomial σ S₁
ha : a ∉ p.coeff.support
hs : s ≠ 0
hp : ↑p.coeffs ⊆ range ⇑f → p ∈ range ⇑(map f)
ih : ↑((monomial a) s).coeffs ⊆ range ⇑f → (monomial a) s ∈ range ⇑(map f)
hx : ↑(((monomial a) s).coeffs ∪ p.coeffs) ⊆ range ⇑f
⊢ (monomial a) s + p ∈ range ⇑(map f)
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
⊢ (p.support.sup fun s ↦ toMultiset s) = p.degrees

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommSemiring S₁
inst✝¹ : Algebra R S₁
B : Type u_2
inst✝ : CommSemiring B
g : σ → S₁
φ : S₁ →+* B
p : MvPolynomial σ R
⊢ φ ((aeval g) p) = (φ.comp (eval₂Hom (algebraMap R S₁) g)) p

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars = s✝.biUnion fun i ↦ (φ i).vars
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ a ∈ (φ i).vars, ∀ b ∈ (φ j).vars, a ≠ b
⊢ ∀ a ∈ (φ a✝).vars, ∀ b ∈ (∑ x ∈ s✝, φ x).vars, a ≠ b

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: case zero
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
⊢ (cons 0 (single i y)) 0 = (single i.succ y) 0

Tactic:
simp [single_apply]

Goal state after:
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: case succ
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
i✝ : Fin n
⊢ (cons 0 (single i y)) i✝.succ = (single i.succ y) i✝.succ

Tactic:
simp [single_apply]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
d : σ →₀ ℕ
hd : d ∈ φ.support
i : σ
hi : i ∈ d.support
hgi : g i = 0
⊢ 0 ^ d i = 0

Tactic:
zero_pow

Goal state after:
R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
d : σ →₀ ℕ
hd : d ∈ φ.support
i : σ
hi : i ∈ d.support
hgi : g i = 0
⊢ 0 = 0

R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
d : σ →₀ ℕ
hd : d ∈ φ.support
i : σ
hi : i ∈ d.support
hgi : g i = 0
⊢ d i ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case neg
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬constantCoeff p = 0
⊢ f (coeff 0 p) = f (constantCoeff p)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case pos
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
i : σ
hi : i ∈ d.support
⊢ (f (coeff d p) * d.prod fun i k ↦ g i ^ k) = 0

Tactic:
rw [Finsupp.prod, Finset.prod_eq_zero hi, mul_zero]

Goal state after:
case pos
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
i : σ
hi : i ∈ d.support
⊢ g i ^ d i = 0
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case neg.h₀
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
i : σ
hi : i ∈ d.support
⊢ (f (coeff d p) * d.prod fun i k ↦ g i ^ k) = 0

Tactic:
rw [Finsupp.prod, Finset.prod_eq_zero hi, mul_zero]

Goal state after:
case neg.h₀
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
i : σ
hi : i ∈ d.support
⊢ g i ^ d i = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case h
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ f.support
h : ∀ (i : σ), n ≤ d i
i✝ : σ
⊢ 0 = 0

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case refine_3
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ p = p

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case e_a
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : ↑q.vars ⊆ s
inst✝ : (i : σ) → Decidable (i ∈ s)
u : σ →₀ ℕ
hu : u ∈ q.support
⊢ (u.prod fun i k ↦ (if i ∈ s then X i else 0) ^ k) = u.prod fun n e ↦ X n ^ e

Tactic:
exact Finsupp.prod_congr (fun i hi ↦ by simp [hs ((mem_vars_iff_mem_support _).mpr ⟨u, hu, hi⟩)])

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

Goal state before:
pp: R : Type u
a : R
n : ℕ
inst✝ : Semiring R
ha : a ≠ 0
⊢ ↑n = ↑n

Tactic:
rfl

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

Goal state before:
pp: R : Type u
a : R
n : ℕ
inst✝ : Semiring R
ha : a ≠ 0
⊢ (↑n).toNat = n

Tactic:
rfl

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

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ai : R
au : ai * a = 1
⊢ (C 1 * p).natDegree = (C ai * (C a * p)).natDegree

Tactic:
← au,

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ai : R
au : ai * a = 1
⊢ (C (ai * a) * p).natDegree = (C ai * (C a * p)).natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ai : R
au : a * ai = 1
⊢ (p * C 1).natDegree = (p * C a * C ai).natDegree

Tactic:
← au,

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ai : R
au : a * ai = 1
⊢ (p * C (a * ai)).natDegree = (p * C a * C ai).natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case succ
R : Type u
m✝ n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
m : ℕ
hm : (p ^ m).coeff (m * n) = p.coeff n ^ m
⊢ (p ^ m * p).coeff ((m + 1) * n) = (p ^ m).coeff (m * n) * p.coeff n

Tactic:
Nat.succ_mul,

Goal state after:
case succ
R : Type u
m✝ n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
m : ℕ
hm : (p ^ m).coeff (m * n) = p.coeff n ^ m
⊢ (p ^ m * p).coeff (m * n + n) = (p ^ m).coeff (m * n) * p.coeff n
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.coeff 0 = 0
⊢ p.nextCoeffUp = p.coeff (p.natTrailingDegree + 1)

Tactic:
obtain rfl | hp₀ := eq_or_ne p 0

Goal state after:
case inl
R : Type u
inst✝ : Semiring R
hp : coeff 0 0 = 0
⊢ nextCoeffUp 0 = coeff 0 (natTrailingDegree 0 + 1)

case inr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.coeff 0 = 0
hp₀ : p ≠ 0
⊢ p.nextCoeffUp = p.coeff (p.natTrailingDegree + 1)
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
n✝ : ℕ
h₁ : c = n✝ + 1
⊢ n✝ + 1 - 1 + 1 = n✝ + 1

Tactic:
rfl

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

Goal state before:
pp: N i : ℕ
⊢ (if (if i ≤ N then N - i else i) ≤ N then N - if i ≤ N then N - i else i else if i ≤ N then N - i else i) = i

Tactic:
grind

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
N n : ℕ
c : R
n✝ : ℕ
⊢ (reflect N (C c * X ^ n)).coeff n✝ = (C c * X ^ (revAt N) n).coeff n✝

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝³ : CommSemiring R
inst✝² : IsEmpty σ
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
this : aeval f = (Algebra.ofId R S₁).comp ↑(isEmptyAlgEquiv R σ)
⊢ Injective ⇑((Algebra.ofId R S₁).comp ↑(isEmptyAlgEquiv R σ)) ↔ Injective (⇑(algebraMap R S₁) ∘ ⇑(isEmptyAlgEquiv R σ))

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ (algebraMap R (MvPolynomial S₁ R)[X]) r *
      ((none.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m none *
        m.some.prod fun a k ↦ ((Option.some a).elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ k) =
    (Polynomial.monomial (m none)) ((monomial m.some) r)

Tactic:
MvPolynomial.monomial_eq,

Goal state after:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ (algebraMap R (MvPolynomial S₁ R)[X]) r *
      ((none.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ m none *
        m.some.prod fun a k ↦ ((Option.some a).elim Polynomial.X fun s ↦ Polynomial.C (X s)) ^ k) =
    (Polynomial.monomial (m none)) (C r * m.some.prod fun n e ↦ X n ^ e)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial (Option σ) R
h : f ≠ 0
⊢ f.support.sup ((fun x ↦ x) ∘ fun m ↦ m none) = f.support.sup fun m ↦ m none

Tactic:
Function.comp_def

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial (Option σ) R
h : f ≠ 0
⊢ (f.support.sup fun x ↦ x none) = f.support.sup fun m ↦ m none
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial (Option σ) R
h : f ≠ 0
h' : (((optionEquivLeft R σ) f).support.sup fun x ↦ x) = degreeOf none f
⊢ ((optionEquivLeft R σ) f).support.sup WithBot.some = ((optionEquivLeft R σ) f).support.sup (WithBot.some ∘ fun x ↦ x)

Tactic:
Function.comp_def

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial (Option σ) R
h : f ≠ 0
h' : (((optionEquivLeft R σ) f).support.sup fun x ↦ x) = degreeOf none f
⊢ ((optionEquivLeft R σ) f).support.sup WithBot.some = ((optionEquivLeft R σ) f).support.sup fun x ↦ ↑x
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case succ.succ.refine_3
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ motive f.eraseLead

pp: case succ.succ.refine_4
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ motive (C f.leadingCoeff * X ^ f.natDegree)

Tactic:
· exact hc _ (eraseLead_natDegree_le_aux.trans df) (card_support_eraseLead' hf)

Goal state after:
case succ.succ.refine_4
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ motive (C f.leadingCoeff * X ^ f.natDegree)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case hC
R : Type u
inst✝ : CommSemiring R
n : ℕ
i : R
⊢ (algebraMap R (MvPolynomial (Fin n) R)[X]) i = Polynomial.C (C i)

Tactic:
rfl

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : R
g : R[X]
hfg : (X + C a) * g = 1
hgf : g * (X + C a) = 1
h : 0 = 1 + g.natDegree
⊢ False

Tactic:
grind

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
hn : (p ^ n).natDegree = n * p.natDegree
⊢ n * p.natDegree + p.natDegree = (n + 1) * p.natDegree

Tactic:
Nat.succ_mul,

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
n : ℕ
hn : (p ^ n).natDegree = n * p.natDegree
⊢ n * p.natDegree + p.natDegree = n * p.natDegree + p.natDegree
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case cons
S : Type u_1
inst✝ : Semiring S
n : WithBot ℕ
hd : S[X]
tl : List S[X]
ih : (∀ p ∈ tl, p.degree ≤ n) → tl.sum.degree ≤ n
hl : ∀ p ∈ hd :: tl, p.degree ≤ n
⊢ (hd :: tl).sum.degree ≤ n

Tactic:
| cons hd tl ih =>

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

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
⊢ (∏ i ∈ s, f i).degree ≤ ∑ i ∈ s, (f i).degree

Tactic:
simpa only [Multiset.map_map] using! degree_multiset_prod_le (s.1.map f)

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u_1
σ : Type u_3
inst✝ : CommSemiring R
i : σ
⊢ Injective ⇑(toMvPolynomial i)

Tactic:
by
  simp only [toMvPolynomial_eq_rename_comp, AlgHom.coe_comp, AlgEquiv.coe_toAlgHom,
    EquivLike.injective_comp]
  exact MvPolynomial.rename_injective (fun x ↦ i) fun _ _ _ ↦ rfl

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
n j : ℕ
j_in : j ∈ range n
⊢ op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = op y ^ j * op x ^ (n - 1 - j)

Tactic:
grind

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

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ ¬(p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)) ↔
    ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂

Tactic:
and_iff_right,

Goal state after:
case inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ (¬∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)) ↔
    ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂

case inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ p ≠ 1
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
m n : ℕ
⊢ x ^ m - 1 ∣ (x ^ m) ^ n - 1

Tactic:
exact sub_one_dvd_pow_sub_one (x ^ m) n

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r

Tactic:
by
  by_cases hp₀ : p = 0
  · by_cases hb₀ : b = 0
    · rw [hp₀, hb₀, pow_zero, pow_one, sub_self]
      exact dvd_zero _
    have ha₀ : a ≠ 0 := by rintro rfl; rw [zero_dvd_iff] at h; tauto
    rw [hp₀, zero_pow ha₀, zero_pow hb₀]
  have hp (c) : 1 ≤ p ^ c := Nat.pow_pos <| pos_of_ne_zero hp₀
  rw [← Nat.sub_add_cancel (hp a), ← Nat.sub_add_cancel (hp b), pow_succ', pow_succ',
    ← mul_sub_one, ← mul_sub_one]
  refine mul_dvd_mul_left _ <| dvd_pow_sub_one_of_dvd <| Int.natCast_dvd_natCast.mp ?_
  push_cast [hp a, hp b]
  exact dvd_pow_sub_one_of_dvd h

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
h : 0 ∉ t
⊢ t.prod.natDegree = (Multiset.map natDegree t).sum

Tactic:
nontriviality R
  rw [natDegree_multiset_prod']
  simp_rw [Ne, Multiset.prod_eq_zero_iff, Multiset.mem_map, leadingCoeff_eq_zero]
  rintro ⟨_, h, rfl⟩
  contradiction

Goal state after: