Theorem: DividedPowerAlgebra.liftAux_isHomogeneous (DividedPowers/DPAlgebra/Graded/Basic.lean)

State before:
R : Type u_1
M : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : DecidableEq R
inst✝⁷ : DecidableEq M
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
𝒜 : ℕ → Submodule S A
inst✝ : GradedAlgebra 𝒜
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (x, y) => f (x, u) * f (y, v)
hf : ∀ (n : ℕ) (m : M), f (n, m) ∈ 𝒜 n
⊢ GalgHom.IsHomogeneous (grade R M) 𝒜 (lift' f hf_zero hf_smul hf_mul hf_add)
Tactic:
intro i a
State after:
R : Type u_1
M : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : DecidableEq R
inst✝⁷ : DecidableEq M
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
𝒜 : ℕ → Submodule S A
inst✝ : GradedAlgebra 𝒜
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (x, y) => f (x, u) * f (y, v)
hf : ∀ (n : ℕ) (m : M), f (n, m) ∈ 𝒜 n
i : ℕ
a : DividedPowerAlgebra R M
⊢ a ∈ grade R M i → (lift' f hf_zero hf_smul hf_mul hf_add) a ∈ 𝒜 i

State before:
R : Type u_1
M : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : DecidableEq R
inst✝⁷ : DecidableEq M
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
𝒜 : ℕ → Submodule S A
inst✝ : GradedAlgebra 𝒜
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (x, y) => f (x, u) * f (y, v)
hf : ∀ (n : ℕ) (m : M), f (n, m) ∈ 𝒜 n
i : ℕ
a : DividedPowerAlgebra R M
⊢ a ∈ grade R M i → (lift' f hf_zero hf_smul hf_mul hf_add) a ∈ 𝒜 i
Tactic:
simp only [mem_grade_iff]
State after:
R : Type u_1
M : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : DecidableEq R
inst✝⁷ : DecidableEq M
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
𝒜 : ℕ → Submodule S A
inst✝ : GradedAlgebra 𝒜
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (x, y) => f (x, u) * f (y, v)
hf : ∀ (n : ℕ) (m : M), f (n, m) ∈ 𝒜 n
i : ℕ
a : DividedPowerAlgebra R M
⊢ (∃ p ∈ weightedHomogeneousSubmodule R Prod.fst i, mk p = a) → (lift' f hf_zero hf_smul hf_mul hf_add) a ∈ 𝒜 i

State before:
R : Type u_1
M : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : DecidableEq R
inst✝⁷ : DecidableEq M
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
𝒜 : ℕ → Submodule S A
inst✝ : GradedAlgebra 𝒜
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (x, y) => f (x, u) * f (y, v)
hf : ∀ (n : ℕ) (m : M), f (n, m) ∈ 𝒜 n
i : ℕ
a : DividedPowerAlgebra R M
⊢ (∃ p ∈ weightedHomogeneousSubmodule R Prod.fst i, mk p = a) → (lift' f hf_zero hf_smul hf_mul hf_add) a ∈ 𝒜 i
Tactic:
rintro ⟨p, hp, rfl⟩
State after:
case intro.intro
R : Type u_1
M : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : DecidableEq R
inst✝⁷ : DecidableEq M
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
𝒜 : ℕ → Submodule S A
inst✝ : GradedAlgebra 𝒜
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (x, y) => f (x, u) * f (y, v)
hf : ∀ (n : ℕ) (m : M), f (n, m) ∈ 𝒜 n
i : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
⊢ (lift' f hf_zero hf_smul hf_mul hf_add) (mk p) ∈ 𝒜 i

State before:
case intro.intro
R : Type u_1
M : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : DecidableEq R
inst✝⁷ : DecidableEq M
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
𝒜 : ℕ → Submodule S A
inst✝ : GradedAlgebra 𝒜
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (x, y) => f (x, u) * f (y, v)
hf : ∀ (n : ℕ) (m : M), f (n, m) ∈ 𝒜 n
i : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
⊢ (lift' f hf_zero hf_smul hf_mul hf_add) (mk p) ∈ 𝒜 i
Tactic:
rw [lift'AlgHom_apply, p.as_sum, aeval_sum]
State after:
case intro.intro
R : Type u_1
M : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : DecidableEq R
inst✝⁷ : DecidableEq M
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
𝒜 : ℕ → Submodule S A
inst✝ : GradedAlgebra 𝒜
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (x, y) => f (x, u) * f (y, v)
hf : ∀ (n : ℕ) (m : M), f (n, m) ∈ 𝒜 n
i : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
⊢ ∑ i ∈ p.support, (aeval f) ((monomial i) (coeff i p)) ∈ 𝒜 i

State before:
case intro.intro
R : Type u_1
M : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : DecidableEq R
inst✝⁷ : DecidableEq M
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
𝒜 : ℕ → Submodule S A
inst✝ : GradedAlgebra 𝒜
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (x, y) => f (x, u) * f (y, v)
hf : ∀ (n : ℕ) (m : M), f (n, m) ∈ 𝒜 n
i : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
⊢ ∑ i ∈ p.support, (aeval f) ((monomial i) (coeff i p)) ∈ 𝒜 i
Tactic:
apply _root_.sum_mem
State after:
case intro.intro.h
R : Type u_1
M : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : DecidableEq R
inst✝⁷ : DecidableEq M
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
𝒜 : ℕ → Submodule S A
inst✝ : GradedAlgebra 𝒜
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (x, y) => f (x, u) * f (y, v)
hf : ∀ (n : ℕ) (m : M), f (n, m) ∈ 𝒜 n
i : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
⊢ ∀ c ∈ p.support, (aeval f) ((monomial c) (coeff c p)) ∈ 𝒜 i

State before:
case intro.intro.h
R : Type u_1
M : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : DecidableEq R
inst✝⁷ : DecidableEq M
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
𝒜 : ℕ → Submodule S A
inst✝ : GradedAlgebra 𝒜
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (x, y) => f (x, u) * f (y, v)
hf : ∀ (n : ℕ) (m : M), f (n, m) ∈ 𝒜 n
i : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
⊢ ∀ c ∈ p.support, (aeval f) ((monomial c) (coeff c p)) ∈ 𝒜 i
Tactic:
intro c hc
State after:
case intro.intro.h
R : Type u_1
M : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : DecidableEq R
inst✝⁷ : DecidableEq M
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
𝒜 : ℕ → Submodule S A
inst✝ : GradedAlgebra 𝒜
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (x, y) => f (x, u) * f (y, v)
hf : ∀ (n : ℕ) (m : M), f (n, m) ∈ 𝒜 n
i : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
c : ℕ × M →₀ ℕ
hc : c ∈ p.support
⊢ (aeval f) ((monomial c) (coeff c p)) ∈ 𝒜 i

State before:
case intro.intro.h
R : Type u_1
M : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : DecidableEq R
inst✝⁷ : DecidableEq M
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
𝒜 : ℕ → Submodule S A
inst✝ : GradedAlgebra 𝒜
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (x, y) => f (x, u) * f (y, v)
hf : ∀ (n : ℕ) (m : M), f (n, m) ∈ 𝒜 n
i : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
c : ℕ × M →₀ ℕ
hc : c ∈ p.support
⊢ (aeval f) ((monomial c) (coeff c p)) ∈ 𝒜 i
Tactic:
rw [aeval_monomial, ← smul_eq_mul, algebraMap_smul A, algebra_compatible_smul S (coeff c p)]
State after:
case intro.intro.h
R : Type u_1
M : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : DecidableEq R
inst✝⁷ : DecidableEq M
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
𝒜 : ℕ → Submodule S A
inst✝ : GradedAlgebra 𝒜
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (x, y) => f (x, u) * f (y, v)
hf : ∀ (n : ℕ) (m : M), f (n, m) ∈ 𝒜 n
i : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
c : ℕ × M →₀ ℕ
hc : c ∈ p.support
⊢ ((algebraMap R S) (coeff c p) • c.prod fun i k => f i ^ k) ∈ 𝒜 i

State before:
case intro.intro.h
R : Type u_1
M : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : DecidableEq R
inst✝⁷ : DecidableEq M
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
𝒜 : ℕ → Submodule S A
inst✝ : GradedAlgebra 𝒜
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (x, y) => f (x, u) * f (y, v)
hf : ∀ (n : ℕ) (m : M), f (n, m) ∈ 𝒜 n
i : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
c : ℕ × M →₀ ℕ
hc : c ∈ p.support
⊢ ((algebraMap R S) (coeff c p) • c.prod fun i k => f i ^ k) ∈ 𝒜 i
Tactic:
apply Submodule.smul_mem
State after:
case intro.intro.h.h
R : Type u_1
M : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : DecidableEq R
inst✝⁷ : DecidableEq M
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
𝒜 : ℕ → Submodule S A
inst✝ : GradedAlgebra 𝒜
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (x, y) => f (x, u) * f (y, v)
hf : ∀ (n : ℕ) (m : M), f (n, m) ∈ 𝒜 n
i : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
c : ℕ × M →₀ ℕ
hc : c ∈ p.support
⊢ (c.prod fun i k => f i ^ k) ∈ 𝒜 i

State before:
case intro.intro.h.h
R : Type u_1
M : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : DecidableEq R
inst✝⁷ : DecidableEq M
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
𝒜 : ℕ → Submodule S A
inst✝ : GradedAlgebra 𝒜
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (x, y) => f (x, u) * f (y, v)
hf : ∀ (n : ℕ) (m : M), f (n, m) ∈ 𝒜 n
i : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
c : ℕ × M →₀ ℕ
hc : c ∈ p.support
⊢ (c.prod fun i k => f i ^ k) ∈ 𝒜 i
Tactic:
rw [← hp (mem_support_iff.mp hc)]
State after:
case intro.intro.h.h
R : Type u_1
M : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : DecidableEq R
inst✝⁷ : DecidableEq M
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
𝒜 : ℕ → Submodule S A
inst✝ : GradedAlgebra 𝒜
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (x, y) => f (x, u) * f (y, v)
hf : ∀ (n : ℕ) (m : M), f (n, m) ∈ 𝒜 n
i : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
c : ℕ × M →₀ ℕ
hc : c ∈ p.support
⊢ (c.prod fun i k => f i ^ k) ∈ 𝒜 ((weightedDegree Prod.fst) c)

State before:
case intro.intro.h.h
R : Type u_1
M : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : DecidableEq R
inst✝⁷ : DecidableEq M
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
A : Type u_4
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
𝒜 : ℕ → Submodule S A
inst✝ : GradedAlgebra 𝒜
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ antidiagonal n,
        match x with
        | (x, y) => f (x, u) * f (y, v)
hf : ∀ (n : ℕ) (m : M), f (n, m) ∈ 𝒜 n
i : ℕ
p : MvPolynomial (ℕ × M) R
hp : p ∈ weightedHomogeneousSubmodule R Prod.fst i
c : ℕ × M →₀ ℕ
hc : c ∈ p.support
⊢ (c.prod fun i k => f i ^ k) ∈ 𝒜 ((weightedDegree Prod.fst) c)
Tactic:
exact Finsupp.prod.mem_grade _ _ _ _ fun ⟨n, m⟩ _ => hf n m
State after:
no goals