internlm/Lean-Github huggingface dataset:
Theorem: MvPowerSeries.StronglySummable.sum_mul
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ (coeff α d) ⋯.sum = (coeff α d) (hf.sum * hg.sum)
Tactic:
simp_rw [coeff_sum d (support_mul hf hg d), coeff_mul]
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ ∑ x ∈ ((antidiagonal d).biUnion fun b => ⋯.toFinset).product ((antidiagonal d).biUnion fun b => ⋯.toFinset),
      ∑ p ∈ antidiagonal d, (coeff α p.1) (f x.1) * (coeff α p.2) (g x.2) =
    ∑ p ∈ antidiagonal d, (coeff α p.1) hf.sum * (coeff α p.2) hg.sum
Theorem: MvPowerSeries.StronglySummable.sum_mul
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ ∑ x ∈ ((antidiagonal d).biUnion fun b => ⋯.toFinset).product ((antidiagonal d).biUnion fun b => ⋯.toFinset),
      ∑ p ∈ antidiagonal d, (coeff α p.1) (f x.1) * (coeff α p.2) (g x.2) =
    ∑ p ∈ antidiagonal d, (coeff α p.1) hf.sum * (coeff α p.2) hg.sum
Tactic:
rw [sum_comm]
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ ∑ y ∈ antidiagonal d,
      ∑ x ∈ ((antidiagonal d).biUnion fun b => ⋯.toFinset).product ((antidiagonal d).biUnion fun b => ⋯.toFinset),
        (coeff α y.1) (f x.1) * (coeff α y.2) (g x.2) =
    ∑ p ∈ antidiagonal d, (coeff α p.1) hf.sum * (coeff α p.2) hg.sum
Theorem: MvPowerSeries.StronglySummable.sum_mul
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ ∑ y ∈ antidiagonal d,
      ∑ x ∈ ((antidiagonal d).biUnion fun b => ⋯.toFinset).product ((antidiagonal d).biUnion fun b => ⋯.toFinset),
        (coeff α y.1) (f x.1) * (coeff α y.2) (g x.2) =
    ∑ p ∈ antidiagonal d, (coeff α p.1) hf.sum * (coeff α p.2) hg.sum
Tactic:
apply Finset.sum_congr rfl
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ ∀ x ∈ antidiagonal d,
    ∑ x_1 ∈ ((antidiagonal d).biUnion fun b => ⋯.toFinset).product ((antidiagonal d).biUnion fun b => ⋯.toFinset),
        (coeff α x.1) (f x_1.1) * (coeff α x.2) (g x_1.2) =
      (coeff α x.1) hf.sum * (coeff α x.2) hg.sum
Theorem: MvPowerSeries.StronglySummable.sum_mul
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
⊢ ∀ x ∈ antidiagonal d,
    ∑ x_1 ∈ ((antidiagonal d).biUnion fun b => ⋯.toFinset).product ((antidiagonal d).biUnion fun b => ⋯.toFinset),
        (coeff α x.1) (f x_1.1) * (coeff α x.2) (g x_1.2) =
      (coeff α x.1) hf.sum * (coeff α x.2) hg.sum
Tactic:
rintro bc hbc
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
⊢ ∑ x ∈ ((antidiagonal d).biUnion fun b => ⋯.toFinset).product ((antidiagonal d).biUnion fun b => ⋯.toFinset),
      (coeff α bc.1) (f x.1) * (coeff α bc.2) (g x.2) =
    (coeff α bc.1) hf.sum * (coeff α bc.2) hg.sum
Theorem: MvPowerSeries.StronglySummable.sum_mul
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
⊢ ∑ x ∈ ((antidiagonal d).biUnion fun b => ⋯.toFinset).product ((antidiagonal d).biUnion fun b => ⋯.toFinset),
      (coeff α bc.1) (f x.1) * (coeff α bc.2) (g x.2) =
    (coeff α bc.1) hf.sum * (coeff α bc.2) hg.sum
Tactic:
erw [Finset.sum_product]
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
⊢ ∑ x ∈ (antidiagonal d).biUnion fun b => ⋯.toFinset,
      ∑ y ∈ (antidiagonal d).biUnion fun b => ⋯.toFinset, (coeff α bc.1) (f (x, y).1) * (coeff α bc.2) (g (x, y).2) =
    (coeff α bc.1) hf.sum * (coeff α bc.2) hg.sum
Theorem: MvPowerSeries.StronglySummable.sum_mul
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
⊢ ∑ x ∈ (antidiagonal d).biUnion fun b => ⋯.toFinset,
      ∑ y ∈ (antidiagonal d).biUnion fun b => ⋯.toFinset, (coeff α bc.1) (f (x, y).1) * (coeff α bc.2) (g (x, y).2) =
    (coeff α bc.1) hf.sum * (coeff α bc.2) hg.sum
Tactic:
rw [coeff_sum _, coeff_sum _, sum_mul_sum]
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
⊢ (support fun i => (coeff α bc.2) (g i)) ⊆ ↑((antidiagonal d).biUnion fun b => ⋯.toFinset)

case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
⊢ (support fun i => (coeff α bc.1) (f i)) ⊆ ↑((antidiagonal d).biUnion fun b => ⋯.toFinset)
Theorem: MvPowerSeries.StronglySummable.sum_mul
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
⊢ (support fun i => (coeff α bc.2) (g i)) ⊆ ↑((antidiagonal d).biUnion fun b => ⋯.toFinset)

case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
⊢ (support fun i => (coeff α bc.1) (f i)) ⊆ ↑((antidiagonal d).biUnion fun b => ⋯.toFinset)
Tactic:
all_goals
  intro x hx
  apply @Finset.subset_biUnion_of_mem _ _ _ _ _ bc hbc
  exact (Finite.mem_toFinset _).mpr hx
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.sum_mul
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
⊢ (support fun i => (coeff α bc.1) (f i)) ⊆ ↑((antidiagonal d).biUnion fun b => ⋯.toFinset)
Tactic:
intro x hx
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
x : ι
hx : x ∈ support fun i => (coeff α bc.1) (f i)
⊢ x ∈ ↑((antidiagonal d).biUnion fun b => ⋯.toFinset)
Theorem: MvPowerSeries.StronglySummable.sum_mul
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
x : ι
hx : x ∈ support fun i => (coeff α bc.1) (f i)
⊢ x ∈ ↑((antidiagonal d).biUnion fun b => ⋯.toFinset)
Tactic:
apply @Finset.subset_biUnion_of_mem _ _ _ _ _ bc hbc
Proof state after:
case h.a
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
x : ι
hx : x ∈ support fun i => (coeff α bc.1) (f i)
⊢ x ∈ ⋯.toFinset
Theorem: MvPowerSeries.StronglySummable.sum_mul
Proof state before:
case h.a
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
d : σ →₀ ℕ
bc : (σ →₀ ℕ) × (σ →₀ ℕ)
hbc : bc ∈ antidiagonal d
x : ι
hx : x ∈ support fun i => (coeff α bc.1) (f i)
⊢ x ∈ ⋯.toFinset
Tactic:
exact (Finite.mem_toFinset _).mpr hx
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.sum_mul'
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
hh : StronglySummable fun i => f i.1 * g i.2
⊢ hh.sum = hf.sum * hg.sum
Tactic:
rw [← sum_mul]
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.of_indicator
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
⊢ StronglySummable fun i => s.indicator f i
Tactic:
intro d
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((fun i => s.indicator f i) i)).Finite
Theorem: MvPowerSeries.StronglySummable.of_indicator
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((fun i => s.indicator f i) i)).Finite
Tactic:
apply (hf d).subset
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((fun i => s.indicator f i) i)) ⊆ support fun i => (coeff α d) (f i)
Theorem: MvPowerSeries.StronglySummable.of_indicator
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((fun i => s.indicator f i) i)) ⊆ support fun i => (coeff α d) (f i)
Tactic:
intro i
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
i : ι
⊢ (i ∈ support fun i => (coeff α d) ((fun i => s.indicator f i) i)) → i ∈ support fun i => (coeff α d) (f i)
Theorem: MvPowerSeries.StronglySummable.of_indicator
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
i : ι
⊢ (i ∈ support fun i => (coeff α d) ((fun i => s.indicator f i) i)) → i ∈ support fun i => (coeff α d) (f i)
Tactic:
simp only [mem_support, ne_eq, not_imp_not]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
i : ι
⊢ (coeff α d) (f i) = 0 → (coeff α d) (s.indicator f i) = 0
Theorem: MvPowerSeries.StronglySummable.of_indicator
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
i : ι
⊢ (coeff α d) (f i) = 0 → (coeff α d) (s.indicator f i) = 0
Tactic:
intro hi
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
i : ι
hi : (coeff α d) (f i) = 0
⊢ (coeff α d) (s.indicator f i) = 0
Theorem: MvPowerSeries.StronglySummable.of_indicator
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
i : ι
hi : (coeff α d) (f i) = 0
⊢ (coeff α d) (s.indicator f i) = 0
Tactic:
cases' s.indicator_eq_zero_or_self f i with h h <;>
. simp only [h, hi, map_zero]
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.of_indicator
Proof state before:
case inr
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
i : ι
hi : (coeff α d) (f i) = 0
h : s.indicator f i = f i
⊢ (coeff α d) (s.indicator f i) = 0
Tactic:
simp only [h, hi, map_zero]
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.add_compl
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
⊢ hf.sum = ⋯.sum + ⋯.sum
Tactic:
rw [← sum_add (hf.of_indicator s) (hf.of_indicator (sᶜ))]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
⊢ hf.sum = ⋯.sum
Theorem: MvPowerSeries.StronglySummable.add_compl
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
⊢ hf.sum = ⋯.sum
Tactic:
exact sum_congr (s.indicator_self_add_compl f).symm
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.on_subtype
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
⊢ StronglySummable (f ∘ Subtype.val)
Tactic:
intro d
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((f ∘ Subtype.val) i)).Finite
Theorem: MvPowerSeries.StronglySummable.on_subtype
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((f ∘ Subtype.val) i)).Finite
Tactic:
apply Finite.of_finite_image _ (injOn_of_injective Subtype.coe_injective _)
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
⊢ ((fun a => ↑a) '' support fun i => (coeff α d) ((f ∘ Subtype.val) i)).Finite
Theorem: MvPowerSeries.StronglySummable.on_subtype
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
⊢ ((fun a => ↑a) '' support fun i => (coeff α d) ((f ∘ Subtype.val) i)).Finite
Tactic:
apply (hf d).subset
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
⊢ ((fun a => ↑a) '' support fun i => (coeff α d) ((f ∘ Subtype.val) i)) ⊆ support fun i => (coeff α d) (f i)
Theorem: MvPowerSeries.StronglySummable.on_subtype
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
⊢ ((fun a => ↑a) '' support fun i => (coeff α d) ((f ∘ Subtype.val) i)) ⊆ support fun i => (coeff α d) (f i)
Tactic:
rintro i ⟨j, hj, rfl⟩
Proof state after:
case intro.intro
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
j : { x // x ∈ s }
hj : j ∈ support fun i => (coeff α d) ((f ∘ Subtype.val) i)
⊢ (fun a => ↑a) j ∈ support fun i => (coeff α d) (f i)
Theorem: MvPowerSeries.StronglySummable.on_subtype
Proof state before:
case intro.intro
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
j : { x // x ∈ s }
hj : j ∈ support fun i => (coeff α d) ((f ∘ Subtype.val) i)
⊢ (fun a => ↑a) j ∈ support fun i => (coeff α d) (f i)
Tactic:
simp only [comp_apply, mem_support, ne_eq] at hj ⊢
Proof state after:
case intro.intro
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
j : { x // x ∈ s }
hj : ¬(coeff α d) (f ↑j) = 0
⊢ ¬(coeff α d) (f ↑j) = 0
Theorem: MvPowerSeries.StronglySummable.on_subtype
Proof state before:
case intro.intro
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
s : Set ι
d : σ →₀ ℕ
j : { x // x ∈ s }
hj : ¬(coeff α d) (f ↑j) = 0
⊢ ¬(coeff α d) (f ↑j) = 0
Tactic:
exact hj
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.hasSum_coeff
Proof state before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ HasSum (fun i => (coeff α d) (f i)) ((coeff α d) hf.sum)
Tactic:
apply hasSum_sum_of_ne_finset_zero
Proof state after:
case hf
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ ∀ b ∉ ⋯.toFinset, (coeff α d) (f b) = 0
Theorem: MvPowerSeries.StronglySummable.hasSum_coeff
Proof state before:
case hf
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ ∀ b ∉ ⋯.toFinset, (coeff α d) (f b) = 0
Tactic:
intro b hb
Proof state after:
case hf
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
b : ι
hb : b ∉ ⋯.toFinset
⊢ (coeff α d) (f b) = 0
Theorem: MvPowerSeries.StronglySummable.hasSum_coeff
Proof state before:
case hf
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
b : ι
hb : b ∉ ⋯.toFinset
⊢ (coeff α d) (f b) = 0
Tactic:
rw [Finite.mem_toFinset, Function.mem_support, Classical.not_not] at hb
Proof state after:
case hf
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
b : ι
hb : (coeff α d) (f b) = 0
⊢ (coeff α d) (f b) = 0
Theorem: MvPowerSeries.StronglySummable.hasSum_coeff
Proof state before:
case hf
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
ι : Type u_3
inst✝¹ : Semiring α
inst✝ : TopologicalSpace α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
b : ι
hb : (coeff α d) (f b) = 0
⊢ (coeff α d) (f b) = 0
Tactic:
exact hb
Proof state after:
no goals
Theorem: MvPowerSeries.homogeneous_components_self_stronglySummable
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.66393
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ StronglySummable fun p => (homogeneousComponent w p) f
Tactic:
intro d
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.66393
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((fun p => (homogeneousComponent w p) f) i)).Finite
Theorem: MvPowerSeries.homogeneous_components_self_stronglySummable
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.66393
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((fun p => (homogeneousComponent w p) f) i)).Finite
Tactic:
apply (finite_toSet {weight w d}).subset
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.66393
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((fun p => (homogeneousComponent w p) f) i)) ⊆ ↑{(weight w) d}
Theorem: MvPowerSeries.homogeneous_components_self_stronglySummable
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.66393
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ (support fun i => (coeff α d) ((fun p => (homogeneousComponent w p) f) i)) ⊆ ↑{(weight w) d}
Tactic:
intro p
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.66393
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
p : ℕ
⊢ (p ∈ support fun i => (coeff α d) ((fun p => (homogeneousComponent w p) f) i)) → p ∈ ↑{(weight w) d}
Theorem: MvPowerSeries.homogeneous_components_self_stronglySummable
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.66393
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
p : ℕ
⊢ (p ∈ support fun i => (coeff α d) ((fun p => (homogeneousComponent w p) f) i)) → p ∈ ↑{(weight w) d}
Tactic:
rw [Function.mem_support, ne_eq, mem_coe, coeff_homogeneousComponent, Finset.mem_singleton,
  ite_eq_right_iff, not_forall, exists_prop, and_imp]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.66393
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
p : ℕ
⊢ (weight w) d = p → ¬(coeff α d) f = 0 → p = (weight w) d
Theorem: MvPowerSeries.homogeneous_components_self_stronglySummable
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.66393
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
p : ℕ
⊢ (weight w) d = p → ¬(coeff α d) f = 0 → p = (weight w) d
Tactic:
intro h _
Proof state after:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.66393
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
p : ℕ
h : (weight w) d = p
a✝ : ¬(coeff α d) f = 0
⊢ p = (weight w) d
Theorem: MvPowerSeries.homogeneous_components_self_stronglySummable
Proof state before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.66393
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
p : ℕ
h : (weight w) d = p
a✝ : ¬(coeff α d) f = 0
⊢ p = (weight w) d
Tactic:
exact h.symm
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.68273
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
⊢ f = ⋯.sum
Tactic:
ext d
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type ?u.68273
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ (coeff α d) f = (coeff α d) ⋯.sum
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 : σ →₀ ℕ
⊢ (coeff α d) f = (coeff α d) ⋯.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.68273
inst✝ : Semiring α
w : σ → ℕ
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ f d = ∑ i ∈ ⋯.toFinset, if (weight w) d = i then (coeff α d) f else 0