Theorem: DividedPowerAlgebra.grade_one_eq_span (DividedPowers/DPAlgebra/Graded/GradeOne.lean)

State before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ grade R M 1 = Submodule.span R (Set.range (dp R 1))
Tactic:
apply le_antisymm
State after:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ grade R M 1 ≤ Submodule.span R (Set.range (dp R 1))

case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ Submodule.span R (Set.range (dp R 1)) ≤ grade R M 1

State before:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ grade R M 1 ≤ Submodule.span R (Set.range (dp R 1))
Tactic:
intro p hp
State after:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
⊢ p ∈ Submodule.span R (Set.range (dp R 1))

State before:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
⊢ p ∈ Submodule.span R (Set.range (dp R 1))
Tactic:
obtain ⟨q, hq1, hqp⟩ := surjective_of_supported' R M ⟨p, hp⟩
State after:
case a.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : IsWeightedHomogeneous Prod.fst (↑q) 1
hqp : mk ↑q = ↑⟨p, hp⟩
⊢ p ∈ Submodule.span R (Set.range (dp R 1))

State before:
case a.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : IsWeightedHomogeneous Prod.fst (↑q) 1
hqp : mk ↑q = ↑⟨p, hp⟩
⊢ p ∈ Submodule.span R (Set.range (dp R 1))
Tactic:
simp only at hqp
State after:
case a.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : IsWeightedHomogeneous Prod.fst (↑q) 1
hqp : mk ↑q = p
⊢ p ∈ Submodule.span R (Set.range (dp R 1))

State before:
case a.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : IsWeightedHomogeneous Prod.fst (↑q) 1
hqp : mk ↑q = p
⊢ p ∈ Submodule.span R (Set.range (dp R 1))
Tactic:
simp only [IsWeightedHomogeneous, ne_eq] at hq1
State after:
case a.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
⊢ p ∈ Submodule.span R (Set.range (dp R 1))

State before:
case a.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
⊢ p ∈ Submodule.span R (Set.range (dp R 1))
Tactic:
rw [← hqp, (q : MvPolynomial (ℕ × M) R).as_sum, map_sum]
State after:
case a.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
⊢ ∑ x ∈ (↑q).support, mk ((monomial x) (coeff x ↑q)) ∈ Submodule.span R (Set.range (dp R 1))

State before:
case a.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
⊢ ∑ x ∈ (↑q).support, mk ((monomial x) (coeff x ↑q)) ∈ Submodule.span R (Set.range (dp R 1))
Tactic:
apply Submodule.sum_mem (Submodule.span R (Set.range (dp R 1)))
State after:
case a.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
⊢ ∀ c ∈ (↑q).support, mk ((monomial c) (coeff c ↑q)) ∈ Submodule.span R (Set.range (dp R 1))

State before:
case a.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
⊢ ∀ c ∈ (↑q).support, mk ((monomial c) (coeff c ↑q)) ∈ Submodule.span R (Set.range (dp R 1))
Tactic:
intro d hd
State after:
case a.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
d : ℕ × M →₀ ℕ
hd : d ∈ (↑q).support
⊢ mk ((monomial d) (coeff d ↑q)) ∈ Submodule.span R (Set.range (dp R 1))

State before:
case a.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
d : ℕ × M →₀ ℕ
hd : d ∈ (↑q).support
⊢ mk ((monomial d) (coeff d ↑q)) ∈ Submodule.span R (Set.range (dp R 1))
Tactic:
have hsupp : ∀ nm : ℕ × M, nm ∈ d.support → 0 < nm.fst := by
  intro nm hnm
  apply mem_supported.mp q.2
  rw [mem_coe, mem_vars]
  exact ⟨d, hd, hnm⟩
State after:
case a.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
d : ℕ × M →₀ ℕ
hd : d ∈ (↑q).support
hsupp : ∀ nm ∈ d.support, 0 < nm.1
⊢ mk ((monomial d) (coeff d ↑q)) ∈ Submodule.span R (Set.range (dp R 1))

State before:
case a.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
d : ℕ × M →₀ ℕ
hd : d ∈ (↑q).support
hsupp : ∀ nm ∈ d.support, 0 < nm.1
⊢ mk ((monomial d) (coeff d ↑q)) ∈ Submodule.span R (Set.range (dp R 1))
Tactic:
obtain ⟨m, hm⟩ := eq_finsupp_single_of_degree_one M (hq1 (mem_support_iff.mp hd)) hsupp
State after:
case a.intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
d : ℕ × M →₀ ℕ
hd : d ∈ (↑q).support
hsupp : ∀ nm ∈ d.support, 0 < nm.1
m : M
hm : Finsupp.single (1, m) 1 = d
⊢ mk ((monomial d) (coeff d ↑q)) ∈ Submodule.span R (Set.range (dp R 1))

State before:
case a.intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
d : ℕ × M →₀ ℕ
hd : d ∈ (↑q).support
hsupp : ∀ nm ∈ d.support, 0 < nm.1
m : M
hm : Finsupp.single (1, m) 1 = d
⊢ mk ((monomial d) (coeff d ↑q)) ∈ Submodule.span R (Set.range (dp R 1))
Tactic:
rw [← hm, monomial_eq, C_mul', map_smul, Finsupp.prod_single_index, pow_one]
State after:
case a.intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
d : ℕ × M →₀ ℕ
hd : d ∈ (↑q).support
hsupp : ∀ nm ∈ d.support, 0 < nm.1
m : M
hm : Finsupp.single (1, m) 1 = d
⊢ coeff (Finsupp.single (1, m) 1) ↑q • mk (X (1, m)) ∈ Submodule.span R (Set.range (dp R 1))

case a.intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
d : ℕ × M →₀ ℕ
hd : d ∈ (↑q).support
hsupp : ∀ nm ∈ d.support, 0 < nm.1
m : M
hm : Finsupp.single (1, m) 1 = d
⊢ X (1, m) ^ 0 = 1

State before:
case a.intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
d : ℕ × M →₀ ℕ
hd : d ∈ (↑q).support
hsupp : ∀ nm ∈ d.support, 0 < nm.1
m : M
hm : Finsupp.single (1, m) 1 = d
⊢ coeff (Finsupp.single (1, m) 1) ↑q • mk (X (1, m)) ∈ Submodule.span R (Set.range (dp R 1))

case a.intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
d : ℕ × M →₀ ℕ
hd : d ∈ (↑q).support
hsupp : ∀ nm ∈ d.support, 0 < nm.1
m : M
hm : Finsupp.single (1, m) 1 = d
⊢ X (1, m) ^ 0 = 1
Tactic:
exact Submodule.smul_mem (Submodule.span R (Set.range (dp R 1))) _
  (Submodule.subset_span (Set.mem_range.mpr ⟨m, rfl⟩))
State after:
case a.intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
d : ℕ × M →₀ ℕ
hd : d ∈ (↑q).support
hsupp : ∀ nm ∈ d.support, 0 < nm.1
m : M
hm : Finsupp.single (1, m) 1 = d
⊢ X (1, m) ^ 0 = 1

State before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
d : ℕ × M →₀ ℕ
hd : d ∈ (↑q).support
⊢ ∀ nm ∈ d.support, 0 < nm.1
Tactic:
intro nm hnm
State after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
d : ℕ × M →₀ ℕ
hd : d ∈ (↑q).support
nm : ℕ × M
hnm : nm ∈ d.support
⊢ 0 < nm.1

State before:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
d : ℕ × M →₀ ℕ
hd : d ∈ (↑q).support
nm : ℕ × M
hnm : nm ∈ d.support
⊢ 0 < nm.1
Tactic:
apply mem_supported.mp q.2
State after:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
d : ℕ × M →₀ ℕ
hd : d ∈ (↑q).support
nm : ℕ × M
hnm : nm ∈ d.support
⊢ nm ∈ ↑(↑q).vars

State before:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
d : ℕ × M →₀ ℕ
hd : d ∈ (↑q).support
nm : ℕ × M
hnm : nm ∈ d.support
⊢ nm ∈ ↑(↑q).vars
Tactic:
rw [mem_coe, mem_vars]
State after:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
d : ℕ × M →₀ ℕ
hd : d ∈ (↑q).support
nm : ℕ × M
hnm : nm ∈ d.support
⊢ ∃ d ∈ (↑q).support, nm ∈ d.support

State before:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
d : ℕ × M →₀ ℕ
hd : d ∈ (↑q).support
nm : ℕ × M
hnm : nm ∈ d.support
⊢ ∃ d ∈ (↑q).support, nm ∈ d.support
Tactic:
exact ⟨d, hd, hnm⟩
State after:
no goals

State before:
case a.intro.intro.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ grade R M 1
q : ↥(supported R {nm | 0 < nm.1})
hq1 : ∀ ⦃d : ℕ × M →₀ ℕ⦄, ¬coeff d ↑q = 0 → (weightedDegree Prod.fst) d = 1
hqp : mk ↑q = p
d : ℕ × M →₀ ℕ
hd : d ∈ (↑q).support
hsupp : ∀ nm ∈ d.support, 0 < nm.1
m : M
hm : Finsupp.single (1, m) 1 = d
⊢ X (1, m) ^ 0 = 1
Tactic:
rw [pow_zero]
State after:
no goals

State before:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ Submodule.span R (Set.range (dp R 1)) ≤ grade R M 1
Tactic:
rw [Submodule.span_le]
State after:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ Set.range (dp R 1) ⊆ ↑(grade R M 1)

State before:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ Set.range (dp R 1) ⊆ ↑(grade R M 1)
Tactic:
intro p hp
State after:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ Set.range (dp R 1)
⊢ p ∈ ↑(grade R M 1)

State before:
case a
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ Set.range (dp R 1)
⊢ p ∈ ↑(grade R M 1)
Tactic:
obtain ⟨m, hm⟩ := Set.mem_range.mp hp
State after:
case a.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ Set.range (dp R 1)
m : M
hm : dp R 1 m = p
⊢ p ∈ ↑(grade R M 1)

State before:
case a.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ Set.range (dp R 1)
m : M
hm : dp R 1 m = p
⊢ p ∈ ↑(grade R M 1)
Tactic:
rw [← hm]
State after:
case a.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ Set.range (dp R 1)
m : M
hm : dp R 1 m = p
⊢ dp R 1 m ∈ ↑(grade R M 1)

State before:
case a.intro
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
p : DividedPowerAlgebra R M
hp : p ∈ Set.range (dp R 1)
m : M
hm : dp R 1 m = p
⊢ dp R 1 m ∈ ↑(grade R M 1)
Tactic:
exact dp_mem_grade R M 1 m
State after:
no goals