mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : 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₂
⊢ a₁ ≤ a₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: κ : Type u_4
γ : Type u_5
inst✝⁶ : CommGroup γ
inst✝⁵ : PartialOrder γ
inst✝⁴ : IsOrderedMonoid γ
inst✝³ : UniformSpace γ
inst✝² : IsUniformGroup γ
inst✝¹ : OrderClosedTopology γ
inst✝ : CompleteSpace γ
f : κ → γ
β : Set κ
h : ∀ (a : κ), 1 ≤ f a
hf : Multipliable f
⊢ ∀ c ∉ Set.range fun a ↦ ↑a, 1 ≤ f c

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: κ : Type u_4
γ : Type u_5
inst✝⁶ : CommGroup γ
inst✝⁵ : PartialOrder γ
inst✝⁴ : IsOrderedMonoid γ
inst✝³ : UniformSpace γ
inst✝² : IsUniformGroup γ
inst✝¹ : OrderClosedTopology γ
inst✝ : CompleteSpace γ
f : κ → γ
β : Set κ
h : ∀ (a : κ), 1 ≤ f a
hf : Multipliable f
⊢ ∀ (i : { x // x ∈ β }), f ↑i ≤ f ↑i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: κ : Type u_4
γ : Type u_5
inst✝⁶ : CommGroup γ
inst✝⁵ : PartialOrder γ
inst✝⁴ : IsOrderedMonoid γ
inst✝³ : UniformSpace γ
inst✝² : IsUniformGroup γ
inst✝¹ : OrderClosedTopology γ
inst✝ : CompleteSpace γ
f : κ → γ
β : Set κ
h : ∀ (a : κ), 1 ≤ f a
hf : Multipliable f
⊢ Multipliable fun b ↦ f ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: κ : Type u_4
γ : Type u_5
inst✝⁶ : CommGroup γ
inst✝⁵ : PartialOrder γ
inst✝⁴ : IsOrderedMonoid γ
inst✝³ : UniformSpace γ
inst✝² : IsUniformGroup γ
inst✝¹ : OrderClosedTopology γ
inst✝ : CompleteSpace γ
f : κ → γ
β : Set κ
h : ∀ (a : κ), 1 ≤ f a
hf : Multipliable f
⊢ ∏' (b : ↑β), f ↑b ≤ ∏' (a : κ), f a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁶ : CommMonoid α
inst✝⁵ : Preorder α
inst✝⁴ : IsOrderedMonoid α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
f : ι → α
a : α
inst✝¹ : L.NeBot
inst✝ : L.LeAtTop
s : Finset ι
hs : ∀ i ∉ s, 1 ≤ f i
hf : HasProd f a L
⊢ ∏ i ∈ s, f i ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a : α
h : ∀ (i : ι), 1 ≤ f i
hf : HasProd f a
⊢ IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
hf : Multipliable f L
hL : ¬L.NeBot
hfs : ¬(mulSupport fun x ↦ g (f x)).Finite
⊢ g 1 = ∏'[L] (i : β), g (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁶ : CommMonoid α
inst✝⁵ : Preorder α
inst✝⁴ : IsOrderedMonoid α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
f : ι → α
a : α
inst✝¹ : L.NeBot
inst✝ : L.LeAtTop
hf : HasProd f a L
i : ι
hb : ∀ (j : ι), j ≠ i → 1 ≤ f j
⊢ f i = ∏ i ∈ {i}, f i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁶ : CommMonoid α
inst✝⁵ : Preorder α
inst✝⁴ : IsOrderedMonoid α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
f : ι → α
a : α
inst✝¹ : L.NeBot
inst✝ : L.LeAtTop
hf : HasProd f a L
i : ι
hb : ∀ (j : ι), j ≠ i → 1 ≤ f j
⊢ ∀ i_1 ∉ {i}, 1 ≤ f i_1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁷ : CommMonoid α
inst✝⁶ : Preorder α
inst✝⁵ : IsOrderedMonoid α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderClosedTopology α
f : ι → α
a : α
inst✝² : L.NeBot
inst✝¹ : L.LeAtTop
inst✝ : MulRightStrictMono α
hf : HasProd f a L
i : ι
hi : ∀ (j : ι), j ≠ i → 1 ≤ f j
j : ι
hij : j ≠ i
hj : 1 < f j
⊢ f j * f i = ∏ k ∈ {j, i}, f k

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁷ : CommMonoid α
inst✝⁶ : Preorder α
inst✝⁵ : IsOrderedMonoid α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderClosedTopology α
f : ι → α
a : α
inst✝² : L.NeBot
inst✝¹ : L.LeAtTop
inst✝ : MulRightStrictMono α
hf : HasProd f a L
i : ι
hi : ∀ (j : ι), j ≠ i → 1 ≤ f j
j : ι
hij : j ≠ i
hj : 1 < f j
⊢ f i < a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
⊢ Multipliable f L → Multipliable (⇑g ∘ f) L ∧ ∏'[L] (i : β), g (f i) ∈ Set.range ⇑g

pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
⊢ Multipliable (⇑g ∘ f) L ∧ ∏'[L] (i : β), g (f i) ∈ Set.range ⇑g → Multipliable f L

Tactic:
· intro hf
    constructor
    · exact hf.map g hg.continuous
    · by_cases hL : L.NeBot
      · exact ⟨_, hf.map_tprod g hg.continuous⟩
      · by_cases hfs : (mulSupport fun x ↦ g (f x)).Finite
        · simp [tprod_bot hL, finprod_eq_prod _ hfs, ← _root_.map_prod]
        · exact ⟨1, by simp [tprod_bot hL, finprod_of_infinite_mulSupport hfs]⟩

Goal state after:
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
⊢ Multipliable (⇑g ∘ f) L ∧ ∏'[L] (i : β), g (f i) ∈ Set.range ⇑g → Multipliable f L
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℕ → M
h : HasProd (fun n ↦ f (n + 1)) m
⊢ HasProd f (f 0 * m)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℕ → M
he : HasProd (fun k ↦ f (2 * k)) m
ho : HasProd (fun k ↦ f (2 * k + 1)) m'
⊢ HasProd f (m * m')

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : CommMonoid α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
⊢ ∏'[L] (i : ι), f i ≤ a₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
⊢ Multipliable f L ↔ Multipliable (⇑g ∘ f) L ∧ ∏'[L] (i : β), g (f i) ∈ Set.range ⇑g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : T2Space M
f : ℕ → M
hf : Multipliable f
⊢ HasProd f m ↔ Tendsto (fun n ↦ ∏ i ∈ range n, f i) atTop (𝓝 m)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
o : Set α
ho : o ∈ 𝓝 1
o_closed : IsClosed[inst✝².toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
t : Set β
hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ ↑s
ht : Multipliable fun a ↦ f ↑a
t' : Finset ↑t
x✝¹ : { x // x ∈ t }
x✝ : x✝¹ ∈ t'
⊢ ?m.138 ↑x✝¹ = f ↑x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
⊢ 1 ≤ ∏'[L] (i : ι), g i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a b : α
L : SummationFilter β
inst✝ : ContinuousMul α
hf : HasProd f a L
hg : HasProd g b L
⊢ HasProd (fun b ↦ f b * g b) (a * b) L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
⊢ ∏'[L] (i : ι), f i ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case inr
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
α : Type u_3
β : Type u_4
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
s : β → α
n : ℕ
hn : n ∉ Set.range encode
⊢ m (⨆ b ∈ decode₂ β n, s b) = 1 n

Tactic:
← decode₂_ne_none_iff,

Goal state after:
case inr
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
α : Type u_3
β : Type u_4
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
s : β → α
n : ℕ
hn : ¬decode₂ β n ≠ none
⊢ m (⨆ b ∈ decode₂ β n, s b) = 1 n
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
a : α
L : SummationFilter β
inst✝ : ContinuousMul α
hf : HasProd f a L
n : ℕ
⊢ HasProd (fun x ↦ f x ^ n) (a ^ n) L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
inst✝ : ContinuousMul α
f : γ → β → α
a : γ → α
s : Finset γ
⊢ (∀ i ∈ ∅, HasProd (f i) (a i) L) → HasProd (fun b ↦ ∏ i ∈ ∅, f i b) (∏ i ∈ ∅, a i) L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_4
α : Type u_5
L : SummationFilter ι
inst✝⁶ : CommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedMonoid α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
f : ι → α
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
hf : ∀ (i : ι), 1 ≤ f i
⊢ HasProd f 1 L ↔ f = 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
α : Type u_3
β : Type u_4
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
s : β → α
⊢ ∏' (i : ℕ), m (⨆ b ∈ decode₂ β i, s b) = ∏' (b : β), m (s b)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
inst✝ : ContinuousMul α
f : γ → β → α
a : γ → α
s : Finset γ
⊢ ∀ (a_1 : γ) (s : Finset γ),
    a_1 ∉ s →
      ((∀ i ∈ s, HasProd (f i) (a i) L) → HasProd (fun b ↦ ∏ i ∈ s, f i b) (∏ i ∈ s, a i) L) →
        (∀ i ∈ insert a_1 s, HasProd (f i) (a i) L) →
          HasProd (fun b ↦ ∏ i ∈ insert a_1 s, f i b) (∏ i ∈ insert a_1 s, a i) L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
α : Type u_3
β : Type u_4
inst✝¹ : Countable β
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s : β → α
⊢ R (m (⨆ b, s b)) (∏' (b : β), m (s b))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁷ : CommGroup α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedMonoid α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsTopologicalGroup α
inst✝² : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
inst✝¹ : L.NeBot
inst✝ : L.LeAtTop
h : f ≤ g
hi : f i < g i
hf : HasProd f a₁ L
hg : HasProd g a₂ L
⊢ a₁ < a₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁷ : CommGroup α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedMonoid α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsTopologicalGroup α
inst✝² : OrderClosedTopology α
g : ι → α
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
hsum : Multipliable g L
hg : ∀ (i : ι), 1 ≤ g i
i : ι
hi : 1 < g i
⊢ 1 < ∏'[L] (i : ι), g i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
α : Type u_3
γ : Type u_5
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s : γ → α
t : Finset γ
⊢ R (m (⨆ d ∈ t, s d)) (∏ d ∈ t, m (s d))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
inst✝ : ContinuousMul α
f : γ → β → α
a : γ → α
s : Finset γ
⊢ (∀ i ∈ s, HasProd (f i) (a i) L) → HasProd (fun b ↦ ∏ i ∈ s, f i b) (∏ i ∈ s, a i) L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
⊢ (CauchySeq fun s ↦ ∏ b ∈ s, f b) ↔ ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set β), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
f : β → α
inst✝ : CompleteSpace α
⊢ Multipliable f ↔ ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁵ : CommMonoidWithZero α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : ZeroLEOneClass α
inst✝¹ : PosMulMono α
inst✝ : ClosedIciTopology α
f : ι → α
hf : ∀ (i : ι), 0 ≤ f i
⊢ 0 ≤ ∏'[L] (x : ι), f x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
α : Type u_3
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s₁ s₂ : α
⊢ R (m (s₁ ⊔ s₂)) (m s₁ * m s₂)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedMonoid α
inst✝² : CanonicallyOrderedMul α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
hf : Multipliable f
⊢ ∏' (i : ι), f i = 1 ↔ ∀ (x : ι), f x = 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
f : β → α
inst✝ : CompleteSpace α
⊢ Multipliable f ↔ ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set β), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
a b : α
inst✝ : ContinuousMul α
s t : Set β
hs : Disjoint s t
ha : HasProd (f ∘ Subtype.val) a
hb : HasProd (f ∘ Subtype.val) b
⊢ HasProd (f ∘ Subtype.val) (a * b)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : T2Space M
inst✝ : ContinuousMul M
f : ℕ → M
hf : Multipliable fun n ↦ f (n + 1)
⊢ ∏' (b : ℕ), f b = f 0 * ∏' (b : ℕ), f (b + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedMonoid α
inst✝² : CanonicallyOrderedMul α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
hf : Multipliable f
⊢ ∏' (i : ι), f i ≠ 1 ↔ ∃ x, f x ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedMul α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a : α
hf : HasProd f a
⊢ IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
g : G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℕ → G
k : ℕ
⊢ HasProd (fun n ↦ f (n + k)) g ↔ HasProd f (g * ∏ i ∈ range k, f i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : CommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : IsOrderedMonoid α
inst✝² : UniformSpace α
inst✝¹ : IsUniformGroup α
inst✝ : CompleteSpace α
f : ι → α
s : Set ι := {x | 1 ≤ f x}
h1 : ∀ (x : ↑s), |f ↑x|ₘ = f ↑x
h2 : ∀ (x : ↑sᶜ), |f ↑x|ₘ = (f ↑x)⁻¹
⊢ ((Multipliable fun x ↦ |f ↑x|ₘ) ∧ Multipliable fun x ↦ |f ↑x|ₘ) ↔
    (Multipliable fun x ↦ f ↑x) ∧ Multipliable fun x ↦ (f ↑x)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
g : G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
f : ℕ → G
k : ℕ
⊢ HasProd (fun n ↦ f (n + k)) (g / ∏ i ∈ range k, f i) ↔ HasProd f g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : CommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : IsOrderedMonoid α
inst✝² : UniformSpace α
inst✝¹ : IsUniformGroup α
inst✝ : CompleteSpace α
f : ι → α
s : Set ι := {x | 1 ≤ f x}
h1 : ∀ (x : ↑s), |f ↑x|ₘ = f ↑x
h2 : ∀ (x : ↑sᶜ), |f ↑x|ₘ = (f ↑x)⁻¹
⊢ ((Multipliable fun x ↦ f ↑x) ∧ Multipliable fun x ↦ (f ↑x)⁻¹) ↔ Multipliable f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x ↦ b
s : Finset ι
⊢ #s • b ≤ ∑' (x : ι), b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
f g : β → α
inst✝ : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
e : Set α
he : e ∈ 𝓝 1
s : Finset β
hs : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
t : Finset β
ht : Disjoint t s
⊢ ∏ b ∈ t with g b = f b, g b = ∏ b ∈ t, g b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
f g : β → α
inst✝ : CompleteSpace α
hf : Multipliable f
h : ∀ (b : β), g b = 1 ∨ g b = f b
⊢ Multipliable g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : Multipliable f
⊢ (fun i ↦ (∏' (i : ℕ), f i) / ∏ j ∈ range i, f j) = fun i ↦ ∏' (k : ℕ), f (k + i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
f : β → α
inst✝ : CompleteSpace α
i : γ → β
hf : Multipliable f
hi : Injective i
⊢ Multipliable (f ∘ i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x ↦ b
H : ∀ (s : Finset ι), #s • b ≤ ∑' (x : ι), b
n : ℕ
hn : ∑' (x : ι), b ≤ n • b
s : Finset ι
⊢ #s ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x ↦ b
⊢ Finite ι

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : CommGroup α
inst✝² : IsUniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T2Space α
f : β → α
hf : Multipliable f
s : Finset β
⊢ (∏ x ∈ s, f x) * ∏' (x : { x // x ∉ s }), f ↑x = ∏' (x : β), f x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁴ : CommRing α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : ι → α
x : α
hfx : HasProd f x
⊢ HasProd (fun x ↦ |f x|) |x|

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
⊢ Tendsto (fun i ↦ ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
inst✝ : ContinuousMul α
ι : Type u_4
s : Finset ι
t : ι → Set β
a : ι → α
hs : (↑s).Pairwise (Disjoint on t)
hf : ∀ i ∈ s, HasProd (f ∘ Subtype.val) (a i)
⊢ HasProd (f ∘ Subtype.val) (∏ i ∈ s, a i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
⊢ ∃ s, ∀ (t : Set α), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e

Tactic:
by

Goal state after: