Theorem: tprod_pos (DividedPowers/ForMathlib/InfiniteSum/Order.lean)

State before:
ι : Type u_1
κ : Type ?u.10181
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : OrderedCommGroup α
inst✝¹ : TopologicalGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i✝ : ι
hprod : Multipliable g
hg : ∀ (i : ι), 1 ≤ g i
i : ι
hi : 1 < g i
⊢ 1 < ∏' (i : ι), g i
Tactic:
rw [← tprod_one]
State after:
ι : Type u_1
κ : Type ?u.10181
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : OrderedCommGroup α
inst✝¹ : TopologicalGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i✝ : ι
hprod : Multipliable g
hg : ∀ (i : ι), 1 ≤ g i
i : ι
hi : 1 < g i
⊢ ∏' (x : ?m.11469), 1 < ∏' (i : ι), g i

ι : Type u_1
κ : Type ?u.10181
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : OrderedCommGroup α
inst✝¹ : TopologicalGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i✝ : ι
hprod : Multipliable g
hg : ∀ (i : ι), 1 ≤ g i
i : ι
hi : 1 < g i
⊢ Type ?u.11467

State before:
ι : Type u_1
κ : Type ?u.10181
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : OrderedCommGroup α
inst✝¹ : TopologicalGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i✝ : ι
hprod : Multipliable g
hg : ∀ (i : ι), 1 ≤ g i
i : ι
hi : 1 < g i
⊢ ∏' (x : ?m.11469), 1 < ∏' (i : ι), g i

ι : Type u_1
κ : Type ?u.10181
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : OrderedCommGroup α
inst✝¹ : TopologicalGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i✝ : ι
hprod : Multipliable g
hg : ∀ (i : ι), 1 ≤ g i
i : ι
hi : 1 < g i
⊢ Type ?u.11467
Tactic:
exact tprod_lt_tprod hg hi multipliable_one hprod
State after:
no goals