Theorem: MvPowerSeries.StronglyMultipliable.finset_prod_eq (DividedPowers/ForMathlib/MvPowerSeries/StronglySummable/Basic.lean)

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]
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

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
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

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]
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 ι)

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
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)

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
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)

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
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

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]
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}

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
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}

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
State after:
no goals

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
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

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]
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

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'
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

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]
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}

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'
State after:
no goals