internlm/Lean-Github huggingface dataset:
Theorem: GalgHom.isHomogeneous'_aeval
Proof 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
Proof 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
Theorem: GalgHom.isHomogeneous'_aeval
Proof 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]
Proof 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
Theorem: GalgHom.isHomogeneous'_aeval
Proof 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]
Proof state after:
no goals
Theorem: GalgHom.isHomogeneous'_aeval
Proof 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 _
Proof 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)
Theorem: GalgHom.isHomogeneous'_aeval
Proof 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]
Proof state after:
no goals
Theorem: GalgHom.isHomogeneous'_aeval
Proof 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 _
Proof 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
Theorem: GalgHom.isHomogeneous'_aeval
Proof 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]
Proof state after:
no goals
Theorem: MvPolynomial.vars_X_subset
Proof state before:
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
⊢ (X n).vars ⊆ {n}
Tactic:
intro u
Proof state after:
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
⊢ u ∈ (X n).vars → u ∈ {n}
Theorem: MvPolynomial.vars_X_subset
Proof state before:
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
⊢ u ∈ (X n).vars → u ∈ {n}
Tactic:
rw [X, mem_vars, mem_singleton]
Proof state after:
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
⊢ (∃ d ∈ ((monomial (Finsupp.single n 1)) 1).support, u ∈ d.support) → u = n
Theorem: MvPolynomial.vars_X_subset
Proof state before:
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
⊢ (∃ d ∈ ((monomial (Finsupp.single n 1)) 1).support, u ∈ d.support) → u = n
Tactic:
rintro ⟨c, hc, hc'⟩
Proof state after:
case intro.intro
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : c ∈ ((monomial (Finsupp.single n 1)) 1).support
hc' : u ∈ c.support
⊢ u = n
Theorem: MvPolynomial.vars_X_subset
Proof state before:
case intro.intro
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : c ∈ ((monomial (Finsupp.single n 1)) 1).support
hc' : u ∈ c.support
⊢ u = n
Tactic:
by_contra h'
Proof state after:
case intro.intro
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : c ∈ ((monomial (Finsupp.single n 1)) 1).support
hc' : u ∈ c.support
h' : ¬u = n
⊢ False
Theorem: MvPolynomial.vars_X_subset
Proof state before:
case intro.intro
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : c ∈ ((monomial (Finsupp.single n 1)) 1).support
hc' : u ∈ c.support
h' : ¬u = n
⊢ False
Tactic:
rw [mem_support_iff, coeff_monomial, ne_eq] at hc
Proof state after:
case intro.intro
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : ¬(if Finsupp.single n 1 = c then 1 else 0) = 0
hc' : u ∈ c.support
h' : ¬u = n
⊢ False
Theorem: MvPolynomial.vars_X_subset
Proof state before:
case intro.intro
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : ¬(if Finsupp.single n 1 = c then 1 else 0) = 0
hc' : u ∈ c.support
h' : ¬u = n
⊢ False
Tactic:
by_cases h : Finsupp.single n 1 = c
Proof state after:
case pos
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : ¬(if Finsupp.single n 1 = c then 1 else 0) = 0
hc' : u ∈ c.support
h' : ¬u = n
h : Finsupp.single n 1 = c
⊢ False

case neg
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : ¬(if Finsupp.single n 1 = c then 1 else 0) = 0
hc' : u ∈ c.support
h' : ¬u = n
h : ¬Finsupp.single n 1 = c
⊢ False
Theorem: MvPolynomial.vars_X_subset
Proof state before:
case pos
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : ¬(if Finsupp.single n 1 = c then 1 else 0) = 0
hc' : u ∈ c.support
h' : ¬u = n
h : Finsupp.single n 1 = c
⊢ False
Tactic:
rw [← h, Finsupp.mem_support_iff, ne_eq, Finsupp.single_apply] at hc'
Proof state after:
case pos
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : ¬(if Finsupp.single n 1 = c then 1 else 0) = 0
hc' : ¬(if n = u then 1 else 0) = 0
h' : ¬u = n
h : Finsupp.single n 1 = c
⊢ False
Theorem: MvPolynomial.vars_X_subset
Proof state before:
case pos
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : ¬(if Finsupp.single n 1 = c then 1 else 0) = 0
hc' : ¬(if n = u then 1 else 0) = 0
h' : ¬u = n
h : Finsupp.single n 1 = c
⊢ False
Tactic:
apply hc'
Proof state after:
case pos
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : ¬(if Finsupp.single n 1 = c then 1 else 0) = 0
hc' : ¬(if n = u then 1 else 0) = 0
h' : ¬u = n
h : Finsupp.single n 1 = c
⊢ (if n = u then 1 else 0) = 0
Theorem: MvPolynomial.vars_X_subset
Proof state before:
case pos
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : ¬(if Finsupp.single n 1 = c then 1 else 0) = 0
hc' : ¬(if n = u then 1 else 0) = 0
h' : ¬u = n
h : Finsupp.single n 1 = c
⊢ (if n = u then 1 else 0) = 0
Tactic:
rw [if_neg (Ne.symm h')]
Proof state after:
no goals
Theorem: MvPolynomial.vars_X_subset
Proof state before:
case neg
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : ¬(if Finsupp.single n 1 = c then 1 else 0) = 0
hc' : u ∈ c.support
h' : ¬u = n
h : ¬Finsupp.single n 1 = c
⊢ False
Tactic:
apply hc
Proof state after:
case neg
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : ¬(if Finsupp.single n 1 = c then 1 else 0) = 0
hc' : u ∈ c.support
h' : ¬u = n
h : ¬Finsupp.single n 1 = c
⊢ (if Finsupp.single n 1 = c then 1 else 0) = 0
Theorem: MvPolynomial.vars_X_subset
Proof state before:
case neg
R : Type u_1
σ : Type u_2
n : σ
inst✝ : CommSemiring R
u : σ
c : σ →₀ ℕ
hc : ¬(if Finsupp.single n 1 = c then 1 else 0) = 0
hc' : u ∈ c.support
h' : ¬u = n
h : ¬Finsupp.single n 1 = c
⊢ (if Finsupp.single n 1 = c then 1 else 0) = 0
Tactic:
rw [if_neg h]
Proof state after:
no goals
Theorem: variable_mem_supported
Proof state before:
R : Type u_2
M : Type u_1
inst✝ : CommSemiring R
nm : ℕ × M
hn : 0 < nm.1
⊢ X nm ∈ supported R {nm | 0 < nm.1}
Tactic:
rw [mem_supported]
Proof state after:
R : Type u_2
M : Type u_1
inst✝ : CommSemiring R
nm : ℕ × M
hn : 0 < nm.1
⊢ ↑(X nm).vars ⊆ {nm | 0 < nm.1}
Theorem: variable_mem_supported
Proof state before:
R : Type u_2
M : Type u_1
inst✝ : CommSemiring R
nm : ℕ × M
hn : 0 < nm.1
⊢ ↑(X nm).vars ⊆ {nm | 0 < nm.1}
Tactic:
refine' Set.Subset.trans (Finset.coe_subset.mpr (vars_X_subset nm)) _
Proof state after:
R : Type u_2
M : Type u_1
inst✝ : CommSemiring R
nm : ℕ × M
hn : 0 < nm.1
⊢ ↑{nm} ⊆ {nm | 0 < nm.1}
Theorem: variable_mem_supported
Proof state before:
R : Type u_2
M : Type u_1
inst✝ : CommSemiring R
nm : ℕ × M
hn : 0 < nm.1
⊢ ↑{nm} ⊆ {nm | 0 < nm.1}
Tactic:
rw [coe_singleton, Set.singleton_subset_iff, Set.mem_setOf_eq]
Proof state after:
R : Type u_2
M : Type u_1
inst✝ : CommSemiring R
nm : ℕ × M
hn : 0 < nm.1
⊢ 0 < nm.1
Theorem: variable_mem_supported
Proof state before:
R : Type u_2
M : Type u_1
inst✝ : CommSemiring R
nm : ℕ × M
hn : 0 < nm.1
⊢ 0 < nm.1
Tactic:
exact hn
Proof state after:
no goals
Theorem: toSupported_isHomogeneous'
Proof state before:
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
⊢ GalgHom.isHomogeneous' (MvPolynomial (ℕ × M) R) (weightedHomogeneousSubmodule R Prod.fst) (MvPolynomial (ℕ × M) R)
    (weightedHomogeneousSubmodule R Prod.fst) id ((supported R {nm | 0 < nm.1}).val.comp (toSupported R))
Tactic:
have heq : aeval
  ((supported R {nm : ℕ × M | 0 < nm.fst}).val.toFun ∘
      fun nm : ℕ × M =>
        if h : 0 < nm.fst
        then ⟨X nm, variable_mem_supported R nm h⟩
        else 1) =
    (supported R {nm : ℕ × M | 0 < nm.fst}).val.comp (toSupported R) :=
  by
  apply MvPolynomial.algHom_ext
  intro nm
  simp only [toSupported, AlgHom.toFun_eq_coe, Function.comp_apply, AlgHom.coe_comp, aeval_X]
Proof state after:
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
⊢ GalgHom.isHomogeneous' (MvPolynomial (ℕ × M) R) (weightedHomogeneousSubmodule R Prod.fst) (MvPolynomial (ℕ × M) R)
    (weightedHomogeneousSubmodule R Prod.fst) id ((supported R {nm | 0 < nm.1}).val.comp (toSupported R))
Theorem: toSupported_isHomogeneous'
Proof state before:
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
⊢ GalgHom.isHomogeneous' (MvPolynomial (ℕ × M) R) (weightedHomogeneousSubmodule R Prod.fst) (MvPolynomial (ℕ × M) R)
    (weightedHomogeneousSubmodule R Prod.fst) id ((supported R {nm | 0 < nm.1}).val.comp (toSupported R))
Tactic:
rw [← heq]
Proof state after:
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
⊢ GalgHom.isHomogeneous' (MvPolynomial (ℕ × M) R) (weightedHomogeneousSubmodule R Prod.fst) (MvPolynomial (ℕ × M) R)
    (weightedHomogeneousSubmodule R Prod.fst) id
    (aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1))
Theorem: toSupported_isHomogeneous'
Proof state before:
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
⊢ GalgHom.isHomogeneous' (MvPolynomial (ℕ × M) R) (weightedHomogeneousSubmodule R Prod.fst) (MvPolynomial (ℕ × M) R)
    (weightedHomogeneousSubmodule R Prod.fst) id
    (aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1))
Tactic:
apply GalgHom.isHomogeneous'_aeval (ℕ × M) (MvPolynomial (ℕ × M) R)
  (weightedHomogeneousSubmodule R Prod.fst) Prod.fst (AddMonoidHom.id ℕ)
Proof state after:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
⊢ ∀ (s : ℕ × M),
    ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) s ∈
      weightedHomogeneousSubmodule R Prod.fst ((AddMonoidHom.id ℕ) s.1)
Theorem: toSupported_isHomogeneous'
Proof state before:
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
⊢ aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
Tactic:
apply MvPolynomial.algHom_ext
Proof state after:
case hf
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
⊢ ∀ (i : ℕ × M),
    (aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1))
        (X i) =
      ((supported R {nm | 0 < nm.1}).val.comp (toSupported R)) (X i)
Theorem: toSupported_isHomogeneous'
Proof state before:
case hf
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
⊢ ∀ (i : ℕ × M),
    (aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1))
        (X i) =
      ((supported R {nm | 0 < nm.1}).val.comp (toSupported R)) (X i)
Tactic:
intro nm
Proof state after:
case hf
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
nm : ℕ × M
⊢ (aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1))
      (X nm) =
    ((supported R {nm | 0 < nm.1}).val.comp (toSupported R)) (X nm)
Theorem: toSupported_isHomogeneous'
Proof state before:
case hf
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
nm : ℕ × M
⊢ (aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1))
      (X nm) =
    ((supported R {nm | 0 < nm.1}).val.comp (toSupported R)) (X nm)
Tactic:
simp only [toSupported, AlgHom.toFun_eq_coe, Function.comp_apply, AlgHom.coe_comp, aeval_X]
Proof state after:
no goals
Theorem: toSupported_isHomogeneous'
Proof state before:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
⊢ ∀ (s : ℕ × M),
    ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) s ∈
      weightedHomogeneousSubmodule R Prod.fst ((AddMonoidHom.id ℕ) s.1)
Tactic:
intro nm
Proof state after:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
nm : ℕ × M
⊢ ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) nm ∈
    weightedHomogeneousSubmodule R Prod.fst ((AddMonoidHom.id ℕ) nm.1)
Theorem: toSupported_isHomogeneous'
Proof state before:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
nm : ℕ × M
⊢ ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) nm ∈
    weightedHomogeneousSubmodule R Prod.fst ((AddMonoidHom.id ℕ) nm.1)
Tactic:
simp only [mem_weightedHomogeneousSubmodule, AlgHom.toFun_eq_coe, Subalgebra.coe_val,
  Function.comp_apply, AddMonoidHom.id_apply]
Proof state after:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
nm : ℕ × M
⊢ IsWeightedHomogeneous Prod.fst (↑(if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1)) nm.1
Theorem: toSupported_isHomogeneous'
Proof state before:
case h
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
nm : ℕ × M
⊢ IsWeightedHomogeneous Prod.fst (↑(if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1)) nm.1
Tactic:
split_ifs with h
Proof state after:
case pos
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
nm : ℕ × M
h : 0 < nm.1
⊢ IsWeightedHomogeneous Prod.fst (↑⟨X nm, ⋯⟩) nm.1

case neg
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
nm : ℕ × M
h : ¬0 < nm.1
⊢ IsWeightedHomogeneous Prod.fst (↑1) nm.1
Theorem: toSupported_isHomogeneous'
Proof state before:
case pos
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq M
inst✝ : DecidableEq R
heq :
  aeval ((↑↑(supported R {nm | 0 < nm.1}).val.toRingHom).toFun ∘ fun nm => if h : 0 < nm.1 then ⟨X nm, ⋯⟩ else 1) =
    (supported R {nm | 0 < nm.1}).val.comp (toSupported R)
nm : ℕ × M
h : 0 < nm.1
⊢ IsWeightedHomogeneous Prod.fst (↑⟨X nm, ⋯⟩) nm.1
Tactic:
apply isWeightedHomogeneous_X
Proof state after:
no goals