Theorem: DividedPowerAlgebra.rel_isPureHomogeneous (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
⊢ Rel.IsPureHomogeneous (weightedHomogeneousSubmodule R Prod.fst) (Rel R M)
Tactic:
intro a b h
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
a b : MvPolynomial (ℕ × M) R
h : Rel R M a b
⊢ ∃ i, a ∈ weightedHomogeneousSubmodule R Prod.fst i ∧ b ∈ weightedHomogeneousSubmodule R Prod.fst 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
a b : MvPolynomial (ℕ × M) R
h : Rel R M a b
⊢ ∃ i, a ∈ weightedHomogeneousSubmodule R Prod.fst i ∧ b ∈ weightedHomogeneousSubmodule R Prod.fst i
Tactic:
cases' h with a r n a m n a n a b
State after:
case rfl_zero
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ ∃ i, 0 ∈ weightedHomogeneousSubmodule R Prod.fst i ∧ 0 ∈ weightedHomogeneousSubmodule R Prod.fst i

case zero
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
a : M
⊢ ∃ i, X (0, a) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧ 1 ∈ weightedHomogeneousSubmodule R Prod.fst i

case smul
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
n : ℕ
a : M
⊢ ∃ i,
    X (n, r • a) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      r ^ n • X (n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i

case mul
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
m n : ℕ
a : M
⊢ ∃ i,
    X (m, a) * X (n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      (m + n).choose m • X (m + n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i

case add
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
a b : M
⊢ ∃ i,
    X (n, a + b) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      ∑ k ∈ antidiagonal n, X (k.1, a) * X (k.2, b) ∈ weightedHomogeneousSubmodule R Prod.fst i

State before:
case rfl_zero
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ ∃ i, 0 ∈ weightedHomogeneousSubmodule R Prod.fst i ∧ 0 ∈ weightedHomogeneousSubmodule R Prod.fst i

case zero
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
a : M
⊢ ∃ i, X (0, a) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧ 1 ∈ weightedHomogeneousSubmodule R Prod.fst i

case smul
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
n : ℕ
a : M
⊢ ∃ i,
    X (n, r • a) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      r ^ n • X (n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i

case mul
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
m n : ℕ
a : M
⊢ ∃ i,
    X (m, a) * X (n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      (m + n).choose m • X (m + n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i

case add
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
a b : M
⊢ ∃ i,
    X (n, a + b) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      ∑ k ∈ antidiagonal n, X (k.1, a) * X (k.2, b) ∈ weightedHomogeneousSubmodule R Prod.fst i
Tactic:
. exact ⟨0, zero_mem _, zero_mem _⟩
State after:
case zero
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
a : M
⊢ ∃ i, X (0, a) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧ 1 ∈ weightedHomogeneousSubmodule R Prod.fst i

case smul
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
n : ℕ
a : M
⊢ ∃ i,
    X (n, r • a) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      r ^ n • X (n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i

case mul
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
m n : ℕ
a : M
⊢ ∃ i,
    X (m, a) * X (n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      (m + n).choose m • X (m + n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i

case add
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
a b : M
⊢ ∃ i,
    X (n, a + b) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      ∑ k ∈ antidiagonal n, X (k.1, a) * X (k.2, b) ∈ weightedHomogeneousSubmodule R Prod.fst i

State before:
case zero
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
a : M
⊢ ∃ i, X (0, a) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧ 1 ∈ weightedHomogeneousSubmodule R Prod.fst i

case smul
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
n : ℕ
a : M
⊢ ∃ i,
    X (n, r • a) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      r ^ n • X (n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i

case mul
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
m n : ℕ
a : M
⊢ ∃ i,
    X (m, a) * X (n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      (m + n).choose m • X (m + n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i

case add
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
a b : M
⊢ ∃ i,
    X (n, a + b) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      ∑ k ∈ antidiagonal n, X (k.1, a) * X (k.2, b) ∈ weightedHomogeneousSubmodule R Prod.fst i
Tactic:
. use 0
  simp only [mem_weightedHomogeneousSubmodule, isWeightedHomogeneous_X,
    isWeightedHomogeneous_one, and_self]
State after:
case smul
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
n : ℕ
a : M
⊢ ∃ i,
    X (n, r • a) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      r ^ n • X (n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i

case mul
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
m n : ℕ
a : M
⊢ ∃ i,
    X (m, a) * X (n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      (m + n).choose m • X (m + n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i

case add
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
a b : M
⊢ ∃ i,
    X (n, a + b) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      ∑ k ∈ antidiagonal n, X (k.1, a) * X (k.2, b) ∈ weightedHomogeneousSubmodule R Prod.fst i

State before:
case smul
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
n : ℕ
a : M
⊢ ∃ i,
    X (n, r • a) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      r ^ n • X (n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i

case mul
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
m n : ℕ
a : M
⊢ ∃ i,
    X (m, a) * X (n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      (m + n).choose m • X (m + n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i

case add
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
a b : M
⊢ ∃ i,
    X (n, a + b) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      ∑ k ∈ antidiagonal n, X (k.1, a) * X (k.2, b) ∈ weightedHomogeneousSubmodule R Prod.fst i
Tactic:
. use n
  simp only [mem_weightedHomogeneousSubmodule, isWeightedHomogeneous_X,
    Submodule.smul_mem, and_self]
State after:
case mul
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
m n : ℕ
a : M
⊢ ∃ i,
    X (m, a) * X (n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      (m + n).choose m • X (m + n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i

case add
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
a b : M
⊢ ∃ i,
    X (n, a + b) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      ∑ k ∈ antidiagonal n, X (k.1, a) * X (k.2, b) ∈ weightedHomogeneousSubmodule R Prod.fst i

State before:
case mul
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
m n : ℕ
a : M
⊢ ∃ i,
    X (m, a) * X (n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      (m + n).choose m • X (m + n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i

case add
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
a b : M
⊢ ∃ i,
    X (n, a + b) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      ∑ k ∈ antidiagonal n, X (k.1, a) * X (k.2, b) ∈ weightedHomogeneousSubmodule R Prod.fst i
Tactic:
. use m + n
  exact ⟨IsWeightedHomogeneous.mul (isWeightedHomogeneous_X _ _ _)
    (isWeightedHomogeneous_X _ _ _), nsmul_mem ((mem_weightedHomogeneousSubmodule _ _ _ _).mpr
    (isWeightedHomogeneous_X _ _ _)) _⟩
State after:
case add
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
a b : M
⊢ ∃ i,
    X (n, a + b) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      ∑ k ∈ antidiagonal n, X (k.1, a) * X (k.2, b) ∈ weightedHomogeneousSubmodule R Prod.fst i

State before:
case add
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
a b : M
⊢ ∃ i,
    X (n, a + b) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      ∑ k ∈ antidiagonal n, X (k.1, a) * X (k.2, b) ∈ weightedHomogeneousSubmodule R Prod.fst i
Tactic:
. use n
  refine' ⟨(mem_weightedHomogeneousSubmodule _ _ _ _).mpr (isWeightedHomogeneous_X _ _ _), _⟩
  . apply Submodule.sum_mem
    intro (c, d) hcd
    simp only [mem_antidiagonal] at hcd
    rw [← hcd]
    apply IsWeightedHomogeneous.mul <;> simp only [isWeightedHomogeneous_X]
State after:
no goals

State before:
case rfl_zero
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
⊢ ∃ i, 0 ∈ weightedHomogeneousSubmodule R Prod.fst i ∧ 0 ∈ weightedHomogeneousSubmodule R Prod.fst i
Tactic:
exact ⟨0, zero_mem _, zero_mem _⟩
State after:
no goals

State before:
case zero
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
a : M
⊢ ∃ i, X (0, a) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧ 1 ∈ weightedHomogeneousSubmodule R Prod.fst i
Tactic:
use 0
State after:
case 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
a : M
⊢ X (0, a) ∈ weightedHomogeneousSubmodule R Prod.fst 0 ∧ 1 ∈ weightedHomogeneousSubmodule R Prod.fst 0

State before:
case 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
a : M
⊢ X (0, a) ∈ weightedHomogeneousSubmodule R Prod.fst 0 ∧ 1 ∈ weightedHomogeneousSubmodule R Prod.fst 0
Tactic:
simp only [mem_weightedHomogeneousSubmodule, isWeightedHomogeneous_X,
  isWeightedHomogeneous_one, and_self]
State after:
no goals

State before:
case smul
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
r : R
n : ℕ
a : M
⊢ ∃ i,
    X (n, r • a) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      r ^ n • X (n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i
Tactic:
use n
State after:
case 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
r : R
n : ℕ
a : M
⊢ X (n, r • a) ∈ weightedHomogeneousSubmodule R Prod.fst n ∧
    r ^ n • X (n, a) ∈ weightedHomogeneousSubmodule R Prod.fst n

State before:
case 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
r : R
n : ℕ
a : M
⊢ X (n, r • a) ∈ weightedHomogeneousSubmodule R Prod.fst n ∧
    r ^ n • X (n, a) ∈ weightedHomogeneousSubmodule R Prod.fst n
Tactic:
simp only [mem_weightedHomogeneousSubmodule, isWeightedHomogeneous_X,
  Submodule.smul_mem, and_self]
State after:
no goals

State before:
case mul
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
m n : ℕ
a : M
⊢ ∃ i,
    X (m, a) * X (n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      (m + n).choose m • X (m + n, a) ∈ weightedHomogeneousSubmodule R Prod.fst i
Tactic:
use m + n
State after:
case 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
m n : ℕ
a : M
⊢ X (m, a) * X (n, a) ∈ weightedHomogeneousSubmodule R Prod.fst (m + n) ∧
    (m + n).choose m • X (m + n, a) ∈ weightedHomogeneousSubmodule R Prod.fst (m + n)

State before:
case 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
m n : ℕ
a : M
⊢ X (m, a) * X (n, a) ∈ weightedHomogeneousSubmodule R Prod.fst (m + n) ∧
    (m + n).choose m • X (m + n, a) ∈ weightedHomogeneousSubmodule R Prod.fst (m + n)
Tactic:
exact ⟨IsWeightedHomogeneous.mul (isWeightedHomogeneous_X _ _ _)
  (isWeightedHomogeneous_X _ _ _), nsmul_mem ((mem_weightedHomogeneousSubmodule _ _ _ _).mpr
  (isWeightedHomogeneous_X _ _ _)) _⟩
State after:
no goals

State before:
case add
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
a b : M
⊢ ∃ i,
    X (n, a + b) ∈ weightedHomogeneousSubmodule R Prod.fst i ∧
      ∑ k ∈ antidiagonal n, X (k.1, a) * X (k.2, b) ∈ weightedHomogeneousSubmodule R Prod.fst i
Tactic:
use n
State after:
case 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
n : ℕ
a b : M
⊢ X (n, a + b) ∈ weightedHomogeneousSubmodule R Prod.fst n ∧
    ∑ k ∈ antidiagonal n, X (k.1, a) * X (k.2, b) ∈ weightedHomogeneousSubmodule R Prod.fst n

State before:
case 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
n : ℕ
a b : M
⊢ X (n, a + b) ∈ weightedHomogeneousSubmodule R Prod.fst n ∧
    ∑ k ∈ antidiagonal n, X (k.1, a) * X (k.2, b) ∈ weightedHomogeneousSubmodule R Prod.fst n
Tactic:
refine' ⟨(mem_weightedHomogeneousSubmodule _ _ _ _).mpr (isWeightedHomogeneous_X _ _ _), _⟩
State after:
case 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
n : ℕ
a b : M
⊢ ∑ k ∈ antidiagonal n, X (k.1, a) * X (k.2, b) ∈ weightedHomogeneousSubmodule R Prod.fst n

State before:
case 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
n : ℕ
a b : M
⊢ ∑ k ∈ antidiagonal n, X (k.1, a) * X (k.2, b) ∈ weightedHomogeneousSubmodule R Prod.fst n
Tactic:
. apply Submodule.sum_mem
  intro (c, d) hcd
  simp only [mem_antidiagonal] at hcd
  rw [← hcd]
  apply IsWeightedHomogeneous.mul <;> simp only [isWeightedHomogeneous_X]
State after:
no goals

State before:
case 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
n : ℕ
a b : M
⊢ ∑ k ∈ antidiagonal n, X (k.1, a) * X (k.2, b) ∈ weightedHomogeneousSubmodule R Prod.fst n
Tactic:
apply Submodule.sum_mem
State after:
case h.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
a b : M
⊢ ∀ c ∈ antidiagonal n, X (c.1, a) * X (c.2, b) ∈ weightedHomogeneousSubmodule R Prod.fst n

State before:
case h.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
a b : M
⊢ ∀ c ∈ antidiagonal n, X (c.1, a) * X (c.2, b) ∈ weightedHomogeneousSubmodule R Prod.fst n
Tactic:
intro (c, d) hcd
State after:
case h.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
a b : M
c d : ℕ
hcd : (c, d) ∈ antidiagonal n
⊢ X ((c, d).1, a) * X ((c, d).2, b) ∈ weightedHomogeneousSubmodule R Prod.fst n

State before:
case h.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
a b : M
c d : ℕ
hcd : (c, d) ∈ antidiagonal n
⊢ X ((c, d).1, a) * X ((c, d).2, b) ∈ weightedHomogeneousSubmodule R Prod.fst n
Tactic:
simp only [mem_antidiagonal] at hcd
State after:
case h.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
a b : M
c d : ℕ
hcd : c + d = n
⊢ X ((c, d).1, a) * X ((c, d).2, b) ∈ weightedHomogeneousSubmodule R Prod.fst n

State before:
case h.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
a b : M
c d : ℕ
hcd : c + d = n
⊢ X ((c, d).1, a) * X ((c, d).2, b) ∈ weightedHomogeneousSubmodule R Prod.fst n
Tactic:
rw [← hcd]
State after:
case h.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
a b : M
c d : ℕ
hcd : c + d = n
⊢ X ((c, d).1, a) * X ((c, d).2, b) ∈ weightedHomogeneousSubmodule R Prod.fst (c + d)

State before:
case h.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
n : ℕ
a b : M
c d : ℕ
hcd : c + d = n
⊢ X ((c, d).1, a) * X ((c, d).2, b) ∈ weightedHomogeneousSubmodule R Prod.fst (c + d)
Tactic:
apply IsWeightedHomogeneous.mul <;> simp only [isWeightedHomogeneous_X]
State after:
no goals