-- Mathlib/Topology/Algebra/InfiniteSum/Module.lean
/-- Infinite sums commute with scalar multiplication. Version for scalars living in a `Group`, but
  not requiring any summability hypothesis. -/
lemma tsum_const_smul' {γ : Type*} [Group γ] [DistribMulAction γ α] [ContinuousConstSMul γ α]
    [T2Space α] (g : γ) : ∑' (i : β), g • f i = g • ∑' (i : β), f i

Proof state:
case neg.h.hg'
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
γ : Type u_5
inst✝³ : Group γ
inst✝² : DistribMulAction γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
hf : ¬Summable f
mul_g : α ≃+ α := DistribMulAction.toAddEquiv α g
⊢ Continuous (EquivLike.inv mul_g)

Tactic:
apply continuous_const_smul

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
γ : Type u_5
inst✝³ : Group γ
inst✝² : DistribMulAction γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
hf : ¬Summable f
mul_g : α ≃+ α := DistribMulAction.toAddEquiv α g
⊢ ∑' (i : β), g • f i = 0

Tactic:
apply tsum_eq_zero_of_not_summable

Result:
case neg.h
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
γ : Type u_5
inst✝³ : Group γ
inst✝² : DistribMulAction γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
hf : ¬Summable f
mul_g : α ≃+ α := DistribMulAction.toAddEquiv α g
⊢ ¬Summable fun b => g • f b

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
γ : Type u_5
inst✝³ : Group γ
inst✝² : DistribMulAction γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
hf : ¬Summable f
⊢ ∑' (i : β), g • f i = 0

Tactic:
let mul_g : α ≃+ α := DistribMulAction.toAddEquiv α g

Result:
case neg
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
γ : Type u_5
inst✝³ : Group γ
inst✝² : DistribMulAction γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
hf : ¬Summable f
mul_g : α ≃+ α := DistribMulAction.toAddEquiv α g
⊢ ∑' (i : β), g • f i = 0

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
γ : Type u_5
inst✝³ : Group γ
inst✝² : DistribMulAction γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
⊢ ∑' (i : β), g • f i = g • ∑' (i : β), f i

Tactic:
by_cases hf : Summable f

Result:
case pos
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
γ : Type u_5
inst✝³ : Group γ
inst✝² : DistribMulAction γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
hf : Summable f
⊢ ∑' (i : β), g • f i = g • ∑' (i : β), f i

case neg
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
γ : Type u_5
inst✝³ : Group γ
inst✝² : DistribMulAction γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
hf : ¬Summable f
⊢ ∑' (i : β), g • f i = g • ∑' (i : β), f i

Proof state:
case neg.h.hg
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
γ : Type u_5
inst✝³ : Group γ
inst✝² : DistribMulAction γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
hf : ¬Summable f
mul_g : α ≃+ α := DistribMulAction.toAddEquiv α g
⊢ Continuous ⇑mul_g

Tactic:
apply continuous_const_smul

Result:
no goals

Proof state:
case neg.h
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
γ : Type u_5
inst✝³ : Group γ
inst✝² : DistribMulAction γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
hf : ¬Summable f
mul_g : α ≃+ α := DistribMulAction.toAddEquiv α g
⊢ ¬Summable (⇑mul_g ∘ f)

Tactic:
rwa [Summable.map_iff_of_equiv mul_g]

Result:
case neg.h.hg
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
γ : Type u_5
inst✝³ : Group γ
inst✝² : DistribMulAction γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
hf : ¬Summable f
mul_g : α ≃+ α := DistribMulAction.toAddEquiv α g
⊢ Continuous ⇑mul_g

case neg.h.hg'
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
γ : Type u_5
inst✝³ : Group γ
inst✝² : DistribMulAction γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
hf : ¬Summable f
mul_g : α ≃+ α := DistribMulAction.toAddEquiv α g
⊢ Continuous (EquivLike.inv mul_g)

Proof state:
case neg.h
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
γ : Type u_5
inst✝³ : Group γ
inst✝² : DistribMulAction γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
hf : ¬Summable f
mul_g : α ≃+ α := DistribMulAction.toAddEquiv α g
⊢ ¬Summable fun b => g • f b

Tactic:
change ¬ Summable (mul_g ∘ f)

Result:
case neg.h
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
γ : Type u_5
inst✝³ : Group γ
inst✝² : DistribMulAction γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
hf : ¬Summable f
mul_g : α ≃+ α := DistribMulAction.toAddEquiv α g
⊢ ¬Summable (⇑mul_g ∘ f)

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
γ : Type u_5
inst✝³ : Group γ
inst✝² : DistribMulAction γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
hf : ¬Summable f
⊢ ∑' (i : β), g • f i = g • 0

Tactic:
simp only [smul_zero]

Result:
case neg
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
γ : Type u_5
inst✝³ : Group γ
inst✝² : DistribMulAction γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
hf : ¬Summable f
⊢ ∑' (i : β), g • f i = 0

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
γ : Type u_5
inst✝³ : Group γ
inst✝² : DistribMulAction γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
hf : Summable f
⊢ ∑' (i : β), g • f i = g • ∑' (i : β), f i

Tactic:
exact tsum_const_smul g hf

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
γ : Type u_5
inst✝³ : Group γ
inst✝² : DistribMulAction γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
hf : ¬Summable f
⊢ ∑' (i : β), g • f i = g • ∑' (i : β), f i

Tactic:
rw [tsum_eq_zero_of_not_summable hf]

Result:
case neg
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
γ : Type u_5
inst✝³ : Group γ
inst✝² : DistribMulAction γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
hf : ¬Summable f
⊢ ∑' (i : β), g • f i = g • 0