Theorem: MvPowerSeries.support_partialProduct_subset (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 : σ →₀ ℕ
⊢ (support fun I => (coeff α d) (partialProduct f I)) ⊆ ↑(hf.unionOfSupportOfCoeffLe d).powerset
Tactic:
intro I
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

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

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

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

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

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

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

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

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

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

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