internlm/Lean-Github huggingface dataset:
Theorem: MvPowerSeries.as_sum_of_homogeneous_components
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.68273
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ f d = ∑ i ∈ ⋯.toFinset, if (weight w) d = i then (coeff α d) f else 0
Tactic:
rw [sum_eq_single (weight w d)]
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.68273
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ f d = if (weight w) d = (weight w) d then (coeff α d) f else 0

case h.h₀
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.68273
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ ∀ b ∈ ⋯.toFinset, b ≠ (weight w) d → (if (weight w) d = b then (coeff α d) f else 0) = 0

case h.h₁
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.68273
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ (weight w) d ∉ ⋯.toFinset → (if (weight w) d = (weight w) d then (coeff α d) f else 0) = 0
Theorem: MvPowerSeries.as_sum_of_homogeneous_components
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.68273
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ f d = if (weight w) d = (weight w) d then (coeff α d) f else 0
Tactic:
simp only [eq_self_iff_true, if_true]
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.68273
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ f d = (coeff α d) f
Theorem: MvPowerSeries.as_sum_of_homogeneous_components
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.68273
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ f d = (coeff α d) f
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPowerSeries.as_sum_of_homogeneous_components
Proof state before:
case h.h₀
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.68273
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ ∀ b ∈ ⋯.toFinset, b ≠ (weight w) d → (if (weight w) d = b then (coeff α d) f else 0) = 0
Tactic:
intro b _ h'
Proof state after:
case h.h₀
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.68273
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
b : ℕ
a✝ : b ∈ ⋯.toFinset
h' : b ≠ (weight w) d
⊢ (if (weight w) d = b then (coeff α d) f else 0) = 0
Theorem: MvPowerSeries.as_sum_of_homogeneous_components
Proof state before:
case h.h₀
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.68273
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
b : ℕ
a✝ : b ∈ ⋯.toFinset
h' : b ≠ (weight w) d
⊢ (if (weight w) d = b then (coeff α d) f else 0) = 0
Tactic:
rw [if_neg (Ne.symm h')]
Proof state after:
no goals
Theorem: MvPowerSeries.as_sum_of_homogeneous_components
Proof state before:
case h.h₁
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.68273
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ (weight w) d ∉ ⋯.toFinset → (if (weight w) d = (weight w) d then (coeff α d) f else 0) = 0
Tactic:
simp only [Finite.mem_toFinset, Function.mem_support, Classical.not_not, imp_self]
Proof state after:
no goals
Theorem: MvPowerSeries.as_sum_of_homogeneous_components'
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ ∀ (hf : StronglySummable fun p => (homogeneousComponent w p) f), f = hf.sum
Tactic:
intro hf
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
⊢ f = hf.sum
Theorem: MvPowerSeries.as_sum_of_homogeneous_components'
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
⊢ f = hf.sum
Tactic:
ext d
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
⊢ (coeff α d) f = (coeff α d) hf.sum
Theorem: MvPowerSeries.as_sum_of_homogeneous_components'
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
⊢ (coeff α d) f = (coeff α d) hf.sum
Tactic:
simp_rw [coeff_apply, StronglySummable.sum, coeff_homogeneousComponent]
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
⊢ f d = ∑ i ∈ ⋯.toFinset, if (weight w) d = i then (coeff α d) f else 0
Theorem: MvPowerSeries.as_sum_of_homogeneous_components'
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
⊢ f d = ∑ i ∈ ⋯.toFinset, if (weight w) d = i then (coeff α d) f else 0
Tactic:
rw [sum_eq_single (weight w d)]
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
⊢ f d = if (weight w) d = (weight w) d then (coeff α d) f else 0

case h.h₀
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
⊢ ∀ b ∈ ⋯.toFinset, b ≠ (weight w) d → (if (weight w) d = b then (coeff α d) f else 0) = 0

case h.h₁
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
⊢ (weight w) d ∉ ⋯.toFinset → (if (weight w) d = (weight w) d then (coeff α d) f else 0) = 0
Theorem: MvPowerSeries.as_sum_of_homogeneous_components'
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
⊢ f d = if (weight w) d = (weight w) d then (coeff α d) f else 0
Tactic:
simp only [eq_self_iff_true, if_true]
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
⊢ f d = (coeff α d) f
Theorem: MvPowerSeries.as_sum_of_homogeneous_components'
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
⊢ f d = (coeff α d) f
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPowerSeries.as_sum_of_homogeneous_components'
Proof state before:
case h.h₀
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
⊢ ∀ b ∈ ⋯.toFinset, b ≠ (weight w) d → (if (weight w) d = b then (coeff α d) f else 0) = 0
Tactic:
intro b _ h'
Proof state after:
case h.h₀
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
b : ℕ
a✝ : b ∈ ⋯.toFinset
h' : b ≠ (weight w) d
⊢ (if (weight w) d = b then (coeff α d) f else 0) = 0
Theorem: MvPowerSeries.as_sum_of_homogeneous_components'
Proof state before:
case h.h₀
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
b : ℕ
a✝ : b ∈ ⋯.toFinset
h' : b ≠ (weight w) d
⊢ (if (weight w) d = b then (coeff α d) f else 0) = 0
Tactic:
rw [if_neg (Ne.symm h')]
Proof state after:
no goals
Theorem: MvPowerSeries.as_sum_of_homogeneous_components'
Proof state before:
case h.h₁
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.70732
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
hf : StronglySummable fun p => (homogeneousComponent w p) f
d : σ →₀ ℕ
⊢ (weight w) d ∉ ⋯.toFinset → (if (weight w) d = (weight w) d then (coeff α d) f else 0) = 0
Tactic:
simp only [Finite.mem_toFinset, Function.mem_support, Classical.not_not, imp_self]
Proof state after:
no goals
Theorem: MvPowerSeries.support_partialProduct_subset
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 : σ →₀ ℕ
⊢ (support fun I => (coeff α d) (partialProduct f I)) ⊆ ↑(hf.unionOfSupportOfCoeffLe d).powerset
Tactic:
intro I
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 : σ →₀ ℕ
I : Finset ι
⊢ (I ∈ support fun I => (coeff α d) (partialProduct f I)) → I ∈ ↑(hf.unionOfSupportOfCoeffLe d).powerset
Theorem: MvPowerSeries.support_partialProduct_subset
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 : σ →₀ ℕ
I : Finset ι
⊢ (I ∈ support fun I => (coeff α d) (partialProduct f I)) → I ∈ ↑(hf.unionOfSupportOfCoeffLe d).powerset
Tactic:
simp only [mem_support, ne_eq, coe_powerset, Set.mem_preimage, Set.mem_powerset_iff,
  Finset.coe_subset, not_imp_comm, Finset.not_subset]
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 : σ →₀ ℕ
I : Finset ι
⊢ (∃ x ∈ I, x ∉ hf.unionOfSupportOfCoeffLe d) → (coeff α d) (partialProduct f I) = 0
Theorem: MvPowerSeries.support_partialProduct_subset
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 : σ →₀ ℕ
I : Finset ι
⊢ (∃ x ∈ I, x ∉ hf.unionOfSupportOfCoeffLe d) → (coeff α d) (partialProduct f I) = 0
Tactic:
rintro ⟨i, hi, h⟩
Proof state after:
case 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 : σ →₀ ℕ
I : Finset ι
i : ι
hi : i ∈ I
h : i ∉ hf.unionOfSupportOfCoeffLe d
⊢ (coeff α d) (partialProduct f I) = 0
Theorem: MvPowerSeries.support_partialProduct_subset
Proof state before:
case 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 : σ →₀ ℕ
I : Finset ι
i : ι
hi : i ∈ I
h : i ∉ hf.unionOfSupportOfCoeffLe d
⊢ (coeff α d) (partialProduct f I) = 0
Tactic:
rw [StronglySummable.not_mem_unionOfSupportOfCoeffLe_iff] at h
Proof state after:
case 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 : σ →₀ ℕ
I : Finset ι
i : ι
hi : i ∈ I
h : ∀ e ≤ d, (coeff α e) (f i) = 0
⊢ (coeff α d) (partialProduct f I) = 0
Theorem: MvPowerSeries.support_partialProduct_subset
Proof state before:
case 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 : σ →₀ ℕ
I : Finset ι
i : ι
hi : i ∈ I
h : ∀ e ≤ d, (coeff α e) (f i) = 0
⊢ (coeff α d) (partialProduct f I) = 0
Tactic:
simp only [partialProduct, prod_eq_mul_prod_diff_singleton hi, coeff_mul]
Proof state after:
case 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 : σ →₀ ℕ
I : Finset ι
i : ι
hi : i ∈ I
h : ∀ e ≤ d, (coeff α e) (f i) = 0
⊢ ∑ p ∈ antidiagonal d, (coeff α p.1) (f i) * (coeff α p.2) (∏ i ∈ I \ {i}, f i) = 0
Theorem: MvPowerSeries.support_partialProduct_subset
Proof state before:
case 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 : σ →₀ ℕ
I : Finset ι
i : ι
hi : i ∈ I
h : ∀ e ≤ d, (coeff α e) (f i) = 0
⊢ ∑ p ∈ antidiagonal d, (coeff α p.1) (f i) * (coeff α p.2) (∏ i ∈ I \ {i}, f i) = 0
Tactic:
apply sum_eq_zero
Proof state after:
case 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 : σ →₀ ℕ
I : Finset ι
i : ι
hi : i ∈ I
h : ∀ e ≤ d, (coeff α e) (f i) = 0
⊢ ∀ x ∈ antidiagonal d, (coeff α x.1) (f i) * (coeff α x.2) (∏ i ∈ I \ {i}, f i) = 0
Theorem: MvPowerSeries.support_partialProduct_subset
Proof state before:
case 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 : σ →₀ ℕ
I : Finset ι
i : ι
hi : i ∈ I
h : ∀ e ≤ d, (coeff α e) (f i) = 0
⊢ ∀ x ∈ antidiagonal d, (coeff α x.1) (f i) * (coeff α x.2) (∏ i ∈ I \ {i}, f i) = 0
Tactic:
rintro ⟨x, y⟩
Proof state after:
case 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 : σ →₀ ℕ
I : Finset ι
i : ι
hi : i ∈ I
h : ∀ e ≤ d, (coeff α e) (f i) = 0
x y : σ →₀ ℕ
⊢ (x, y) ∈ antidiagonal d → (coeff α (x, y).1) (f i) * (coeff α (x, y).2) (∏ i ∈ I \ {i}, f i) = 0
Theorem: MvPowerSeries.support_partialProduct_subset
Proof state before:
case 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 : σ →₀ ℕ
I : Finset ι
i : ι
hi : i ∈ I
h : ∀ e ≤ d, (coeff α e) (f i) = 0
x y : σ →₀ ℕ
⊢ (x, y) ∈ antidiagonal d → (coeff α (x, y).1) (f i) * (coeff α (x, y).2) (∏ i ∈ I \ {i}, f i) = 0
Tactic:
rw [mem_antidiagonal]
Proof state after:
case 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 : σ →₀ ℕ
I : Finset ι
i : ι
hi : i ∈ I
h : ∀ e ≤ d, (coeff α e) (f i) = 0
x y : σ →₀ ℕ
⊢ (x, y).1 + (x, y).2 = d → (coeff α (x, y).1) (f i) * (coeff α (x, y).2) (∏ i ∈ I \ {i}, f i) = 0
Theorem: MvPowerSeries.support_partialProduct_subset
Proof state before:
case 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 : σ →₀ ℕ
I : Finset ι
i : ι
hi : i ∈ I
h : ∀ e ≤ d, (coeff α e) (f i) = 0
x y : σ →₀ ℕ
⊢ (x, y).1 + (x, y).2 = d → (coeff α (x, y).1) (f i) * (coeff α (x, y).2) (∏ i ∈ I \ {i}, f i) = 0
Tactic:
intro hxy
Proof state after:
case 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 : σ →₀ ℕ
I : Finset ι
i : ι
hi : i ∈ I
h : ∀ e ≤ d, (coeff α e) (f i) = 0
x y : σ →₀ ℕ
hxy : (x, y).1 + (x, y).2 = d
⊢ (coeff α (x, y).1) (f i) * (coeff α (x, y).2) (∏ i ∈ I \ {i}, f i) = 0
Theorem: MvPowerSeries.support_partialProduct_subset
Proof state before:
case 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 : σ →₀ ℕ
I : Finset ι
i : ι
hi : i ∈ I
h : ∀ e ≤ d, (coeff α e) (f i) = 0
x y : σ →₀ ℕ
hxy : (x, y).1 + (x, y).2 = d
⊢ (coeff α (x, y).1) (f i) * (coeff α (x, y).2) (∏ i ∈ I \ {i}, f i) = 0
Tactic:
rw [h 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 : σ →₀ ℕ
I : Finset ι
i : ι
hi : i ∈ I
h : ∀ e ≤ d, (coeff α e) (f i) = 0
x y : σ →₀ ℕ
hxy : (x, y).1 + (x, y).2 = d
⊢ x ≤ d
Theorem: MvPowerSeries.support_partialProduct_subset
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 : σ →₀ ℕ
I : Finset ι
i : ι
hi : i ∈ I
h : ∀ e ≤ d, (coeff α e) (f i) = 0
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: MvPowerSeries.StronglySummable.toStronglyMultipliable
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
hf : StronglySummable f
⊢ StronglyMultipliable f
Tactic:
classical
exact fun d => Finite.subset (finite_toSet _) (support_partialProduct_subset f hf d)
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.toStronglyMultipliable
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
hf : StronglySummable f
⊢ StronglyMultipliable f
Tactic:
exact fun d => Finite.subset (finite_toSet _) (support_partialProduct_subset f hf d)
Proof state after:
no goals
Theorem: MvPowerSeries.StronglyMultipliable.finset_prod_eq
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
inst✝¹ : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝ : DecidableEq ι
s : Finset ι
hf : StronglyMultipliable f
⊢ ∏ i ∈ s, (1 + f i) = ⋯.sum
Tactic:
rw [Finset.prod_one_add]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
inst✝¹ : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝ : DecidableEq ι
s : Finset ι
hf : StronglyMultipliable f
⊢ ∑ t ∈ s.powerset, ∏ i ∈ t, f i = ⋯.sum
Theorem: MvPowerSeries.StronglyMultipliable.finset_prod_eq
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
inst✝¹ : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝ : DecidableEq ι
s : Finset ι
hf : StronglyMultipliable f
⊢ ∑ t ∈ s.powerset, ∏ i ∈ t, f i = ⋯.sum
Tactic:
ext d
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 : σ →₀ ℕ
⊢ (coeff α d) (∑ t ∈ s.powerset, ∏ i ∈ t, f i) = (coeff α d) ⋯.sum
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 : σ →₀ ℕ
⊢ (coeff α d) (∑ t ∈ s.powerset, ∏ i ∈ t, f i) = (coeff α d) ⋯.sum
Tactic:
rw [map_sum, StronglySummable.coeff_sum d]
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 : σ →₀ ℕ
⊢ ∑ x ∈ s.powerset, (coeff α d) (∏ i ∈ x, f i) =
    ∑ i ∈ ?m.81701, (coeff α d) ({I | I ⊆ s}.indicator (partialProduct f) i)

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)) ⊆ ↑?m.81701

σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
inst✝¹ : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝ : DecidableEq ι
s : Finset ι
hf : StronglyMultipliable f
d : σ →₀ ℕ
⊢ Finset (Finset ι)
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 : σ →₀ ℕ
⊢ ∑ x ∈ s.powerset, (coeff α d) (∏ i ∈ x, f i) =
    ∑ i ∈ ?m.81701, (coeff α d) ({I | I ⊆ s}.indicator (partialProduct f) i)
Tactic:
apply sum_congr rfl
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 : σ →₀ ℕ
⊢ ∀ x ∈ s.powerset, (coeff α d) (∏ i ∈ x, f i) = (coeff α d) ({I | I ⊆ s}.indicator (partialProduct f) x)
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 : σ →₀ ℕ
⊢ ∀ x ∈ s.powerset, (coeff α d) (∏ i ∈ x, f i) = (coeff α d) ({I | I ⊆ s}.indicator (partialProduct f) x)
Tactic:
intro t 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.powerset
⊢ (coeff α d) (∏ i ∈ t, f i) = (coeff α d) ({I | I ⊆ s}.indicator (partialProduct f) t)
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.powerset
⊢ (coeff α d) (∏ i ∈ t, f i) = (coeff α d) ({I | I ⊆ s}.indicator (partialProduct f) t)
Tactic:
apply congr_arg
Proof state after:
case h.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.powerset
⊢ ∏ i ∈ t, f i = {I | I ⊆ s}.indicator (partialProduct f) t
Theorem: MvPowerSeries.StronglyMultipliable.finset_prod_eq
Proof state before:
case h.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.powerset
⊢ ∏ i ∈ t, f i = {I | I ⊆ s}.indicator (partialProduct f) t
Tactic:
rw [indicator, if_pos]
Proof state after:
case h.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.powerset
⊢ ∏ i ∈ t, f i = partialProduct f t

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}
Theorem: MvPowerSeries.StronglyMultipliable.finset_prod_eq
Proof state before:
case h.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.powerset
⊢ ∏ i ∈ t, f i = partialProduct f t

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:
rfl
Proof state after:
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}