Theorem: MvPowerSeries.StronglyMultipliable.coeff_prod_apply_eq_finset_prod (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 ι
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]
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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