awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a : α
inst_5 : L.NeBot
inst_6 : L.LeAtTop
inst_7 : MulRightStrictMono α
hf : HasProd f a L
i : ι
hi : ∀ (j : ι), j ≠ i → 1 ≤ f j
j : ι
hij : j ≠ i
hj : 1 < f j
f₁ : f j * f i = ∏ k ∈ {j, i}, f k
⊢ f i < a

Tactic:
classical
  calc
    f i < f j * f i := lt_mul_of_one_lt_left' (f i) hj
    _ = ∏ k ∈ {j, i}, f k := by rw [Finset.prod_pair hij]
    _ ≤ a := prod_le_hasProd _ (fun k hk ↦ hi k (hk ∘ mem_insert_of_mem ∘ mem_singleton.mpr)) hf

Premises used: lt_mul_of_one_lt_left'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
inst_5 : L.NeBot
inst_6 : L.LeAtTop
f : ι → α
s : Finset ι
hs : ∀ i ∉ s, 1 ≤ f i
hf : Multipliable f L
⊢ LE.le.{u_3} (α := α) (∏ i ∈ s, f i) (∏'[L] (i : ι), f i)

Tactic:
prod_le_hasProd s hs hf.hasProd

Premises used: prod_le_hasProd, Multipliable.hasProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
inst_5 : L.NeBot
inst_6 : L.LeAtTop
hf : Multipliable f L
i : ι
hb : ∀ (j : ι), j ≠ i → 1 ≤ f j
⊢ f i ≤ ∏'[L] (i : ι), f i

Tactic:
le_hasProd hf.hasProd i hb

Premises used: le_hasProd, Multipliable.hasProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f g : ι → α
inst_5 : L.NeBot
h : ∀ (i : ι), f i ≤ g i
hf : Multipliable f L
hg : Multipliable g L
⊢ LE.le.{u_3} (α := α) (∏'[L] (i : ι), f i) (∏'[L] (i : ι), g i)

Tactic:
hasProd_le h hf.hasProd hg.hasProd

Premises used: Multipliable.hasProd, hasProd_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f g : ι → α
inst_5 : L.NeBot
hf : Multipliable f L
hg : Multipliable g L
h : f ≤ g
⊢ LE.le.{u_3} (α := α) (∏'[L] (n : ι), f n) (∏'[L] (n : ι), g n)

Tactic:
hf.tprod_le_tprod h hg

Premises used: Multipliable.tprod_le_tprod
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
f : ι → α
a₂ : α
inst_4 : L.NeBot
hf : Multipliable f L
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
⊢ ∏'[L] (i : ι), f i ≤ a₂

Tactic:
hasProd_le_of_prod_le hf.hasProd h

Premises used: Multipliable.hasProd, hasProd_le_of_prod_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
pos : ∀ (hL : L.NeBot), ∏'[L] (i : ι), f i ≤ a₂
neg : ∀ (hL : ¬L.NeBot), ∏'[L] (i : ι), f i ≤ a₂
⊢ ∏'[L] (i : ι), f i ≤ a₂

Tactic:
by_cases hL : L.NeBot

Premises used: SummationFilter.NeBot
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : L.NeBot
pos : ∀ (hf : Multipliable f L), ∏'[L] (i : ι), f i ≤ a₂
neg : ∀ (hf : ¬Multipliable f L), ∏'[L] (i : ι), f i ≤ a₂
⊢ ∏'[L] (i : ι), f i ≤ a₂

Tactic:
by_cases hf : Multipliable f L

Premises used: Multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : L.NeBot
hf : Multipliable f L
⊢ ∏'[L] (i : ι), f i ≤ a₂

Tactic:
hf.tprod_le_of_prod_le h

Premises used: Multipliable.tprod_le_of_prod_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : L.NeBot
hf : Multipliable f L
⊢ ∏'[L] (i : ι), f i ≤ a₂

Tactic:
exact hf.tprod_le_of_prod_le h

Premises used: Multipliable.tprod_le_of_prod_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : L.NeBot
hf : ¬Multipliable f L
neg neg₁ neg₂ neg₃ : 1 ≤ a₂
⊢ ∏'[L] (i : ι), f i ≤ a₂

Tactic:
rwa [tprod_eq_one_of_not_multipliable hf]

Premises used: tprod_eq_one_of_not_multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : ¬L.NeBot
pos : ∀ (hf : (mulSupport f).Finite), ∏'[L] (i : ι), f i ≤ a₂
neg : ∀ (hf : ¬(mulSupport f).Finite), ∏'[L] (i : ι), f i ≤ a₂
⊢ ∏'[L] (i : ι), f i ≤ a₂

Tactic:
by_cases hf : f.mulSupport.Finite

Premises used: Set.Finite, Function.mulSupport
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : ¬L.NeBot
hf : (mulSupport f).Finite
⊢ ∏'[L] (i : ι), f i ≤ a₂

Tactic:
simpa [tprod_bot hL, finprod_eq_prod _ hf] using h _

Premises used: tprod_bot, finprod_eq_prod
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : TopologicalSpace α
inst_3 : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : ¬L.NeBot
hf : ¬(mulSupport f).Finite
neg : ∏ᶠ (b : ι), f b ≤ a₂
neg₁ neg₂ neg₃ neg₄ : 1 ≤ a₂
⊢ ∏'[L] (i : ι), f i ≤ a₂

Tactic:
rwa [tprod_bot hL, finprod_of_infinite_mulSupport hf]

Premises used: finprod_of_infinite_mulSupport, tprod_bot
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
g : ι → α
a : α
inst_5 : L.NeBot
h : ∀ (i : ι), 1 ≤ g i
ha : HasProd g a L
⊢ 1 ≤ a

Tactic:
hasProd_le h hasProd_one ha

Premises used: hasProd_one, hasProd_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
g : ι → α
a : α
inst_5 : L.NeBot
h : ∀ (i : ι), g i ≤ 1
ha : HasProd g a L
⊢ a ≤ 1

Tactic:
hasProd_le h ha hasProd_one

Premises used: hasProd_one, hasProd_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
pos : ∀ (hg : Multipliable g L), LE.le.{u_3} (α := α) 1 (∏'[L] (i : ι), g i)
neg : ∀ (hg : ¬Multipliable g L), LE.le.{u_3} (α := α) 1 (∏'[L] (i : ι), g i)
⊢ LE.le.{u_3} (α := α) 1 (∏'[L] (i : ι), g i)

Tactic:
by_cases hg : Multipliable g L

Premises used: Multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
hg : Multipliable g L
pos : ∀ (hL : L.NeBot), LE.le.{u_3} (α := α) 1 (∏'[L] (i : ι), g i)
neg : ∀ (hL : ¬L.NeBot), LE.le.{u_3} (α := α) 1 (∏'[L] (i : ι), g i)
⊢ LE.le.{u_3} (α := α) 1 (∏'[L] (i : ι), g i)

Tactic:
by_cases hL : L.NeBot

Premises used: SummationFilter.NeBot
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
hg : Multipliable g L
hL : L.NeBot
⊢ LE.le.{u_3} (α := α) 1 (∏'[L] (i : ι), g i)

Tactic:
hg.hasProd.one_le h

Premises used: Multipliable.hasProd, HasProd.one_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
hg : Multipliable g L
hL : L.NeBot
⊢ LE.le.{u_3} (α := α) 1 (∏'[L] (i : ι), g i)

Tactic:
exact hg.hasProd.one_le h

Premises used: Multipliable.hasProd, HasProd.one_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
hg : Multipliable g L
hL : ¬L.NeBot
⊢ LE.le.{u_3} (α := α) 1 (∏'[L] (i : ι), g i)

Tactic:
simpa [tprod_bot hL] using one_le_finprod' h

Premises used: tprod_bot, one_le_finprod'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
hg : ¬Multipliable g L
neg neg₁ : LE.le.{u_3} (α := α) 1 1
⊢ LE.le.{u_3} (α := α) 1 (∏'[L] (i : ι), g i)

Tactic:
rw [tprod_eq_one_of_not_multipliable hg]

Premises used: tprod_eq_one_of_not_multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
pos : ∀ (hf : Multipliable f L), LE.le.{u_3} (α := α) (∏'[L] (i : ι), f i) 1
neg : ∀ (hf : ¬Multipliable f L), LE.le.{u_3} (α := α) (∏'[L] (i : ι), f i) 1
⊢ LE.le.{u_3} (α := α) (∏'[L] (i : ι), f i) 1

Tactic:
by_cases hf : Multipliable f L

Premises used: Multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
hf : Multipliable f L
pos : ∀ (hL : L.NeBot), LE.le.{u_3} (α := α) (∏'[L] (i : ι), f i) 1
neg : ∀ (hL : ¬L.NeBot), LE.le.{u_3} (α := α) (∏'[L] (i : ι), f i) 1
⊢ LE.le.{u_3} (α := α) (∏'[L] (i : ι), f i) 1

Tactic:
by_cases hL : L.NeBot

Premises used: SummationFilter.NeBot
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
hf : Multipliable f L
hL : L.NeBot
⊢ LE.le.{u_3} (α := α) (∏'[L] (i : ι), f i) 1

Tactic:
hf.hasProd.le_one h

Premises used: Multipliable.hasProd, HasProd.le_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
hf : Multipliable f L
hL : L.NeBot
⊢ LE.le.{u_3} (α := α) (∏'[L] (i : ι), f i) 1

Tactic:
exact hf.hasProd.le_one h

Premises used: Multipliable.hasProd, HasProd.le_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
hf : Multipliable f L
hL : ¬L.NeBot
neg : LE.le.{u_3} (α := α) (∏ᶠ (i : ι), f i) 1
⊢ LE.le.{u_3} (α := α) (∏'[L] (i : ι), f i) 1

Tactic:
simp only [tprod_bot hL]

Premises used: tprod_bot
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
hf : Multipliable f L
hL : ¬L.NeBot
⊢ LE.le.{u_3} (α := α) (∏ᶠ (i : ι), f i) 1

Tactic:
finprod_induction (· ≤ 1) le_rfl (fun _ _ ↦ mul_le_one') h

Premises used: le_rfl, finprod_induction, LE.le, OfNat.ofNat, mul_le_one'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
hf : Multipliable f L
hL : ¬L.NeBot
⊢ LE.le.{u_3} (α := α) (∏ᶠ (i : ι), f i) 1

Tactic:
exact finprod_induction (· ≤ 1) le_rfl (fun _ _ ↦ mul_le_one') h

Premises used: le_rfl, finprod_induction, LE.le, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
hf : ¬Multipliable f L
neg neg₁ : LE.le.{u_3} (α := α) 1 1
⊢ LE.le.{u_3} (α := α) (∏'[L] (i : ι), f i) 1

Tactic:
rw [tprod_eq_one_of_not_multipliable hf]

Premises used: tprod_eq_one_of_not_multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_4
α : Type u_5
L : SummationFilter ι
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
inst_5 : L.LeAtTop
inst_6 : L.NeBot
hf : ∀ (i : ι), 1 ≤ f i
⊢ HasProd f 1 L ↔ f = 1

Tactic:
⟨fun hf' ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_4
α : Type u_5
L : SummationFilter ι
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
inst_5 : L.LeAtTop
inst_6 : L.NeBot
hf : ∀ (i : ι), 1 ≤ f i
refine_1 : ∀ (hf' : HasProd f 1 L), f = 1
refine_2 : f = 1 → HasProd f 1 L
⊢ HasProd f 1 L ↔ f = 1

Tactic:
refine ⟨fun hf' ↦ ?_, ?_⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_4
α : Type u_5
L : SummationFilter ι
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
inst_5 : L.LeAtTop
inst_6 : L.NeBot
hf : ∀ (i : ι), 1 ≤ f i
hf' : HasProd f 1 L
refine_1 : ∀ (i : ι), f i = 1 i
⊢ f = 1

Tactic:
ext i
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_4
α : Type u_5
L : SummationFilter ι
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
inst_5 : L.LeAtTop
inst_6 : L.NeBot
hf : ∀ (i : ι), 1 ≤ f i
hf' : HasProd f 1 L
i : ι
⊢ f i = 1 i

Tactic:
(hf i).antisymm' (le_hasProd hf' _ fun j _ ↦ hf j)

Premises used: LE.le.antisymm', le_hasProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_4
α : Type u_5
L : SummationFilter ι
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
inst_5 : L.LeAtTop
inst_6 : L.NeBot
hf : ∀ (i : ι), 1 ≤ f i
hf' : HasProd f 1 L
i : ι
⊢ f i = 1 i

Tactic:
exact (hf i).antisymm' (le_hasProd hf' _ fun j _ ↦ hf j)

Premises used: LE.le.antisymm', le_hasProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_4
α : Type u_5
L : SummationFilter ι
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
inst_5 : L.LeAtTop
inst_6 : L.NeBot
hf : ∀ (i : ι), LE.le.{u_5} (α := α) 1 (1 i)
⊢ HasProd.{u_5, u_4} (α := α) 1 1 L

Tactic:
hasProd_one

Premises used: hasProd_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_4
α : Type u_5
L : SummationFilter ι
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
inst_5 : L.LeAtTop
inst_6 : L.NeBot
hf : ∀ (i : ι), LE.le.{u_5} (α := α) 1 (1 i)
⊢ HasProd.{u_5, u_4} (α := α) 1 1 L

Tactic:
exact hasProd_one

Premises used: hasProd_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : IsTopologicalGroup α
inst_5 : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
inst_6 : L.NeBot
inst_7 : L.LeAtTop
h : f ≤ g
hi : f i < g i
hf : HasProd f a₁ L
hg : HasProd g a₂ L
⊢ update (β := fun (a : ι) ↦ α) f i 1 ≤ update (β := fun (a : ι) ↦ α) g i 1

Tactic:
have : update f i 1 ≤ update g i 1 := update_le_update_iff.mpr ⟨rfl.le, fun i _ ↦ h i⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : IsTopologicalGroup α
inst_5 : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
inst_6 : L.NeBot
inst_7 : L.LeAtTop
h : f ≤ g
hi : f i < g i
hf : HasProd f a₁ L
hg : HasProd g a₂ L
this : update (β := fun (a : ι) ↦ α) f i 1 ≤ update (β := fun (a : ι) ↦ α) g i 1
⊢ 1 / f i * a₁ ≤ 1 / g i * a₂

Tactic:
have : 1 / f i * a₁ ≤ 1 / g i * a₂ := hasProd_le this (hf.update i 1) (hg.update i 1)
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : IsTopologicalGroup α
inst_5 : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
inst_6 : L.NeBot
inst_7 : L.LeAtTop
h : f ≤ g
hi : f i < g i
hf : HasProd f a₁ L
hg : HasProd g a₂ L
this_1 : update (β := fun (a : ι) ↦ α) f i 1 ≤ update (β := fun (a : ι) ↦ α) g i 1
this : 1 / f i * a₁ ≤ 1 / g i * a₂
⊢ a₁ < a₂

Tactic:
simpa only [one_div, mul_inv_cancel_left] using mul_lt_mul_of_lt_of_le hi this

Premises used: one_div, mul_inv_cancel_left, mul_lt_mul_of_lt_of_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : IsTopologicalGroup α
inst_5 : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
inst_6 : L.NeBot
inst_7 : L.LeAtTop
h : f ≤ g
hi : f i < g i
hf : HasProd f a₁ L
hg : HasProd g a₂ L
have have₁ have₂ : ∀ (this : update (β := fun (a : ι) ↦ α) f i 1 ≤ update (β := fun (a : ι) ↦ α) g i 1), a₁ < a₂
have₃ :
  ∀ (this : update (β := fun (a : ι) ↦ α) f i 1 ≤ update (β := fun (a : ι) ↦ α) g i 1)
    (this : 1 / f i * a₁ ≤ 1 / g i * a₂), a₁ < a₂
⊢ a₁ < a₂

Tactic:
classical
  have : update f i 1 ≤ update g i 1 := update_le_update_iff.mpr ⟨rfl.le, fun i _ ↦ h i⟩
  have : 1 / f i * a₁ ≤ 1 / g i * a₂ := hasProd_le this (hf.update i 1) (hg.update i 1)
  simpa only [one_div, mul_inv_cancel_left] using mul_lt_mul_of_lt_of_le hi this

Premises used: one_div, mul_inv_cancel_left
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : IsTopologicalGroup α
inst_5 : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
hf : HasProd f a₁
hg : HasProd g a₂
h : f < g
⊢ a₁ < a₂

Tactic:
let ⟨hle, _i, hi⟩ := Pi.lt_def.mp h
  hasProd_lt hle hi hf hg

Premises used: hasProd_lt, Pi.lt_def, _private.0.hasProd_strict_mono.match_1, LT.lt, Iff.mp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : IsTopologicalGroup α
inst_5 : OrderClosedTopology α
f g : ι → α
i : ι
inst_6 : L.NeBot
inst_7 : L.LeAtTop
h : f ≤ g
hi : f i < g i
hf : Multipliable f L
hg : Multipliable g L
⊢ LT.lt.{u_3} (α := α) (∏'[L] (n : ι), f n) (∏'[L] (n : ι), g n)

Tactic:
hasProd_lt h hi hf.hasProd hg.hasProd

Premises used: hasProd_lt, Multipliable.hasProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : IsTopologicalGroup α
inst_5 : OrderClosedTopology α
f g : ι → α
inst_6 : L.NeBot
inst_7 : L.LeAtTop
hf : Multipliable f L
hg : Multipliable g L
h : f < g
⊢ LT.lt.{u_3} (α := α) (∏'[L] (n : ι), f n) (∏'[L] (n : ι), g n)

Tactic:
let ⟨hle, _i, hi⟩ := Pi.lt_def.mp h
  hf.tprod_lt_tprod hle hi hg

Premises used: Pi.lt_def, Multipliable.tprod_lt_tprod, _private.0.hasProd_strict_mono.match_1, LT.lt, Iff.mp, tprod
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : IsTopologicalGroup α
inst_5 : OrderClosedTopology α
g : ι → α
inst_6 : L.LeAtTop
inst_7 : L.NeBot
hsum : Multipliable g L
hg : ∀ (i : ι), 1 ≤ g i
i : ι
hi : 1 < g i
rw : LT.lt.{u_3} (α := α) (∏'[L] (x : ι), 1) (∏'[L] (i : ι), g i)
⊢ LT.lt.{u_3} (α := α) 1 (∏'[L] (i : ι), g i)

Tactic:
rw [← tprod_one (L := L)]

Premises used: tprod_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : IsTopologicalGroup α
inst_5 : OrderClosedTopology α
g : ι → α
inst_6 : L.LeAtTop
inst_7 : L.NeBot
hsum : Multipliable g L
hg : ∀ (i : ι), 1 ≤ g i
i : ι
hi : 1 < g i
⊢ LT.lt.{u_3} (α := α) (∏'[L] (x : ι), 1) (∏'[L] (i : ι), g i)

Tactic:
multipliable_one.tprod_lt_tprod hg hi hsum

Premises used: multipliable_one, Multipliable.tprod_lt_tprod
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : IsTopologicalGroup α
inst_5 : OrderClosedTopology α
g : ι → α
inst_6 : L.LeAtTop
inst_7 : L.NeBot
hsum : Multipliable g L
hg : ∀ (i : ι), 1 ≤ g i
i : ι
hi : 1 < g i
⊢ LT.lt.{u_3} (α := α) (∏'[L] (x : ι), 1) (∏'[L] (i : ι), g i)

Tactic:
exact multipliable_one.tprod_lt_tprod hg hi hsum

Premises used: multipliable_one, Multipliable.tprod_lt_tprod
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : CanonicallyOrderedMul α
inst_4 : TopologicalSpace α
inst_5 : OrderClosedTopology α
f : ι → α
a : α
hf : HasProd f a
i : ι
⊢ f i ≤ a

Tactic:
le_hasProd hf i fun _ _ ↦ one_le

Premises used: le_hasProd, one_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : CanonicallyOrderedMul α
inst_4 : TopologicalSpace α
inst_5 : OrderClosedTopology α
f : ι → α
hf : Multipliable f
i : ι
⊢ f i ≤ ∏' (i : ι), f i

Tactic:
hf.le_tprod i fun _ _ ↦ one_le

Premises used: one_le, Multipliable.le_tprod