internlm/Lean-Github huggingface dataset:
Theorem: MvPowerSeries.has_submodules_basis_topology
Proof state before:
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
⊢ nhds 0 = nhds 0
Tactic:
ext s
Proof state after:
case a
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 ↔ s ∈ nhds 0
Theorem: MvPowerSeries.has_submodules_basis_topology
Proof state before:
case a
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 ↔ s ∈ nhds 0
Tactic:
rw [(RingSubgroupsBasis.hasBasis_nhds (toRingSubgroupsBasis σ α) 0).mem_iff]
Proof state after:
case a
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 ↔ ∃ i, True ∧ {b | b - 0 ∈ Submodule.toAddSubgroup (basis σ α i)} ⊆ s
Theorem: MvPowerSeries.has_submodules_basis_topology
Proof state before:
case a
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 ↔ ∃ i, True ∧ {b | b - 0 ∈ Submodule.toAddSubgroup (basis σ α i)} ⊆ s
Tactic:
simp only [sub_zero, Submodule.mem_toAddSubgroup, true_and]
Proof state after:
case a
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 ↔ ∃ i, {b | b ∈ basis σ α i} ⊆ s
Theorem: MvPowerSeries.has_submodules_basis_topology
Proof state before:
case a
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 ↔ ∃ i, {b | b ∈ basis σ α i} ⊆ s
Tactic:
exact mem_nhds_zero_iff σ α s
Proof state after:
no goals
Theorem: DividedPowerAlgebra.toTrivSqZeroExt_apply_dp_of_two_le
Proof 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
n : ℕ
m : M
hn : 2 ≤ n
⊢ (toTrivSqZeroExt R M) (dp R n m) = 0
Tactic:
rw [toTrivSqZeroExt, liftAlgHom_apply_dp, DividedPowers.OfSquareZero.dpow_of_two_le]
Proof state after:
case hn
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
n : ℕ
m : M
hn : 2 ≤ n
⊢ 2 ≤ n
Theorem: DividedPowerAlgebra.toTrivSqZeroExt_apply_dp_of_two_le
Proof state before:
case hn
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
n : ℕ
m : M
hn : 2 ≤ n
⊢ 2 ≤ n
Tactic:
exact hn
Proof state after:
no goals
Theorem: DividedPowerAlgebra.grade_one_eq_span
Proof 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
Proof 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
Theorem: DividedPowerAlgebra.grade_one_eq_span
Proof 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
Proof 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))
Theorem: DividedPowerAlgebra.grade_one_eq_span
Proof 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⟩
Proof 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))
Theorem: DividedPowerAlgebra.grade_one_eq_span
Proof 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
Proof 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))
Theorem: DividedPowerAlgebra.grade_one_eq_span
Proof 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
Proof 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))
Theorem: DividedPowerAlgebra.grade_one_eq_span
Proof 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]
Proof 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))
Theorem: DividedPowerAlgebra.grade_one_eq_span
Proof 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)))
Proof 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))
Theorem: DividedPowerAlgebra.grade_one_eq_span
Proof 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
Proof 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))
Theorem: DividedPowerAlgebra.grade_one_eq_span
Proof 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⟩
Proof 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))
Theorem: DividedPowerAlgebra.grade_one_eq_span
Proof 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
Proof 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))
Theorem: DividedPowerAlgebra.grade_one_eq_span
Proof 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]
Proof 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
Theorem: DividedPowerAlgebra.grade_one_eq_span
Proof 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⟩))
Proof 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
Theorem: DividedPowerAlgebra.grade_one_eq_span
Proof 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
Proof 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
Theorem: DividedPowerAlgebra.grade_one_eq_span
Proof 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
Proof 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
Theorem: DividedPowerAlgebra.grade_one_eq_span
Proof 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]
Proof 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
Theorem: DividedPowerAlgebra.grade_one_eq_span
Proof 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⟩
Proof state after:
no goals
Theorem: DividedPowerAlgebra.grade_one_eq_span
Proof 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]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.grade_one_eq_span
Proof 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]
Proof 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)
Theorem: DividedPowerAlgebra.grade_one_eq_span
Proof 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
Proof 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)
Theorem: DividedPowerAlgebra.grade_one_eq_span
Proof 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
Proof 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)
Theorem: DividedPowerAlgebra.grade_one_eq_span
Proof 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]
Proof 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)