Theorem: GalgHom.isHomogeneous'_aeval (DividedPowers/DPAlgebra/Misc.lean)

State before:
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
⊢ isHomogeneous' (MvPolynomial σ R) (weightedHomogeneousSubmodule R w) A 𝒜 (⇑φ) (aeval f)
Tactic:
intro i p hp
State after:
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : p ∈ weightedHomogeneousSubmodule R w i
⊢ (aeval f) p ∈ 𝒜 (φ i)

State before:
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : p ∈ weightedHomogeneousSubmodule R w i
⊢ (aeval f) p ∈ 𝒜 (φ i)
Tactic:
simp only [mem_weightedHomogeneousSubmodule, IsWeightedHomogeneous] at hp
State after:
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
⊢ (aeval f) p ∈ 𝒜 (φ i)

State before:
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
⊢ (aeval f) p ∈ 𝒜 (φ i)
Tactic:
rw [p.as_sum, map_sum]
State after:
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
⊢ ∑ x ∈ p.support, (aeval f) ((monomial x) (coeff x p)) ∈ 𝒜 (φ i)

State before:
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
⊢ ∑ x ∈ p.support, (aeval f) ((monomial x) (coeff x p)) ∈ 𝒜 (φ i)
Tactic:
apply Submodule.sum_mem
State after:
case a
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
⊢ ∀ c ∈ p.support, (aeval f) ((monomial c) (coeff c p)) ∈ 𝒜 (φ i)

State before:
case a
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
⊢ ∀ c ∈ p.support, (aeval f) ((monomial c) (coeff c p)) ∈ 𝒜 (φ i)
Tactic:
intro c hc
State after:
case a
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ (aeval f) ((monomial c) (coeff c p)) ∈ 𝒜 (φ i)

State before:
case a
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ (aeval f) ((monomial c) (coeff c p)) ∈ 𝒜 (φ i)
Tactic:
rw [aeval_monomial, ← smul_eq_mul, algebraMap_smul]
State after:
case a
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ (coeff c p • c.prod fun i k => f i ^ k) ∈ 𝒜 (φ i)

State before:
case a
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ (coeff c p • c.prod fun i k => f i ^ k) ∈ 𝒜 (φ i)
Tactic:
apply Submodule.smul_mem
State after:
case a.h
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ (c.prod fun i k => f i ^ k) ∈ 𝒜 (φ i)

State before:
case a.h
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ (c.prod fun i k => f i ^ k) ∈ 𝒜 (φ i)
Tactic:
convert Finsupp.prod.mem_grade 𝒜 c f _ fun s _ => h s
State after:
case h.e'_5.h.e'_1
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ φ i = c.sum fun s e => e • φ (w s)

State before:
case h.e'_5.h.e'_1
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ φ i = c.sum fun s e => e • φ (w s)
Tactic:
rw [← hp (mem_support_iff.mp hc), MvPolynomial.weightedDegree_apply]
State after:
case h.e'_5.h.e'_1
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ φ (c.sum fun i c => c • w i) = c.sum fun s e => e • φ (w s)

State before:
case h.e'_5.h.e'_1
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ φ (c.sum fun i c => c • w i) = c.sum fun s e => e • φ (w s)
Tactic:
rw [Finsupp.sum, map_sum, Finsupp.sum_of_support_subset _ le_rfl]
State after:
case h.e'_5.h.e'_1
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ ∑ x ∈ c.support, φ (c x • w x) = ∑ x ∈ c.support, c x • φ (w x)

case h.e'_5.h.e'_1.h
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ ∀ i ∈ c.support, 0 • φ (w i) = 0

State before:
case h.e'_5.h.e'_1
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ ∑ x ∈ c.support, φ (c x • w x) = ∑ x ∈ c.support, c x • φ (w x)

case h.e'_5.h.e'_1.h
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ ∀ i ∈ c.support, 0 • φ (w i) = 0
Tactic:
apply Finset.sum_congr rfl
State after:
case h.e'_5.h.e'_1
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ ∀ x ∈ c.support, φ (c x • w x) = c x • φ (w x)

case h.e'_5.h.e'_1.h
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ ∀ i ∈ c.support, 0 • φ (w i) = 0

State before:
case h.e'_5.h.e'_1
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ ∀ x ∈ c.support, φ (c x • w x) = c x • φ (w x)

case h.e'_5.h.e'_1.h
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ ∀ i ∈ c.support, 0 • φ (w i) = 0
Tactic:
. intro x _ ; simp only [map_nsmul]
State after:
case h.e'_5.h.e'_1.h
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ ∀ i ∈ c.support, 0 • φ (w i) = 0

State before:
case h.e'_5.h.e'_1.h
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ ∀ i ∈ c.support, 0 • φ (w i) = 0
Tactic:
. intro s _ ; simp only [zero_smul]
State after:
no goals

State before:
case h.e'_5.h.e'_1
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ ∀ x ∈ c.support, φ (c x • w x) = c x • φ (w x)
Tactic:
intro x _
State after:
case h.e'_5.h.e'_1
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
x : σ
a✝ : x ∈ c.support
⊢ φ (c x • w x) = c x • φ (w x)

State before:
case h.e'_5.h.e'_1
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
x : σ
a✝ : x ∈ c.support
⊢ φ (c x • w x) = c x • φ (w x)
Tactic:
simp only [map_nsmul]
State after:
no goals

State before:
case h.e'_5.h.e'_1.h
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
⊢ ∀ i ∈ c.support, 0 • φ (w i) = 0
Tactic:
intro s _
State after:
case h.e'_5.h.e'_1.h
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
s : σ
a✝ : s ∈ c.support
⊢ 0 • φ (w s) = 0

State before:
case h.e'_5.h.e'_1.h
R : Type u_5
inst✝⁸ : CommSemiring R
S : Type ?u.178387
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
σ : Type u_1
ι : Type u_2
κ : Type u_3
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
A : Type u_4
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
w : σ → ι
φ : ι →+ κ
f : σ → A
h : ∀ (s : σ), f s ∈ 𝒜 (φ (w s))
i : ι
p : MvPolynomial σ R
hp : ∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weightedDegree w) d = i
c : σ →₀ ℕ
hc : c ∈ p.support
s : σ
a✝ : s ∈ c.support
⊢ 0 • φ (w s) = 0
Tactic:
simp only [zero_smul]
State after:
no goals