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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
x : R
⊢ eval x p = ∑ i ∈ range n, p.coeff i * x ^ i

Tactic:
by
  rw [eval_eq_sum, p.sum_over_range' _ _ hn]; simp

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

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
s✝ : Finset ι
hf : f.support ⊆ s✝
h : ∀ i ∈ s✝, f i ≤ g i
s : ι
H : s ∈ f.support
⊢ f s ≤ g s

pp: case neg
ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
s✝ : Finset ι
hf : f.support ⊆ s✝
h : ∀ i ∈ s✝, f i ≤ g i
s : ι
H : s ∉ f.support
⊢ f s ≤ g s

Tactic:
· exact h s (hf H)

Goal state after:
case neg
ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
s✝ : Finset ι
hf : f.support ⊆ s✝
h : ∀ i ∈ s✝, f i ≤ g i
s : ι
H : s ∉ f.support
⊢ f s ≤ g s
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case e_a.e_a
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
C : σ →₀ ℕ
hc : C ∈ p.coeff.support
i : σ
hi : i ∈ C.support
⊢ g₁ i = g₂ i

Tactic:
apply h hi

Goal state after:
case e_a.e_a
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
C : σ →₀ ℕ
hc : C ∈ p.coeff.support
i : σ
hi : i ∈ C.support
⊢ coeff C p ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p = 0 ↔ ∀ (d : σ →₀ ℕ), coeff d p = 0

Tactic:
rw [MvPolynomial.ext_iff]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (∀ (m : σ →₀ ℕ), coeff m p = coeff m 0) ↔ ∀ (d : σ →₀ ℕ), coeff d p = 0
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.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
d : σ →₀ ℕ
r : R
⊢ constantCoeff ((monomial d) r) = if d = 0 then r else 0

Tactic:
rw [constantCoeff_eq, coeff_monomial]

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

Goal state before:
pp: case refine_2
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
⊢ {x | ∃ m ∈ M, ∃ i, (monomial i) m = x} ⊆ ↑(coeffsIn σ M)

Tactic:
rintro _ ⟨m, hm, s, n, rfl⟩ i

Goal state after:
case refine_2
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
m : S
hm : m ∈ M
s i : σ →₀ ℕ
⊢ coeff i ((monomial s) m) ∈ M
Module: Mathlib.Algebra.MvPolynomial.Eval

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

Tactic:
Finset.union_subset_iff

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f : MvPolynomial σ R
d : ℕ
h : 0 < d
⊢ degreeOf n f < d ↔ ∀ m ∈ f.support, m n < d

Tactic:
rwa [degreeOf_eq_sup, Finset.sup_lt_iff]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
⊢ degreeOf n 0 = 0

Tactic:
by
  classical simp only [degreeOf_def, degrees_zero, Multiset.count_zero]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
a : R
⊢ (if a = 0 then ⊥ else sum 0 fun x e ↦ e) = 0

Tactic:
sum_zero_index,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
a : R
⊢ (if a = 0 then ⊥ else 0) = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m ↦ (toMultiset m).card) = (toMultiset b).card
hb : b ∉ q.support
hbb : b ∈ (p + q).support
⊢ p.totalDegree ≤ (p + q).totalDegree

Tactic:
rw [totalDegree_eq, hb₂, totalDegree_eq]

Goal state after:
case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m ↦ (toMultiset m).card) = (toMultiset b).card
hb : b ∉ q.support
hbb : b ∈ (p + q).support
⊢ (toMultiset b).card ≤ (p + q).support.sup fun m ↦ (toMultiset m).card
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
⊢ (s.sum f).totalDegree ≤ s.sup fun i ↦ (f i).totalDegree

Tactic:
induction s using Finset.cons_induction with
  | empty => exact zero_le
  | cons a s has hind =>
    rw [Finset.sum_cons, Finset.sup_cons]
    exact (MvPolynomial.totalDegree_add _ _).trans (max_le_max le_rfl hind)

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

Goal state before:
pp: n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + (n' + (o + o')))) (n + o) = n + n' - n + (o + o' - o)

Tactic:
add_left_comm n' o,

Goal state after:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + (o + (n' + o')))) (n + o) = n + n' - n + (o + o' - o)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case hX
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ✝ →₀ ℕ
inst✝¹ : CommSemiring R
σ : Type u_2
inst✝ : Unique σ
f : R[X] →+* MvPolynomial σ R := ⋯
g : MvPolynomial σ R →+* R[X] := ⋯
⊢ ∀ (n : σ), (f.comp g) (X n) = X n

Tactic:
intro i
      dsimp [f, g]
      rw [eval₂_X, Polynomial.eval₂_X]
      rw [← Unique.eq_default i]

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : ¬q.natDegree = 0
p0 : p = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

pp: case neg
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : ¬q.natDegree = 0
p0 : ¬p = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
· simp only [p0, zero_comp, natDegree_zero, zero_mul]

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : ¬q.natDegree = 0
p0 : ¬p = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg.inr
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
⊢ ((X - C x) * P).eraseLead.eraseLead.coeff n = ((X - C x) * P.eraseLead).coeff n

Tactic:
trans 0 <;> rw [coeff_eq_zero_of_natDegree_lt]
    · grw [eraseLead_natDegree_le, eraseLead_natDegree_le]
      simpa [h₁, hdP] using! hn
    · grw [natDegree_mul (X_sub_C_ne_zero x) he, natDegree_eraseLead_le_of_nextCoeff_eq_zero h]
      simpa [add_comm, hdP] using! hn

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : b * p.leadingCoeff = 1
a✝ : Nontrivial R
⊢ (C b * p).leadingCoeff = 1

Tactic:
leadingCoeff_mul' _

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : b * p.leadingCoeff = 1
a✝ : Nontrivial R
⊢ (C b).leadingCoeff * p.leadingCoeff = 1

R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : b * p.leadingCoeff = 1
a✝ : Nontrivial R
⊢ (C b).leadingCoeff * p.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : p.leadingCoeff * b = 1
a✝ : Nontrivial R
⊢ (p * C b).leadingCoeff = 1

Tactic:
leadingCoeff_mul' _

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : p.leadingCoeff * b = 1
a✝ : Nontrivial R
⊢ p.leadingCoeff * (C b).leadingCoeff = 1

R : Type u
inst✝ : Semiring R
p : R[X]
b : R
hp : p.leadingCoeff * b = 1
a✝ : Nontrivial R
⊢ p.leadingCoeff * (C b).leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
r : R
a✝ : Nontrivial R
ha : 1 = 0
⊢ False

Tactic:
exact one_ne_zero ha

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

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

Tactic:
by
  by_cases h : q = 0
  · simp [h]
  rw [hp.natDegree_mul' h, Polynomial.natDegree_mul', add_comm]
  simpa [hp.leadingCoeff, leadingCoeff_ne_zero]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
⊢ (finprod f).Monic

Tactic:
finprod_def

Goal state after:
R : Type u
inst✝ : CommSemiring R
α : Type u_1
f : α → R[X]
hf : ∀ i ∈ Function.mulSupport f, (f i).Monic
⊢ (if h : Function.HasFiniteMulSupport f then ∏ i ∈ Set.Finite.toFinset h, f i else 1).Monic
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
h : ∀ f ∈ t, f.Monic
⊢ t.prod.natDegree = (Multiset.map natDegree t).sum

Tactic:
by
  nontriviality R
  apply natDegree_multiset_prod'
  simp_all

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : AddLeftReflectLE R
inst✝³ : AddLeftMono R
inst✝² : ExistsAddOfLE R
inst✝¹ : Sub R
inst✝ : OrderedSub R
x : R
hx : 1 ≤ x
n : ℕ
⊢ (∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1

Tactic:
by simpa using geom_sum₂_mul_of_ge hx n

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
⊢ ¬Irreducible p ↔ ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂

Tactic:
by
  cases subsingleton_or_nontrivial R
  · simp [natDegree_of_subsingleton] at hnd
  rw [hm.irreducible_iff_natDegree', and_iff_right, hnd]
  · push Not
    constructor
    · 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
    · rintro ⟨c₁, c₂, hmul, hadd⟩
      refine
        ⟨X + C c₁, X + C c₂, monic_X_add_C _, monic_X_add_C _, ?_, ?_⟩
      · rw [p.as_sum_range_C_mul_X_pow, hnd, Finset.sum_range_succ, Finset.sum_range_succ,
          Finset.sum_range_one, ← hnd, hm.coeff_natDegree, hnd, hmul, hadd, C_mul, C_add, C_1]
        ring
      · simp
  · rintro rfl
    simp [natDegree_one] at hnd

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

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

Tactic:
hp.degree_mul,

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬q.degree + p.degree = ⊥
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Semiring R
k : ℕ
x : R
hx : x ≠ 0
⊢ #(C x * X ^ k).support = 1

Tactic:
support_C_mul_X_pow k hx,

Goal state after:
case refine_2
R : Type u_1
inst✝ : Semiring R
k : ℕ
x : R
hx : x ≠ 0
⊢ #{k} = 1
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
k : Fin 2 → ℕ
x : Fin 2 → R
hk : StrictMono k
hx : ∀ (i : Fin 2), x i ≠ 0
h : #(∑ i, C (x i) * X ^ k i).support = 2
⊢ ∑ i, C (x i) * X ^ k i = C (x 0) * X ^ k 0 + C (x 1) * X ^ k 1

Tactic:
rw [Fin.sum_univ_castSucc, Fin.sum_univ_one]

Goal state after:
case refine_1
R : Type u_1
inst✝ : Semiring R
k : Fin 2 → ℕ
x : Fin 2 → R
hk : StrictMono k
hx : ∀ (i : Fin 2), x i ≠ 0
h : #(∑ i, C (x i) * X ^ k i).support = 2
⊢ C (x (Fin.castSucc 0)) * X ^ k (Fin.castSucc 0) + C (x (Fin.last 1)) * X ^ k (Fin.last 1) =
    C (x 0) * X ^ k 0 + C (x 1) * X ^ k 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
⊢ ∑ a ∈ l.support, l a • _root_.id a ∈ span R (p * q)

Tactic:
refine sum_mem ?_

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
⊢ ∀ c ∈ l.support, l c • _root_.id c ∈ span R (p * q)
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
l2 : A →₀ R
hlp : l2 ∈ Finsupp.supported R R p
hl : (l2.sum fun i a ↦ a • _root_.id i) = ↑(l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    (Finsupp.linearCombination R v) l = l.sum fun i a ↦ a • v i
⊢ (l2.sum fun a c ↦ c • _root_.id a * _root_.id z) ∈ span R (p * q)

Tactic:
refine sum_mem ?_

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 : (l2.sum fun i a ↦ a • _root_.id i) = ↑(l z)
this :
  ∀ [inst : Semiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A] {v : A → A} (l : A →₀ R),
    (Finsupp.linearCombination R v) l = l.sum fun i a ↦ a • v i
⊢ ∀ c ∈ l2.support, (fun a c ↦ c • _root_.id a * _root_.id z) c (l2 c) ∈ span R (p * q)
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
a✝ : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
⊢ ⊥ < (P ^ n).degree

Tactic:
bot_lt_iff_ne_bot,

Goal state after:
R : Type u
inst✝ : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
a✝ : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
⊢ (P ^ n).degree ≠ ⊥
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
x✝ : (toSubmodule S).FG
t : Finset A
ht : span R ↑t = toSubmodule S
x : A
hx : x ∈ toSubmodule S
⊢ x ∈ toSubmodule S

Tactic:
exact hx

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

Goal state before:
pp: case insert
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
i j : ℕ
e : (i, j) ∈ antidiagonal (i + j)
⊢ (f a).coeff (i, j).1 * (∏ x ∈ s, f x).coeff (i, j).2 ∈ I ^ (n a + ∑ x ∈ s, n x - (i + j))

Tactic:
apply Ideal.pow_le_pow_right add_tsub_add_le_tsub_add_tsub

Goal state after:
case insert
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
i j : ℕ
e : (i, j) ∈ antidiagonal (i + j)
⊢ (f a).coeff (i, j).1 * (∏ x ∈ s, f x).coeff (i, j).2 ∈ I ^ (n a - i + (∑ x ∈ s, n x - j))
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mpr
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ (∃ s f, Surjective ⇑f) → FiniteType R A

Tactic:
rintro ⟨s, f, hsur⟩
    exact .of_surjective f hsur

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: case mpr
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (∃ s f, Surjective ⇑f) → FiniteType R S

Tactic:
rintro ⟨s, f, hsur⟩
    exact .of_surjective f hsur

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
⊢ of' R M '' ⋃ f ∈ S, ↑f.coeff.support = ⋃ f ∈ S, of' R M '' ↑f.coeff.support

Tactic:
simp only [Set.image_iUnion]

Goal state after:
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Monoid M
S : Set R[M]
hS : adjoin R S = ⊤
⊢ ⇑(of R M) '' ⋃ f ∈ S, ↑f.coeff.support = ⋃ f ∈ S, ⇑(of R M) '' ↑f.coeff.support

Tactic:
simp only [Set.image_iUnion]

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

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) p).ker ⊔ ((aeval f) q).ker
x : M
hx : x ∈ ((aeval f) p).ker
y : M
hy : y ∈ ((aeval f) q).ker
hxy : x + y = v
h_eval_x : ((aeval f) (p * q)) x = 0
h_eval_y : ((aeval f) (p * q)) y = 0
⊢ ((aeval f) (p * q)) v = 0

Tactic:
← hxy,

Goal state after:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ ((aeval f) p).ker ⊔ ((aeval f) q).ker
x : M
hx : x ∈ ((aeval f) p).ker
y : M
hy : y ∈ ((aeval f) q).ker
hxy : x + y = v
h_eval_x : ((aeval f) (p * q)) x = 0
h_eval_y : ((aeval f) (p * q)) y = 0
⊢ ((aeval f) (p * q)) (x + y) = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
⊢ ((aeval f) p).ker ⊔ ((aeval f) q).ker = ((aeval f) (p * q)).ker

Tactic:
by
  apply le_antisymm sup_ker_aeval_le_ker_aeval_mul
  intro v hv
  rw [Submodule.mem_sup]
  rcases hpq with ⟨p', q', hpq'⟩
  have h_eval₂_qpp' :=
    calc
      aeval f (q * (p * p')) v = aeval f (p' * (p * q)) v := by
        rw [mul_comm, mul_assoc, mul_comm, mul_assoc, mul_comm q p]
      _ = 0 := by rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hv, map_zero]
  have h_eval₂_pqq' :=
    calc
      aeval f (p * (q * q')) v = aeval f (q' * (p * q)) v := by rw [← mul_assoc, mul_comm]
      _ = 0 := by rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hv, map_zero]
  rw [aeval_mul] at h_eval₂_qpp' h_eval₂_pqq'
  refine
    ⟨aeval f (q * q') v, LinearMap.mem_ker.1 h_eval₂_pqq', aeval f (p * p') v,
      LinearMap.mem_ker.1 h_eval₂_qpp', ?_⟩
  rw [add_comm, mul_comm p p', mul_comm q q']
  simpa only [map_add, map_mul, aeval_one] using! congr_arg (fun p : R[X] => aeval f p v) hpq'

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

Goal state before:
pp: σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.coeff.support
⊢ ∑ i ∈ d.support, d i ≤ F.totalDegree

Tactic:
MvPolynomial.totalDegree

Goal state after:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.coeff.support
⊢ ∑ i ∈ d.support, d i ≤ F.support.sup fun s ↦ s.sum fun x e ↦ e
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
⊢ ∀ m ∈ p.support, (monomial m) (coeff m p) ∈ I

Tactic:
intro m _

Goal state after:
R : Type u
σ : Type v
inst✝ : CommRing R
I : Ideal (MvPolynomial σ R)
p : MvPolynomial σ R
hcoe : ∀ (m : σ →₀ ℕ), coeff m p ∈ Ideal.comap C I
m : σ →₀ ℕ
a✝ : m ∈ p.support
⊢ (monomial m) (coeff m p) ∈ I