mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ

Goal state before:
pp: R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ (univ R n).coeff (Fintype.card n) = 1

Tactic:
suffices Polynomial.coeff (univ ℤ n) (Fintype.card n) = 1 by
    rw [← univ_map_map n (Int.castRingHom R), Polynomial.coeff_map, this, map_one]
  rw [← univ_natDegree ℤ n]
  exact (univ_monic ℤ n).leadingCoeff

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ

Goal state before:
pp: case hφ
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i, 1
i : Equiv.Perm n
⊢ (↑↑(Equiv.Perm.sign i)).IsHomogeneous 0

pp: case hψ
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i, 1
i : Equiv.Perm n
⊢ (∏ x,
        ((Polynomial.aevalTower (rename some) (X none)) (if i x = x then Polynomial.X else 0) -
          X (some (i x, x)))).IsHomogeneous
    (∑ i, 1)

Tactic:
·

Goal state after:
case hφ
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i, 1
i : Equiv.Perm n
⊢ (↑↑(Equiv.Perm.sign i)).IsHomogeneous 0
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ

Goal state before:
pp: case hψ
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i, 1
i : Equiv.Perm n
⊢ (∏ x,
        ((Polynomial.aevalTower (rename some) (X none)) (if i x = x then Polynomial.X else 0) -
          X (some (i x, x)))).IsHomogeneous
    (∑ i, 1)

Tactic:
·

Goal state after:
case hψ
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i, 1
i : Equiv.Perm n
⊢ (∏ x,
        ((Polynomial.aevalTower (rename some) (X none)) (if i x = x then Polynomial.X else 0) -
          X (some (i x, x)))).IsHomogeneous
    (∑ i, 1)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ

Goal state before:
pp: case pos
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i, 1
i : Equiv.Perm n
j : n
h : i j = j
⊢ ((Polynomial.aevalTower (rename some) (X none)) (if i j = j then Polynomial.X else 0) -
        X (some (i j, j))).IsHomogeneous
    1

pp: case neg
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i, 1
i : Equiv.Perm n
j : n
h : ¬i j = j
⊢ ((Polynomial.aevalTower (rename some) (X none)) (if i j = j then Polynomial.X else 0) -
        X (some (i j, j))).IsHomogeneous
    1

Tactic:
·

Goal state after:
case pos
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i, 1
i : Equiv.Perm n
j : n
h : i j = j
⊢ ((Polynomial.aevalTower (rename some) (X none)) (if i j = j then Polynomial.X else 0) -
        X (some (i j, j))).IsHomogeneous
    1
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Univ

Goal state before:
pp: case neg
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i, 1
i : Equiv.Perm n
j : n
h : ¬i j = j
⊢ ((Polynomial.aevalTower (rename some) (X none)) (if i j = j then Polynomial.X else 0) -
        X (some (i j, j))).IsHomogeneous
    1

Tactic:
·

Goal state after:
case neg
R : Type u_1
n : Type u_3
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
aux : Fintype.card n = 0 + ∑ i, 1
i : Equiv.Perm n
j : n
h : ¬i j = j
⊢ ((Polynomial.aevalTower (rename some) (X none)) (if i j = j then Polynomial.X else 0) -
        X (some (i j, j))).IsHomogeneous
    1
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
⊢ homogeneousSubmodule σ R 1 ^ n ≤ homogeneousSubmodule σ R n

pp: case refine_2
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
x : MvPolynomial σ R
hx : x ∈ homogeneousSubmodule σ R n
⊢ x ∈ homogeneousSubmodule σ R 1 ^ n

Tactic:
·

Goal state after:
case refine_1
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
⊢ homogeneousSubmodule σ R 1 ^ n ≤ homogeneousSubmodule σ R n
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
x : MvPolynomial σ R
hx : x ∈ homogeneousSubmodule σ R n
⊢ x ∈ homogeneousSubmodule σ R 1 ^ n

Tactic:
·

Goal state after:
case refine_2
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
x : MvPolynomial σ R
hx : x ∈ homogeneousSubmodule σ R n
⊢ x ∈ homogeneousSubmodule σ R 1 ^ n
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
ι : Type u_5
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
⊢ (∀ i ∈ ∅, (φ i).IsHomogeneous (n i)) → (∏ i ∈ ∅, φ i).IsHomogeneous (∑ i ∈ ∅, n i)

pp: case refine_2
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
ι : Type u_5
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, (φ i).IsHomogeneous (n i)) → (∏ i ∈ s, φ i).IsHomogeneous (∑ i ∈ s, n i)) →
        (∀ i ∈ insert a s, (φ i).IsHomogeneous (n i)) → (∏ i ∈ insert a s, φ i).IsHomogeneous (∑ i ∈ insert a s, n i)

Tactic:
·

Goal state after:
case refine_1
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
ι : Type u_5
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
⊢ (∀ i ∈ ∅, (φ i).IsHomogeneous (n i)) → (∏ i ∈ ∅, φ i).IsHomogeneous (∑ i ∈ ∅, n i)
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
ι : Type u_5
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, (φ i).IsHomogeneous (n i)) → (∏ i ∈ s, φ i).IsHomogeneous (∑ i ∈ s, n i)) →
        (∀ i ∈ insert a s, (φ i).IsHomogeneous (n i)) → (∏ i ∈ insert a s, φ i).IsHomogeneous (∑ i ∈ insert a s, n i)

Tactic:
·

Goal state after:
case refine_2
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
ι : Type u_5
s : Finset ι
φ : ι → MvPolynomial σ R
n : ι → ℕ
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, (φ i).IsHomogeneous (n i)) → (∏ i ∈ s, φ i).IsHomogeneous (∑ i ∈ s, n i)) →
        (∀ i ∈ insert a s, (φ i).IsHomogeneous (n i)) → (∏ i ∈ insert a s, φ i).IsHomogeneous (∑ i ∈ insert a s, n i)
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: case pos
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : ↑(((decompose 𝒜) r) 0) = 0
h : i = 0
⊢ ↑(((decompose 𝒜) ↑(((decompose 𝒜) r) i)) 0) = 0

pp: case neg
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : ↑(((decompose 𝒜) r) 0) = 0
h : ¬i = 0
⊢ ↑(((decompose 𝒜) ↑(((decompose 𝒜) r) i)) 0) = 0

Tactic:
·

Goal state after:
case pos
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : ↑(((decompose 𝒜) r) 0) = 0
h : i = 0
⊢ ↑(((decompose 𝒜) ↑(((decompose 𝒜) r) i)) 0) = 0
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: case neg
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : ↑(((decompose 𝒜) r) 0) = 0
h : ¬i = 0
⊢ ↑(((decompose 𝒜) ↑(((decompose 𝒜) r) i)) 0) = 0

Tactic:
·

Goal state after:
case neg
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
hr : ↑(((decompose 𝒜) r) 0) = 0
h : ¬i = 0
⊢ ↑(((decompose 𝒜) ↑(((decompose 𝒜) r) i)) 0) = 0
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ (if (weight w) d = (weight w) d then coeff d φ else 0) = coeff d φ

pp: case h₀
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ ∀ b ∈ Finite.toFinset ⋯, b ≠ (weight w) d → (if (weight w) d = b then coeff d φ else 0) = 0

pp: case h₁
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ (weight w) d ∉ Finite.toFinset ⋯ → (if (weight w) d = (weight w) d then coeff d φ else 0) = 0

Tactic:
·

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ (if (weight w) d = (weight w) d then coeff d φ else 0) = coeff d φ
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case h₀
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ ∀ b ∈ Finite.toFinset ⋯, b ≠ (weight w) d → (if (weight w) d = b then coeff d φ else 0) = 0

pp: case h₁
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ (weight w) d ∉ Finite.toFinset ⋯ → (if (weight w) d = (weight w) d then coeff d φ else 0) = 0

Tactic:
·

Goal state after:
case h₀
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ ∀ b ∈ Finite.toFinset ⋯, b ≠ (weight w) d → (if (weight w) d = b then coeff d φ else 0) = 0
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case h₁
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ (weight w) d ∉ Finite.toFinset ⋯ → (if (weight w) d = (weight w) d then coeff d φ else 0) = 0

Tactic:
·

Goal state after:
case h₁
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ (weight w) d ∉ Finite.toFinset ⋯ → (if (weight w) d = (weight w) d then coeff d φ else 0) = 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case e'_1
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), (f r).IsHomogeneous 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : i ∈ φ.coeff.support
⊢ n * m = ∑ i_1 ∈ i.support, n * i i_1

pp: case convert_6
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), (f r).IsHomogeneous 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : i ∈ φ.coeff.support
⊢ ∀ i_1 ∈ i.support, ((fun n e ↦ g n ^ e) i_1 (i i_1)).IsHomogeneous (n * i i_1)

Tactic:
·

Goal state after:
case e'_1
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), (f r).IsHomogeneous 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : i ∈ φ.coeff.support
⊢ n * m = ∑ i_1 ∈ i.support, n * i i_1
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: case pos
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : A
hx : x ∈ 𝒜₊.toAddSubmonoid
j : ι
hj : j ∈ DFinsupp.support ((decompose 𝒜) x)
hj₀ : j = 0
⊢ ↑(((decompose 𝒜) x) j) ∈ ⨆ i, ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i)

pp: case neg
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : A
hx : x ∈ 𝒜₊.toAddSubmonoid
j : ι
hj : j ∈ DFinsupp.support ((decompose 𝒜) x)
hj₀ : ¬j = 0
⊢ ↑(((decompose 𝒜) x) j) ∈ ⨆ i, ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i)

Tactic:
·

Goal state after:
case pos
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : A
hx : x ∈ 𝒜₊.toAddSubmonoid
j : ι
hj : j ∈ DFinsupp.support ((decompose 𝒜) x)
hj₀ : j = 0
⊢ ↑(((decompose 𝒜) x) j) ∈ ⨆ i, ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i)
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: case neg
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : A
hx : x ∈ 𝒜₊.toAddSubmonoid
j : ι
hj : j ∈ DFinsupp.support ((decompose 𝒜) x)
hj₀ : ¬j = 0
⊢ ↑(((decompose 𝒜) x) j) ∈ ⨆ i, ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i)

Tactic:
·

Goal state after:
case neg
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
x : A
hx : x ∈ 𝒜₊.toAddSubmonoid
j : ι
hj : j ∈ DFinsupp.support ((decompose 𝒜) x)
hj₀ : ¬j = 0
⊢ ↑(((decompose 𝒜) x) j) ∈ ⨆ i, ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i)
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
⊢ (if (weight w) x = m then coeff x p else 0) = coeff x p

pp: case neg
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if (weight w) x = m then coeff x p else 0) = coeff x p

Tactic:
·

Goal state after:
case pos
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
⊢ (if (weight w) x = m then coeff x p else 0) = coeff x p
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝ : (weight w) x = m
⊢ coeff x p = coeff x p

pp: case neg
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝ : ¬(weight w) x = m
⊢ 0 = coeff x p

Tactic:
·

Goal state after:
case pos
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
h✝ : (weight w) x = m
⊢ coeff x p = coeff x p
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case convert_6
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), (f r).IsHomogeneous 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : i ∈ φ.coeff.support
⊢ ∀ i_1 ∈ i.support, ((fun n e ↦ g n ^ e) i_1 (i i_1)).IsHomogeneous (n * i i_1)

Tactic:
·

Goal state after:
case convert_6
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : MvPolynomial σ R
m n : ℕ
hφ : φ.IsHomogeneous m
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
hf : ∀ (r : R), (f r).IsHomogeneous 0
hg : ∀ (i : σ), (g i).IsHomogeneous n
i : σ →₀ ℕ
hi : i ∈ φ.coeff.support
⊢ ∀ i_1 ∈ i.support, ((fun n e ↦ g n ^ e) i_1 (i i_1)).IsHomogeneous (n * i i_1)
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if (weight w) x = m then coeff x p else 0) = coeff x p

Tactic:
·

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if (weight w) x = m then coeff x p else 0) = coeff x p
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
⊢ (if (weight w) x = n then coeff x p else 0) = coeff x 0

pp: case neg
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if (weight w) x = n then coeff x p else 0) = coeff x 0

Tactic:
·

Goal state after:
case pos
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
⊢ (if (weight w) x = n then coeff x p else 0) = coeff x 0
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if (weight w) x = n then coeff x p else 0) = coeff x 0

Tactic:
·

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if (weight w) x = n then coeff x p else 0) = coeff x 0
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ 0 = coeff x 0

pp: case neg.hnc
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ ¬(weight w) x = n

Tactic:
·

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ 0 = coeff x 0
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case neg.hnc
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ ¬(weight w) x = n

Tactic:
·

Goal state after:
case neg.hnc
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m n : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
hn : n ≠ m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ ¬(weight w) x = n
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i : n
⊢ (monomial (Finsupp.single i 1)) (1 i i) = X i

pp: case h₀
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i : n
⊢ ∀ b ∈ Finset.univ, b ≠ i → (monomial (Finsupp.single b 1)) (1 i b) = 0

pp: case h₁
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i : n
⊢ i ∉ Finset.univ → (monomial (Finsupp.single i 1)) (1 i i) = 0

Tactic:
·

Goal state after:
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i : n
⊢ (monomial (Finsupp.single i 1)) (1 i i) = X i
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
h : ((rename f) φ).IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (weight 1) (mapDomain f d) = (weight 1) d

pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
h : ((rename f) φ).IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ coeff (mapDomain f d) ((rename f) φ) ≠ 0

Tactic:
·

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
hf : Function.Injective f
h : ((rename f) φ).IsHomogeneous n
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (weight 1) (mapDomain f d) = (weight 1) d
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: case h₀
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i : n
⊢ ∀ b ∈ Finset.univ, b ≠ i → (monomial (Finsupp.single b 1)) (1 i b) = 0

pp: case h₁
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i : n
⊢ i ∉ Finset.univ → (monomial (Finsupp.single i 1)) (1 i i) = 0

Tactic:
·

Goal state after:
case h₀
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i : n
⊢ ∀ b ∈ Finset.univ, b ≠ i → (monomial (Finsupp.single b 1)) (1 i b) = 0
Module: Mathlib.Algebra.Module.LinearMap.Polynomial

Goal state before:
pp: case h₀
n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : CommSemiring R
inst✝ : DecidableEq n
i : n
⊢ ∀ b ∈ Finset.univ, b ≠ i → (monomial (Finsupp.single b 1)) (1 i b) = 0

Tactic:
rintro j - hj
    simp only [one_apply_ne hj.symm, map_zero]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
⊢ (if (weight w) x = m then coeff x p else 0) = coeff x (if m = n then p else 0)

pp: case neg
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if (weight w) x = m then coeff x p else 0) = coeff x (if m = n then p else 0)

Tactic:
·

Goal state after:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
inst✝ : DecidableEq M
m n : M
p : MvPolynomial σ R
h : IsWeightedHomogeneous w p n
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
⊢ (if (weight w) x = m then coeff x p else 0) = coeff x (if m = n then p else 0)