internlm/Lean-Github huggingface dataset:
Theorem: Submodule.mem_span_iff_exists_sum'
Proof state before:
case h.mpr
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
h : (a.sum fun i c => c • f ↑i) = x
⊢ ∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • f ↑i) = x
Tactic:
simp only [mem_top, Subtype.forall, implies_true, exists_prop, true_and]
Proof state after:
case h.mpr
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
h : (a.sum fun i c => c • f ↑i) = x
⊢ (a.sum fun i c => c • f ↑i) = x
Theorem: Submodule.mem_span_iff_exists_sum'
Proof state before:
case h.mpr
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
s : Set ι
f : ι → M
x : M
a : ↑s →₀ R
h : (a.sum fun i c => c • f ↑i) = x
⊢ (a.sum fun i c => c • f ↑i) = x
Tactic:
exact h
Proof state after:
no goals
Theorem: Submodule.mem_span_set_iff_exists_sum
Proof state before:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
⊢ x ∈ span R s ↔ ∃ a, (a.sum fun i c => c • ↑i) = x
Tactic:
conv_lhs => rw [← Set.image_id s]
Proof state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
⊢ x ∈ span R (id '' s) ↔ ∃ a, (a.sum fun i c => c • ↑i) = x
Theorem: Submodule.mem_span_set_iff_exists_sum
Proof state before:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
⊢ x ∈ span R (id '' s) ↔ ∃ a, (a.sum fun i c => c • ↑i) = x
Tactic:
rw [← top_smul (span R (id '' s)), mem_ideal_smul_span_iff_exists_sum']
Proof state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
⊢ (∃ a, ∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • id ↑i) = x) ↔ ∃ a, (a.sum fun i c => c • ↑i) = x
Theorem: Submodule.mem_span_set_iff_exists_sum
Proof state before:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
⊢ (∃ a, ∃ (_ : ∀ (i : ↑s), a i ∈ ⊤), (a.sum fun i c => c • id ↑i) = x) ↔ ∃ a, (a.sum fun i c => c • ↑i) = x
Tactic:
exact exists_congr fun a => ⟨fun ⟨_, h⟩ => h, fun h => ⟨fun i => mem_top, h⟩⟩
Proof state after:
no goals
Theorem: DividedPowerAlgebra.coeff_exp'
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
n : ℕ
⊢ (coeff (DividedPowerAlgebra R M) n) (exp' R m) = dp R n m
Tactic:
simp only [coeff_mk, exp']
Proof state after:
no goals
Theorem: DividedPowerAlgebra.isExponential_exp'
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
⊢ (exp' R m).IsExponential
Tactic:
rw [isExponential_iff]
Proof state after:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
⊢ (constantCoeff (DividedPowerAlgebra R M)) (exp' R m) = 1 ∧
    ∀ (p q : ℕ),
      ↑((p + q).choose p) * (coeff (DividedPowerAlgebra R M) (p + q)) (exp' R m) =
        (coeff (DividedPowerAlgebra R M) p) (exp' R m) * (coeff (DividedPowerAlgebra R M) q) (exp' R m)
Theorem: DividedPowerAlgebra.isExponential_exp'
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
⊢ (constantCoeff (DividedPowerAlgebra R M)) (exp' R m) = 1 ∧
    ∀ (p q : ℕ),
      ↑((p + q).choose p) * (coeff (DividedPowerAlgebra R M) (p + q)) (exp' R m) =
        (coeff (DividedPowerAlgebra R M) p) (exp' R m) * (coeff (DividedPowerAlgebra R M) q) (exp' R m)
Tactic:
constructor
Proof state after:
case left
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
⊢ (constantCoeff (DividedPowerAlgebra R M)) (exp' R m) = 1

case right
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
⊢ ∀ (p q : ℕ),
    ↑((p + q).choose p) * (coeff (DividedPowerAlgebra R M) (p + q)) (exp' R m) =
      (coeff (DividedPowerAlgebra R M) p) (exp' R m) * (coeff (DividedPowerAlgebra R M) q) (exp' R m)
Theorem: DividedPowerAlgebra.isExponential_exp'
Proof state before:
case left
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
⊢ (constantCoeff (DividedPowerAlgebra R M)) (exp' R m) = 1
Tactic:
rw [← coeff_zero_eq_constantCoeff, coeff_exp', dp_zero]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.isExponential_exp'
Proof state before:
case right
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
⊢ ∀ (p q : ℕ),
    ↑((p + q).choose p) * (coeff (DividedPowerAlgebra R M) (p + q)) (exp' R m) =
      (coeff (DividedPowerAlgebra R M) p) (exp' R m) * (coeff (DividedPowerAlgebra R M) q) (exp' R m)
Tactic:
intro p q
Proof state after:
case right
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
p q : ℕ
⊢ ↑((p + q).choose p) * (coeff (DividedPowerAlgebra R M) (p + q)) (exp' R m) =
    (coeff (DividedPowerAlgebra R M) p) (exp' R m) * (coeff (DividedPowerAlgebra R M) q) (exp' R m)
Theorem: DividedPowerAlgebra.isExponential_exp'
Proof state before:
case right
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
p q : ℕ
⊢ ↑((p + q).choose p) * (coeff (DividedPowerAlgebra R M) (p + q)) (exp' R m) =
    (coeff (DividedPowerAlgebra R M) p) (exp' R m) * (coeff (DividedPowerAlgebra R M) q) (exp' R m)
Tactic:
simp only [coeff_exp', dp_mul, nsmul_eq_mul]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.coeff_exp
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
n : ℕ
⊢ (coeff (DividedPowerAlgebra R M) n) ↑(exp R m) = dp R n m
Tactic:
simp only [coe_exp, coeff_exp']
Proof state after:
no goals
Theorem: DividedPowerAlgebra.coeff_exp_LinearMap
Proof state before:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
n : ℕ
m : M
⊢ (coeff (DividedPowerAlgebra R M) n) ↑((exp_LinearMap R M) m) = dp R n m
Tactic:
rw [coe_exp_LinearMap, coeff_exp]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dividedPowerAlgebra_exponentialModule_equiv_symm_apply
Proof state before:
R : Type u_1
inst✝⁸ : CommRing R
A : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
β : M →ₗ[R] ↥(ExponentialModule S)
n : ℕ
m : M
⊢ ((dividedPowerAlgebra_exponentialModule_equiv R M S).symm β) (dp R n m) = (coeff S n) ↑(β m)
Tactic:
unfold dividedPowerAlgebra_exponentialModule_equiv
Proof state after:
R : Type u_1
inst✝⁸ : CommRing R
A : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
β : M →ₗ[R] ↥(ExponentialModule S)
n : ℕ
m : M
⊢ ({ toFun := fun α => linearMap α ∘ₗ exp_LinearMap R M,
            invFun := fun β =>
              lift'
                (fun x =>
                  match x with
                  | (n, m) => (coeff S n) ↑(β m))
                ⋯ ⋯ ⋯ ⋯,
            left_inv := ⋯, right_inv := ⋯ }.symm
        β)
      (dp R n m) =
    (coeff S n) ↑(β m)
Theorem: DividedPowerAlgebra.dividedPowerAlgebra_exponentialModule_equiv_symm_apply
Proof state before:
R : Type u_1
inst✝⁸ : CommRing R
A : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
β : M →ₗ[R] ↥(ExponentialModule S)
n : ℕ
m : M
⊢ ({ toFun := fun α => linearMap α ∘ₗ exp_LinearMap R M,
            invFun := fun β =>
              lift'
                (fun x =>
                  match x with
                  | (n, m) => (coeff S n) ↑(β m))
                ⋯ ⋯ ⋯ ⋯,
            left_inv := ⋯, right_inv := ⋯ }.symm
        β)
      (dp R n m) =
    (coeff S n) ↑(β m)
Tactic:
simp only [Equiv.coe_fn_symm_mk, lift'AlgHom_apply_dp]
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.sum_eq_tsum
Proof state before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
⊢ hf.sum = tsum f
Tactic:
ext d
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ (coeff α d) hf.sum = (coeff α d) (tsum f)
Theorem: MvPowerSeries.StronglySummable.sum_eq_tsum
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ (coeff α d) hf.sum = (coeff α d) (tsum f)
Tactic:
rw [tsum_def, dif_pos hf.summable]
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ (coeff α d) hf.sum = (coeff α d) (if (support f).Finite then finsum f else Exists.choose ⋯)
Theorem: MvPowerSeries.StronglySummable.sum_eq_tsum
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ (coeff α d) hf.sum = (coeff α d) (if (support f).Finite then finsum f else Exists.choose ⋯)
Tactic:
apply HasSum.unique (hf.hasSum_coeff d)
Proof state after:
case h
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ HasSum (fun i => (coeff α d) (f i)) ((coeff α d) (if (support f).Finite then finsum f else Exists.choose ⋯))
Theorem: MvPowerSeries.StronglySummable.sum_eq_tsum
Proof state before:
case h
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ HasSum (fun i => (coeff α d) (f i)) ((coeff α d) (if (support f).Finite then finsum f else Exists.choose ⋯))
Tactic:
apply HasSum.map
Proof state after:
case h.hf
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ HasSum (fun i => f i) (if (support f).Finite then finsum f else Exists.choose ⋯)

case h.hg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ Continuous ⇑(coeff α d)
Theorem: MvPowerSeries.StronglySummable.sum_eq_tsum
Proof state before:
case h.hf
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ HasSum (fun i => f i) (if (support f).Finite then finsum f else Exists.choose ⋯)

case h.hg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ Continuous ⇑(coeff α d)
Tactic:
. split_ifs with h
  . rw [← tsum_eq_finsum h]
    exact hf.summable.hasSum
  . exact (Classical.choose_spec hf.summable)
Proof state after:
case h.hg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ Continuous ⇑(coeff α d)
Theorem: MvPowerSeries.StronglySummable.sum_eq_tsum
Proof state before:
case h.hg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ Continuous ⇑(coeff α d)
Tactic:
. exact continuous_component σ α d
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.sum_eq_tsum
Proof state before:
case h.hf
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ HasSum (fun i => f i) (if (support f).Finite then finsum f else Exists.choose ⋯)
Tactic:
split_ifs with h
Proof state after:
case pos
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
h : (support f).Finite
⊢ HasSum (fun i => f i) (finsum f)

case neg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
h : ¬(support f).Finite
⊢ HasSum (fun i => f i) (Exists.choose ⋯)
Theorem: MvPowerSeries.StronglySummable.sum_eq_tsum
Proof state before:
case pos
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
h : (support f).Finite
⊢ HasSum (fun i => f i) (finsum f)

case neg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
h : ¬(support f).Finite
⊢ HasSum (fun i => f i) (Exists.choose ⋯)
Tactic:
. rw [← tsum_eq_finsum h]
  exact hf.summable.hasSum
Proof state after:
case neg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
h : ¬(support f).Finite
⊢ HasSum (fun i => f i) (Exists.choose ⋯)
Theorem: MvPowerSeries.StronglySummable.sum_eq_tsum
Proof state before:
case neg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
h : ¬(support f).Finite
⊢ HasSum (fun i => f i) (Exists.choose ⋯)
Tactic:
. exact (Classical.choose_spec hf.summable)
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.sum_eq_tsum
Proof state before:
case pos
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
h : (support f).Finite
⊢ HasSum (fun i => f i) (finsum f)
Tactic:
rw [← tsum_eq_finsum h]
Proof state after:
case pos
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
h : (support f).Finite
⊢ HasSum (fun i => f i) (∑' (b : ι), f b)
Theorem: MvPowerSeries.StronglySummable.sum_eq_tsum
Proof state before:
case pos
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
h : (support f).Finite
⊢ HasSum (fun i => f i) (∑' (b : ι), f b)
Tactic:
exact hf.summable.hasSum
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.sum_eq_tsum
Proof state before:
case neg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
h : ¬(support f).Finite
⊢ HasSum (fun i => f i) (Exists.choose ⋯)
Tactic:
exact (Classical.choose_spec hf.summable)
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.sum_eq_tsum
Proof state before:
case h.hg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Semiring α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : ι → MvPowerSeries σ α
hf : StronglySummable f
d : σ →₀ ℕ
⊢ Continuous ⇑(coeff α d)
Tactic:
exact continuous_component σ α d
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.iff_summable'
Proof state before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → MvPowerSeries σ α
⊢ StronglySummable f ↔ Filter.Tendsto f Filter.cofinite (nhds 0)
Tactic:
haveI := topologicalRing σ α
Proof state after:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → MvPowerSeries σ α
this : TopologicalRing (MvPowerSeries σ α)
⊢ StronglySummable f ↔ Filter.Tendsto f Filter.cofinite (nhds 0)
Theorem: MvPowerSeries.StronglySummable.iff_summable'
Proof state before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → MvPowerSeries σ α
this : TopologicalRing (MvPowerSeries σ α)
⊢ StronglySummable f ↔ Filter.Tendsto f Filter.cofinite (nhds 0)
Tactic:
refine' ⟨fun hf => hf.summable.tendsto_cofinite_zero, _⟩
Proof state after:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → MvPowerSeries σ α
this : TopologicalRing (MvPowerSeries σ α)
⊢ Filter.Tendsto f Filter.cofinite (nhds 0) → StronglySummable f
Theorem: MvPowerSeries.StronglySummable.iff_summable'
Proof state before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → MvPowerSeries σ α
this : TopologicalRing (MvPowerSeries σ α)
⊢ Filter.Tendsto f Filter.cofinite (nhds 0) → StronglySummable f
Tactic:
rw [StronglySummable, nhds_pi, Filter.tendsto_pi]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → MvPowerSeries σ α
this : TopologicalRing (MvPowerSeries σ α)
⊢ (∀ (i : σ →₀ ℕ), Filter.Tendsto (fun x => f x i) Filter.cofinite (nhds (0 i))) →
    ∀ (d : σ →₀ ℕ), (support fun i => (coeff α d) (f i)).Finite
Theorem: MvPowerSeries.StronglySummable.iff_summable'
Proof state before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
inst✝² : Ring α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → MvPowerSeries σ α
this : TopologicalRing (MvPowerSeries σ α)
⊢ (∀ (i : σ →₀ ℕ), Filter.Tendsto (fun x => f x i) Filter.cofinite (nhds (0 i))) →
    ∀ (d : σ →₀ ℕ), (support fun i => (coeff α d) (f i)).Finite
Tactic:
exact forall_imp fun d => finite_support_of_tendsto_zero
Proof state after:
no goals
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
⊢ HasProd (fun i => 1 + f i) ⋯.prod
Tactic:
haveI := uniformAddGroup σ α
Proof state after:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
⊢ HasProd (fun i => 1 + f i) ⋯.prod
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
⊢ HasProd (fun i => 1 + f i) ⋯.prod
Tactic:
intro V hV
Proof state after:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
⊢ V ∈ Filter.map (fun s => ∏ b ∈ s, (fun i => 1 + f i) b) Filter.atTop
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
⊢ V ∈ Filter.map (fun s => ∏ b ∈ s, (fun i => 1 + f i) b) Filter.atTop
Tactic:
simp only [Filter.mem_map, Filter.mem_atTop_sets, ge_iff_le, Finset.le_eq_subset,
  Set.mem_preimage]
Proof state after:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
⊢ ∃ a, ∀ (b : Finset ι), a ⊆ b → ∏ x ∈ b, (1 + f x) ∈ V
Theorem: MvPowerSeries.StronglySummable.hasProd_of_one_add
Proof state before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
⊢ ∃ a, ∀ (b : Finset ι), a ⊆ b → ∏ x ∈ b, (1 + f x) ∈ V
Tactic:
let V₀ := Add.add hf.toStronglyMultipliable.prod ⁻¹' V
Proof state after:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
hf : StronglySummable f
this : UniformAddGroup (MvPowerSeries σ α)
V : Set (MvPowerSeries σ α)
hV : V ∈ nhds ⋯.prod
V₀ : Set (MvPowerSeries σ α) := Add.add ⋯.prod ⁻¹' V
⊢ ∃ a, ∀ (b : Finset ι), a ⊆ b → ∏ x ∈ b, (1 + f x) ∈ V