mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
p q : MvPolynomial σ R
⊢ (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e) →
    (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (q * (monomial s) a) = eval₂ f g q * f a * s.prod fun n e ↦ g n ^ e) →
      ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g ((p + q) * (monomial s) a) = eval₂ f g (p + q) * f a * s.prod fun n e ↦ g n ^ e

Tactic:
ih_p

Goal state after:
case add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
p q : MvPolynomial σ R
ih_p : ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e
⊢ (∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (q * (monomial s) a) = eval₂ f g q * f a * s.prod fun n e ↦ g n ^ e) →
    ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g ((p + q) * (monomial s) a) = eval₂ f g (p + q) * f a * s.prod fun n e ↦ g n ^ e
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) = (eval₂Hom (φ.comp f) fun i ↦ φ (g i)) p

Tactic:
by
  rw [← comp_eval₂Hom]
  rfl

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
⊢ coeff m (X i) = if Finsupp.single i 1 = m then 1 else 0

Tactic:
← coeff_X_pow,

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
⊢ coeff m (X i) = coeff m (X i ^ 1)
Module: Mathlib.Algebra.MvPolynomial.Eval

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

Tactic:
by
  apply MvPolynomial.induction_on p
  · intro r
    rw [eval₂_C, map_C, eval₂_C]
  · intro p q hp hq
    rw [eval₂_add, k.map_add, (map f).map_add, eval₂_add, hp, hq]
  · intro p s hp
    rw [eval₂_mul, k.map_mul, (map f).map_mul, eval₂_mul, map_X, hp, eval₂_X, eval₂_X, comp_apply]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
⊢ (φ * ψ).vars ⊆ φ.vars ∪ ψ.vars

Tactic:
simp_rw [vars_def, ← Multiset.toFinset_add, Multiset.toFinset_subset]

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
φ ψ : MvPolynomial σ R
⊢ (φ * ψ).degrees ⊆ φ.degrees + ψ.degrees
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq σ
f : ι → MvPolynomial σ R
a✝ : ι
s✝ : Finset ι
hs : a✝ ∉ s✝
hsub : (∏ i ∈ s✝, f i).vars ⊆ s✝.biUnion fun i ↦ (f i).vars
⊢ (∏ i ∈ insert a✝ s✝, f i).vars ⊆ (insert a✝ s✝).biUnion fun i ↦ (f i).vars

Tactic:
| insert _ _ hs hsub =>

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
⊢ (∑ i ∈ insert a✝ s✝, φ i).vars ⊆ (φ a✝).vars ∪ s✝.biUnion fun i ↦ (φ i).vars

Tactic:
Finset.sum_insert has

Goal state after:
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
⊢ (φ a✝ + ∑ x ∈ s✝, φ x).vars ⊆ (φ a✝).vars ∪ s✝.biUnion fun i ↦ (φ i).vars
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) = (eval₂Hom (φ.comp (algebraMap R S₁)) fun i ↦ φ (g i)) p

Tactic:
by
  rw [← comp_eval₂Hom]
  rfl

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

Goal state before:
pp: n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
j : Fin (n + 1)
⊢ (cons y 0) j = (single 0 y) j

Tactic:
cases j using Fin.cases <;> simp

Goal state after:
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
⊢ (∑ x ∈ p.support, f (coeff x p) * x.prod fun i k ↦ g i ^ k) = f (constantCoeff p)

Tactic:
rw [Finset.sum_eq_single (0 : σ →₀ ℕ)]
    · rw [Finsupp.prod_zero_index, mul_one]
      rfl
    on_goal 1 => intro d hd hd0

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
⊢ (f (coeff d p) * d.prod fun i k ↦ g i ^ k) = 0

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
⊢ 0 ∉ p.support → (f (coeff 0 p) * Finsupp.prod 0 fun i k ↦ g i ^ k) = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ (p + q).totalDegree ≤ p.totalDegree

Tactic:
rw [← max_eq_left_of_lt h]
      exact totalDegree_add p q

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

Goal state before:
pp: case mul_X.inl
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_2
T : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Type u_4
τ : Type u_5
f : τ → S
g : σ → T
p : MvPolynomial (σ ⊕ τ) R
h : (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) p = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) p)
val✝ : σ
⊢ (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) (p * X (Sum.inl val✝)) =
    (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) (p * X (Sum.inl val✝)))

Tactic:
simp [h]

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

Goal state before:
pp: case mul_X.inr
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_2
T : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Type u_4
τ : Type u_5
f : τ → S
g : σ → T
p : MvPolynomial (σ ⊕ τ) R
h : (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) p = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) p)
val✝ : τ
⊢ (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) (p * X (Sum.inr val✝)) =
    (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) (p * X (Sum.inr val✝)))

Tactic:
simp [h]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : ↑q.vars ⊆ s
inst✝ : (i : σ) → Decidable (i ∈ s)
⊢ (aeval fun i ↦ if i ∈ s then X i else 0) q = q

Tactic:
by
  rw [MvPolynomial.as_sum q, MvPolynomial.aeval_sum]
  refine Finset.sum_congr rfl fun u hu ↦ ?_
  rw [MvPolynomial.aeval_monomial, MvPolynomial.monomial_eq]
  congr 1
  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
inst✝ : Semiring R
p : R[X]
h : p = 0
⊢ p.trailingDegree = ⊤

Tactic:
simp [h]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p ≠ 0
hq : q = 0
⊢ p * q = 0

Tactic:
rw [hq, mul_zero]

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

Goal state before:
pp: case refine_2.inl
R : Type u
inst✝ : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
hn : n < p.natDegree
⊢ p.coeff n = 0

Tactic:
coeff_eq_zero_of_lt_natTrailingDegree (hn.trans_le h)

Goal state after:
case refine_2.inl
R : Type u
inst✝ : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
hn : n < p.natDegree
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.nextCoeff ≠ 0
⊢ f.eraseLead.natDegree + 1 = f.natDegree

Tactic:
rw [natDegree_eraseLead h, tsub_add_cancel_of_le]
  exact natDegree_pos_of_nextCoeff_ne_zero h

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

Goal state before:
pp: R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
⊢ (s.sum f).natDegree = s.sup fun i ↦ (f i).natDegree

Tactic:
by
  by_cases! H : ∃ x ∈ s, f x ≠ 0
  · obtain ⟨x, hx, hx'⟩ := H
    have hs : s.Nonempty := ⟨x, hx⟩
    refine natDegree_eq_of_degree_eq_some ?_
    rw [degree_sum_eq_of_disjoint]
    · rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs,
        Nat.cast_withBot, Finset.coe_sup' hs, ←
        Finset.sup'_eq_sup hs]
      refine le_antisymm ?_ ?_
      · rw [Finset.sup'_le_iff]
        intro b hb
        by_cases hb' : f b = 0
        · simpa [hb'] using! hs
        rw [degree_eq_natDegree hb', Nat.cast_withBot]
        exact Finset.le_sup' (fun i : S => (natDegree (f i) : WithBot ℕ)) hb
      · rw [Finset.sup'_le_iff]
        intro b hb
        simp only [Finset.le_sup'_iff, Function.comp_apply]
        by_cases hb' : f b = 0
        · refine ⟨x, hx, ?_⟩
          contrapose! hx'
          simpa [← Nat.cast_withBot, hb', degree_eq_bot] using! hx'
        exact ⟨b, hb, (degree_eq_natDegree hb').ge⟩
    · exact h.imp fun x y hxy hxy' => hxy (natDegree_eq_of_degree_eq hxy')
  · rw [Finset.sum_eq_zero H, natDegree_zero, eq_comm, show 0 = ⊥ from rfl, Finset.sup_eq_bot_iff]
    intro x hx
    simp [H x hx]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p = 0
⊢ ↑n < p.degree ↔ n < p.natDegree

Tactic:
simp [h]

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

Goal state before:
pp: case inl
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p = 0
⊢ (map f p).degree = p.degree ↔ f p.leadingCoeff ≠ 0 ∨ p = 0

Tactic:
simp [h]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
ha : a ≠ 0
c : R
⊢ (C a * X + C c).nextCoeff = c

Tactic:
by
  rw [nextCoeff_of_natDegree_pos] <;> simp [ha]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Ring R
p : R[X]
a✝ : Nontrivial R
h : p = 0
⊢ (p.comp (-X)).leadingCoeff = (-1) ^ p.natDegree * p.leadingCoeff

Tactic:
simp [h]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p = 0
⊢ p.comp q = 0

Tactic:
simp [h]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : q = 0
⊢ (p * q).degree = (q * p).degree

Tactic:
simp [h]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : q = 0
⊢ (p * q).natDegree = (q * p).natDegree

Tactic:
simp [h]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ k i < f.natDegree

Tactic:
apply lt_natDegree_of_mem_eraseLead_support

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ k i ∈ f.eraseLead.support
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ (Multiset.map (fun x ↦ X - C x) t).prod.coeff (t.card - 1) =
    (Multiset.map (fun x ↦ X - C x) t).prod.coeff ((Multiset.map (fun x ↦ X - C x) t).prod.natDegree - 1)

pp: case hnc
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ¬(Multiset.map (fun x ↦ X - C x) t).prod.natDegree = 0

Tactic:
swap

Goal state after:
case hnc
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ¬(Multiset.map (fun x ↦ X - C x) t).prod.natDegree = 0

R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ (Multiset.map (fun x ↦ X - C x) t).prod.coeff (t.card - 1) =
    (Multiset.map (fun x ↦ X - C x) t).prod.coeff ((Multiset.map (fun x ↦ X - C x) t).prod.natDegree - 1)
Module: Mathlib.Algebra.Polynomial.Monic

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

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

Tactic:
· rintro ⟨a, b, ha, hb, rfl, hdb⟩
      simp only [Nat.Ioc_succ_singleton, zero_add, mem_singleton] at hdb
      have hda := hnd
      rw [ha.natDegree_mul hb, hdb] at hda
      use a.coeff 0, b.coeff 0, mul_coeff_zero a b
      simpa only [nextCoeff, hnd, add_right_cancel hda, hdb] using! ha.nextCoeff_mul hb

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

Goal state before:
pp: case hnc
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ¬(Multiset.map natDegree (Multiset.map (fun x ↦ X - C x) t)).sum = 0

pp: case hnc.h
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ∀ f ∈ Multiset.map (fun x ↦ X - C x) t, f.Monic

Tactic:
swap

Goal state after:
case hnc.h
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ∀ f ∈ Multiset.map (fun x ↦ X - C x) t, f.Monic

case hnc
R : Type u
inst✝ : CommRing R
t : Multiset R
ht : 0 < t.card
a✝ : Nontrivial R
⊢ ¬(Multiset.map natDegree (Multiset.map (fun x ↦ X - C x) t)).sum = 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
⊢ ¬IsUnit (X ^ n - 1)

Tactic:
intro h
  rcases eq_or_ne n 0 with (rfl | hn)
  · simp at h
  apply hn
  rw [← @natDegree_one R, ← (monic_X_pow_sub_C _ hn).eq_one_of_isUnit h, natDegree_X_pow_sub_C]

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

Goal state before:
pp: case mp
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ p * q = 0 → q = 0

Tactic:
intro hp
    rw [← smul_eq_zero_iff_eq h.unit⁻¹] at hp
    have : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q := by
      ext
      simp only [Units.smul_def, coeff_smul, coeff_mul, smul_eq_mul, mul_sum]
      refine sum_congr rfl fun x _ => ?_
      rw [← mul_assoc]
    rwa [this, Monic.mul_right_eq_zero_iff] at hp
    exact monic_of_isUnit_leadingCoeff_inv_smul _

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
⊢ p ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range n))

Tactic:
replace hp := mem_degreeLT.1 hp

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
hp : p.degree < ↑n
⊢ p ∈ Submodule.span R ↑(image (fun n ↦ X ^ n) (range n))
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝ : Semiring R
n : ℕ
f : Fin n → R
⊢ (fun p n_1 ↦ (↑p).coeff ↑n_1) ((fun f ↦ ⟨∑ i, (monomial ↑i) (f i), ⋯⟩) f) = f

Tactic:
by ext i; grind [finsetSum_coeff, Finset.sum_eq_single i, coeff_monomial]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
m n : ℕ
hmn : m ≤ n
⊢ (∑ i ∈ Ico m n, x ^ i) * (1 - x) = x ^ m - x ^ n

Tactic:
by
  rw [sum_Ico_eq_sub _ hmn, sub_mul, geom_sum_mul_neg, geom_sum_mul_neg, sub_sub_sub_cancel_left]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ ¬Module.Finite R R[X]

Tactic:
Module.finite_def,

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ ¬⊤.FG
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ((∑ i ∈ range n, X ^ i).comp (X + 1)).coeff i = ↑(n.choose (i + 1))

pp: R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ↑(n.choose (i + 1)) = (∑ i ∈ range n, ↑(n.choose (i + 1)) * X ^ i).coeff i

Tactic:
swap

Goal state after:
R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ↑(n.choose (i + 1)) = (∑ i ∈ range n, ↑(n.choose (i + 1)) * X ^ i).coeff i

R : Type u
inst✝ : Semiring R
n i : ℕ
⊢ ((∑ i ∈ range n, X ^ i).comp (X + 1)).coeff i = ↑(n.choose (i + 1))
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
l : A →₀ ↥(adjoin R s)
hlq : l ∈ Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q
this✝ :
  ∀ [inst : Semiring ↥(adjoin R s)] [inst_1 : AddCommMonoid A] [inst_2 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)), (Finsupp.linearCombination (↥(adjoin R s)) v) l = l.sum fun i a ↦ a • v i
z : A
hz : z ∈ l.support
this : ∃ l_1 ∈ Finsupp.supported R R p, (Finsupp.linearCombination R _root_.id) l_1 = ↑(l z)
⊢ ↑(l z) * _root_.id z ∈ span R (p * q)

Tactic:
rcases this with ⟨l2, hlp, hl⟩

Goal state after:
case refine_2
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
l : A →₀ ↥(adjoin R s)
hlq : l ∈ Finsupp.supported (↥(adjoin R s)) (↥(adjoin R s)) q
this :
  ∀ [inst : Semiring ↥(adjoin R s)] [inst_1 : AddCommMonoid A] [inst_2 : Module (↥(adjoin R s)) A] {v : A → A}
    (l : A →₀ ↥(adjoin R s)), (Finsupp.linearCombination (↥(adjoin R s)) v) l = l.sum fun i a ↦ a • v i
z : A
hz : z ∈ l.support
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (Finsupp.linearCombination R _root_.id) l2 = ↑(l z)
⊢ ↑(l z) * _root_.id z ∈ span R (p * q)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ⇑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
h : n = 0
⊢ (if n = 0 then x else 0) ∈ I

pp: case neg
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ⇑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
h : ¬n = 0
⊢ (if n = 0 then x else 0) ∈ I

Tactic:
· simpa [h] using hx.left

Goal state after:
case neg
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ⇑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
h : ¬n = 0
⊢ (if n = 0 then x else 0) ∈ I
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case neg
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ⇑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
h : ¬n = 0
⊢ (if n = 0 then x else 0) ∈ I

Tactic:
simp [h]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
x : R
x✝ : ∃ p ∈ I, p.degree ≤ ↑0 ∧ p.leadingCoeff = x
p : R[X]
hpI : p ∈ I
hpdeg : p.degree ≤ ↑0
hpx : p.leadingCoeff = x
⊢ C x ∈ I

Tactic:
by
      rwa [← hpx, Polynomial.leadingCoeff,
        Nat.eq_zero_of_le_zero (natDegree_le_of_degree_le hpdeg), ← eq_C_of_degree_le_zero hpdeg]

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case refine_1.mem
R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝³ : AddCommMonoid M
x✝² : Module R M
x✝¹ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x✝ x : ↥N
hx : x ∈ {n} ∪ Set.range nj
⊢ (↑↥A i) x ∈ M'

Tactic:
change i x ∈ M'

Goal state after:
case refine_1.mem
R : Type u_1
inst✝ : CommRing R
M : Type u_1
x✝³ : AddCommMonoid M
x✝² : Module R M
x✝¹ : Module.Finite R M
N : Submodule R M
f : ↥N →ₗ[R] M
hf : Surjective ⇑f
this✝² : AddCommGroup M := addCommMonoidToAddCommGroup R
this✝¹ : AddCommGroup ↥N := addCommMonoidToAddCommGroup R
i : ↥N →ₗ[R] M := N.subtype
hi : Function.Injective ⇑i := injective_subtype N
n : ↥N
hn : f n = 0
k : ℕ
mj : Fin k → M
hmj : Surjective ⇑((Module.piEquiv (Fin k) R M) mj)
b : Fin k → R
hb : ((Module.piEquiv (Fin k) R M) mj) b = i n
nj : Fin k → ↥N
hnj : ∀ (j : Fin k), f (nj j) = mj j
c : Fin k → Fin k → R
hc : ∀ (j : Fin k), ((Module.piEquiv (Fin k) R M) mj) (c j) = i (nj j)
A : Subring R := Subring.closure (Set.range b ∪ Set.range (Function.uncurry c))
N' : Submodule ↥A ↥N := span (↥A) ({n} ∪ Set.range nj)
M' : Submodule (↥A) M := span (↥A) (Set.range mj)
this✝ : IsNoetherianRing ↥A
this : Module.Finite ↥A ↥M'
x✝ x : ↥N
hx : x ∈ {n} ∪ Set.range nj
⊢ i x ∈ M'