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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
f : R →+* S
n : ℕ
inst✝ : n.AtLeastTwo
⊢ eval₂ f (OfNat.ofNat n) p = f (eval (OfNat.ofNat n) p)

Tactic:
by
  simp [OfNat.ofNat]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
x : R
h : p.IsRoot x
hpq : p ∣ q
⊢ q.IsRoot x

Tactic:
IsRoot,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
x : R
h : p.IsRoot x
hpq : p ∣ q
⊢ eval x q = 0
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
⊢ ∀ (a : R), ((C a).comp ψ).comp χ = (C a).comp (ψ.comp χ)

Tactic:
intros
      simp_all only [add_comp, mul_comp, C_comp, X_comp, pow_succ, ← mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
⊢ ∀ (p q : R[X]),
    (p.comp ψ).comp χ = p.comp (ψ.comp χ) →
      (q.comp ψ).comp χ = q.comp (ψ.comp χ) → ((p + q).comp ψ).comp χ = (p + q).comp (ψ.comp χ)

Tactic:
intros
      simp_all only [add_comp, mul_comp, C_comp, X_comp, pow_succ, ← mul_assoc]

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

Goal state before:
pp: case add
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
x : S
p q r s : R[X]
hr : eval₂ (algebraMap R S) x (r.comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) r
hs : eval₂ (algebraMap R S) x (s.comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) s
⊢ eval₂ (algebraMap R S) x ((r + s).comp q) = eval₂ (algebraMap R S) (eval₂ (algebraMap R S) x q) (r + s)

Tactic:
simp only [add_comp, eval₂_add, hr, hs]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: case refine_3
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
⊢ ∀ (n : ℕ) (a : R),
    ((C a * X ^ n).comp ψ).comp χ = (C a * X ^ n).comp (ψ.comp χ) →
      ((C a * X ^ (n + 1)).comp ψ).comp χ = (C a * X ^ (n + 1)).comp (ψ.comp χ)

Tactic:
intros
      simp_all only [add_comp, mul_comp, C_comp, X_comp, pow_succ, ← mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
⊢ (p.comp q).IsRoot r ↔ p.IsRoot (eval r q)

Tactic:
IsRoot,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
⊢ eval r (p.comp q) = 0 ↔ eval (eval r q) p = 0
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
a : R
inst✝ : CommSemiring R
p q : R[X]
H : q.IsRoot a
⊢ (p * q).IsRoot a

Tactic:
IsRoot,

Goal state after:
R : Type u
a : R
inst✝ : CommSemiring R
p q : R[X]
H : q.IsRoot a
⊢ eval a (p * q) = 0
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
a : R
inst✝ : CommSemiring R
p q : R[X]
H : p.IsRoot a
⊢ (p * q).IsRoot a

Tactic:
IsRoot,

Goal state after:
R : Type u
a : R
inst✝ : CommSemiring R
p q : R[X]
H : p.IsRoot a
⊢ eval a (p * q) = 0
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
a : R
inst✝¹ : CommSemiring R
p q : R[X]
inst✝ : NoZeroDivisors R
⊢ (p * q).IsRoot a ↔ p.IsRoot a ∨ q.IsRoot a

Tactic:
IsRoot,

Goal state after:
R : Type u
a : R
inst✝¹ : CommSemiring R
p q : R[X]
inst✝ : NoZeroDivisors R
⊢ eval a (p * q) = 0 ↔ eval a p = 0 ∨ eval a q = 0
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
y : ↥f.domain
hx : ↑y = x.1 ∧ ↑f y = x.2
⊢ ↑y = ↑⟨x.1, ⋯⟩

Tactic:
simp only [hx.1]

Goal state after:
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: α : Type u
β : Type v
δ : Type x
inst✝ : Preorder β
f : α → β
s : Set α
a : α
t : Set δ
g : δ → α
b : δ
hf : IsMinOn f s a
hg : MapsTo g t s
ha : g b = a
y : δ
hy : y ∈ t
⊢ y ∈ {x | (fun x ↦ (f ∘ g) b ≤ (f ∘ g) x) x}

Tactic:
simpa only [ha, (· ∘ ·)] using! hf (hg hy)

Goal state after:
Module: Mathlib.Order.Filter.Extr

Goal state before:
pp: case neg
α : Type u
β : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
f : α → β
h₀ : MonotoneOn f (Iic b)
h₁ : AntitoneOn f (Ico b a)
x : α
hx : x ∈ Iio a
g₀ : b < x
⊢ x ∈ {x | (fun x ↦ f x ≤ f b) x}

Tactic:
· exact h₁ (left_mem_Ico.2 (g₀.trans hx)) ⟨g₀.le, hx⟩ g₀.le

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : SemilatticeSup B
inst✝¹ : OrderBot B
inst✝ : Semiring R
degb : A → B
f g : R[A]
⊢ (f + g).coeff.support.sup degb ≤ f.coeff.support.sup degb ⊔ g.coeff.support.sup degb

Tactic:
by
  classical
  exact (Finset.sup_mono Finsupp.support_add).trans_eq Finset.sup_union

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

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

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
hp : ¬p = 0
⊢ p.degree < ↑n

Tactic:
· subst hp
    exact WithBot.bot_lt_coe n

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
hp : ¬p = 0
⊢ p.degree < ↑n
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hpq : p.degree ≤ q.degree
hp : p ≠ 0
⊢ ¬p.degree = ⊥

Tactic:
Polynomial.degree_eq_bot

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hpq : p.degree ≤ q.degree
hp : p ≠ 0
⊢ ¬p = 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s : Finset ι
f : ι → R[A]
⊢ supDegree D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i)

Tactic:
by
  classical
  refine s.induction ?_ ?_
  · rw [Finset.prod_empty, Finset.sum_empty, one_def, supDegree_single]
    split_ifs; exacts [bot_le, hzero.le]
  · intro i s his ih
    rw [Finset.prod_insert his, Finset.sum_insert his]
    exact (supDegree_mul_le hadd).trans (by gcongr)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
ι : Type u_1
s✝ : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : (∑ i ∈ s, f i).degree ≤ s.sup fun b ↦ (f b).degree
⊢ max (f a).degree (∑ i ∈ s, f i).degree ≤ max (f a).degree (s.sup fun b ↦ (f b).degree)

Tactic:
exact max_le_max le_rfl ih

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

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : p.natDegree < i
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
coeff_eq_zero_of_degree_lt
              (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 H)),

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : p.natDegree < i
⊢ 0 * q.coeff (i, j).2 = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff = q.leadingCoeff

pp: case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
hp.leadingCoeff,

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

case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
hp.leadingCoeff,

Goal state after:
case inr
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
⊢ 1 * q.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
H : p.leadingCoeff ≠ 0
⊢ (p * q).leadingCoeff = p.leadingCoeff

Tactic:
rw [leadingCoeff_mul', hq.leadingCoeff, mul_one]
      rwa [hq.leadingCoeff, mul_one]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case pos
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j : ι
hj : j ∈ s
hne✝ : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
h : ∀ k ∈ s, k = i
k : ι
hk : k ∈ s
hne : i ≠ j
⊢ f k = 0

Tactic:
h j hj

Goal state after:
case pos
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j : ι
hj : j ∈ s
hne✝ : f j ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
h : ∀ k ∈ s, k = i
k : ι
hk : k ∈ s
hne : i ≠ i
⊢ f k = 0
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
⊢ eval (↑n) (map f p) = f (eval (↑n) p)

Tactic:
by
  induction p using Polynomial.induction_on' with
  | add p q hp hq => simp only [hp, hq, Polynomial.map_add, map_add, eval_add]
  | monomial n r => simp only [map_natCast f, eval_monomial, map_monomial, f.map_pow, f.map_mul]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
x : R
p : R[X]
h : p.IsRoot x
⊢ (Polynomial.map f p).IsRoot (f x)

Tactic:
IsRoot,

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
x : R
p : R[X]
h : p.IsRoot x
⊢ eval (f x) (Polynomial.map f p) = 0
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: S : Type v
inst✝¹ : CommSemiring S
R : Type u_1
inst✝ : Ring R
f : R →+* S
x : R
p : R[X]
h : (Polynomial.map f p).IsRoot (f x)
hf : Function.Injective ⇑f
⊢ p.IsRoot x

Tactic:
IsRoot,

Goal state after:
S : Type v
inst✝¹ : CommSemiring S
R : Type u_1
inst✝ : Ring R
f : R →+* S
x : R
p : R[X]
h : (Polynomial.map f p).IsRoot (f x)
hf : Function.Injective ⇑f
⊢ eval x p = 0
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
⊢ toLex x < toLex (update x i a) → x i < a

Tactic:
rintro ⟨j, hj, h⟩

Goal state after:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
j : ι
hj : ∀ (j_1 : ι), (fun x1 x2 ↦ x1 < x2) j_1 j → toLex x j_1 = toLex (update x i a) j_1
h : toLex x j < toLex (update x i a) j
⊢ x i < a
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
⊢ toLex (update x i a) < toLex x → a < x i

Tactic:
rintro ⟨j, hj, h⟩

Goal state after:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
x : (i : ι) → β i
i : ι
a : β i
inst✝¹ : (i : ι) → PartialOrder (β i)
inst✝ : WellFoundedLT ι
j : ι
hj : ∀ (j_1 : ι), (fun x1 x2 ↦ x1 < x2) j_1 j → toLex (update x i a) j_1 = toLex x j_1
h : toLex (update x i a) j < toLex x j
⊢ a < x i
Module: Mathlib.Order.PiLex

Goal state before:
pp: case refine_1
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
j : ι
hj : (fun x1 x2 ↦ x1 < x2) j i
⊢ a₁✝ j = Function.update a₂ i a j

Tactic:
h j hj

Goal state after:
case refine_1
ι : Type u_1
β : ι → Type u_2
r : ι → ι → Prop
s : {i : ι} → β i → β i → Prop
inst✝² : Preorder ι
inst✝¹ : (i : ι) → LT (β i)
inst✝ : ∀ (i : ι), DenselyOrdered (β i)
a₁✝ a₂ : Lex ((i : ι) → β i)
i : ι
h : ∀ (j : ι), (fun x1 x2 ↦ x1 < x2) j i → a₁✝ j = a₂ j
hi : a₁✝ i < a₂ i
a : β i
ha₁ : a₁✝ i < a
ha₂ : a < a₂ i
j : ι
hj : (fun x1 x2 ↦ x1 < x2) j i
⊢ a₂ j = Function.update a₂ i a j
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
r : R
⊢ eval r (p * X) - eval r (p * C r) = 0

Tactic:
eval_mul_X,

Goal state after:
R : Type u
inst✝ : Ring R
p : R[X]
r : R
⊢ eval r p * r - eval r (p * C r) = 0
Module: Mathlib.Algebra.MvPolynomial.Eval

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

Tactic:
exact Finsupp.sum_add_index (by simp [f.map_zero]) (by simp [add_mul, f.map_add])

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
s s' : σ
n n' : ℕ
⊢ coeff (Finsupp.single s' n') (X s ^ n) = if s = s' ∧ n = n' ∨ n = 0 ∧ n' = 0 then 1 else 0

Tactic:
simp only [coeff_X_pow, single_eq_single_iff]

Goal state after:
Module: Mathlib.Data.DFinsupp.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
r : ι → ι → Prop
inst✝ : IsStrictOrder ι r
x y : Π₀ (i : ι), α i
hlt : x < y
⊢ ∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i

Tactic:
exact lex_lt_of_lt_of_preorder r hlt

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ ↪ τ
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff (Finsupp.mapDomain (⇑f) d) ((rename ⇑f) φ) = coeff d φ

Tactic:
coeff_rename_mapDomain f f.injective

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ ↪ τ
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d φ = coeff d φ
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
⊢ coeff d ((rename f) φ) = 0

Tactic:
by
  classical
  rw [← notMem_support_iff]
  intro H
  replace H := mapDomain_support H
  rw [Finset.mem_image] at H
  obtain ⟨u, hu, rfl⟩ := H
  specialize h u rfl
  rw [Finsupp.mem_support_iff] at hu
  contradiction

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

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
⊢ ((rename f) φ).degrees ⊆ Multiset.map f φ.degrees

Tactic:
by
  classical
  intro i
  rw [mem_degrees, Multiset.mem_map]
  rintro ⟨d, hd, hi⟩
  obtain ⟨x, rfl, hx⟩ := coeff_rename_ne_zero _ _ _ hd
  simp only [Finsupp.mapDomain, Finsupp.mem_support_iff] at hi
  rw [sum_apply, Finsupp.sum] at hi
  contrapose! hi
  rw [Finset.sum_eq_zero]
  intro j hj
  simp only [mem_degrees] at hi
  specialize hi j ⟨x, hx, hj⟩
  rw [Finsupp.single_apply, if_neg hi]

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

Goal state before:
pp: case mul_X
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    constantCoeff ((rename f) p) = constantCoeff p → constantCoeff ((rename f) (p * X n)) = constantCoeff (p * X n)

Tactic:
intro p n hp
    simp only [hp, rename_X, constantCoeff_X, map_mul]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
c : R
hc : c = 0
⊢ ((monomial s) c).totalDegree ≤ s.sum fun x ↦ id

Tactic:
then

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ →₀ ℕ
c : R
hc : c = 0
⊢ ((monomial s) c).totalDegree ≤ s.sum fun x ↦ id
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case refine_2
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : τ → σ
hfi : Injective f
hf : ↑p.vars ⊆ range f
⊢ ∀ i ∈ p.vars,
    i ∈ p.vars →
      ((rename f).comp (aeval fun i ↦ Option.elim' 0 X (partialInv f i)).toRingHom) (X i) =
        (RingHom.id (MvPolynomial σ R)) (X i)

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:
· intro i hip _
        rcases hf hip with ⟨i, rfl⟩
        simp [partialInv_left hfi]

Goal state after:
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
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
h : p.IsRoot a
hlt : p.degree ≤ 0
this : p = C (p.coeff 0)
⊢ False

Tactic:
IsRoot,

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
h : eval a p = 0
hlt : p.degree ≤ 0
this : p = C (p.coeff 0)
⊢ False
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : ∑ x ∈ antidiagonal n, p.coeff x.1 * q.coeff x.2 ≠ 0
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hpq : p.coeff (i, j).1 * q.coeff (i, j).2 ≠ 0
⊢ ↑(i, j).1 + ↑(i, j).2 = ↑n

Tactic:
← WithTop.coe_add,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : ∑ x ∈ antidiagonal n, p.coeff x.1 * q.coeff x.2 ≠ 0
i j : ℕ
hij : (i, j) ∈ antidiagonal n
hpq : p.coeff (i, j).1 * q.coeff (i, j).2 ≠ 0
⊢ ↑((i, j).1 + (i, j).2) = ↑n
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

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

Tactic:
induction m with

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
⊢ p * q = 0

Tactic:
by rw [hp, zero_mul]

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

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

Tactic:
← one_mul (X ^ n),

Goal state after:
R : Type u_1
inst✝ : Semiring R
N n : ℕ
⊢ reflect N (1 * X ^ n) = X ^ (revAt N) n
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support ≤ 1
⊢ f.eraseLead = 0

Tactic:
rw [← C_mul_X_pow_eq_self h]

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : #f.support ≤ 1
⊢ (C f.leadingCoeff * X ^ f.natDegree).eraseLead = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
i : ℕ
m : σ →₀ ℕ
hm : ¬coeff m (((optionEquivLeft R σ) p).coeff i) = 0
⊢ ∃ a, ¬coeff a.some (((optionEquivLeft R σ) p).coeff (a none)) = 0 ∧ a none = i

Tactic:
exact ⟨optionElim i m, by simpa using! hm, optionElim_apply_none _ _⟩

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
h : q.natDegree ≠ 0
a✝ : Nontrivial R
this : (p.comp q).natDegree = p.natDegree * q.natDegree
⊢ p.leadingCoeff * q.leadingCoeff ^ p.natDegree = 1

Tactic:
hp.leadingCoeff,

Goal state after:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
a✝ : Nontrivial R
this : (p.comp q).natDegree = p.natDegree * q.natDegree
⊢ 1 * q.leadingCoeff ^ p.natDegree = 1
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.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
hp.leadingCoeff,

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f.natDegree = 0
⊢ f.natDegree < 1

Tactic:
simp only [hf, zero_lt_one]

Goal state after:
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
⊢ p.degree = 0

Tactic:
rw [← degree_map_eq_of_leadingCoeff_ne_zero f _, map_eq, degree_one]

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

Tactic:
hp.leadingCoeff,

Goal state after:
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
⊢ f 1 ≠ 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
hdeg : p.degree = 0
hndeg : p.natDegree = 0
⊢ 1 = C p.leadingCoeff

Tactic:
hp.leadingCoeff,

Goal state after:
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
hdeg : p.degree = 0
hndeg : p.natDegree = 0
⊢ 1 = C 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (Multiset.map f (a ::ₘ t)).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) (a ::ₘ t)).sum

Tactic:
rw [Multiset.map_cons, Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons,
      Monic.nextCoeff_mul, ih]

Goal state after:
case refine_2
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ ∀ i ∈ t, (f i).Monic

case refine_2.hp
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (f a).Monic

case refine_2.hq
R : Type u
ι : Type y
inst✝ : CommSemiring R
t✝ : Multiset ι
f : ι → R[X]
a : ι
t : Multiset ι
ih : (∀ i ∈ t, (f i).Monic) → (Multiset.map f t).prod.nextCoeff = (Multiset.map (fun i ↦ (f i).nextCoeff) t).sum
ht : ∀ i ∈ a ::ₘ t, (f i).Monic
⊢ (Multiset.map f t).prod.Monic
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case refine_3
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ g * f * C p.leadingCoeff = p

Tactic:
hp.leadingCoeff,

Goal state after:
case refine_3
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
h : ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
f g : R[X]
hfg : p = f * g
⊢ g * f * C 1 = p