awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion
Goal:
α : Type u_1
β : Type u_2
inst : AddCommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
f : β → α
mp :
  Summable f →
    (CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b) ∧
      Membership.mem (γ := Set (UniformSpace.Completion α))
        (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
        (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
mpr :
  (CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b) ∧
      Membership.mem (γ := Set (UniformSpace.Completion α))
        (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
        (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i)) →
    Summable f
⊢ Summable f ↔
    (CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b) ∧
      Membership.mem (γ := Set (UniformSpace.Completion α))
        (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
        (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion
Goal:
α : Type u_1
β : Type u_2
inst : AddCommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
f : β → α
a : α
ha : HasSum f a
⊢ (CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b) ∧
    Membership.mem (γ := Set (UniformSpace.Completion α))
      (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
      (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))

Tactic:
⟨ha.cauchySeq, ((summable_iff_summable_compl_and_tsum_mem f).mp ⟨a, ha⟩).2⟩

Premises used: Filter.Tendsto.cauchySeq, And.right, And.intro, Exists.intro, Iff.mp, summable_iff_summable_compl_and_tsum_mem
-- Module: Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion
Goal:
α : Type u_1
β : Type u_2
inst : AddCommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
f : β → α
a : α
ha : HasSum f a
⊢ (CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b) ∧
    Membership.mem (γ := Set (UniformSpace.Completion α))
      (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
      (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))

Tactic:
exact ⟨ha.cauchySeq, ((summable_iff_summable_compl_and_tsum_mem f).mp ⟨a, ha⟩).2⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion
Goal:
α : Type u_1
β : Type u_2
inst : AddCommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
f : β → α
h_cauchy : CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b
h_tsum :
  Membership.mem (γ := Set (UniformSpace.Completion α))
    (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
    (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
mpr :
  Summable (α := UniformSpace.Completion α) ((⇑toCompl : (a : α) → UniformSpace.Completion α) ∘ f) ∧
    Membership.mem (γ := Set (UniformSpace.Completion α))
      (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
      (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
⊢ Summable f

Tactic:
apply (summable_iff_summable_compl_and_tsum_mem f).mpr

Premises used: Iff.mpr, summable_iff_summable_compl_and_tsum_mem
-- Module: Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion
Goal:
α : Type u_1
β : Type u_2
inst : AddCommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
f : β → α
h_cauchy : CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b
h_tsum :
  Membership.mem (γ := Set (UniformSpace.Completion α))
    (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
    (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
mpr : Summable (α := UniformSpace.Completion α) ((⇑toCompl : (a : α) → UniformSpace.Completion α) ∘ f)
mpr₁ :
  Membership.mem (γ := Set (UniformSpace.Completion α))
    (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
    (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
⊢ Summable (α := UniformSpace.Completion α) ((⇑toCompl : (a : α) → UniformSpace.Completion α) ∘ f) ∧
    Membership.mem (γ := Set (UniformSpace.Completion α))
      (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
      (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion
Goal:
α : Type u_1
β : Type u_2
inst : AddCommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
f : β → α
h_cauchy : CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b
h_tsum :
  Membership.mem (γ := Set (UniformSpace.Completion α))
    (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
    (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
mpr :
  CauchySeq.{u_1, u_2} (α := UniformSpace.Completion α) fun (s : Finset β) ↦
    ∑ b ∈ s, ((⇑toCompl : (a : α) → UniformSpace.Completion α) ∘ f) b
⊢ Summable (α := UniformSpace.Completion α) ((⇑toCompl : (a : α) → UniformSpace.Completion α) ∘ f)

Tactic:
apply summable_iff_cauchySeq_finset.mpr

Premises used: Iff.mpr, summable_iff_cauchySeq_finset
-- Module: Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion
Goal:
α : Type u_1
β : Type u_2
inst : AddCommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
f : β → α
h_cauchy : CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b
h_tsum :
  Membership.mem (γ := Set (UniformSpace.Completion α))
    (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
    (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
mpr :
  CauchySeq.{u_1, u_2} (α := UniformSpace.Completion α) fun (s : Finset β) ↦
    (toCompl : (a : α) → UniformSpace.Completion α) (∑ x ∈ s, f x)
⊢ CauchySeq.{u_1, u_2} (α := UniformSpace.Completion α) fun (s : Finset β) ↦
    ∑ b ∈ s, ((⇑toCompl : (a : α) → UniformSpace.Completion α) ∘ f) b

Tactic:
simp_rw [Function.comp_apply, ← map_sum]

Premises used: map_sum, Function.comp_apply
-- Module: Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion
Goal:
α : Type u_1
β : Type u_2
inst : AddCommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
f : β → α
h_cauchy : CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b
h_tsum :
  Membership.mem (γ := Set (UniformSpace.Completion α))
    (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
    (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
⊢ CauchySeq.{u_1, u_2} (α := UniformSpace.Completion α) fun (s : Finset β) ↦
    (toCompl : (a : α) → UniformSpace.Completion α) (∑ x ∈ s, f x)

Tactic:
h_cauchy.map (uniformContinuous_coe α)

Premises used: Multiset.sum, UniformSpace.Completion.coe', Multiset.foldr, CauchySeq, Set.Mem, Filter.map, Cauchy.map, setOf, Set.Subset, Set.preimage, SeparationQuotient.mk, UniformSpace.Completion.uniformContinuous_coe, Finset.sum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion
Goal:
α : Type u_1
β : Type u_2
inst : AddCommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
f : β → α
h_cauchy : CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b
h_tsum :
  Membership.mem (γ := Set (UniformSpace.Completion α))
    (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
    (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
⊢ CauchySeq.{u_1, u_2} (α := UniformSpace.Completion α) fun (s : Finset β) ↦
    (toCompl : (a : α) → UniformSpace.Completion α) (∑ x ∈ s, f x)

Tactic:
exact h_cauchy.map (uniformContinuous_coe α)

Premises used: Cauchy.map, UniformSpace.Completion.uniformContinuous_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion
Goal:
α : Type u_1
β : Type u_2
inst : AddCommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
f : β → α
h_cauchy : CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b
h_tsum :
  Membership.mem (γ := Set (UniformSpace.Completion α))
    (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
    (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
⊢ Membership.mem (γ := Set (UniformSpace.Completion α))
    (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
    (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))

Tactic:
h_tsum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion
Goal:
α : Type u_1
β : Type u_2
inst : AddCommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
f : β → α
h_cauchy : CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b
h_tsum :
  Membership.mem (γ := Set (UniformSpace.Completion α))
    (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
    (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
⊢ Membership.mem (γ := Set (UniformSpace.Completion α))
    (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
    (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))

Tactic:
exact h_tsum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion
Goal:
α : Type u_1
β : Type u_2
inst : AddCommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
f : β → α
mp :
  Summable f →
    (CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b) ∧
      Membership.mem (γ := Set (UniformSpace.Completion α))
        (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
        (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
mpr mpr₁ :
  (CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b) ∧
      Membership.mem (γ := Set (UniformSpace.Completion α))
        (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
        (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i)) →
    Summable f
⊢ Summable f ↔
    (CauchySeq.{u_1, u_2} (α := α) fun (s : Finset β) ↦ ∑ b ∈ s, f b) ∧
      Membership.mem (γ := Set (UniformSpace.Completion α))
        (Set.range (ι := α) (⇑toCompl : (a : α) → UniformSpace.Completion α))
        (∑' (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))

Tactic:
classical
  constructor
  · rintro ⟨a, ha⟩
    exact ⟨ha.cauchySeq, ((summable_iff_summable_compl_and_tsum_mem f).mp ⟨a, ha⟩).2⟩
  · rintro ⟨h_cauchy, h_tsum⟩
    apply (summable_iff_summable_compl_and_tsum_mem f).mpr
    constructor
    · apply summable_iff_cauchySeq_finset.mpr
      simp_rw [Function.comp_apply, ← map_sum]
      exact h_cauchy.map (uniformContinuous_coe α)
    · exact h_tsum

Premises used: Iff.mpr, map_sum, summable_iff_cauchySeq_finset, Function.comp_apply, summable_iff_summable_compl_and_tsum_mem
-- Module: Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion
Goal:
α : Type u_1
β : Type u_2
inst : AddCommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
L : SummationFilter β
inst_3 : L.NeBot
f : β → α
hf : Summable f L
⊢ Eq.{u_1 + 1} (α := UniformSpace.Completion α) (∑'[L] (i : β), (toCompl : (a : α) → UniformSpace.Completion α) (f i))
    (↑(∑'[L] (i : β), f i) : UniformSpace.Completion α)

Tactic:
(hf.map_tsum toCompl (continuous_coe α)).symm

Premises used: UniformSpace.Completion.coe', Summable.map_tsum, UniformSpace.Completion.continuous_coe, SeparationQuotient.mk, UniformSpace.Completion.toCompl, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : AddCommMonoid α
inst_2 : DistribSMul γ α
inst_3 : ContinuousConstSMul γ α
f : β → α
L : SummationFilter β
a : α
b : γ
hf : HasSum f a L
⊢ HasSum (fun (i : β) ↦ b • f i) (b • a) L

Tactic:
hf.map (DistribSMul.toAddMonoidHom α _) <| continuous_const_smul _

Premises used: HasSum.map, ContinuousConstSMul.continuous_const_smul, DistribSMul.toAddMonoidHom
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : AddCommMonoid α
inst_2 : DistribSMul γ α
inst_3 : ContinuousConstSMul γ α
f : β → α
L : SummationFilter β
b : γ
hf : Summable f L
⊢ Summable.{u_1, u_2} (α := α) (fun (i : β) ↦ b • f i) L

Tactic:
(hf.hasSum.const_smul _).summable

Premises used: HasSum.summable, Summable.hasSum, HasSum.const_smul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : AddCommMonoid α
inst_2 : DistribSMul γ α
inst_3 : ContinuousConstSMul γ α
f : β → α
L : SummationFilter β
inst_4 : T2Space α
inst_5 : L.NeBot
b : γ
hf : Summable f L
⊢ ∑'[L] (i : β), b • f i = HSMul.hSMul (β := α) b (∑'[L] (i : β), f i)

Tactic:
(hf.hasSum.const_smul _).tsum_eq

Premises used: HasSum.tsum_eq, Summable.hasSum, HasSum.const_smul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : AddCommMonoid α
f : β → α
L : SummationFilter β
γ : Type u_5
inst_2 : Group γ
inst_3 : DistribMulAction γ α
inst_4 : ContinuousConstSMul γ α
inst_5 : T2Space α
g : γ
a : α
⊢ (DistribSMul.toAddMonoidHom α g⁻¹ : (a : α) → α) (ZeroHom.toFun (↑(DistribSMul.toAddMonoidHom α g) : ZeroHom α α) a) =
    a

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : AddCommMonoid α
f : β → α
L : SummationFilter β
γ : Type u_5
inst_2 : Group γ
inst_3 : DistribMulAction γ α
inst_4 : ContinuousConstSMul γ α
inst_5 : T2Space α
g : γ
a : α
⊢ ZeroHom.toFun (↑(DistribSMul.toAddMonoidHom α g) : ZeroHom α α) ((DistribSMul.toAddMonoidHom α g⁻¹ : (a : α) → α) a) =
    a

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : AddCommMonoid α
f : β → α
L : SummationFilter β
γ : Type u_5
inst_2 : DivisionSemiring γ
inst_3 : Module γ α
inst_4 : ContinuousConstSMul γ α
inst_5 : T2Space α
g : γ
inl :
  ∑'[L] (i : β), HSMul.hSMul.{u_5, u_1, u_1} (α := γ) 0 (f i) =
    HSMul.hSMul.{u_5, u_1, u_1} (α := γ) (β := α) 0 (∑'[L] (i : β), f i)
inr : ∀ (hg : g ≠ 0), ∑'[L] (i : β), g • f i = HSMul.hSMul (β := α) g (∑'[L] (i : β), f i)
⊢ ∑'[L] (i : β), g • f i = HSMul.hSMul (β := α) g (∑'[L] (i : β), f i)

Tactic:
rcases eq_or_ne g 0 with rfl | hg

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : AddCommMonoid α
f : β → α
L : SummationFilter β
γ : Type u_5
inst_2 : DivisionSemiring γ
inst_3 : Module γ α
inst_4 : ContinuousConstSMul γ α
inst_5 : T2Space α
⊢ ∑'[L] (i : β), HSMul.hSMul.{u_5, u_1, u_1} (α := γ) 0 (f i) =
    HSMul.hSMul.{u_5, u_1, u_1} (α := γ) (β := α) 0 (∑'[L] (i : β), f i)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : AddCommMonoid α
f : β → α
L : SummationFilter β
γ : Type u_5
inst_2 : DivisionSemiring γ
inst_3 : Module γ α
inst_4 : ContinuousConstSMul γ α
inst_5 : T2Space α
g : γ
hg : g ≠ 0
⊢ ∑'[L] (i : β), g • f i = HSMul.hSMul (β := α) g (∑'[L] (i : β), f i)

Tactic:
tsum_const_smul' (Units.mk0 g hg)

Premises used: tsum_const_smul', Units.mk0
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : AddCommMonoid α
f : β → α
L : SummationFilter β
γ : Type u_5
inst_2 : DivisionSemiring γ
inst_3 : Module γ α
inst_4 : ContinuousConstSMul γ α
inst_5 : T2Space α
g : γ
hg : g ≠ 0
⊢ ∑'[L] (i : β), g • f i = HSMul.hSMul (β := α) g (∑'[L] (i : β), f i)

Tactic:
exact tsum_const_smul' (Units.mk0 g hg)

Premises used: tsum_const_smul', Units.mk0
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
M : Type u_9
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : ContinuousSMul R M
f : ι → R
L : SummationFilter ι
r : R
hf : HasSum f r L
a : M
⊢ HasSum (fun (z : ι) ↦ f z • a) (r • a) L

Tactic:
hf.map ((smulAddHom R M).flip a) (continuous_id.smul continuous_const)

Premises used: HasSum.map, continuous_const, Continuous.smul, AddMonoidHom.flip, continuous_id, smulAddHom, DFunLike.coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
M : Type u_9
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : ContinuousSMul R M
f : ι → R
L : SummationFilter ι
hf : Summable f L
a : M
⊢ Summable.{u_9, u_5} (α := M) (fun (z : ι) ↦ f z • a) L

Tactic:
(hf.hasSum.smul_const _).summable

Premises used: HasSum.summable, Summable.hasSum, HasSum.smul_const
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
M : Type u_9
inst : Semiring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : ContinuousSMul R M
f : ι → R
L : SummationFilter ι
inst_6 : T2Space M
inst_7 : L.NeBot
hf : Summable f L
a : M
⊢ ∑'[L] (z : ι), f z • a = HSMul.hSMul.{u_7, u_9, u_9} (α := R) (∑'[L] (z : ι), f z) a

Tactic:
(hf.hasSum.smul_const _).tsum_eq

Premises used: HasSum.tsum_eq, Summable.hasSum, HasSum.smul_const
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
κ : Type u_6
R : Type u_7
M : Type u_9
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace M
inst_5 : T3Space M
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
f : ι → R
g : κ → M
s : R
t u : M
hf : HasSum f s
hg : HasSum g t
hfg : HasSum (fun (x : ι × κ) ↦ f x.1 • g x.2) u
⊢ s • t = u

Tactic:
have key₁ : HasSum (fun i ↦ f i • t) (s • t) := hf.smul_const t
  have this : ∀ i : ι, HasSum (fun c : κ ↦ f i • g c) (f i • t) := fun i ↦ hg.const_smul (f i)
  have key₂ : HasSum (fun i ↦ f i • t) u := HasSum.prod_fiberwise hfg this
  key₁.unique key₂

Premises used: HasSum.prod_fiberwise, HasSum.unique, HasSum.smul_const, HasSum.const_smul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
κ : Type u_6
R : Type u_7
M : Type u_9
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace M
inst_5 : T3Space M
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
f : ι → R
g : κ → M
s : R
t : M
hf : HasSum f s
hg : HasSum g t
hfg : Summable (α := M) fun (x : ι × κ) ↦ f x.1 • g x.2
⊢ HasSum (fun (x : ι × κ) ↦ f x.1 • g x.2) (s • t)

Tactic:
let ⟨_u, hu⟩ := hfg
  (hf.smul_eq hg hu).symm ▸ hu

Premises used: HasSum.smul_eq, Eq.rec, Prod.fst, HasSum, HSMul.hSMul, Prod, _private.0.HasSum.smul.match_1, Eq.symm, Prod.snd, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
κ : Type u_6
R : Type u_7
M : Type u_9
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : TopologicalSpace R
inst_4 : TopologicalSpace M
inst_5 : T3Space M
inst_6 : ContinuousAdd M
inst_7 : ContinuousSMul R M
f : ι → R
g : κ → M
hf : Summable f
hg : Summable g
hfg : Summable (α := M) fun (x : ι × κ) ↦ f x.1 • g x.2
⊢ HSMul.hSMul.{u_7, u_9, u_9} (α := R) (β := M) (∑' (x : ι), f x) (∑' (y : κ), g y) = ∑' (z : ι × κ), f z.1 • g z.2

Tactic:
hf.hasSum.smul_eq hg.hasSum hfg.hasSum

Premises used: HasSum.smul_eq, Summable.hasSum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
L : SummationFilter ι
f : ι → M
φ : M →SL[σ] M₂
x : M
hf : HasSum f x L
⊢ HasSum.{u_10, u_5} (α := M₂) (fun (b : ι) ↦ ((φ : (a : M) → M₂) (f b) : M₂)) ((φ : (a : M) → M₂) x : M₂) L

Tactic:
simpa only using hf.map φ.toLinearMap.toAddMonoidHom φ.continuous

Premises used: LinearMap.toAddMonoidHom, HasSum.map, ContinuousLinearMap.toLinearMap, ContinuousLinearMap.continuous
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
L : SummationFilter ι
f : ι → M
φ : M →SL[σ] M₂
hf : Summable f L
⊢ Summable.{u_10, u_5} (α := M₂) (fun (b : ι) ↦ (φ : (a : M) → M₂) (f b)) L

Tactic:
(hf.hasSum.mapL φ).summable

Premises used: HasSum.mapL, HasSum.summable, Summable.hasSum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
L : SummationFilter ι
inst_8 : T2Space M₂
inst_9 : L.NeBot
f : ι → M
φ : M →SL[σ] M₂
hf : Summable f L
⊢ Eq.{u_10 + 1} (α := M₂) ((φ : (a : M) → M₂) (∑'[L] (z : ι), f z) : M₂) (∑'[L] (z : ι), (φ : (a : M) → M₂) (f z) : M₂)

Tactic:
(hf.hasSum.mapL φ).tsum_eq.symm

Premises used: HasSum.mapL, HasSum.tsum_eq, Summable.hasSum, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
h : HasSum (fun (b : ι) ↦ (e : (a : M) → M₂) (f b)) y L
⊢ HasSum f ((e.symm : (a : M₂) → M) y) L

Tactic:
simpa only [e.symm.coe_coe, e.symm_apply_apply] using h.mapL (e.symm : M₂ →SL[σ'] M)

Premises used: ContinuousLinearEquiv.symm, HasSum.mapL, ContinuousLinearEquiv.symm_apply_apply, ContinuousLinearEquiv.coe_coe, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
h : HasSum f ((e.symm : (a : M₂) → M) y) L
⊢ HasSum (fun (b : ι) ↦ (e : (a : M) → M₂) (f b)) y L

Tactic:
simpa only [e.coe_coe, e.apply_symm_apply] using (e : M →SL[σ] M₂).hasSum h

Premises used: ContinuousLinearEquiv.apply_symm_apply, ContinuousLinearMap.hasSum, ContinuousLinearEquiv.coe_coe, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
f : ι → M
e : M ≃SL[σ] M₂
x : M
rw : HasSum f ((e.symm : (a : M₂) → M) ((e : (a : M) → M₂) x : M₂)) L ↔ HasSum f x L
rw₁ rw₂ : HasSum f x L ↔ HasSum f x L
⊢ HasSum.{u_10, u_5} (α := M₂) (fun (b : ι) ↦ ((e : (a : M) → M₂) (f b) : M₂)) ((e : (a : M) → M₂) x : M₂) L ↔
    HasSum f x L

Tactic:
rw [e.hasSum, ContinuousLinearEquiv.symm_apply_apply]

Premises used: ContinuousLinearEquiv.hasSum, ContinuousLinearEquiv.symm_apply_apply