Theorem: MvPowerSeries.StronglySummable.tprod_eq_of_one_add (DividedPowers/ForMathlib/MvPowerSeries/StronglySummable/Topology.lean)

State before:
σ : Type u_1
α : Type u_2
inst✝⁴ : DecidableEq σ
ι✝ : Type u_3
f✝ : ι✝ → MvPowerSeries σ α
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : T2Space α
ι : Type u_4
f : ι → MvPowerSeries σ α
hf : StronglySummable f
⊢ ∏' (i : ι), (1 + f i) = tsum (partialProduct f)
Tactic:
haveI : T2Space (MvPowerSeries σ α) := t2Space σ α
State after:
σ : Type u_1
α : Type u_2
inst✝⁴ : DecidableEq σ
ι✝ : Type u_3
f✝ : ι✝ → MvPowerSeries σ α
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : T2Space α
ι : Type u_4
f : ι → MvPowerSeries σ α
hf : StronglySummable f
this : T2Space (MvPowerSeries σ α)
⊢ ∏' (i : ι), (1 + f i) = tsum (partialProduct f)

State before:
σ : Type u_1
α : Type u_2
inst✝⁴ : DecidableEq σ
ι✝ : Type u_3
f✝ : ι✝ → MvPowerSeries σ α
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : T2Space α
ι : Type u_4
f : ι → MvPowerSeries σ α
hf : StronglySummable f
this : T2Space (MvPowerSeries σ α)
⊢ ∏' (i : ι), (1 + f i) = tsum (partialProduct f)
Tactic:
rw [hf.hasProd_of_one_add.tprod_eq, StronglyMultipliable.prod_eq, sum_eq_tsum]
State after:
no goals