mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: case e'_3
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
coe_mono : Monotone toIdeal
x : Ideal A
⊢ IsHomogeneous 𝒜 x ∧ x ≤ I ↔ ∃ x_1 ∈ {b | b.toIdeal ≤ I}, x_1.toIdeal = x

Tactic:
]

Goal state after:
case e'_3
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
coe_mono : Monotone toIdeal
x : Ideal A
⊢ IsHomogeneous 𝒜 x ∧ x ≤ I ↔ ∃ x_1 ∈ {b | b.toIdeal ≤ I}, x_1.toIdeal = x
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ (∀ m ∈ p.support, ∀ (x : σ), m x = 0) ↔ ∀ m ∈ p.support, ∀ (x : σ), m x = 0

pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ NonTorsionWeight 1

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ NonTorsionWeight 1
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ IsWeightedHomogeneous 1 p 0 ↔ IsWeightedHomogeneous 1 p 0

Tactic:
]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
x✝ : MvPolynomial σ R
⊢ x✝ = C (coeff 0 x✝) ↔ ∃ y, C y = x✝

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
x✝ : MvPolynomial σ R
⊢ x✝ = C (coeff 0 x✝) ↔ ∃ y, C y = x✝
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
f : MvPolynomial σ R
⊢ (C (coeff 0 f)).IsHomogeneous 0

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
f : MvPolynomial σ R
⊢ (C (coeff 0 f)).IsHomogeneous 0
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) r), ↑(((decompose 𝒜) r) i) ∈ (homogeneousHull 𝒜 I).toIdeal

Tactic:
]

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
r : A
hr : r ∈ I
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) r), ↑(((decompose 𝒜) r) i) ∈ (homogeneousHull 𝒜 I).toIdeal
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case single_add
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
r : R
a : σ
b : ℕ
f : σ →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : b ≠ 0
h : (monomial f) r ∈ homogeneousSubmodule σ R 1 ^ degree f
⊢ X a ^ b * (monomial f) r ∈ homogeneousSubmodule σ R 1 ^ b * homogeneousSubmodule σ R 1 ^ degree f

Tactic:
]

Goal state after:
case single_add
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
r : R
a : σ
b : ℕ
f : σ →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : b ≠ 0
h : (monomial f) r ∈ homogeneousSubmodule σ R 1 ^ degree f
⊢ X a ^ b * (monomial f) r ∈ homogeneousSubmodule σ R 1 ^ b * homogeneousSubmodule σ R 1 ^ degree f
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case refine_1.succ
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
ih : homogeneousSubmodule σ R 1 ^ n ≤ homogeneousSubmodule σ R n
⊢ homogeneousSubmodule σ R n * homogeneousSubmodule σ R 1 ≤ homogeneousSubmodule σ R (n + 1)

Tactic:
]

Goal state after:
case refine_1.succ
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
ih : homogeneousSubmodule σ R 1 ^ n ≤ homogeneousSubmodule σ R n
⊢ homogeneousSubmodule σ R n * homogeneousSubmodule σ R 1 ≤ homogeneousSubmodule σ R (n + 1)
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
n : M
φ : MvPolynomial σ R
d : σ →₀ ℕ
hd : (weight w) d ≠ n
⊢ 0 = 0

Tactic:
]

Goal state after:
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
m : M
⊢ IsWeightedHomogeneous w ((weightedHomogeneousComponent w m) φ) m

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
m : M
⊢ IsWeightedHomogeneous w ((weightedHomogeneousComponent w m) φ) m
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: case e'_4
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
x : MvPolynomial σ R
d : σ →₀ ℕ
r : R
hr : (weight 1) d = n
⊢ (weight 1) d = (weight 1) d

Tactic:
]

Goal state after:
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
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w) d ≠ n
⊢ 0 = 0

pp: R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w) d ≠ n
⊢ ∀ x ∈ {d ∈ φ.support | (weight w) d = n}, (monomial x) (coeff x φ) = 0

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w) d ≠ n
⊢ ∀ x ∈ {d ∈ φ.support | (weight w) d = n}, (monomial x) (coeff x φ) = 0
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : (weight fun x ↦ 1) d ≠ n
⊢ coeff d φ = 0

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
hφ : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : (weight fun x ↦ 1) d ≠ n
⊢ coeff d φ = 0
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ (homogeneousHull 𝒜 I).toIdeal = span (⋃ i, ⇑(GradedRing.proj 𝒜 i) '' ↑I)

Tactic:
]

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ (homogeneousHull 𝒜 I).toIdeal = span (⋃ i, ⇑(GradedRing.proj 𝒜 i) '' ↑I)
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m n : ℕ
hm : φ.IsHomogeneous m
hn : φ.IsHomogeneous n
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (weight 1) d = (weight 1) d

Tactic:
]

Goal state after:
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
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w) d ≠ n
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w) d = n
⊢ (monomial d) (coeff d φ) = 0

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
h : ∀ d ∈ φ.support, (weight w) d ≠ n
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w) d = n
⊢ (monomial d) (coeff d φ) = 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
n : M
φ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
⊢ 0 = 0

pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
⊢ ∀ x ∈ {d ∈ φ.support | (weight w) d = n}, (monomial x) (coeff x φ) = 0

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
⊢ ∀ x ∈ {d ∈ φ.support | (weight w) d = n}, (monomial x) (coeff x φ) = 0
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
I : Ideal A
⊢ ⨆ i, span (⇑(GradedRing.proj 𝒜 i) '' ↑I) =
    ⨆ i, toIdeal { toSubmodule := span (⇑(GradedRing.proj 𝒜 i) '' ↑I), is_homogeneous' := ⋯ }

Tactic:
]

Goal state after:
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
n : M
φ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w) d = n
⊢ (monomial d) (coeff d φ) = 0

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w) d = n
⊢ (monomial d) (coeff d φ) = 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
n : M
φ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w) d = n
⊢ (weight w) d < n

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
h : weightedTotalDegree w φ < n
d : σ →₀ ℕ
hd : d ∈ φ.support ∧ (weight w) d = n
⊢ (weight w) d < n
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
⊢ ∑ i ∈ Finite.toFinset ⋯, (weightedHomogeneousComponent w i) φ = φ

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
⊢ ∑ i ∈ Finite.toFinset ⋯, (weightedHomogeneousComponent w i) φ = φ
Module: Mathlib.RingTheory.MvPolynomial.Homogeneous

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
n : ℕ
⊢ (∏ _i ∈ Finset.range n, φ).IsHomogeneous (m * n)

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
n : ℕ
⊢ (∏ _i ∈ Finset.range n, φ).IsHomogeneous (m * n)
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
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
n : ℕ
⊢ (∏ _i ∈ Finset.range n, φ).IsHomogeneous (∑ _i ∈ Finset.range n, m)

Tactic:
]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
n : ℕ
⊢ (∏ _i ∈ Finset.range n, φ).IsHomogeneous (∑ _i ∈ Finset.range n, m)
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
⊢ 0 = 0

Tactic:
]

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

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

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.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 : σ →₀ ℕ
⊢ coeff d φ = coeff d φ

Tactic:
]

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

Goal state before:
pp: σ : 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
⊢ ((fun s a ↦ f a * s.prod fun n e ↦ g n ^ e) i (φ.coeff i)).IsHomogeneous (0 + n * m)

Tactic:
]

Goal state after:
σ : 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
⊢ ((fun s a ↦ f a * s.prod fun n e ↦ g n ^ e) i (φ.coeff i)).IsHomogeneous (0 + n * m)
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 : σ →₀ ℕ
m : M
a✝ : m ∈ Finite.toFinset ⋯
hm' : m ≠ (weight w) d
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : 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
i : ι
hi : 0 < i
hx : x ∈ 𝒜 i
⊢ 0 = 0

Tactic:
]

Goal state after:
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 : σ →₀ ℕ
hm : (weight w) d ∉ Finite.toFinset ⋯
⊢ coeff d φ = 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 : σ →₀ ℕ
hm : (weight w) d ∉ Finite.toFinset ⋯
⊢ coeff d φ = 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 : σ →₀ ℕ
hm : (weightedHomogeneousComponent w ((weight w) d)) φ = 0
this :
  coeff d ((weightedHomogeneousComponent w ((weight w) d)) φ) = if (weight w) d = (weight w) d then coeff d φ else 0
⊢ coeff d φ = 0

Tactic:
hm,

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 : σ →₀ ℕ
hm : (weightedHomogeneousComponent w ((weight w) d)) φ = 0
this : coeff d 0 = if (weight w) d = (weight w) d then coeff d φ else 0
⊢ coeff d φ = 0
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : 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
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) x), ↑(((decompose 𝒜) x) i) ∈ ⨆ i, ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i)

Tactic:
]

Goal state after:
ι : 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
⊢ ∑ i ∈ DFinsupp.support ((decompose 𝒜) x), ↑(((decompose 𝒜) x) i) ∈ ⨆ i, ⨆ (_ : i > 0), AddSubmonoid.ofClass (𝒜 i)
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 : σ →₀ ℕ
hm : (weightedHomogeneousComponent w ((weight w) d)) φ = 0
this : 0 = coeff d φ
⊢ coeff d φ = 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 : σ →₀ ℕ
hm : (weightedHomogeneousComponent w ((weight w) d)) φ = 0
this : 0 = coeff d φ
⊢ coeff d φ = 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 : φ.coeff i ≠ 0
⊢ n * m = ∑ i_1 ∈ i.support, 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 : φ.coeff i ≠ 0
⊢ n * m = ∑ i_1 ∈ i.support, n * i i_1
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
⊢ φ = φ

Tactic:
]

Goal state after:
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
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
⊢ (if (weight w) x = m then coeff x p else 0) = coeff x p

Tactic:
]

Goal state after:
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 : σ →₀ ℕ
⊢ (if (weight w) x = m then coeff x p else 0) = coeff x p
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 : φ.coeff i ≠ 0
⊢ (n * i.sum fun i c ↦ c • 1 i) = n * ∑ i_1 ∈ i.support, 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 : φ.coeff i ≠ 0
⊢ (n * i.sum fun i c ↦ c • 1 i) = n * ∑ i_1 ∈ i.support, i i_1
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : 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, ⨆ (_ : i > 0), ofClass (𝒜 i) = closure (⋃ i, ⋃ (_ : i > 0), ↑(𝒜 i))

Tactic:
]

Goal state after:
ι : 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, ⨆ (_ : i > 0), ofClass (𝒜 i) = closure (⋃ i, ⋃ (_ : i > 0), ↑(𝒜 i))
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal

Goal state before:
pp: ι : 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 𝒜
P : AddSubmonoid A
⊢ (∀ i > 0, AddSubmonoid.ofClass (𝒜 i) ≤ P) ↔ ∀ i > 0, AddSubmonoid.ofClass (𝒜 i) ≤ P

Tactic:
]

Goal state after:
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
h✝ : ¬(weight w) x = m
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Free R M
φ : End R M
h : IsNilpotent φ
⊢ LinearMap.charpoly φ - X ^ finrank R M = 0

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Free R M
φ : End R M
h : IsNilpotent φ
⊢ LinearMap.charpoly φ - X ^ finrank R M = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Free R M
φ : End R M
h : IsNilpotent φ
⊢ IsNilpotent (LinearMap.charpoly φ - X ^ Fintype.card (ChooseBasisIndex R M))

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Free R M
φ : End R M
h : IsNilpotent φ
⊢ IsNilpotent (LinearMap.charpoly φ - X ^ Fintype.card (ChooseBasisIndex R M))
Module: Mathlib.LinearAlgebra.Eigenspace.Zero

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Free R M
φ : End R M
h : charpoly φ = X ^ finrank R M
⊢ 0 = 0

Tactic:
]

Goal state after: