Theorem: Finsupp.prod.mem_grade (DividedPowers/DPAlgebra/Misc.lean)

State before:
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
⊢ (c.prod fun s e => f s ^ e) ∈ 𝒜 (c.sum fun s e => e • d s)
Tactic:
rw [Finsupp.prod, Finsupp.sum]
State after:
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
⊢ ∏ a ∈ c.support, f a ^ c a ∈ 𝒜 (∑ a ∈ c.support, c a • d a)

State before:
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
⊢ ∏ a ∈ c.support, f a ^ c a ∈ 𝒜 (∑ a ∈ c.support, c a • d a)
Tactic:
let p : Finset σ → Prop := fun s =>
  s ⊆ c.support → (s.prod fun i => f i ^ c i) ∈ 𝒜 (s.sum fun i => c i • d i)
State after:
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
p : Finset σ → Prop := fun s => s ⊆ c.support → ∏ i ∈ s, f i ^ c i ∈ 𝒜 (∑ i ∈ s, c i • d i)
⊢ ∏ a ∈ c.support, f a ^ c a ∈ 𝒜 (∑ a ∈ c.support, c a • d a)

State before:
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
p : Finset σ → Prop := fun s => s ⊆ c.support → ∏ i ∈ s, f i ^ c i ∈ 𝒜 (∑ i ∈ s, c i • d i)
⊢ ∏ a ∈ c.support, f a ^ c a ∈ 𝒜 (∑ a ∈ c.support, c a • d a)
Tactic:
apply @Finset.induction_on σ p _ c.support
State after:
case empty
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
p : Finset σ → Prop := fun s => s ⊆ c.support → ∏ i ∈ s, f i ^ c i ∈ 𝒜 (∑ i ∈ s, c i • d i)
⊢ p ∅

case insert
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
p : Finset σ → Prop := fun s => s ⊆ c.support → ∏ i ∈ s, f i ^ c i ∈ 𝒜 (∑ i ∈ s, c i • d i)
⊢ ∀ ⦃a : σ⦄ {s : Finset σ}, a ∉ s → p s → p (insert a s)

case a
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
p : Finset σ → Prop := fun s => s ⊆ c.support → ∏ i ∈ s, f i ^ c i ∈ 𝒜 (∑ i ∈ s, c i • d i)
⊢ c.support ⊆ c.support

State before:
case empty
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
p : Finset σ → Prop := fun s => s ⊆ c.support → ∏ i ∈ s, f i ^ c i ∈ 𝒜 (∑ i ∈ s, c i • d i)
⊢ p ∅
Tactic:
exact imp_intro (SetLike.one_mem_graded 𝒜)
State after:
no goals

State before:
case insert
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
p : Finset σ → Prop := fun s => s ⊆ c.support → ∏ i ∈ s, f i ^ c i ∈ 𝒜 (∑ i ∈ s, c i • d i)
⊢ ∀ ⦃a : σ⦄ {s : Finset σ}, a ∉ s → p s → p (insert a s)
Tactic:
intro a s ha hs hs'
State after:
case insert
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
p : Finset σ → Prop := fun s => s ⊆ c.support → ∏ i ∈ s, f i ^ c i ∈ 𝒜 (∑ i ∈ s, c i • d i)
a : σ
s : Finset σ
ha : a ∉ s
hs : p s
hs' : insert a s ⊆ c.support
⊢ ∏ i ∈ insert a s, f i ^ c i ∈ 𝒜 (∑ i ∈ insert a s, c i • d i)

State before:
case insert
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
p : Finset σ → Prop := fun s => s ⊆ c.support → ∏ i ∈ s, f i ^ c i ∈ 𝒜 (∑ i ∈ s, c i • d i)
a : σ
s : Finset σ
ha : a ∉ s
hs : p s
hs' : insert a s ⊆ c.support
⊢ ∏ i ∈ insert a s, f i ^ c i ∈ 𝒜 (∑ i ∈ insert a s, c i • d i)
Tactic:
rw [Finset.prod_insert ha, Finset.sum_insert ha]
State after:
case insert
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
p : Finset σ → Prop := fun s => s ⊆ c.support → ∏ i ∈ s, f i ^ c i ∈ 𝒜 (∑ i ∈ s, c i • d i)
a : σ
s : Finset σ
ha : a ∉ s
hs : p s
hs' : insert a s ⊆ c.support
⊢ f a ^ c a * ∏ x ∈ s, f x ^ c x ∈ 𝒜 (c a • d a + ∑ x ∈ s, c x • d x)

State before:
case insert
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
p : Finset σ → Prop := fun s => s ⊆ c.support → ∏ i ∈ s, f i ^ c i ∈ 𝒜 (∑ i ∈ s, c i • d i)
a : σ
s : Finset σ
ha : a ∉ s
hs : p s
hs' : insert a s ⊆ c.support
⊢ f a ^ c a * ∏ x ∈ s, f x ^ c x ∈ 𝒜 (c a • d a + ∑ x ∈ s, c x • d x)
Tactic:
exact
  SetLike.mul_mem_graded (SetLike.pow_mem_graded _ (hc a (hs' (mem_insert_self a s))))
    (hs (subset_trans (subset_insert a s) hs'))
State after:
no goals

State before:
case a
R : Type u_3
inst✝⁷ : CommSemiring R
S : Type ?u.167638
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
κ : Type u_1
A : Type u_2
inst✝⁴ : AddCommMonoid κ
inst✝³ : DecidableEq κ
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
𝒜 : κ → Submodule R A
inst✝ : GradedAlgebra 𝒜
σ : Type u_4
c : σ →₀ ℕ
f : σ → A
d : σ → κ
hc : ∀ s ∈ c.support, f s ∈ 𝒜 (d s)
p : Finset σ → Prop := fun s => s ⊆ c.support → ∏ i ∈ s, f i ^ c i ∈ 𝒜 (∑ i ∈ s, c i • d i)
⊢ c.support ⊆ c.support
Tactic:
exact subset_rfl
State after:
no goals