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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
⊢ p.update n a = p + C (a - p.coeff n) * X ^ n

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
⊢ (p.update n a).coeff n✝ = (p + C (a - p.coeff n) * X ^ n).coeff n✝
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ ↑m = ↑n ↔ m = n

Tactic:
constructor

Goal state after:
case mp
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ ↑m = ↑n → m = n

case mpr
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ m = n → ↑m = ↑n
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ ↑m = ↑n ↔ m = n

Tactic:
by
  constructor
  · intro h
    apply_fun fun p => p.coeff 0 at h
    simpa using h
  · rintro rfl
    rfl

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

Goal state before:
pp: m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ ↑m = ↑n ↔ m = n

Tactic:
constructor

Goal state after:
case mp
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ ↑m = ↑n → m = n

case mpr
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ m = n → ↑m = ↑n
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ ↑m = ↑n ↔ m = n

Tactic:
by
  constructor
  · intro h
    apply_fun fun p => p.coeff 0 at h
    simpa using h
  · rintro rfl
    rfl

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
⊢ (p ^ i * p).natDegree < i * p.natDegree + p.natDegree

Tactic:
have h1 : (p ^ i).natDegree < i * p.natDegree := by
          refine lt_of_le_of_ne natDegree_pow_le fun h => hp2 ?_
          rw [← h, hp1] at hi
          exact leadingCoeff_eq_zero.mp hi

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
h1 : (p ^ i).natDegree < i * p.natDegree
⊢ (p ^ i * p).natDegree < i * p.natDegree + p.natDegree
Module: Mathlib.Algebra.Polynomial.Monomial

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
⊢ f.support.card ≤ 1 ↔ ∃ n a, f = (monomial n) a

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝ : Semiring R
f : R[X]
⊢ f.support.card ≤ 1 → ∃ n a, f = (monomial n) a

case mpr
R : Type u
inst✝ : Semiring R
f : R[X]
⊢ (∃ n a, f = (monomial n) a) → f.support.card ≤ 1
Module: Mathlib.Algebra.Polynomial.Monomial

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
⊢ f' = g'

Tactic:
ext

Goal state after:
case h₁
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := f.comp (toFinsuppIso R).symm.toRingHom
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := g.comp (toFinsuppIso R).symm.toRingHom
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
x✝ : R
⊢ (f'.comp AddMonoidAlgebra.singleZeroRingHom) x✝ = (g'.comp AddMonoidAlgebra.singleZeroRingHom) x✝

case h_of
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), f (C a) = g (C a)
h₂ : f X = g X
f' : AddMonoidAlgebra R ℕ →+* S := ⋯
hf' : f' = f.comp (toFinsuppIso R).symm.toRingHom
g' : AddMonoidAlgebra R ℕ →+* S := ⋯
hg' : g' = g.comp (toFinsuppIso R).symm.toRingHom
⊢ ((↑f').comp (AddMonoidAlgebra.of R ℕ)) (Multiplicative.ofAdd 1) =
    ((↑g').comp (AddMonoidAlgebra.of R ℕ)) (Multiplicative.ofAdd 1)
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : R[X]
e : R ≃+* S
⊢ (mapRingHom ↑e).comp (mapRingHom ↑e.symm) = RingHom.id S[X]

Tactic:
ext

Goal state after:
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : R[X]
e : R ≃+* S
x✝ : S[X]
n✝ : ℕ
⊢ (((mapRingHom ↑e).comp (mapRingHom ↑e.symm)) x✝).coeff n✝ = ((RingHom.id S[X]) x✝).coeff n✝
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : R[X]
e : R ≃+* S
⊢ (mapRingHom ↑e.symm).comp (mapRingHom ↑e) = RingHom.id R[X]

Tactic:
ext

Goal state after:
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : R[X]
e : R ≃+* S
x✝ : R[X]
n✝ : ℕ
⊢ (((mapRingHom ↑e.symm).comp (mapRingHom ↑e)) x✝).coeff n✝ = ((RingHom.id R[X]) x✝).coeff n✝
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
⊢ x + y = single a n ↔ ∃ a_1 b, a_1 + b = n ∧ single a a_1 = x ∧ single a b = y

Tactic:
constructor

Goal state after:
case mp
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
⊢ x + y = single a n → ∃ a_2 b, a_2 + b = n ∧ single a a_2 = x ∧ single a b = y

case mpr
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
⊢ (∃ a_1 b, a_1 + b = n ∧ single a a_1 = x ∧ single a b = y) → x + y = single a n
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : Zero α
inst✝¹ : LE α
inst✝ : Std.Refl fun x1 x2 ↦ x1 ≤ x2
f : ι ↪ κ
g₁ g₂ : ι →₀ α
⊢ embDomain f g₁ ≤ embDomain f g₂ ↔ g₁ ≤ g₂

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : Zero α
inst✝¹ : LE α
inst✝ : Std.Refl fun x1 x2 ↦ x1 ≤ x2
f : ι ↪ κ
g₁ g₂ : ι →₀ α
⊢ embDomain f g₁ ≤ embDomain f g₂ → g₁ ≤ g₂

case mpr
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : Zero α
inst✝¹ : LE α
inst✝ : Std.Refl fun x1 x2 ↦ x1 ≤ x2
f : ι ↪ κ
g₁ g₂ : ι →₀ α
⊢ g₁ ≤ g₂ → embDomain f g₁ ≤ embDomain f g₂
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
C : Type u_3
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : B →ₐ[R] C
g : A →ₐ[R] B
⊢ (mapAlgHom f).comp (mapAlgHom g) = mapAlgHom (f.comp g)

Tactic:
ext

Goal state after:
case hC
R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
C : Type u_3
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : B →ₐ[R] C
g : A →ₐ[R] B
x✝ : A
n✝ : ℕ
⊢ ((((mapAlgHom f).comp (mapAlgHom g)).comp CAlgHom) x✝).coeff n✝ = (((mapAlgHom (f.comp g)).comp CAlgHom) x✝).coeff n✝

case hX
R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
C : Type u_3
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : B →ₐ[R] C
g : A →ₐ[R] B
n✝ : ℕ
⊢ (((mapAlgHom f).comp (mapAlgHom g)) X).coeff n✝ = ((mapAlgHom (f.comp g)) X).coeff n✝
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
C : Type u_3
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A ≃ₐ[R] B
g : B ≃ₐ[R] C
⊢ (mapAlgEquiv f).trans (mapAlgEquiv g) = mapAlgEquiv (f.trans g)

Tactic:
ext

Goal state after:
R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
C : Type u_3
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A ≃ₐ[R] B
g : B ≃ₐ[R] C
a✝ : A[X]
n✝ : ℕ
⊢ (((mapAlgEquiv f).trans (mapAlgEquiv g)) a✝).coeff n✝ = ((mapAlgEquiv (f.trans g)) a✝).coeff n✝
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : IsBotZeroClass α
inst✝ : DecidableEq ι
f g : ι →₀ α
⊢ (f ⊓ g).support = f.support ∩ g.support

Tactic:
ext

Goal state after:
ι : Type u_1
α : Type u_3
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : IsBotZeroClass α
inst✝ : DecidableEq ι
f g : ι →₀ α
a✝ : ι
⊢ a✝ ∈ (f ⊓ g).support ↔ a✝ ∈ f.support ∩ g.support
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : IsBotZeroClass α
inst✝ : DecidableEq ι
f g : ι →₀ α
⊢ (f ⊔ g).support = f.support ∪ g.support

Tactic:
ext

Goal state after:
ι : Type u_1
α : Type u_3
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : IsBotZeroClass α
inst✝ : DecidableEq ι
f g : ι →₀ α
a✝ : ι
⊢ a✝ ∈ (f ⊔ g).support ↔ a✝ ∈ f.support ∪ g.support
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: S : Type v
A' : Type u_1
inst✝² : CommSemiring A'
inst✝¹ : CommSemiring S
inst✝ : Algebra S A'
⊢ aevalTower (Algebra.ofId S A') = aeval

Tactic:
ext

Goal state after:
S : Type v
A' : Type u_1
inst✝² : CommSemiring A'
inst✝¹ : CommSemiring S
inst✝ : Algebra S A'
x✝ : A'
⊢ (aevalTower (Algebra.ofId S A') x✝) X = (aeval x✝) X
Module: Mathlib.Data.DFinsupp.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → Zero (α i)
inst✝² : (i : ι) → Lattice (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
⊢ (↑((f ⊓ g).support ∪ (f ⊔ g).support))ᶜ = (↑(f.support ∪ g.support))ᶜ

Tactic:
ext

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → Zero (α i)
inst✝² : (i : ι) → Lattice (α i)
f g : Π₀ (i : ι), α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x✝ : ι
⊢ x✝ ∈ (↑((f ⊓ g).support ∪ (f ⊔ g).support))ᶜ ↔ x✝ ∈ (↑(f.support ∪ g.support))ᶜ
Module: Mathlib.Algebra.Polynomial.AlgebraMap

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

Tactic:
rw [mul_sub, eval_sub, eval_mul_X, eval_mul_C_of_commute] <;> simp

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsBotZeroClass (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ (f ⊓ g).support = f.support ∩ g.support

Tactic:
ext

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsBotZeroClass (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
a✝ : ι
⊢ a✝ ∈ (f ⊓ g).support ↔ a✝ ∈ f.support ∩ g.support
Module: Mathlib.Data.DFinsupp.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsBotZeroClass (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ (f ⊔ g).support = f.support ∪ g.support

Tactic:
ext

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsBotZeroClass (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
a✝ : ι
⊢ a✝ ∈ (f ⊔ g).support ↔ a✝ ∈ f.support ∪ g.support
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f : Π₀ (a : α), N a
⊢ f.neLocus 0 = f.support

Tactic:
ext

Goal state after:
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f : Π₀ (a : α), N a
a✝ : α
⊢ a✝ ∈ f.neLocus 0 ↔ a✝ ∈ f.support
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : IsEmpty σ
p : MvPolynomial σ R
⊢ (C (p.coeff 0)).coeff = p.coeff

Tactic:
ext

Goal state after:
R : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : IsEmpty σ
p : MvPolynomial σ R
⊢ (C (p.coeff 0)).coeff default = p.coeff default
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝² : CommSemiring R
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : MvPolynomial σ R →ₐ[R] A
hf : ∀ (i : σ), f (X i) = g (X i)
⊢ f.comp singleZeroAlgHom = g.comp singleZeroAlgHom

Tactic:
ext

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

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
⊢ φ.comp (eval₂Hom f g) = eval₂Hom (φ.comp f) fun i ↦ φ (g i)

Tactic:
ext

Goal state after:
case hC
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
x✝ : R
⊢ ((φ.comp (eval₂Hom f g)).comp C) x✝ = ((eval₂Hom (φ.comp f) fun i ↦ φ (g i)).comp C) x✝

case hX
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
i✝ : σ
⊢ (φ.comp (eval₂Hom f g)) (X i✝) = (eval₂Hom (φ.comp f) fun i ↦ φ (g i)) (X i✝)
Module: Mathlib.Data.Finsupp.Lex

Goal state before:
pp: case h
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ (∀ d < a, (single b 1) d = (single a 1) d) ∧ (single b 1) a < (single a 1) a

Tactic:
constructor

Goal state after:
case h.left
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ ∀ d < a, (single b 1) d = (single a 1) d

case h.right
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ (single b 1) a < (single a 1) a
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ (m : σ →₀ ℕ), coeff m p = coeff m q
⊢ p.coeff = q.coeff

Tactic:
ext

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ (m : σ →₀ ℕ), coeff m p = coeff m q
a✝ : σ →₀ ℕ
⊢ p.coeff a✝ = q.coeff a✝
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
⊢ C r ∣ φ ↔ ∀ (i : σ →₀ ℕ), r ∣ coeff i φ

Tactic:
constructor

Goal state after:
case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
⊢ C r ∣ φ → ∀ (i : σ →₀ ℕ), r ∣ coeff i φ

case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
⊢ (∀ (i : σ →₀ ℕ), r ∣ coeff i φ) → C r ∣ φ
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
⊢ rename f = aeval (X ∘ f)

Tactic:
ext

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
i✝ : σ
m✝ : τ →₀ ℕ
⊢ coeff m✝ ((rename f) (X i✝)) = coeff m✝ ((aeval (X ∘ f)) (X i✝))
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: 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
p : MvPolynomial σ S
i : σ →₀ ℕ
⊢ (∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M) ↔ ∀ (i : σ →₀ ℕ), coeff i p ∈ M

Tactic:
constructor

Goal state after:
case mp
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
p : MvPolynomial σ S
i : σ →₀ ℕ
⊢ (∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M) → ∀ (i : σ →₀ ℕ), coeff i p ∈ M

case mpr
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
p : MvPolynomial σ S
i : σ →₀ ℕ
⊢ (∀ (i : σ →₀ ℕ), coeff i p ∈ M) → ∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: case h
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial (↥s₁) R
s₂ : Finset σ
q₂ : MvPolynomial (↥s₂) R
⊢ (rename Subtype.val) q₁ = (rename Subtype.val) ((rename fun x ↦ ⟨↑x, ⋯⟩) q₁) ∧
    (rename Subtype.val) q₂ = (rename Subtype.val) ((rename fun x ↦ ⟨↑x, ⋯⟩) q₂)

Tactic:
constructor

Goal state after:
case h.left
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial (↥s₁) R
s₂ : Finset σ
q₂ : MvPolynomial (↥s₂) R
⊢ (rename Subtype.val) q₁ = (rename Subtype.val) ((rename fun x ↦ ⟨↑x, ⋯⟩) q₁)

case h.right
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
s₁ : Finset σ
q₁ : MvPolynomial (↥s₁) R
s₂ : Finset σ
q₂ : MvPolynomial (↥s₂) R
⊢ (rename Subtype.val) q₂ = (rename Subtype.val) ((rename fun x ↦ ⟨↑x, ⋯⟩) q₂)
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
⊢ constantCoeff.comp (map f) = f.comp constantCoeff

Tactic:
ext

Goal state after:
case hC
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
x✝ : R
⊢ ((constantCoeff.comp (map f)).comp C) x✝ = ((f.comp constantCoeff).comp C) x✝

case hX
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
i✝ : σ
⊢ (constantCoeff.comp (map f)) (X i✝) = (f.comp constantCoeff) (X i✝)
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case e_f
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f : MvPolynomial σ R
⊢ (fun a ↦ Multiset.count n (toMultiset a)) = fun m ↦ m n

Tactic:
ext

Goal state after:
case e_f
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f : MvPolynomial σ R
x✝ : σ →₀ ℕ
⊢ Multiset.count n (toMultiset x✝) = x✝ n
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
⊢ (-p).support = p.support

Tactic:
ext

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
a✝ : σ →₀ ℕ
⊢ a✝ ∈ (-p).support ↔ a✝ ∈ p.support
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S₁
inst✝² : CommSemiring S₂
inst✝¹ : Algebra R S₁
inst✝ : Algebra R S₂
f : S₁ →ₐ[R] S₂
⊢ range ⇑(mapAlgHom f) = ↑(coeffsIn σ (Subalgebra.toSubmodule f.range))

Tactic:
ext

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S₁
inst✝² : CommSemiring S₂
inst✝¹ : Algebra R S₁
inst✝ : Algebra R S₂
f : S₁ →ₐ[R] S₂
x✝ : MvPolynomial σ S₂
⊢ x✝ ∈ range ⇑(mapAlgHom f) ↔ x✝ ∈ ↑(coeffsIn σ (Subalgebra.toSubmodule f.range))
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case e_f
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ (fun m ↦ m i) ∘ ⇑(addRightEmbedding (Finsupp.single j 1)) = fun m ↦ m i

Tactic:
ext

Goal state after:
case e_f
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
x✝ : σ →₀ ℕ
⊢ ((fun m ↦ m i) ∘ ⇑(addRightEmbedding (Finsupp.single j 1))) x✝ = x✝ i
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case a
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
p : MvPolynomial σ R
⊢ (aeval f).toRingHom p ∈ Algebra.adjoin R (range f)

Tactic:
simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe]

Goal state after:
case a
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
p : MvPolynomial σ R
⊢ (aeval f) p ∈ Algebra.adjoin R (range f)
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
⊢ eval₂Hom f 0 = f.comp constantCoeff

Tactic:
ext

Goal state after:
case hC
R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
x✝ : R
⊢ ((eval₂Hom f 0).comp C) x✝ = ((f.comp constantCoeff).comp C) x✝

case hX
R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
i✝ : σ
⊢ (eval₂Hom f 0) (X i✝) = (f.comp constantCoeff) (X i✝)
Module: Mathlib.Data.Finsupp.Fin

Goal state before:
pp: n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
⊢ (t.update i.succ y).tail = t.tail.update i y

Tactic:
ext

Goal state after:
n : ℕ
i : Fin n
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
a✝ : Fin n
⊢ (t.update i.succ y).tail a✝ = (t.tail.update i y) a✝
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: σ : Type u_1
S : Type u_2
inst✝ : CommSemiring S
⊢ aevalTower (AlgHom.id S S) = aeval

Tactic:
ext

Goal state after:
σ : Type u_1
S : Type u_2
inst✝ : CommSemiring S
x✝ : σ → S
i✝ : σ
⊢ (aevalTower (AlgHom.id S S) x✝) (X i✝) = (aeval x✝) (X i✝)
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: σ : Type u_1
S : Type u_2
A : Type u_3
inst✝² : CommSemiring S
inst✝¹ : CommSemiring A
inst✝ : Algebra S A
⊢ aevalTower (Algebra.ofId S A) = aeval

Tactic:
ext

Goal state after:
σ : Type u_1
S : Type u_2
A : Type u_3
inst✝² : CommSemiring S
inst✝¹ : CommSemiring A
inst✝ : Algebra S A
x✝ : σ → A
i✝ : σ
⊢ (aevalTower (Algebra.ofId S A) x✝) (X i✝) = (aeval x✝) (X i✝)
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
s : σ
⊢ (X s).totalDegree = 1

Tactic:
by
  rw [totalDegree, support_X]
  simp only [Finset.sup, Finsupp.sum_single_index, Finset.fold_singleton, sup_bot_eq]

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

Goal state before:
pp: case pos
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
⊢ (f (coeff d p) * d.prod fun i k ↦ g i ^ k) = 0

Tactic:
obtain ⟨i, hi⟩ : Finset.Nonempty (Finsupp.support d) := by
      rw [constantCoeff_eq, coeff, ← Finsupp.notMem_support_iff] at h0
      rw [Finset.nonempty_iff_ne_empty, Ne, Finsupp.support_eq_empty]
      rintro rfl
      contradiction

Goal state after:
case pos
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
⊢ (f (coeff d p) * d.prod fun i k ↦ g i ^ k) = 0
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case neg.h₀
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
⊢ (f (coeff d p) * d.prod fun i k ↦ g i ^ k) = 0

Tactic:
obtain ⟨i, hi⟩ : Finset.Nonempty (Finsupp.support d) := by
      rw [constantCoeff_eq, coeff, ← Finsupp.notMem_support_iff] at h0
      rw [Finset.nonempty_iff_ne_empty, Ne, Finsupp.support_eq_empty]
      rintro rfl
      contradiction

Goal state after:
case neg.h₀
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
i : σ
hi : i ∈ d.support
⊢ (f (coeff d p) * d.prod fun i k ↦ g i ^ k) = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree = 0 ↔ p = C (coeff 0 p)

Tactic:
constructor

Goal state after:
case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p.totalDegree = 0 → p = C (coeff 0 p)

case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p = C (coeff 0 p) → p.totalDegree = 0