internlm/Lean-Github huggingface dataset:
Theorem: PolynomialMap.finsupp_polynomialMap_of_coeff
Proof state before:
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
f : M →ₚ[R] N
⊢ Finsupp.polynomialMap b ((coeff ⇑b) f) = f
Tactic:
apply coeff_injective (DFunLike.coe b)
Proof state after:
case hm
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
f : M →ₚ[R] N
⊢ Submodule.span R (Set.range ⇑b) = ⊤

case h
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
f : M →ₚ[R] N
⊢ (coeff ⇑b) (Finsupp.polynomialMap b ((coeff ⇑b) f)) = (coeff ⇑b) f
Theorem: PolynomialMap.finsupp_polynomialMap_of_coeff
Proof state before:
case hm
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
f : M →ₚ[R] N
⊢ Submodule.span R (Set.range ⇑b) = ⊤
Tactic:
rw [_root_.eq_top_iff]
Proof state after:
case hm
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
f : M →ₚ[R] N
⊢ ⊤ ≤ Submodule.span R (Set.range ⇑b)
Theorem: PolynomialMap.finsupp_polynomialMap_of_coeff
Proof state before:
case hm
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
f : M →ₚ[R] N
⊢ ⊤ ≤ Submodule.span R (Set.range ⇑b)
Tactic:
intro m _
Proof state after:
case hm
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
f : M →ₚ[R] N
m : M
a✝ : m ∈ ⊤
⊢ m ∈ Submodule.span R (Set.range ⇑b)
Theorem: PolynomialMap.finsupp_polynomialMap_of_coeff
Proof state before:
case hm
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
f : M →ₚ[R] N
m : M
a✝ : m ∈ ⊤
⊢ m ∈ Submodule.span R (Set.range ⇑b)
Tactic:
apply Submodule.span_mono _ (Basis.mem_span_repr_support b m)
Proof state after:
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
f : M →ₚ[R] N
m : M
a✝ : m ∈ ⊤
⊢ ⇑b '' ↑(b.repr m).support ⊆ Set.range ⇑b
Theorem: PolynomialMap.finsupp_polynomialMap_of_coeff
Proof state before:
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
f : M →ₚ[R] N
m : M
a✝ : m ∈ ⊤
⊢ ⇑b '' ↑(b.repr m).support ⊆ Set.range ⇑b
Tactic:
apply Set.image_subset_range
Proof state after:
no goals
Theorem: PolynomialMap.finsupp_polynomialMap_of_coeff
Proof state before:
case h
R : Type u
inst✝⁹ : CommRing R
M : Type uM
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
N : Type uN
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
ι : Type uι
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
b✝ : Basis ι R M
h : (ι →₀ ℕ) →₀ N
inst✝ : DecidableEq ι
b : Basis ι R M
f : M →ₚ[R] N
⊢ (coeff ⇑b) (Finsupp.polynomialMap b ((coeff ⇑b) f)) = (coeff ⇑b) f
Tactic:
rw [coeff_of_finsupp_polynomialMap]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.rel_isPureHomogeneous
Proof 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
Proof 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
Theorem: DividedPowerAlgebra.rel_isPureHomogeneous
Proof 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
Proof 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
Theorem: DividedPowerAlgebra.rel_isPureHomogeneous
Proof 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 _⟩
Proof 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
Theorem: DividedPowerAlgebra.rel_isPureHomogeneous
Proof 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]
Proof 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
Theorem: DividedPowerAlgebra.rel_isPureHomogeneous
Proof 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]
Proof 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
Theorem: DividedPowerAlgebra.rel_isPureHomogeneous
Proof 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 _ _ _)) _⟩
Proof 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
Theorem: DividedPowerAlgebra.rel_isPureHomogeneous
Proof 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]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.rel_isPureHomogeneous
Proof 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 _⟩
Proof state after:
no goals
Theorem: DividedPowerAlgebra.rel_isPureHomogeneous
Proof 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
Proof 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
Theorem: DividedPowerAlgebra.rel_isPureHomogeneous
Proof 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]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.rel_isPureHomogeneous
Proof 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
Proof 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
Theorem: DividedPowerAlgebra.rel_isPureHomogeneous
Proof 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]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.rel_isPureHomogeneous
Proof 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
Proof 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)
Theorem: DividedPowerAlgebra.rel_isPureHomogeneous
Proof 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 _ _ _)) _⟩
Proof state after:
no goals
Theorem: DividedPowerAlgebra.rel_isPureHomogeneous
Proof 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
Proof 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
Theorem: DividedPowerAlgebra.rel_isPureHomogeneous
Proof 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 _ _ _), _⟩
Proof 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
Theorem: DividedPowerAlgebra.rel_isPureHomogeneous
Proof 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]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.rel_isPureHomogeneous
Proof 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
Proof 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
Theorem: DividedPowerAlgebra.rel_isPureHomogeneous
Proof 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
Proof 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