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

State before:
ι : Type u_2
κ : Type ?u.4976
α : Type u_1
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), 1 ≤ g i
⊢ 1 ≤ ∏' (i : ι), g i
Tactic:
by_cases hg : Multipliable g
State after:
case pos
ι : Type u_2
κ : Type ?u.4976
α : Type u_1
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), 1 ≤ g i
hg : Multipliable g
⊢ 1 ≤ ∏' (i : ι), g i

case neg
ι : Type u_2
κ : Type ?u.4976
α : Type u_1
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), 1 ≤ g i
hg : ¬Multipliable g
⊢ 1 ≤ ∏' (i : ι), g i

State before:
case pos
ι : Type u_2
κ : Type ?u.4976
α : Type u_1
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), 1 ≤ g i
hg : Multipliable g
⊢ 1 ≤ ∏' (i : ι), g i
Tactic:
exact hg.hasProd.one_le h
State after:
no goals

State before:
case neg
ι : Type u_2
κ : Type ?u.4976
α : Type u_1
inst✝² : OrderedCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), 1 ≤ g i
hg : ¬Multipliable g
⊢ 1 ≤ ∏' (i : ι), g i
Tactic:
simp [tprod_eq_one_of_not_multipliable hg]
State after:
no goals