awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
inst : Ring R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
inst_3 : NonarchimedeanRing R
inst_4 : CompleteSpace R
f : α → R
g : β → R
hf : Tendsto f cofinite (𝓝 0)
hg : Tendsto g cofinite (𝓝 0)
⊢ Tendsto (β := R) (fun (i : α × β) ↦ f i.1 * g i.2) cofinite (𝓝 0)

Tactic:
tendsto_mul_cofinite_nhds_zero hf hg

Premises used: tendsto_mul_cofinite_nhds_zero
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
inst : Ring R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
inst_3 : NonarchimedeanRing R
inst_4 : CompleteSpace R
f : α → R
g : β → R
hf : Tendsto f cofinite (𝓝 0)
hg : Tendsto g cofinite (𝓝 0)
⊢ Tendsto (β := R) (fun (i : α × β) ↦ f i.1 * g i.2) cofinite (𝓝 0)

Tactic:
exact tendsto_mul_cofinite_nhds_zero hf hg

Premises used: tendsto_mul_cofinite_nhds_zero
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
inst : Ring R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
inst_3 : NonarchimedeanRing R
f : α → R
g : β → R
a b : R
hf : HasSum f a
hg : HasSum g b
rw :
  ∀
    (hf :
      HasSum (α := UniformSpace.Completion R)
        ((⇑UniformSpace.Completion.toCompl : (a : R) → UniformSpace.Completion R) ∘ f) (↑a : UniformSpace.Completion R))
    (hg :
      HasSum (α := UniformSpace.Completion R)
        ((⇑UniformSpace.Completion.toCompl : (a : R) → UniformSpace.Completion R) ∘ g)
        (↑b : UniformSpace.Completion R)),
    HasSum (α := UniformSpace.Completion R) (β := α × β)
      (Function.comp (β := R) (⇑UniformSpace.Completion.toCompl : (a : R) → UniformSpace.Completion R) fun (i : α × β) ↦
        f i.1 * g i.2)
      (↑(a * b) : UniformSpace.Completion R)
⊢ HasSum (fun (i : α × β) ↦ f i.1 * g i.2) (a * b)

Tactic:
rw [← hasSum_iff_hasSum_compl] at *

Premises used: hasSum_iff_hasSum_compl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
inst : Ring R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
inst_3 : NonarchimedeanRing R
f : α → R
g : β → R
a b : R
hf :
  HasSum (α := UniformSpace.Completion R) ((⇑UniformSpace.Completion.toCompl : (a : R) → UniformSpace.Completion R) ∘ f)
    (↑a : UniformSpace.Completion R)
hg :
  HasSum (α := UniformSpace.Completion R) ((⇑UniformSpace.Completion.toCompl : (a : R) → UniformSpace.Completion R) ∘ g)
    (↑b : UniformSpace.Completion R)
simp :
  HasSum
    (fun (x : α × β) ↦
      HMul.hMul (α := UniformSpace.Completion R) (↑(f x.1) : UniformSpace.Completion R)
        (↑(g x.2) : UniformSpace.Completion R))
    (HMul.hMul (α := UniformSpace.Completion R) (↑a : UniformSpace.Completion R) (↑b : UniformSpace.Completion R))
⊢ HasSum (α := UniformSpace.Completion R) (β := α × β)
    (Function.comp (β := R) (⇑UniformSpace.Completion.toCompl : (a : R) → UniformSpace.Completion R) fun (i : α × β) ↦
      f i.1 * g i.2)
    (↑(a * b) : UniformSpace.Completion R)

Tactic:
simp only [Function.comp_def, UniformSpace.Completion.toCompl_apply,
    UniformSpace.Completion.coe_mul]

Premises used: Function.comp_def, UniformSpace.Completion.coe_mul, UniformSpace.Completion.toCompl_apply
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
inst : Ring R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
inst_3 : NonarchimedeanRing R
f : α → R
g : β → R
a b : R
hf :
  HasSum (α := UniformSpace.Completion R) ((⇑UniformSpace.Completion.toCompl : (a : R) → UniformSpace.Completion R) ∘ f)
    (↑a : UniformSpace.Completion R)
hg :
  HasSum (α := UniformSpace.Completion R) ((⇑UniformSpace.Completion.toCompl : (a : R) → UniformSpace.Completion R) ∘ g)
    (↑b : UniformSpace.Completion R)
⊢ HasSum
    (fun (x : α × β) ↦
      HMul.hMul (α := UniformSpace.Completion R) (↑(f x.1) : UniformSpace.Completion R)
        (↑(g x.2) : UniformSpace.Completion R))
    (HMul.hMul (α := UniformSpace.Completion R) (↑a : UniformSpace.Completion R) (↑b : UniformSpace.Completion R))

Tactic:
(hf.mul hg) (hf.summable.mul_of_complete_nonarchimedean hg.summable :)

Premises used: UniformSpace.Completion.coe', HasSum.summable, SeparationQuotient.mk, _private.0.Summable.mul_of_complete_nonarchimedean, HasSum.mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
inst : Ring R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
inst_3 : NonarchimedeanRing R
f : α → R
g : β → R
a b : R
hf :
  HasSum (α := UniformSpace.Completion R) ((⇑UniformSpace.Completion.toCompl : (a : R) → UniformSpace.Completion R) ∘ f)
    (↑a : UniformSpace.Completion R)
hg :
  HasSum (α := UniformSpace.Completion R) ((⇑UniformSpace.Completion.toCompl : (a : R) → UniformSpace.Completion R) ∘ g)
    (↑b : UniformSpace.Completion R)
⊢ HasSum
    (fun (x : α × β) ↦
      HMul.hMul (α := UniformSpace.Completion R) (↑(f x.1) : UniformSpace.Completion R)
        (↑(g x.2) : UniformSpace.Completion R))
    (HMul.hMul (α := UniformSpace.Completion R) (↑a : UniformSpace.Completion R) (↑b : UniformSpace.Completion R))

Tactic:
exact (hf.mul hg) (hf.summable.mul_of_complete_nonarchimedean hg.summable :)

Premises used: HasSum.summable, _private.0.Summable.mul_of_complete_nonarchimedean, HasSum.mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
inst : Ring R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
inst_3 : NonarchimedeanRing R
f : α → R
g : β → R
hf : Summable f
hg : Summable g
⊢ Summable (α := R) fun (i : α × β) ↦ f i.1 * g i.2

Tactic:
(hf.hasSum.mul_of_nonarchimedean hg.hasSum).summable

Premises used: HasSum.mul_of_nonarchimedean, HasSum.summable, Summable.hasSum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
inst : Ring R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
inst_3 : NonarchimedeanRing R
inst_4 : T0Space R
f : α → R
g : β → R
hf : Summable f
hg : Summable g
⊢ HMul.hMul (α := R) (∑' (i : α), f i) (∑' (i : β), g i) = ∑' (i : α × β), f i.1 * g i.2

Tactic:
(hf.hasSum.mul_of_nonarchimedean hg.hasSum).tsum_eq.symm

Premises used: HasSum.mul_of_nonarchimedean, HasSum.tsum_eq, Summable.hasSum, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : Preorder α
inst_1 : CommMonoid α
inst_2 : TopologicalSpace α
a c : α
f : ι → α
inst_3 : ClosedIicTopology α
inst_4 : L.NeBot
hf : HasProd f a L
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ c
⊢ a ≤ c

Tactic:
le_of_tendsto' hf h

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

Tactic:
ge_of_tendsto' hf h

Premises used: ge_of_tendsto'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
α : Type u_3
inst : Preorder α
inst_1 : CommMonoid α
inst_2 : TopologicalSpace α
c : α
inst_3 : ClosedIicTopology α
f : ℕ → α
hf : Multipliable f
h : ∀ (n : ℕ), ∏ i ∈ range n, f i ≤ c
⊢ ∏' (n : ℕ), f n ≤ c

Tactic:
le_of_tendsto' hf.hasProd.tendsto_prod_nat h

Premises used: HasProd.tendsto_prod_nat, Multipliable.hasProd, le_of_tendsto'
-- 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 : ι → α
a₁ a₂ : α
h : ∀ (i : ι), f i ≤ g i
hf : HasProd f a₁ L
hg : HasProd g a₂ L
inst_5 : L.NeBot
⊢ a₁ ≤ a₂

Tactic:
le_of_tendsto_of_tendsto' hf hg fun _ ↦ prod_le_prod' fun i _ ↦ h i

Premises used: Finset.prod_le_prod', le_of_tendsto_of_tendsto'
-- 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 : ι → α
a₁ a₂ : α
hf : HasProd f a₁ L
hg : HasProd g a₂ L
h : f ≤ g
inst_5 : L.NeBot
⊢ a₁ ≤ a₂

Tactic:
hasProd_le h hf hg

Premises used: hasProd_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd f a₁
hg : HasProd g a₂
⊢ HasProd (extend e f 1) a₁

Tactic:
rw [← hasProd_extend_one he] at hf

Premises used: hasProd_extend_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd f a₁
hg : HasProd g a₂
hf₁ : HasProd (extend e f 1) a₁
⊢ HasProd g a₂

Tactic:
rw [← hasProd_extend_one he] at hf

Premises used: hasProd_extend_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
⊢ a₁ ≤ a₂

Tactic:
hasProd_le (fun c ↦ ?_) hf hg

Premises used: hasProd_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
refine : ∀ (c : κ), extend e f 1 c ≤ g c
⊢ a₁ ≤ a₂

Tactic:
refine hasProd_le (fun c ↦ ?_) hf hg

Premises used: hasProd_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
c : κ
inl : ∀ (i : ι), extend e f 1 (e i) ≤ g (e i)
inr : ∀ (h : c ∉ Set.range e), extend e f 1 c ≤ g c
⊢ extend e f 1 c ≤ g c

Tactic:
obtain ⟨i, rfl⟩ | h := em (c ∈ Set.range e)

Premises used: Membership.mem, em, Set.range, rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
i : ι
inl : f i ≤ g (e i)
⊢ extend e f 1 (e i) ≤ g (e i)

Tactic:
rw [he.extend_apply]

Premises used: Function.Injective.extend_apply
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
i : ι
⊢ f i ≤ g (e i)

Tactic:
h _
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
i : ι
⊢ f i ≤ g (e i)

Tactic:
exact h _
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h_1 : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
c : κ
h : c ∉ Set.range e
inr : 1 c ≤ g c
⊢ extend e f 1 c ≤ g c

Tactic:
rw [extend_apply' _ _ _ h]

Premises used: Function.extend_apply'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h_1 : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
c : κ
h : c ∉ Set.range e
⊢ 1 c ≤ g c

Tactic:
hs _ h
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h_1 : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
c : κ
h : c ∉ Set.range e
⊢ 1 c ≤ g c

Tactic:
exact hs _ h
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : Multipliable f
hg : Multipliable g
⊢ tprod f ≤ tprod g

Tactic:
hasProd_le_inj _ he hs h hf.hasProd hg.hasProd

Premises used: Multipliable.hasProd, hasProd_le_inj
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
κ : Type u_4
γ : Type u_5
inst : CommGroup γ
inst_1 : PartialOrder γ
inst_2 : IsOrderedMonoid γ
inst_3 : UniformSpace γ
inst_4 : IsUniformGroup γ
inst_5 : OrderClosedTopology γ
inst_6 : CompleteSpace γ
f : κ → γ
β : Set κ
h : ∀ (a : κ), 1 ≤ f a
hf : Multipliable f
⊢ ∀ c ∉ Set.range fun (a : { x : κ // x ∈ β }) ↦ (↑a : κ), 1 ≤ f c

Tactic:
simp only [Subtype.range_coe_subtype, Set.setOf_mem_eq, h, implies_true]

Premises used: Subtype.range_coe_subtype, Set.setOf_mem_eq, implies_true
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
κ : Type u_4
γ : Type u_5
inst : CommGroup γ
inst_1 : PartialOrder γ
inst_2 : IsOrderedMonoid γ
inst_3 : UniformSpace γ
inst_4 : IsUniformGroup γ
inst_5 : OrderClosedTopology γ
inst_6 : CompleteSpace γ
f : κ → γ
β : Set κ
h : ∀ (a : κ), 1 ≤ f a
hf : Multipliable f
⊢ ∀ (i : { x : κ // x ∈ β }), f (↑i : κ) ≤ f (↑i : κ)

Tactic:
simp only [le_refl, implies_true]

Premises used: le_refl, implies_true
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
κ : Type u_4
γ : Type u_5
inst : CommGroup γ
inst_1 : PartialOrder γ
inst_2 : IsOrderedMonoid γ
inst_3 : UniformSpace γ
inst_4 : IsUniformGroup γ
inst_5 : OrderClosedTopology γ
inst_6 : CompleteSpace γ
f : κ → γ
β : Set κ
h : ∀ (a : κ), 1 ≤ f a
hf : Multipliable f
⊢ Multipliable.{u_5, u_4} (α := γ) fun (b : (↑β : Type u_4)) ↦ f (↑b : κ)

Tactic:
apply hf.subtype

Premises used: Multipliable.subtype
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
κ : Type u_4
γ : Type u_5
inst : CommGroup γ
inst_1 : PartialOrder γ
inst_2 : IsOrderedMonoid γ
inst_3 : UniformSpace γ
inst_4 : IsUniformGroup γ
inst_5 : OrderClosedTopology γ
inst_6 : CompleteSpace γ
f : κ → γ
β : Set κ
h : ∀ (a : κ), 1 ≤ f a
hf : Multipliable f
apply : Multipliable.{u_5, u_4} (α := γ) fun (a : κ) ↦ f a
⊢ LE.le.{u_5} (α := γ) (∏' (b : (↑β : Type u_4)), f (↑b : κ)) (∏' (a : κ), f a)

Tactic:
apply Multipliable.tprod_le_tprod_of_inj _
    (Subtype.coe_injective)
    (by simp only [Subtype.range_coe_subtype, Set.setOf_mem_eq, h, implies_true])
    (by simp only [le_refl, implies_true])
    (by apply hf.subtype)

Premises used: Subtype.coe_injective, Multipliable.tprod_le_tprod_of_inj
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
κ : Type u_4
γ : Type u_5
inst : CommGroup γ
inst_1 : PartialOrder γ
inst_2 : IsOrderedMonoid γ
inst_3 : UniformSpace γ
inst_4 : IsUniformGroup γ
inst_5 : OrderClosedTopology γ
inst_6 : CompleteSpace γ
f : κ → γ
β : Set κ
h : ∀ (a : κ), 1 ≤ f a
hf : Multipliable f
⊢ Multipliable.{u_5, u_4} (α := γ) fun (a : κ) ↦ f a

Tactic:
apply hf
-- 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
s : Finset ι
hs : ∀ i ∉ s, 1 ≤ f i
hf : HasProd f a L
⊢ ∏ i ∈ s, f i ≤ a

Tactic:
ge_of_tendsto hf <| .filter_mono L.le_atTop <| eventually_atTop.2 ?_

Premises used: Iff.mpr, Filter.Eventually.filter_mono, ge_of_tendsto, SummationFilter.LeAtTop.le_atTop, Filter.eventually_atTop
-- 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
s : Finset ι
hs : ∀ i ∉ s, 1 ≤ f i
hf : HasProd f a L
refine : ∃ (a : Finset ι), ∀ b ≥ a, LE.le.{u_3} (α := α) (∏ i ∈ s, f i) (∏ b ∈ b, f b)
⊢ ∏ i ∈ s, f i ≤ a

Tactic:
refine ge_of_tendsto hf <| .filter_mono L.le_atTop <| eventually_atTop.2 ?_

Premises used: Iff.mpr, ge_of_tendsto, Filter.eventually_atTop
-- 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
s : Finset ι
hs : ∀ i ∉ s, 1 ≤ f i
hf : HasProd f a L
⊢ ∃ (a : Finset ι), ∀ b ≥ a, LE.le.{u_3} (α := α) (∏ i ∈ s, f i) (∏ b ∈ b, f b)

Tactic:
⟨s, fun _t hst ↦ prod_le_prod_of_subset_of_one_le' hst fun i _ hbs ↦ hs i hbs⟩

Premises used: Finset.prod_le_prod_of_subset_of_one_le', Exists.intro
-- 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
s : Finset ι
hs : ∀ i ∉ s, 1 ≤ f i
hf : HasProd f a L
⊢ ∃ (a : Finset ι), ∀ b ≥ a, LE.le.{u_3} (α := α) (∏ i ∈ s, f i) (∏ b ∈ b, f b)

Tactic:
exact ⟨s, fun _t hst ↦ prod_le_prod_of_subset_of_one_le' hst fun i _ hbs ↦ hs i hbs⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a : α
h : ∀ (i : ι), 1 ≤ f i
hf : HasProd f a
⊢ IsLUB (Set.range fun (s : Finset ι) ↦ ∏ i ∈ s, f i) a

Tactic:
isLUB_of_tendsto_atTop (Finset.prod_mono_set_of_one_le' h) hf

Premises used: isLUB_of_tendsto_atTop, Finset.prod_mono_set_of_one_le'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a : α
h : ∀ (i : ι), 1 ≤ f i
hf : HasProd f a
⊢ IsLUB (Set.range fun (s : Finset ι) ↦ ∏ i ∈ s, f i) a

Tactic:
exact isLUB_of_tendsto_atTop (Finset.prod_mono_set_of_one_le' h) hf

Premises used: isLUB_of_tendsto_atTop, Finset.prod_mono_set_of_one_le'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a : α
h : ∀ (i : ι), 1 ≤ f i
hf : HasProd f a
⊢ IsLUB (Set.range fun (s : Finset ι) ↦ ∏ i ∈ s, f i) a

Tactic:
classical
  exact isLUB_of_tendsto_atTop (Finset.prod_mono_set_of_one_le' h) hf

Premises used: isLUB_of_tendsto_atTop, Finset.prod_mono_set_of_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 α
f : ι → α
a : α
inst_5 : L.NeBot
inst_6 : L.LeAtTop
hf : HasProd f a L
i : ι
hb : ∀ (j : ι), j ≠ i → 1 ≤ f j
rw rw₁ : f i = f i
⊢ f i = ∏ i ∈ {i}, f i

Tactic:
rw [prod_singleton]

Premises used: Finset.prod_singleton
-- 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
hf : HasProd f a L
i : ι
hb : ∀ (j : ι), j ≠ i → 1 ≤ f j
⊢ ∀ i_1 ∉ {i}, 1 ≤ f i_1

Tactic:
simpa
-- 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 i < f j * f i

Tactic:
lt_mul_of_one_lt_left' (f i) hj

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 α
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
rw rw₁ : f j * f i = f j * f i
⊢ f j * f i = ∏ k ∈ {j, i}, f k

Tactic:
rw [Finset.prod_pair hij]

Premises used: Finset.prod_pair
-- 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
⊢ ∏ k ∈ {j, i}, f k ≤ a

Tactic:
prod_le_hasProd _ (fun k hk ↦ hi k (hk ∘ mem_insert_of_mem ∘ mem_singleton.mpr)) hf

Premises used: Iff.mpr, Finset.mem_singleton, prod_le_hasProd, Function.comp, Finset.mem_insert_of_mem
-- 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:
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: Iff.mpr, Finset.mem_singleton, prod_le_hasProd, Function.comp, lt_mul_of_one_lt_left', Finset.mem_insert_of_mem