mathlib-initiative/mathlib-tactics huggingface dataset:
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₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv : ∀ i ∈ p₁.vars, i ∈ p₂.vars → f₁ (X i) = f₂ (X i)
hp : p₁ = p₂
⊢ f₁ = eval₂Hom (f₁.comp C) (⇑f₁ ∘ X)

Tactic:
ext

Goal state after:
case hC
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv : ∀ i ∈ p₁.vars, i ∈ p₂.vars → f₁ (X i) = f₂ (X i)
hp : p₁ = p₂
x✝ : R
⊢ (f₁.comp C) x✝ = ((eval₂Hom (f₁.comp C) (⇑f₁ ∘ X)).comp C) x✝

case hX
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv : ∀ i ∈ p₁.vars, i ∈ p₂.vars → f₁ (X i) = f₂ (X i)
hp : p₁ = p₂
i✝ : σ
⊢ f₁ (X i✝) = (eval₂Hom (f₁.comp C) (⇑f₁ ∘ X)) (X i✝)
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R✝
e : ℕ
n m : σ✝
s : σ✝ →₀ ℕ
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ algebraMap R (MvPolynomial σ S) =
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).comp (algebraMap R (MvPolynomial σ R))

Tactic:
ext

Goal state after:
R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ✝ : Type u_1
a a' a₁ a₂ : R✝
e : ℕ
n m : σ✝
s : σ✝ →₀ ℕ
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x✝ : R
m✝ : σ →₀ ℕ
⊢ coeff m✝ ((algebraMap R (MvPolynomial σ S)) x✝) =
    coeff m✝ (((algebraMap (MvPolynomial σ R) (MvPolynomial σ S)).comp (algebraMap R (MvPolynomial σ R))) x✝)
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₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv : ∀ i ∈ p₁.vars, i ∈ p₂.vars → f₁ (X i) = f₂ (X i)
hp : p₁ = p₂
⊢ eval₂Hom (f₂.comp C) (⇑f₂ ∘ X) = f₂

Tactic:
ext

Goal state after:
case hC
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv : ∀ i ∈ p₁.vars, i ∈ p₂.vars → f₁ (X i) = f₂ (X i)
hp : p₁ = p₂
x✝ : R
⊢ ((eval₂Hom (f₂.comp C) (⇑f₂ ∘ X)).comp C) x✝ = (f₂.comp C) x✝

case hX
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv : ∀ i ∈ p₁.vars, i ∈ p₂.vars → f₁ (X i) = f₂ (X i)
hp : p₁ = p₂
i✝ : σ
⊢ (eval₂Hom (f₂.comp C) (⇑f₂ ∘ X)) (X i✝) = f₂ (X i✝)
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.coeff p.natTrailingDegree = 0 ↔ p = 0

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.coeff p.natTrailingDegree = 0 → p = 0

case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p = 0 → p.coeff p.natTrailingDegree = 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ (C a * p).degree = p.degree

Tactic:
rw [degree_mul' (by simpa)]

Goal state after:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ (C a).degree + p.degree = p.degree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case insert.inl
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
H : (f x).degree < (s.sum f).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun i ↦ (f i).degree)

Tactic:
rw [← IH, sup_eq_right.mpr H.le, degree_add_eq_right_of_degree_lt H]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
N : ℕ
p : R[X]
⊢ reflect N (reflect N p) = p

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Semiring R
N : ℕ
p : R[X]
n✝ : ℕ
⊢ (reflect N (reflect N p)).coeff n✝ = p.coeff n✝
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f g : R[X]
N : ℕ
⊢ reflect N (f + g) = reflect N f + reflect N g

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Semiring R
f g : R[X]
N n✝ : ℕ
⊢ (reflect N (f + g)).coeff n✝ = (reflect N f + reflect N g).coeff n✝
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
r : R
N : ℕ
⊢ reflect N (C r * f) = C r * reflect N f

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
r : R
N n✝ : ℕ
⊢ (reflect N (C r * f)).coeff n✝ = (C r * reflect N f).coeff n✝
Module: Mathlib.Algebra.Polynomial.Reverse

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

Tactic:
ext

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
⊢ reflect n (map f p) = map f (reflect n p)

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
f : R →+* S
p : R[X]
n n✝ : ℕ
⊢ (reflect n (map f p)).coeff n✝ = (map f (reflect n p)).coeff n✝
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case neg.Og
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ (C g.leadingCoeff * X ^ g.natDegree).natDegree ≤ O

pp: case neg.Cg
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ #g.eraseLead.support ≤ cg.succ

pp: case neg.Og
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ g.eraseLead.natDegree ≤ O

Tactic:
· exact le_trans (natDegree_C_mul_X_pow_le g.leadingCoeff g.natDegree) Og

Goal state after:
case neg.Cg
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ #g.eraseLead.support ≤ cg.succ

case neg.Og
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg : ∀ (g : R[X]), #g.support ≤ cg.succ → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ g.eraseLead.natDegree ≤ O
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
⊢ (isEmptyRingEquiv R σ).symm.toRingHom = C

Tactic:
ext

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
x✝ : R
m✝ : σ →₀ ℕ
⊢ coeff m✝ ((isEmptyRingEquiv R σ).symm.toRingHom x✝) = coeff m✝ (C x✝)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
r : R
⊢ (sumAlgEquiv R S₁ S₂) (C r) = C (C r)

Tactic:
ext

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
r : R
m✝¹ : S₁ →₀ ℕ
m✝ : S₂ →₀ ℕ
⊢ coeff m✝ (coeff m✝¹ ((sumAlgEquiv R S₁ S₂) (C r))) = coeff m✝ (coeff m✝¹ (C (C r)))
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
r : R
⊢ (sumAlgEquiv R S₁ S₂).symm (C (C r)) = C r

Tactic:
ext

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
r : R
m✝ : S₁ ⊕ S₂ →₀ ℕ
⊢ coeff m✝ ((sumAlgEquiv R S₁ S₂).symm (C (C r))) = coeff m✝ (C r)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
c : S₁
⊢ (sumAlgEquiv R S₁ S₂) (X (Sum.inl c)) = X c

Tactic:
ext

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
c : S₁
m✝¹ : S₁ →₀ ℕ
m✝ : S₂ →₀ ℕ
⊢ coeff m✝ (coeff m✝¹ ((sumAlgEquiv R S₁ S₂) (X (Sum.inl c)))) = coeff m✝ (coeff m✝¹ (X c))
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
c : S₁
⊢ (sumAlgEquiv R S₁ S₂).symm (X c) = X (Sum.inl c)

Tactic:
ext

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
c : S₁
m✝ : S₁ ⊕ S₂ →₀ ℕ
⊢ coeff m✝ ((sumAlgEquiv R S₁ S₂).symm (X c)) = coeff m✝ (X (Sum.inl c))
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
c : S₂
⊢ (sumAlgEquiv R S₁ S₂) (X (Sum.inr c)) = C (X c)

Tactic:
ext

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
c : S₂
m✝¹ : S₁ →₀ ℕ
m✝ : S₂ →₀ ℕ
⊢ coeff m✝ (coeff m✝¹ ((sumAlgEquiv R S₁ S₂) (X (Sum.inr c)))) = coeff m✝ (coeff m✝¹ (C (X c)))
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
c : S₂
⊢ (sumAlgEquiv R S₁ S₂).symm (C (X c)) = X (Sum.inr c)

Tactic:
ext

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
c : S₂
m✝ : S₁ ⊕ S₂ →₀ ℕ
⊢ coeff m✝ ((sumAlgEquiv R S₁ S₂).symm (C (X c))) = coeff m✝ (X (Sum.inr c))
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
⊢ (↑(sumAlgEquiv R S₁ S₂)).comp (rename Sum.inr) =
    IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))

Tactic:
ext

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
i✝ : S₂
m✝¹ : S₁ →₀ ℕ
m✝ : S₂ →₀ ℕ
⊢ coeff m✝ (coeff m✝¹ (((↑(sumAlgEquiv R S₁ S₂)).comp (rename Sum.inr)) (X i✝))) =
    coeff m✝ (coeff m✝¹ ((IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))) (X i✝)))
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
⊢ (↑(sumAlgEquiv R S₁ S₂)).comp (rename Sum.inl) = mapAlgHom (Algebra.ofId R (MvPolynomial S₂ R))

Tactic:
ext

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
i✝ : S₁
m✝¹ : S₁ →₀ ℕ
m✝ : S₂ →₀ ℕ
⊢ coeff m✝ (coeff m✝¹ (((↑(sumAlgEquiv R S₁ S₂)).comp (rename Sum.inl)) (X i✝))) =
    coeff m✝ (coeff m✝¹ ((mapAlgHom (Algebra.ofId R (MvPolynomial S₂ R))) (X i✝)))
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial S₂ R
⊢ (↑(commAlgEquiv R S₁ S₂)).comp (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))) =
    mapAlgHom (Algebra.ofId R (MvPolynomial S₁ R))

Tactic:
ext

Goal state after:
R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial S₂ R
i✝ : S₂
m✝¹ : S₂ →₀ ℕ
m✝ : S₁ →₀ ℕ
⊢ coeff m✝
      (coeff m✝¹
        (((↑(commAlgEquiv R S₁ S₂)).comp
            (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))))
          (X i✝))) =
    coeff m✝ (coeff m✝¹ ((mapAlgHom (Algebra.ofId R (MvPolynomial S₁ R))) (X i✝)))
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]
h : C (eval (q.coeff 0) p) = 0
key✝ : p.natDegree = 0 ∨ q.natDegree = 0
key : q = C (q.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)

Tactic:
C_eq_zero

Goal state after:
case inr
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : eval (q.coeff 0) p = 0
key✝ : p.natDegree = 0 ∨ q.natDegree = 0
key : q = C (q.coeff 0)
⊢ p = 0 ∨ eval (q.coeff 0) p = 0 ∧ q = C (q.coeff 0)
Module: Mathlib.Algebra.MvPolynomial.Equiv

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

Tactic:
constructor

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

case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
i : ℕ
⊢ (∃ a, ¬coeff a.some (((optionEquivLeft R σ) p).coeff (a none)) = 0 ∧ a none = i) →
    ∃ x, ¬coeff x (((optionEquivLeft R σ) p).coeff i) = 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ eval₂ i (⅟x) (reflect N f) = 0 ↔ eval₂ i (⅟x) (reflect N f) * x ^ N = 0

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ eval₂ i (⅟x) (reflect N f) = 0 → eval₂ i (⅟x) (reflect N f) * x ^ N = 0

case mpr
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ eval₂ i (⅟x) (reflect N f) * x ^ N = 0 → eval₂ i (⅟x) (reflect N f) = 0
Module: Mathlib.Algebra.Polynomial.Monic

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

Tactic:
hfg,

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : R
g : R[X]
hfg : (X + C a) * g = 1
hgf : g * (X + C a) = 1
h : natDegree 1 = (X + C a).natDegree + g.natDegree
⊢ False
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.coeff f.natTrailingDegree = f.trailingCoeff

Tactic:
trailingCoeff

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.coeff f.natTrailingDegree = f.coeff f.natTrailingDegree
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ (p * q).trailingCoeff = p.trailingCoeff * q.trailingCoeff

Tactic:
rw [← reverse_leadingCoeff, reverse_mul_of_domain, leadingCoeff_mul, reverse_leadingCoeff,
    reverse_leadingCoeff]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
FG : k ≤ f.natDegree
⊢ (φ f).natDegree < (φ g).natDegree

Tactic:
fk,

Goal state after:
case pos
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
FG : k ≤ f.natDegree
⊢ fu f.natDegree < (φ g).natDegree
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ x, ¬coeff (cons i x) f = 0) ↔ ∃ a, ¬coeff a f = 0 ∧ a 0 = i

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ x, ¬coeff (cons i x) f = 0) → ∃ a, ¬coeff a f = 0 ∧ a 0 = i

case mpr
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ a, ¬coeff a f = 0 ∧ a 0 = i) → ∃ x, ¬coeff (cons i x) f = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case p
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
| fun a ↦ a ∈ (((finSuccEquiv R n) f).coeff i).support ∧ cons i a = m

Tactic:
ext

Goal state after:
case p
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
x✝ : Fin n →₀ ℕ
| x✝ ∈ (((finSuccEquiv R n) f).coeff i).support ∧ cons i x✝ = m
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ (∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m) ↔ coeff m f ≠ 0 ∧ m 0 = i

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ (∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m) → coeff m f ≠ 0 ∧ m 0 = i

case mpr
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ coeff m f ≠ 0 ∧ m 0 = i → ∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
⊢ #f.support = n ↔ ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i

Tactic:
refine ⟨?_, fun ⟨k, x, hk, hx, hf⟩ => hf.symm ▸ card_support_eq' k x hk.injective hx⟩

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
⊢ #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0) ↔
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0) →
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)

case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → ¬(0 < g.natDegree ∧ g.natDegree + g.natDegree ≤ p.natDegree)) →
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u_1
σ : Type u_3
inst✝ : CommSemiring R
i : σ
⊢ toMvPolynomial i = (MvPolynomial.rename fun x ↦ i).comp ↑(MvPolynomial.uniqueAlgEquiv R Unit).symm

Tactic:
ext

Goal state after:
R : Type u_1
σ : Type u_3
inst✝ : CommSemiring R
i : σ
m✝ : σ →₀ ℕ
⊢ MvPolynomial.coeff m✝ ((toMvPolynomial i) X) =
    MvPolynomial.coeff m✝ (((MvPolynomial.rename fun x ↦ i).comp ↑(MvPolynomial.uniqueAlgEquiv R Unit).symm) X)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u_1
σ : Type u_3
inst✝ : CommSemiring R
f : σ → R
i : σ
⊢ (eval f).comp ↑(toMvPolynomial i) = evalRingHom (f i)

Tactic:
ext

Goal state after:
case h₁
R : Type u_1
σ : Type u_3
inst✝ : CommSemiring R
f : σ → R
i : σ
x✝ : R
⊢ (((eval f).comp ↑(toMvPolynomial i)).comp Polynomial.C) x✝ = ((evalRingHom (f i)).comp Polynomial.C) x✝

case h₂
R : Type u_1
σ : Type u_3
inst✝ : CommSemiring R
f : σ → R
i : σ
⊢ ((eval f).comp ↑(toMvPolynomial i)) Polynomial.X = (evalRingHom (f i)) Polynomial.X
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u_1
S : Type u_2
σ : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : σ → S
i : σ
⊢ (aeval f).comp (toMvPolynomial i) = Polynomial.aeval (f i)

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
σ : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : σ → S
i : σ
⊢ ((aeval f).comp (toMvPolynomial i)) Polynomial.X = (Polynomial.aeval (f i)) Polynomial.X
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u_1
σ : Type u_3
τ : Type u_4
inst✝ : CommSemiring R
f : σ → τ
a : σ
⊢ (rename f).comp (toMvPolynomial a) = toMvPolynomial (f a)

Tactic:
ext

Goal state after:
R : Type u_1
σ : Type u_3
τ : Type u_4
inst✝ : CommSemiring R
f : σ → τ
a : σ
m✝ : τ →₀ ℕ
⊢ coeff m✝ (((rename f).comp (toMvPolynomial a)) Polynomial.X) = coeff m✝ ((toMvPolynomial (f a)) Polynomial.X)
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ ∑ i ∈ range (n + 2), 0 ^ i = if n + 2 = 0 then 0 else 1

Tactic:
rw [geom_sum_succ']
    simp [zero_geom_sum]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)) ↔
    ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)) →
    ∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p

case mpr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p ≠ 1
⊢ (∀ (q : R[X]), q.Monic → q.natDegree ∈ Ioc 0 (p.natDegree / 2) → ¬q ∣ p) →
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)
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
⊢ (∃ 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₂

Tactic:
constructor

Goal state after:
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₂

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: R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
i : ι
hi : i ∈ s
hf : ¬f i = 0
| fun b ↦ (v b • map (algebraMap R A) (f b)).coeff (f i).natDegree

Tactic:
ext

Goal state after:
R : Type u
ι : Type w
s : Finset ι
inst✝² : CommRing R
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → R[X]
v : ι → A
h : LinearIndepOn R v ↑s
i : ι
hi : i ∈ s
hf : ¬f i = 0
x✝ : ι
| (v x✝ • map (algebraMap R A) (f x✝)).coeff (f i).natDegree