mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
s : Set α
f : α → β
g : α → γ
Kf Kg : ℝ≥0
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
x✝ : α
hx : x✝ ∈ s
y✝ : α
hy : y✝ ∈ s
⊢ edist ((fun x ↦ (f x, g x)) x✝) ((fun x ↦ (f x, g x)) y✝) ≤ ↑(max Kf Kg) * edist x✝ y✝

Tactic:
rw [ENNReal.coe_mono.map_max, Prod.edist_eq, max_mul]

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
s : Set α
f : α → β
g : α → γ
Kf Kg : ℝ≥0
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
x✝ : α
hx : x✝ ∈ s
y✝ : α
hy : y✝ ∈ s
⊢ max (edist ((fun x ↦ (f x, g x)) x✝).1 ((fun x ↦ (f x, g x)) y✝).1)
      (edist ((fun x ↦ (f x, g x)) x✝).2 ((fun x ↦ (f x, g x)) y✝).2) ≤
    max (↑Kf * edist x✝ y✝) (↑Kg * edist x✝ y✝)
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : ι → Set α
𝓕 : Filter ι
a : α
⊢ a ∈ liminf s 𝓕 ↔ ∀ᶠ (i : ι) in 𝓕, a ∈ s i

Tactic:
simpa using

Goal state after:
α : Type u_1
ι : Type u_4
s : ι → Set α
𝓕 : Filter ι
a : α
⊢ (∃ i, ∃ (_ : i ∈ 𝓕), ∀ i_1 ∈ i, a ∈ s i_1) ↔ ∀ᶠ (i : ι) in 𝓕, a ∈ s i
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : x ∉ {x | {n | p n ∧ x ∈ s n}.Infinite}
⊢ {x_1 | p x_1 ∧ ¬s x_1 ⊆ {x}ᶜ}.Finite

Tactic:
simpa using

Goal state after:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : x ∉ {x | {n | p n ∧ x ∈ s n}.Infinite}
⊢ {x_1 | p x_1 ∧ x ∈ s x_1}.Finite
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ᶠ (x : α) in f, u x ≤ b
⊢ ∀ᶠ (n : β) in map u f, n ≤ b

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ᶠ (x : α) in f, u x ≤ b
⊢ ∀ᶠ (a : α) in f, u a ≤ b
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y
h' : ∃ y > x, ∀ (z : β), z ≤ x ∨ y ≤ z
⊢ ∀ᶠ (n : α) in f, u n ≤ x

Tactic:
rcases h' with ⟨z, x_z, hz⟩

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y
z : β
x_z : z > x
hz : ∀ (z_1 : β), z_1 ≤ x ∨ z ≤ z_1
⊢ ∀ᶠ (n : α) in f, u n ≤ x
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
β : Type u_4
s : Set (Finset α)
t : Finset α
H : ∀ (b : Finset α), t ⊆ b → b ∈ s
b : Finset (α ⊕ β)
hb : t.disjSum ∅ ⊆ b
⊢ t ⊆ b.toLeft

Tactic:
simpa using

Goal state after:
α : Type u_3
β : Type u_4
s : Set (Finset α)
t : Finset α
H : ∀ (b : Finset α), t ⊆ b → b ∈ s
b : Finset (α ⊕ β)
hb : t.disjSum ∅ ⊆ b
⊢ ∀ x ∈ t, Sum.inl x ∈ b
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
β : Type u_4
s : Set (Finset β)
t : Finset β
H : ∀ (b : Finset β), t ⊆ b → b ∈ s
b : Finset (α ⊕ β)
hb : ∅.disjSum t ⊆ b
⊢ t ⊆ b.toRight

Tactic:
simpa using

Goal state after:
α : Type u_3
β : Type u_4
s : Set (Finset β)
t : Finset β
H : ∀ (b : Finset β), t ⊆ b → b ∈ s
b : Finset (α ⊕ β)
hb : ∅.disjSum t ⊆ b
⊢ ∀ x ∈ t, Sum.inr x ∈ b
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
h✝ : Nonempty α
h : IsDirectedOrder α
s : Finset α
a : α
ha : ∀ i ∈ s, i ≤ a
b : α
hb : a ≤ b
c : α
hc : c ∈ s
⊢ c ∈ Finset.Iic b

Tactic:
simpa using

Goal state after:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
h✝ : Nonempty α
h : IsDirectedOrder α
s : Finset α
a : α
ha : ∀ i ∈ s, i ≤ a
b : α
hb : a ≤ b
c : α
hc : c ∈ s
⊢ c ≤ b
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
i : α
⊢ ∀ᶠ (s : Finset α) in atTop, i ∈ s

Tactic:
simpa using

Goal state after:
α : Type u_3
i : α
⊢ ∃ a, ∀ (b : Finset α), a ⊆ b → i ∈ b
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: β : Type u_2
L : SummationFilter β
c : Set β
⊢ L.support ⊆ c ↔ (map SetLike.coe L.filter).limsInf ⊆ c

Tactic:
simpa using

Goal state after:
β : Type u_2
L : SummationFilter β
c : Set β
⊢ (∀ (x : β), (∀ᶠ (s : Finset β) in L.filter, x ∈ s) → x ∈ c) ↔
    ∀ (t' : Set β), (∀ᶠ (a : Finset β) in L.filter, t' ⊆ ↑a) → t' ⊆ c
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: β : Type u_2
L : SummationFilter β
c : Set β
hL : ∀ (t' : Set β), (∀ᶠ (a : Finset β) in L.filter, t' ⊆ ↑a) → t' ⊆ c
x : β
hx : ∀ᶠ (s : Finset β) in L.filter, x ∈ s
⊢ ∀ᶠ (a : Finset β) in L.filter, {x} ⊆ ↑a

Tactic:
simpa using

Goal state after:
β : Type u_2
L : SummationFilter β
c : Set β
hL : ∀ (t' : Set β), (∀ᶠ (a : Finset β) in L.filter, t' ⊆ ↑a) → t' ⊆ c
x : β
hx : ∀ᶠ (s : Finset β) in L.filter, x ∈ s
⊢ ∀ᶠ (a : Finset β) in L.filter, x ∈ a
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
inst✝³ : ConditionallyCompleteLinearOrder β
f✝¹ : Filter α
u : α → β
inst✝² : ConditionallyCompleteLinearOrder α
f✝ : Filter α
b : α
f : ι → α
s : ι' → Set ι
p : ι' → Prop
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
j : Subtype p
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
g : ℕ → Subtype p := ⋯.choose
n : ℕ
hj : ⋯.choose n ∈ m
⊢ ∃ n, g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m

Tactic:
exact ⟨n, Or.inl hj⟩

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
⊢ ⋃ j, ⋂ i, Iic (f ↑i) = ⋃ j, ⋂ i, Iic (f ↑i)

Tactic:
apply Subset.antisymm

Goal state after:
case h₁
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := ⋯
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
⊢ ⋃ j, ⋂ i, Iic (f ↑i) ⊆ ⋃ j, ⋂ i, Iic (f ↑i)

case h₂
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := ⋯
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
⊢ ⋃ j, ⋂ i, Iic (f ↑i) ⊆ ⋃ j, ⋂ i, Iic (f ↑i)
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
j : Subtype p
hj : j ∈ m
⊢ ⋂ i, Iic (f ↑i) ⊆ ⋃ j, ⋂ i, Iic (f ↑i)

Tactic:
have : j = liminfReparam f s p j := by simp only [m, liminfReparam, hj, ite_true]

Goal state after:
case pos
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this✝ : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
j : Subtype p
hj : j ∈ m
this : j = liminfReparam f s p j
⊢ ⋂ i, Iic (f ↑i) ⊆ ⋃ j, ⋂ i, Iic (f ↑i)
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: case mp
γ : Type u_3
β : Type u_4
f : γ ↪ β
s : Set (Finset γ)
t : Finset β
ht : ∀ (b : Finset β), t ⊆ b → b.preimage ⇑f ⋯ ∈ s
x : Finset γ
hx : t.preimage ⇑f ⋯ ⊆ x
⊢ x ∈ s

Tactic:
simpa using

Goal state after:
case mp
γ : Type u_3
β : Type u_4
f : γ ↪ β
s : Set (Finset γ)
t : Finset β
ht : ∀ (b : Finset β), t ⊆ b → b.preimage ⇑f ⋯ ∈ s
x : Finset γ
hx : t.preimage ⇑f ⋯ ⊆ x
⊢ x ∈ s
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: case mk
β : Type u_4
inst✝² : Finite β
this : Fintype β
F : Filter (Finset β)
inst✝¹ : { filter := F }.LeAtTop
inst✝ : { filter := F }.NeBot
hAtTop : True
hL : F ≤ pure Finset.univ
s : Set (Finset β)
hs : s ∈ F
hs' : Finset.univ ∉ s
⊢ ∅ ∈ F

Tactic:
simpa using

Goal state after:
case mk
β : Type u_4
inst✝² : Finite β
this : Fintype β
F : Filter (Finset β)
inst✝¹ : { filter := F }.LeAtTop
inst✝ : { filter := F }.NeBot
hAtTop : True
hL : F ≤ pure Finset.univ
s : Set (Finset β)
hs : s ∈ F
hs' : Finset.univ ∉ s
⊢ ∅ ∈ F
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
A : ⋃ j, ⋂ i, Iic (f ↑i) = ⋃ j, ⋂ i, Iic (f ↑i)
j : Subtype p
Hj : j ∈ m
⊢ liminfReparam f s p j ∈ m

Tactic:
simpa using

Goal state after:
case pos
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
A : ⋃ j, ⋂ i, Iic (f ↑i) = ⋃ j, ⋂ i, Iic (f ↑i)
j : Subtype p
Hj : j ∈ m
⊢ j ∈ {j | BddBelow (range fun i ↦ f ↑i)}
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case neg.hs
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
H' : ¬∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
H : ∀ (j : Subtype p), (s ↑j).Nonempty
⊢ ∀ (j : Subtype p), (s ↑j).Nonempty

Tactic:
simpa using

Goal state after:
case neg.hs
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
H' : ¬∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i)
H : ∀ (j : Subtype p), (s ↑j).Nonempty
⊢ ∀ (j : Subtype p), s ↑j ≠ ∅
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x : EReal
hx_nonneg : 0 ≤ x
hx_ne_top : x ≠ ⊤
y z : EReal
⊢ (y + z) * x = y * x + z * x

Tactic:
simpa using

Goal state after:
x : EReal
hx_nonneg : 0 ≤ x
hx_ne_top : x ≠ ⊤
y z : EReal
⊢ x * (y + z) = x * y + x * z
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
s : Set β
hf : mulSupport f ⊆ s
⊢ ∀ x ∉ Set.range fun a ↦ ↑a, f x = 1

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
s : Set β
hf : mulSupport f ⊆ s
⊢ ∀ x ∉ s, f x = 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set β
hf : mulSupport f ⊆ s
⊢ HasProd (f ∘ Subtype.val) a ↔ HasProd f a

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set β
hf : mulSupport f ⊆ s
⊢ HasProd (f ∘ Subtype.val) a ↔ HasProd f a
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb : ∃ b, a < b
⊢ limsup f (𝓝[>] a) = ⨅ r, ⨅ (_ : r > a), f r

Tactic:
rw [(nhdsGT_basis_of_exists_gt hb).limsup_eq_iInf_iSup]

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb : ∃ b, a < b
⊢ ⨅ i, ⨅ (_ : a < i), ⨆ a_1 ∈ Set.Ioo a i, f a_1 = ⨅ r, ⨅ (_ : r > a), f r
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : Fintype β
f : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
⊢ HasProd f (∏ b, f b) L

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : Fintype β
f : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
⊢ HasProd f (∏ b, f b) L
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
s : Finset β
f : β → α
L : SummationFilter ↑↑s
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
⊢ HasProd (f ∘ Subtype.val) (∏ b ∈ map (Embedding.subtype fun x ↦ x ∈ ↑s) L.support.toFinset, f b) L

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
s : Finset β
f : β → α
L : SummationFilter ↑↑s
inst✝¹ : L.HasSupport
inst✝ : DecidablePred fun x ↦ x ∈ L.support
⊢ HasProd (f ∘ Subtype.val) (∏ x ∈ L.support.toFinset, f ↑x) L
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
s : Finset β
f : β → α
L : SummationFilter ↑↑s
inst✝ : L.LeAtTop
⊢ HasProd (f ∘ Subtype.val) (∏ b ∈ s, f b) L

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
s : Finset β
f : β → α
L : SummationFilter ↑↑s
inst✝ : L.LeAtTop
⊢ HasProd (f ∘ Subtype.val) (∏ b ∈ s, f b) L
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
f : β → α
s : Finset β
hf : ∀ b ∉ s, f b = 1
inst✝ : L.HasSupport
⊢ Multipliable f L

Tactic:
exact (hasProd_prod_support_of_ne_finset_one (fun b _ hb ↦ hf b hb)).multipliable

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

Goal state before:
pp: α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
hf : Multipliable (fun b ↦ (f b)⁻¹) L
⊢ Multipliable f L

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
hf : Multipliable (fun b ↦ (f b)⁻¹) L
⊢ Multipliable f L
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f g : β → α
hg : Multipliable g L
hfg : Multipliable (fun b ↦ f b / g b) L
⊢ Multipliable f L

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f g : β → α
hg : Multipliable g L
hfg : Multipliable (fun b ↦ f b / g b) L
⊢ Multipliable f L
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f g : β → α
hfg : Multipliable (fun b ↦ f b / g b) L
hf : Multipliable f L
⊢ Multipliable (fun b ↦ g b / f b) L

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f g : β → α
hfg : Multipliable (fun b ↦ f b / g b) L
hf : Multipliable f L
⊢ Multipliable (fun b ↦ g b / f b) L
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: case e'_6
α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
a : α
inst✝¹ : L.LeAtTop
inst✝ : DecidableEq β
hf : HasProd f a L
b : β
⊢ a / f b = 1 / f b * a

Tactic:
rw [div_mul_eq_mul_div, one_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 1
L : SummationFilter β
inst✝ : L.LeAtTop
this : HasProd f (∏ b' ∈ {b}, f b') L
⊢ HasProd f (f b) L

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 1
L : SummationFilter β
inst✝ : L.LeAtTop
this : HasProd f (∏ b' ∈ {b}, f b') L
⊢ HasProd f (f b) L
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 : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e

Tactic:
simp only [CauchySeq, cauchy_map_iff, prod_atTop_atTop_eq,
    uniformity_eq_comap_nhds_one α, tendsto_comap_iff, Function.comp_def, atTop_neBot, true_and]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
⊢ Tendsto (fun x ↦ (∏ b ∈ x.2, f b) / ∏ b ∈ x.1, f b) atTop (𝓝 1) ↔
    ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
h✝ : ∀ s ∈ 𝓝 1, ∃ a, ∀ (b : Finset β × Finset β), a ≤ b → (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ s
e : Set α
he : e ∈ 𝓝 1
s₁ s₂ t : Finset β
h : (∏ b ∈ (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t).2, f b) / ∏ b ∈ (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t).1, f b ∈ e
ht : Disjoint t (s₁ ∪ s₂)
⊢ ∏ b ∈ t, f b ∈ e

Tactic:
simpa using

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
h✝ : ∀ s ∈ 𝓝 1, ∃ a, ∀ (b : Finset β × Finset β), a ≤ b → (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ s
e : Set α
he : e ∈ 𝓝 1
s₁ s₂ t : Finset β
h : (∏ b ∈ (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t).2, f b) / ∏ b ∈ (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t).1, f b ∈ e
ht : Disjoint t (s₁ ∪ s₂)
⊢ ∏ b ∈ t, f b ∈ e
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case neg
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : ¬L.NeBot
⊢ g (∏'[L] (i : ι), f i) = ∏'[L] (i : ι), g (f i)

Tactic:
simpa using

Goal state after:
case neg
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : ¬L.NeBot
⊢ g (∏ᶠ (i : ι), f i) = ∏ᶠ (i : ι), g (f i)
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:
simpa using

Goal state after:
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)
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: case pos
ι : 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₂
hL : ¬L.NeBot
hf : (mulSupport f).Finite
⊢ ∏'[L] (i : ι), f i ≤ a₂

Tactic:
simpa using

Goal state after:
case pos
ι : 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₂
hL : ¬L.NeBot
hf : (mulSupport f).Finite
⊢ ∏ i ∈ hf.toFinset, f i ≤ a₂
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
this : Injective fun x ↦ 2 * x
ho : HasProd (fun x ↦ f ↑x) m'
⊢ IsCompl (Set.range fun x ↦ 2 * x) (Set.range ((fun x ↦ x + 1) ∘ fun x ↦ 2 * x))

Tactic:
simpa using

Goal state after:
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
this : Injective fun x ↦ 2 * x
ho : HasProd (fun x ↦ f ↑x) m'
⊢ IsCompl {a | Even a} {a | Odd a}
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

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

Tactic:
simpa using

Goal state after:
case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
hg : Multipliable g L
hL : ¬L.NeBot
⊢ 1 ≤ ∏ᶠ (i : ι), g i
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

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

Tactic:
simpa using

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