mathlib-initiative/mathlib-tactics huggingface dataset:
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₁
f : σ → S₁
⊢ (aeval f).range = Algebra.adjoin R (range f)

Tactic:
apply le_antisymm
  · rintro x ⟨p, rfl⟩
    simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe]
    induction p using induction_on with
    | C a => exact aeval_C f a ▸ Subsemiring.subset_closure (Or.inl (Set.mem_range_self a))
    | add p q hp hq => rw [map_add]; exact Subalgebra.add_mem _ hp hq
    | mul_X p n h =>
      simp only [map_mul, aeval_X]
      exact Subalgebra.mul_mem _ h (Algebra.subset_adjoin (Set.mem_range_self n))
  · rw [Algebra.adjoin_le_iff]
    rintro x ⟨i, rfl⟩
    use X i, by aesop

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

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
hp : ∀ i ∈ p.vars, g i = 0
h0 : 0 ∉ p.coeff.support
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ d.support ≠ ∅

Tactic:
Ne,

Goal state after:
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 : 0 ∉ p.coeff.support
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ ¬d.support = ∅
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case pos.a
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
⊢ i ∈ p.vars

Tactic:
rw [mem_vars_iff_mem_support]

Goal state after:
case pos.a
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
⊢ ∃ d ∈ p.support, i ∈ d.support
Module: Mathlib.Algebra.MvPolynomial.Variables

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
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬0 ∉ p.coeff.support
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
⊢ d.support ≠ ∅

Tactic:
Ne,

Goal state after:
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 : ¬0 ∉ p.coeff.support
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
⊢ ¬d.support = ∅
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case neg.h₀.a
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
⊢ i ∈ p.vars

Tactic:
rw [mem_vars_iff_mem_support]

Goal state after:
case neg.h₀.a
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
⊢ ∃ d ∈ p.support, i ∈ d.support
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
h : f.totalDegree < ∑ i ∈ d.support, d i
⊢ coeff d f = 0

Tactic:
rw [totalDegree, Finset.sup_lt_iff] at h
  · specialize h d
    rw [mem_support_iff] at h
    refine not_not.mp (mt h ?_)
    exact lt_irrefl _
  · exact lt_of_le_of_lt (Nat.zero_le _) h

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

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

Tactic:
simp only [Finsupp.prod]

Goal state after:
case e_a
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
⊢ ∏ x ∈ d.support, g₁ x ^ d x = ∏ x ∈ d.support, g₂ x ^ d x
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
⊢ coeff m p = coeff m (C (coeff 0 p))

Tactic:
classical rw [coeff_C]; split_ifs with hm; · rw [← hm]

Goal state after:
case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
hm : ¬0 = m
⊢ coeff m p = 0
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
i : σ
hi : i ∈ d.support
⊢ i ∈ p₁.vars

Tactic:
rw [mem_vars_iff_mem_support]

Goal state after:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
i : σ
hi : i ∈ d.support
⊢ ∃ d ∈ p₁.support, i ∈ d.support
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
⊢ (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree

Tactic:
have hp : p ≠ 0 := fun hp => h (by rw [hp, trailingCoeff_zero, zero_mul])
  have hq : q ≠ 0 := fun hq => h (by rw [hq, trailingCoeff_zero, mul_zero])
  apply natTrailingDegree_eq_of_trailingDegree_eq_some
  rw [trailingDegree_mul' h, ENat.natCast_add, ← trailingDegree_eq_natTrailingDegree hp,
    ← trailingDegree_eq_natTrailingDegree hq]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
f0 : 2 ≤ #f.support
⊢ f.eraseLead ≠ 0

Tactic:
Ne,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
f0 : 2 ≤ #f.support
⊢ ¬f.eraseLead = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case succ.zero
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
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = 0 → motive f
hf : #f.support = 0 + 1
⊢ f ≠ 0

Tactic:
Ne,

Goal state after:
case succ.zero
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
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = 0 → motive f
hf : #f.support = 0 + 1
⊢ ¬f = 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
hp : p ≠ 0
⊢ p.comp q ≠ 0

Tactic:
Ne,

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hq : 0 < q.degree
hp : p ≠ 0
⊢ ¬p.comp q = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
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
⊢ f.leadingCoeff ≠ 0

Tactic:
Ne,

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
⊢ ¬f.leadingCoeff = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
p : MvPolynomial (Option S₁) R
i : ℕ
hi : i ≤ p.totalDegree
⊢ (((optionEquivLeft R S₁) p).coeff i).totalDegree + i ≤ p.totalDegree

Tactic:
by
  classical
  by_cases hpi : (optionEquivLeft R S₁ p).coeff i = 0
  · rw [hpi]; simpa
  rw [totalDegree, add_comm, Finset.add_sup (by simpa only [support_nonempty]), Finset.sup_le_iff]
  intro σ hσ
  refine le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)
  · simp [Finsupp.sum_add_index, Finsupp.sum_embDomain, add_comm i]
  · simpa [mem_support_iff, ← optionEquivLeft_coeff_some_coeff_none R S₁] using hσ

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

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

Tactic:
nontriviality R
  apply natDegree_mul'
  simp [hp.leadingCoeff, hq.leadingCoeff]

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]
h : ¬q = 0
⊢ (p * q).degree = (q * p).degree

Tactic:
degree_mul',

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.degree + q.degree = (q * p).degree

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

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

Goal state before:
pp: case some.pn
ι : Type w
S : Type u_1
inst✝ : Semiring S
f : ι → S[X]
s : Finset ι
hf : ∑ k ∈ s, (f k).leadingCoeff ≠ 0
d : ℕ
hd : ∀ k ∈ s, (f k).natDegree = d
⊢ (∑ k ∈ s, f k).natDegree ≤ d

pp: case some.p1
ι : Type w
S : Type u_1
inst✝ : Semiring S
f : ι → S[X]
s : Finset ι
hf : ∑ k ∈ s, (f k).leadingCoeff ≠ 0
d : ℕ
hd : ∀ k ∈ s, (f k).natDegree = d
⊢ (∑ k ∈ s, f k).coeff d ≠ 0

Tactic:
· aesop (add safe natDegree_sum_le_of_forall_le)

Goal state after:
case some.p1
ι : Type w
S : Type u_1
inst✝ : Semiring S
f : ι → S[X]
s : Finset ι
hf : ∑ k ∈ s, (f k).leadingCoeff ≠ 0
d : ℕ
hd : ∀ k ∈ s, (f k).natDegree = d
⊢ (∑ k ∈ s, f k).coeff d ≠ 0
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
hhd : hd.degree ≤ n
htl : ∀ a ∈ tl, a.degree ≤ n
⊢ (hd + tl.sum).degree ≤ n

Tactic:
exact le_trans (degree_add_le hd tl.sum) (max_le hhd (ih htl))

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ Finset.image (cons i) (((finSuccEquiv R n) f).coeff i).support = {m ∈ f.support | m 0 = i}

Tactic:
by
  ext m
  rw [Finset.mem_filter, Finset.mem_image, mem_support_iff]
  conv_lhs =>
    congr
    ext
    rw [mem_support_iff, finSuccEquiv_coeff_coeff, Ne]
  constructor
  · grind [cons_zero]
  · intro h
    use tail m
    rw [← h.2, cons_tail]
    simp [h.1]

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]
h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0
⊢ (∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff

Tactic:
simpa using leadingCoeff_multiset_prod' (s.1.map f) (by simpa using h)

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

Goal state before:
pp: case succ.refine_1
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
⊢ StrictMono (Function.extend Fin.castSucc k fun x ↦ f.natDegree)

Tactic:
intro i j hij

Goal state after:
case succ.refine_1
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
i j : Fin (n + 1)
hij : i < j
⊢ Function.extend Fin.castSucc k (fun x ↦ f.natDegree) i < Function.extend Fin.castSucc k (fun x ↦ f.natDegree) j
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

Tactic:
· rintro rfl
    simp [natDegree_one] at hnd

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

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]
hq : q ≠ 0
⊢ q * p ≠ 0

Tactic:
by_cases h : p = 1

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : p = 1
⊢ q * p ≠ 0

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 ≠ 0
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 ≠ 0

Tactic:
Ne,

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 * p = 0
Module: Mathlib.Algebra.Polynomial.Monic

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

Tactic:
by_cases h : p = 1

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : p = 1
⊢ p * q ≠ 0

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ p * q ≠ 0
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
⊢ p * q ≠ 0

Tactic:
Ne,

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
⊢ ¬p * q = 0
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
i : Fin (n + 1)
hi : ¬∃ i₀, i₀.castSucc = i
⊢ f.leadingCoeff ≠ 0

Tactic:
Ne,

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
i : Fin (n + 1)
hi : ¬∃ i₀, i₀.castSucc = i
⊢ ¬f.leadingCoeff = 0
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case h
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
h : 0 ∉ t
a✝ : Nontrivial R
⊢ (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0

Tactic:
Ne,

Goal state after:
case h
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
t : Multiset R[X]
h : 0 ∉ t
a✝ : Nontrivial R
⊢ ¬(Multiset.map (fun f ↦ f.leadingCoeff) t).prod = 0
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
n : ℕ
hn : n ≠ 0
a✝ : Nontrivial R
⊢ (∑ i ∈ range n, P ^ i).Monic

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn

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
⊢ (∑ i ∈ range n.succ, P ^ i).Monic
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:
Ne,

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.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝ : Semiring R
I : Ideal R[X]
c : R
x : R[X]
H : x ∈ I.carrier
⊢ c • x ∈ I.carrier

Tactic:
← C_mul'

Goal state after:
R : Type u
S : Type u_1
inst✝ : Semiring R
I : Ideal R[X]
c : R
x : R[X]
H : x ∈ I.carrier
⊢ C c * x ∈ I.carrier
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ⇑f
hs✝ : (map f S).FG
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ Algebra.adjoin R (⇑f '' ↑(s.preimage ⇑f ⋯)) = map f S

Tactic:
Finset.coe_preimage,

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
f : A →ₐ[R] B
hf : Function.Injective ⇑f
hs✝ : (map f S).FG
s : Finset B
hs : Algebra.adjoin R ↑s = map f S
⊢ Algebra.adjoin R (⇑f '' ⇑f ⁻¹' ↑s) = map f S
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 S' : Subalgebra R A
hS : S.FG
hS' : S'.FG
s : Set A
hs : s.Finite ∧ Algebra.adjoin R s = S
s' : Set A
hs' : s'.Finite ∧ Algebra.adjoin R s' = S'
⊢ Algebra.adjoin R (s ∪ s') = S ⊔ S'

Tactic:
rw [Algebra.adjoin_union, hs.2, hs'.2]

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
h✝ : ∀ (x : C), Function.support (f x) ⊆ ↑y
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
⊢ ∃ B₀, B₀.FG ∧ ⊤.FG

Tactic:
let s : Finset B := Finset.image₂ f (x ∪ y * y) y
  have hxy :
    ∀ xi ∈ x, xi ∈ span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) :=
    fun xi hxi =>
    hf xi ▸
      sum_mem fun yj hyj =>
        smul_mem (span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C))
          ⟨f xi yj, Algebra.subset_adjoin <| mem_image₂_of_mem (mem_union_left _ hxi) hyj⟩
          (subset_span <| mem_insert_of_mem hyj)
  have hyy :
    span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) *
        span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) ≤
      span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) := by
    rw [span_mul_span, span_le, coe_insert]
    rintro _ ⟨yi, rfl | hyi, yj, rfl | hyj, rfl⟩ <;> dsimp
    · rw [mul_one]
      exact subset_span (Set.mem_insert _ _)
    · rw [one_mul]
      exact subset_span (Set.mem_insert_of_mem _ hyj)
    · rw [mul_one]
      exact subset_span (Set.mem_insert_of_mem _ hyi)
    · rw [← hf (yi * yj)]
      exact
        SetLike.mem_coe.2
          (sum_mem fun yk hyk =>
            smul_mem (span (Algebra.adjoin A (↑s : Set B)) (insert 1 ↑y : Set C))
              ⟨f (yi * yj) yk,
                Algebra.subset_adjoin <|
                  mem_image₂_of_mem (mem_union_right _ <| mul_mem_mul hyi hyj) hyk⟩
              (subset_span <| Set.mem_insert_of_mem _ hyk : yk ∈ _))
  refine ⟨Algebra.adjoin A (↑s : Set B), Subalgebra.fg_adjoin_finset _, insert 1 y, ?_⟩
  convert! restrictScalars_injective A (Algebra.adjoin A (s : Set B)) C _
  rw [restrictScalars_top, eq_top_iff, ← Algebra.top_toSubmodule, ← hx, Algebra.adjoin_eq_span,
    span_le]
  refine fun r hr =>
    Submonoid.closure_induction (fun c hc => hxy c hc) (subset_span <| mem_insert_self _ _)
      (fun p q _ _ hp hq => hyy <| Submodule.mul_mem_mul hp hq) hr

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

Goal state before:
pp: case mpr.ne_top'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ map C P ≠ ⊤

Tactic:
Ne,

Goal state after:
case mpr.ne_top'
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ ¬map C P = ⊤
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case e'_2
R : Type u
σ : Type v
r : R
inst✝¹ : CommRing R
inst✝ : Finite σ
this : Fintype σ
d : ℕ
hd : Prime (C r) ↔ Prime r
⊢ Prime r ↔ Prime (Polynomial.C (C r))

Tactic:
simp [← hd, Polynomial.prime_C_iff]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h✝ : N < k
hp0 : p ≠ 0
h : 0 = 1
i : ℕ
⊢ p.coeff i * 1 = coeff 0 i

Tactic:
rw [← h, mul_zero]

Goal state after:
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h✝ : N < k
hp0 : p ≠ 0
h : 0 = 1
i : ℕ
⊢ 0 = coeff 0 i
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
f : R[M]
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ (of R M) ↑s) a = f

Tactic:
induction f using induction_on with
  | of m =>
    have : m ∈ closure S := hS.symm ▸ mem_top _
    refine Submonoid.closure_induction (fun m hm => ?_) ?_ ?_ this
    · exact ⟨MvPolynomial.X ⟨m, hm⟩, MvPolynomial.aeval_X _ _⟩
    · exact ⟨1, map_one _⟩
    · rintro m₁ m₂ _ _ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
      exact
        ⟨P₁ * P₂, by
          rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]⟩
  | add f g ihf ihg =>
    rcases ihf with ⟨P, rfl⟩; rcases ihg with ⟨Q, rfl⟩
    exact ⟨P + Q, map_add _ _ _⟩
  | smul r f ih =>
    rcases ih with ⟨P, rfl⟩
    exact ⟨r • P, map_smul _ _ _⟩

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 * n ≤ m * n

Tactic:
← Finset.sum_mul

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) * n ≤ m * n