internlm/Lean-Github huggingface dataset:
Theorem: MvPowerSeries.StronglyMultipliable.finset_prod_eq
Proof state before:
case h.h.hc
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
inst✝¹ : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝ : DecidableEq ι
s : Finset ι
hf : StronglyMultipliable f
d : σ →₀ ℕ
t : Finset ι
ht : t ∈ s.powerset
⊢ t ∈ {I | I ⊆ s}
Tactic:
exact Finset.mem_powerset.mp ht
Proof state after:
no goals
Theorem: MvPowerSeries.StronglyMultipliable.finset_prod_eq
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
inst✝¹ : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝ : DecidableEq ι
s : Finset ι
hf : StronglyMultipliable f
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ({I | I ⊆ s}.indicator (partialProduct f) i)) ⊆ ↑s.powerset
Tactic:
intro t
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
inst✝¹ : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝ : DecidableEq ι
s : Finset ι
hf : StronglyMultipliable f
d : σ →₀ ℕ
t : Finset ι
⊢ (t ∈ support fun i => (coeff α d) ({I | I ⊆ s}.indicator (partialProduct f) i)) → t ∈ ↑s.powerset
Theorem: MvPowerSeries.StronglyMultipliable.finset_prod_eq
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
inst✝¹ : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝ : DecidableEq ι
s : Finset ι
hf : StronglyMultipliable f
d : σ →₀ ℕ
t : Finset ι
⊢ (t ∈ support fun i => (coeff α d) ({I | I ⊆ s}.indicator (partialProduct f) i)) → t ∈ ↑s.powerset
Tactic:
rw [mem_support, ne_eq, mem_coe, Finset.mem_powerset, not_imp_comm]
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
inst✝¹ : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝ : DecidableEq ι
s : Finset ι
hf : StronglyMultipliable f
d : σ →₀ ℕ
t : Finset ι
⊢ ¬t ⊆ s → (coeff α d) ({I | I ⊆ s}.indicator (partialProduct f) t) = 0
Theorem: MvPowerSeries.StronglyMultipliable.finset_prod_eq
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
inst✝¹ : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝ : DecidableEq ι
s : Finset ι
hf : StronglyMultipliable f
d : σ →₀ ℕ
t : Finset ι
⊢ ¬t ⊆ s → (coeff α d) ({I | I ⊆ s}.indicator (partialProduct f) t) = 0
Tactic:
intro ht'
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
inst✝¹ : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝ : DecidableEq ι
s : Finset ι
hf : StronglyMultipliable f
d : σ →₀ ℕ
t : Finset ι
ht' : ¬t ⊆ s
⊢ (coeff α d) ({I | I ⊆ s}.indicator (partialProduct f) t) = 0
Theorem: MvPowerSeries.StronglyMultipliable.finset_prod_eq
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
inst✝¹ : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝ : DecidableEq ι
s : Finset ι
hf : StronglyMultipliable f
d : σ →₀ ℕ
t : Finset ι
ht' : ¬t ⊆ s
⊢ (coeff α d) ({I | I ⊆ s}.indicator (partialProduct f) t) = 0
Tactic:
rw [indicator, if_neg, map_zero]
Proof state after:
case h.hnc
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
inst✝¹ : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝ : DecidableEq ι
s : Finset ι
hf : StronglyMultipliable f
d : σ →₀ ℕ
t : Finset ι
ht' : ¬t ⊆ s
⊢ t ∉ {I | I ⊆ s}
Theorem: MvPowerSeries.StronglyMultipliable.finset_prod_eq
Proof state before:
case h.hnc
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
inst✝¹ : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝ : DecidableEq ι
s : Finset ι
hf : StronglyMultipliable f
d : σ →₀ ℕ
t : Finset ι
ht' : ¬t ⊆ s
⊢ t ∉ {I | I ⊆ s}
Tactic:
exact ht'
Proof state after:
no goals
Theorem: MvPowerSeries.StronglyMultipliable.prod_eq_sum_add_sum
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
hf : StronglyMultipliable f
s : Set ι
⊢ hf.prod = ⋯.sum + ⋯.sum
Tactic:
rw [hf.prod_eq, ← hf.add_compl]
Proof state after:
no goals
Theorem: MvPowerSeries.StronglyMultipliable.prod_eq_finset_prod_add
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
inst✝¹ : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝ : DecidableEq ι
hf : StronglyMultipliable f
s : Finset ι
⊢ hf.prod = ∏ i ∈ s, (1 + f i) + ⋯.sum
Tactic:
rw [hf.prod_eq_sum_add_sum s, hf.finset_prod_eq s]
Proof state after:
no goals
Theorem: MvPowerSeries.StronglyMultipliable.coeff_prod_apply_eq_finset_prod
Proof state before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
⊢ (coeff α d) ⋯.prod = (coeff α d) (∏ i ∈ J, (1 + f i))
Tactic:
rw [hf.toStronglyMultipliable.prod_eq_finset_prod_add J, map_add, add_right_eq_self,
  StronglySummable.coeff_sum_def]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
⊢ ∑ i ∈ ⋯.toFinset, (coeff α d) ({I | I ⊆ J}ᶜ.indicator (partialProduct f) i) = 0
Theorem: MvPowerSeries.StronglyMultipliable.coeff_prod_apply_eq_finset_prod
Proof state before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
⊢ ∑ i ∈ ⋯.toFinset, (coeff α d) ({I | I ⊆ J}ᶜ.indicator (partialProduct f) i) = 0
Tactic:
apply sum_eq_zero
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
⊢ ∀ x ∈ ⋯.toFinset, (coeff α d) ({I | I ⊆ J}ᶜ.indicator (partialProduct f) x) = 0
Theorem: MvPowerSeries.StronglyMultipliable.coeff_prod_apply_eq_finset_prod
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
⊢ ∀ x ∈ ⋯.toFinset, (coeff α d) ({I | I ⊆ J}ᶜ.indicator (partialProduct f) x) = 0
Tactic:
intro t _
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
t : Finset ι
a✝ : t ∈ ⋯.toFinset
⊢ (coeff α d) ({I | I ⊆ J}ᶜ.indicator (partialProduct f) t) = 0
Theorem: MvPowerSeries.StronglyMultipliable.coeff_prod_apply_eq_finset_prod
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
t : Finset ι
a✝ : t ∈ ⋯.toFinset
⊢ (coeff α d) ({I | I ⊆ J}ᶜ.indicator (partialProduct f) t) = 0
Tactic:
simp only [indicator, mem_compl_iff, mem_setOf_eq]
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
t : Finset ι
a✝ : t ∈ ⋯.toFinset
⊢ (coeff α d) (if ¬t ⊆ J then partialProduct f t else 0) = 0
Theorem: MvPowerSeries.StronglyMultipliable.coeff_prod_apply_eq_finset_prod
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
t : Finset ι
a✝ : t ∈ ⋯.toFinset
⊢ (coeff α d) (if ¬t ⊆ J then partialProduct f t else 0) = 0
Tactic:
split_ifs with h
Proof state after:
case pos
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
t : Finset ι
a✝ : t ∈ ⋯.toFinset
h : t ⊆ J
⊢ (coeff α d) 0 = 0

case neg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
t : Finset ι
a✝ : t ∈ ⋯.toFinset
h : ¬t ⊆ J
⊢ (coeff α d) (partialProduct f t) = 0
Theorem: MvPowerSeries.StronglyMultipliable.coeff_prod_apply_eq_finset_prod
Proof state before:
case neg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
t : Finset ι
a✝ : t ∈ ⋯.toFinset
h : ¬t ⊆ J
⊢ (coeff α d) (partialProduct f t) = 0
Tactic:
. simp only [Finset.not_subset] at h
  obtain ⟨i, hit, hiJ⟩ := h
  simp only [partialProduct, prod_eq_mul_prod_diff_singleton hit, coeff_mul]
  apply sum_eq_zero
  rintro ⟨x, y⟩ hxy
  rw [mem_antidiagonal] at hxy
  rw [(hf.not_mem_unionOfSupportOfCoeffLe_iff d i).mp (fun hi => hiJ (hJ hi)) x _,
    MulZeroClass.zero_mul]
  simp only [← hxy, Finsupp.le_def, Finsupp.coe_add, Pi.add_apply, le_self_add]
Proof state after:
no goals
Theorem: MvPowerSeries.StronglyMultipliable.coeff_prod_apply_eq_finset_prod
Proof state before:
case pos
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
t : Finset ι
a✝ : t ∈ ⋯.toFinset
h : t ⊆ J
⊢ (coeff α d) 0 = 0
Tactic:
rw [map_zero]
Proof state after:
no goals
Theorem: MvPowerSeries.StronglyMultipliable.coeff_prod_apply_eq_finset_prod
Proof state before:
case neg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
t : Finset ι
a✝ : t ∈ ⋯.toFinset
h : ¬t ⊆ J
⊢ (coeff α d) (partialProduct f t) = 0
Tactic:
simp only [Finset.not_subset] at h
Proof state after:
case neg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
t : Finset ι
a✝ : t ∈ ⋯.toFinset
h : ∃ x ∈ t, x ∉ J
⊢ (coeff α d) (partialProduct f t) = 0
Theorem: MvPowerSeries.StronglyMultipliable.coeff_prod_apply_eq_finset_prod
Proof state before:
case neg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
t : Finset ι
a✝ : t ∈ ⋯.toFinset
h : ∃ x ∈ t, x ∉ J
⊢ (coeff α d) (partialProduct f t) = 0
Tactic:
obtain ⟨i, hit, hiJ⟩ := h
Proof state after:
case neg.intro.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
t : Finset ι
a✝ : t ∈ ⋯.toFinset
i : ι
hit : i ∈ t
hiJ : i ∉ J
⊢ (coeff α d) (partialProduct f t) = 0
Theorem: MvPowerSeries.StronglyMultipliable.coeff_prod_apply_eq_finset_prod
Proof state before:
case neg.intro.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
t : Finset ι
a✝ : t ∈ ⋯.toFinset
i : ι
hit : i ∈ t
hiJ : i ∉ J
⊢ (coeff α d) (partialProduct f t) = 0
Tactic:
simp only [partialProduct, prod_eq_mul_prod_diff_singleton hit, coeff_mul]
Proof state after:
case neg.intro.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
t : Finset ι
a✝ : t ∈ ⋯.toFinset
i : ι
hit : i ∈ t
hiJ : i ∉ J
⊢ ∑ p ∈ antidiagonal d, (coeff α p.1) (f i) * (coeff α p.2) (∏ i ∈ t \ {i}, f i) = 0
Theorem: MvPowerSeries.StronglyMultipliable.coeff_prod_apply_eq_finset_prod
Proof state before:
case neg.intro.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
t : Finset ι
a✝ : t ∈ ⋯.toFinset
i : ι
hit : i ∈ t
hiJ : i ∉ J
⊢ ∑ p ∈ antidiagonal d, (coeff α p.1) (f i) * (coeff α p.2) (∏ i ∈ t \ {i}, f i) = 0
Tactic:
apply sum_eq_zero
Proof state after:
case neg.intro.intro.h
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
t : Finset ι
a✝ : t ∈ ⋯.toFinset
i : ι
hit : i ∈ t
hiJ : i ∉ J
⊢ ∀ x ∈ antidiagonal d, (coeff α x.1) (f i) * (coeff α x.2) (∏ i ∈ t \ {i}, f i) = 0
Theorem: MvPowerSeries.StronglyMultipliable.coeff_prod_apply_eq_finset_prod
Proof state before:
case neg.intro.intro.h
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
t : Finset ι
a✝ : t ∈ ⋯.toFinset
i : ι
hit : i ∈ t
hiJ : i ∉ J
⊢ ∀ x ∈ antidiagonal d, (coeff α x.1) (f i) * (coeff α x.2) (∏ i ∈ t \ {i}, f i) = 0
Tactic:
rintro ⟨x, y⟩ hxy
Proof state after:
case neg.intro.intro.h.mk
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
t : Finset ι
a✝ : t ∈ ⋯.toFinset
i : ι
hit : i ∈ t
hiJ : i ∉ J
x y : σ →₀ ℕ
hxy : (x, y) ∈ antidiagonal d
⊢ (coeff α (x, y).1) (f i) * (coeff α (x, y).2) (∏ i ∈ t \ {i}, f i) = 0
Theorem: MvPowerSeries.StronglyMultipliable.coeff_prod_apply_eq_finset_prod
Proof state before:
case neg.intro.intro.h.mk
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
t : Finset ι
a✝ : t ∈ ⋯.toFinset
i : ι
hit : i ∈ t
hiJ : i ∉ J
x y : σ →₀ ℕ
hxy : (x, y) ∈ antidiagonal d
⊢ (coeff α (x, y).1) (f i) * (coeff α (x, y).2) (∏ i ∈ t \ {i}, f i) = 0
Tactic:
rw [mem_antidiagonal] at hxy
Proof state after:
case neg.intro.intro.h.mk
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
t : Finset ι
a✝ : t ∈ ⋯.toFinset
i : ι
hit : i ∈ t
hiJ : i ∉ J
x y : σ →₀ ℕ
hxy : (x, y).1 + (x, y).2 = d
⊢ (coeff α (x, y).1) (f i) * (coeff α (x, y).2) (∏ i ∈ t \ {i}, f i) = 0
Theorem: MvPowerSeries.StronglyMultipliable.coeff_prod_apply_eq_finset_prod
Proof state before:
case neg.intro.intro.h.mk
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
t : Finset ι
a✝ : t ∈ ⋯.toFinset
i : ι
hit : i ∈ t
hiJ : i ∉ J
x y : σ →₀ ℕ
hxy : (x, y).1 + (x, y).2 = d
⊢ (coeff α (x, y).1) (f i) * (coeff α (x, y).2) (∏ i ∈ t \ {i}, f i) = 0
Tactic:
rw [(hf.not_mem_unionOfSupportOfCoeffLe_iff d i).mp (fun hi => hiJ (hJ hi)) x _,
  MulZeroClass.zero_mul]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
t : Finset ι
a✝ : t ∈ ⋯.toFinset
i : ι
hit : i ∈ t
hiJ : i ∉ J
x y : σ →₀ ℕ
hxy : (x, y).1 + (x, y).2 = d
⊢ x ≤ d
Theorem: MvPowerSeries.StronglyMultipliable.coeff_prod_apply_eq_finset_prod
Proof state before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
hf : StronglySummable f
d : σ →₀ ℕ
J : Finset ι
hJ : hf.unionOfSupportOfCoeffLe d ⊆ J
t : Finset ι
a✝ : t ∈ ⋯.toFinset
i : ι
hit : i ∈ t
hiJ : i ∉ J
x y : σ →₀ ℕ
hxy : (x, y).1 + (x, y).2 = d
⊢ x ≤ d
Tactic:
simp only [← hxy, Finsupp.le_def, Finsupp.coe_add, Pi.add_apply, le_self_add]
Proof state after:
no goals
Theorem: Ideal.sub_mem_ofRel_of_rel
Proof state before:
R✝ : Type ?u.35137
M : Type ?u.35140
inst✝³ : CommRing R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_1
inst✝ : Ring R
r : R → R → Prop
a b : R
hr : r a b
⊢ a - b + b = a
Tactic:
rw [sub_add_cancel]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.mk_C
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
⊢ mk (C a) = (algebraMap R (DividedPowerAlgebra R M)) a
Tactic:
rw [← MvPolynomial.algebraMap_eq, AlgHom.commutes]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dp_eq_mkRingHom
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
m : M
⊢ dp R n m = (mkRingHom (Rel R M)) (X (n, m))
Tactic:
rw [dp_def, ← mkAlgHom_coe R]
Proof state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
m : M
⊢ (mkAlgHom R (Rel R M)) (X (n, m)) = ↑(mkAlgHom R (Rel R M)) (X (n, m))
Theorem: DividedPowerAlgebra.dp_eq_mkRingHom
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
m : M
⊢ (mkAlgHom R (Rel R M)) (X (n, m)) = ↑(mkAlgHom R (Rel R M)) (X (n, m))
Tactic:
rfl
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dp_zero
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ dp R 0 m = 1
Tactic:
rw [dp_def, ← map_one (mkAlgHom R (Rel R M))]
Proof state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ (mkAlgHom R (Rel R M)) (X (0, m)) = (mkAlgHom R (Rel R M)) 1
Theorem: DividedPowerAlgebra.dp_zero
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ (mkAlgHom R (Rel R M)) (X (0, m)) = (mkAlgHom R (Rel R M)) 1
Tactic:
exact RingQuot.mkAlgHom_rel R Rel.zero
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dp_smul
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
n : ℕ
m : M
⊢ dp R n (r • m) = r ^ n • dp R n m
Tactic:
rw [dp_def, dp_def, ← map_smul]
Proof state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
n : ℕ
m : M
⊢ (mkAlgHom R (Rel R M)) (X (n, r • m)) = r ^ n • (mkAlgHom R (Rel R M)) (X (n, m))
Theorem: DividedPowerAlgebra.dp_null
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
⊢ dp R n 0 = if n = 0 then 1 else 0
Tactic:
cases' Nat.eq_zero_or_pos n with hn hn
Proof state after:
case inl
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n = 0
⊢ dp R n 0 = if n = 0 then 1 else 0

case inr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n > 0
⊢ dp R n 0 = if n = 0 then 1 else 0
Theorem: DividedPowerAlgebra.dp_null
Proof state before:
case inl
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n = 0
⊢ dp R n 0 = if n = 0 then 1 else 0
Tactic:
rw [if_pos hn]
Proof state after:
case inl
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n = 0
⊢ dp R n 0 = 1
Theorem: DividedPowerAlgebra.dp_null
Proof state before:
case inl
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n = 0
⊢ dp R n 0 = 1
Tactic:
rw [hn]
Proof state after:
case inl
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n = 0
⊢ dp R 0 0 = 1
Theorem: DividedPowerAlgebra.dp_null
Proof state before:
case inl
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n = 0
⊢ dp R 0 0 = 1
Tactic:
rw [dp_zero]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dp_null
Proof state before:
case inr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n > 0
⊢ dp R n 0 = if n = 0 then 1 else 0
Tactic:
rw [if_neg (ne_of_gt hn)]
Proof state after:
case inr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n > 0
⊢ dp R n 0 = 0
Theorem: DividedPowerAlgebra.dp_null
Proof state before:
case inr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n > 0
⊢ dp R n 0 = 0
Tactic:
rw [← zero_smul R (0 : M)]
Proof state after:
case inr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n > 0
⊢ dp R n (0 • 0) = 0
Theorem: DividedPowerAlgebra.dp_null
Proof state before:
case inr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n > 0
⊢ dp R n (0 • 0) = 0
Tactic:
rw [dp_smul]
Proof state after:
case inr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n > 0
⊢ 0 ^ n • dp R n 0 = 0
Theorem: DividedPowerAlgebra.dp_null
Proof state before:
case inr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n > 0
⊢ 0 ^ n • dp R n 0 = 0
Tactic:
rw [zero_pow hn]
Proof state after:
case inr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n > 0
⊢ 0 • dp R n 0 = 0
Theorem: DividedPowerAlgebra.dp_mul
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n p : ℕ
m : M
⊢ dp R n m * dp R p m = (n + p).choose n • dp R (n + p) m
Tactic:
simp only [dp_def, ← _root_.map_mul, ← map_nsmul]
Proof state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n p : ℕ
m : M
⊢ (mkAlgHom R (Rel R M)) (X (n, m)) * (mkAlgHom R (Rel R M)) (X (p, m)) =
    (n + p).choose n • (mkAlgHom R (Rel R M)) (X (n + p, m))
Theorem: DividedPowerAlgebra.dp_add
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ dp R n (x + y) = ∑ k ∈ range (n + 1), dp R k x * dp R (n - k) y
Tactic:
simp only [dp_def]
Proof state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ (mkAlgHom R (Rel R M)) (X (n, x + y)) =
    ∑ x_1 ∈ range (n + 1), (mkAlgHom R (Rel R M)) (X (x_1, x)) * (mkAlgHom R (Rel R M)) (X (n - x_1, y))