mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ l (v x)
hv_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
c : γ
hc : ∀ᶠ (a : α) in f, l (v a) ≤ c
⊢ l (limsup v f) ≤ c

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ l (v x)
hv_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
c : γ
hc : ∀ᶠ (a : α) in f, l (v a) ≤ c
⊢ l (limsup v f) ≤ c
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:
by simpa using mulSupport_subset_iff'.1 hf

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
hgu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
hf : u = fun i ↦ g.symm (g (u i))
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g.symm (g (u x))

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_6
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
hgu : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
hgu_co : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g (u x)
hf : u = fun i ↦ g.symm (g (u i))
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ g.symm (g (u x))
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 γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
a : α
⊢ HasProd (⇑g ∘ f) (g a) L ↔ HasProd f a L

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : TopologicalSpace α
L : SummationFilter β
inst✝³ : CommMonoid γ
inst✝² : TopologicalSpace γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
a : α
⊢ HasProd (⇑g ∘ f) (g a) L ↔ HasProd f a 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 : Set β), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e

Tactic:
[

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

Goal state before:
pp: case h
α : 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 : β → α
hgf : Multipliable (⇑g ∘ f) L
a : α
ha : g a = ∏'[L] (i : β), g (f i)
this : HasProd (⇑g ∘ f) (∏'[L] (b : β), (⇑g ∘ f) b) L
⊢ HasProd f a L

Tactic:
[

Goal state after:
case h
α : 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 : β → α
hgf : Multipliable (⇑g ∘ f) L
a : α
ha : g a = ∏'[L] (i : β), g (f i)
this : HasProd (⇑g ∘ f) (∏'[L] (b : β), (⇑g ∘ f) b) L
⊢ HasProd f a L
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 : Tendsto (fun s ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
hg : Tendsto (fun s ↦ ∏ b ∈ s, g b) L.filter (𝓝 b)
⊢ Tendsto (fun s ↦ ∏ b ∈ s, f b * g b) L.filter (𝓝 (a * b))

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f g : β → α
a b : α
L : SummationFilter β
inst✝ : ContinuousMul α
hf : Tendsto (fun s ↦ ∏ b ∈ s, f b) L.filter (𝓝 a)
hg : Tendsto (fun s ↦ ∏ b ∈ s, g b) L.filter (𝓝 b)
⊢ Tendsto (fun s ↦ ∏ b ∈ s, f b * g b) L.filter (𝓝 (a * b))
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: case pos
α : 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
⊢ ∀ ⦃a : β⦄, a ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ t) t' → a ∉ s

Tactic:
[

Goal state after:
case pos
α : 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
⊢ ∀ ⦃a : β⦄, a ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ t) t' → a ∉ s
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:
[

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

Goal state before:
pp: β : Type u_2
L : SummationFilter β
inst✝⁶ : L.LeAtTop
inst✝⁵ : L.NeBot
α : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a L
b : β
x : α
hf' : HasProd (update f b x) a' L
this : ∀ (b' : β), (f b' * if b' = b then x else 1) = update f b x b' * if b' = b then f b else 1
h : HasProd (fun b_1 ↦ f b_1 * if b_1 = b then x else 1) (a * x) L
⊢ a * x = a' * f b

Tactic:
[

Goal state after:
β : Type u_2
L : SummationFilter β
inst✝⁶ : L.LeAtTop
inst✝⁵ : L.NeBot
α : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a L
b : β
x : α
hf' : HasProd (update f b x) a' L
this : ∀ (b' : β), (f b' * if b' = b then x else 1) = update f b x b' * if b' = b then f b else 1
h : HasProd (fun b_1 ↦ f b_1 * if b_1 = b then x else 1) (a * x) L
⊢ a * x = a' * f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: β : Type u_2
L : SummationFilter β
inst✝⁶ : L.LeAtTop
inst✝⁵ : L.NeBot
α : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a L
b : β
x : α
hf' : HasProd (update f b x) a' L
this : ∀ (b' : β), (f b' * if b' = b then x else 1) = update f b x b' * if b' = b then f b else 1
h : HasProd (fun b_1 ↦ f b_1 * if b_1 = b then x else 1) (a * x) L
⊢ a * x = a' * f b

Tactic:
this

Goal state after:
β : Type u_2
L : SummationFilter β
inst✝⁶ : L.LeAtTop
inst✝⁵ : L.NeBot
α : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a L
b : β
x : α
hf' : HasProd (update f b x) a' L
this : ∀ (b' : β), (f b' * if b' = b then x else 1) = update f b x b' * if b' = b then f b else 1
h : HasProd (fun b_1 ↦ update f b x b_1 * if b_1 = b then f b else 1) (a * x) L
⊢ a * x = a' * f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

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

Tactic:
by simpa using hb'

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

Goal state before:
pp: α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f : α → K
L : SummationFilter α
a : K
inst✝ : ContinuousInv₀ K
h : HasProd f a L
ha : a ≠ 0
⊢ HasProd (fun x ↦ (f x)⁻¹) a⁻¹ L

Tactic:
[

Goal state after:
α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f : α → K
L : SummationFilter α
a : K
inst✝ : ContinuousInv₀ K
h : HasProd f a L
ha : a ≠ 0
⊢ HasProd (fun x ↦ (f x)⁻¹) a⁻¹ L
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
hf_fin : (mulSupport f).Finite
g : γ ↪ β
hf : mulSupport f ⊆ Set.range ⇑g
this : mulSupport f = ⇑g '' mulSupport (f ∘ ⇑g)
hfg_fin : (mulSupport (f ∘ ⇑g)).Finite
⊢ tprod (f ∘ ⇑g) = ∏' (b : β), f b

Tactic:
[

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
hf_fin : (mulSupport f).Finite
g : γ ↪ β
hf : mulSupport f ⊆ Set.range ⇑g
this : mulSupport f = ⇑g '' mulSupport (f ∘ ⇑g)
hfg_fin : (mulSupport (f ∘ ⇑g)).Finite
⊢ tprod (f ∘ ⇑g) = ∏' (b : β), f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : ¬(mulSupport f).Finite
hf_fin' : ¬(mulSupport (f ∘ g)).Finite
⊢ tprod (f ∘ g) = ∏' (b : β), f b

Tactic:
[

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : ¬(mulSupport f).Finite
hf_fin' : ¬(mulSupport (f ∘ g)).Finite
⊢ tprod (f ∘ g) = ∏' (b : β), f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
f : β → α
hg : Injective g
⊢ ∏' (x : ↑Set.univ), f (g ↑x) = ∏' (x : γ), f (g x)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
f : β → α
hg : Injective g
⊢ ∏' (x : ↑Set.univ), f (g ↑x) = ∏' (x : γ), f (g x)
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f x.1 * g x.2
⊢ Summable fun n ↦ ∑ k ∈ range (n + 1), f k * g (n - k)

Tactic:
[

Goal state after:
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f x.1 * g x.2
⊢ Summable fun n ↦ ∑ k ∈ range (n + 1), f k * g (n - k)
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ range (n + 1), f k * g (n - k)

Tactic:
[

Goal state after:
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ range (n + 1), f k * g (n - k)
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
γ : Type u_4
g : γ → β
hg : Injective g
f : γ → α
this : mulSupport (extend g f 1) ⊆ Set.range g
⊢ ∏' (y : β), extend g f 1 y = ∏' (x : γ), f x

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
γ : Type u_4
g : γ → β
hg : Injective g
f : γ → α
this : mulSupport (extend g f 1) ⊆ Set.range g
⊢ ∏' (y : β), extend g f 1 y = ∏' (x : γ), f x
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: G : Type u_2
inst✝⁴ : CommGroup G
inst✝³ : UniformSpace G
inst✝² : IsUniformGroup G
inst✝¹ : CompleteSpace G
inst✝ : T2Space G
f : ℤ → G
hf2 : Multipliable f
h1 : Multipliable fun n ↦ f ↑n
h2 : Multipliable fun n ↦ f (-↑n)
⊢ Multipliable fun n ↦ f ↑↑n

Tactic:
rwa [multipliable_pnat_iff_multipliable_succ (f := (f ·)),
      multipliable_nat_add_iff 1 (f := (f ·))]

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : TopologicalSpace α
f : ι → α
a : α
h : HasSum (fun x ↦ ∏ i ∈ x, f i) a
⊢ HasProd (fun x ↦ 1 + f x) a

Tactic:
[

Goal state after:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : TopologicalSpace α
f : ι → α
a : α
h : HasSum (fun x ↦ ∏ i ∈ x, f i) a
⊢ HasProd (fun x ↦ 1 + f x) a
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
α : Type u_4
f : ι → α
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : IsTopologicalAddGroup α
hsum : Summable fun i ↦ f i * ∏ j < i, (1 - f j)
hprod : Multipliable fun x ↦ 1 - f x
⊢ ∏' (i : ι), (1 - f i) = 1 - ∑' (i : ι), f i * ∏ j < i, (1 - f j)

Tactic:
[

Goal state after:
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
α : Type u_4
f : ι → α
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : IsTopologicalAddGroup α
hsum : Summable fun i ↦ f i * ∏ j < i, (1 - f j)
hprod : Multipliable fun x ↦ 1 - f x
⊢ ∏' (i : ι), (1 - f i) = 1 - ∑' (i : ι), f i * ∏ j < i, (1 - f j)
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
α : Type u_4
f : ι → α
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : IsTopologicalAddGroup α
hsum : Summable fun i ↦ f i * ∏ x < i, (1 + -f x)
hprod : Multipliable fun x ↦ 1 + -f x
hsum' : Summable fun b ↦ -(f b * ∏ x < b, (1 + -f x))
⊢ ∏' (i : ι), (1 + -f i) = 1 + -∑' (i : ι), f i * ∏ i < i, (1 + -f i)

Tactic:
[

Goal state after:
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
α : Type u_4
f : ι → α
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : IsTopologicalAddGroup α
hsum : Summable fun i ↦ f i * ∏ x < i, (1 + -f x)
hprod : Multipliable fun x ↦ 1 + -f x
hsum' : Summable fun b ↦ -(f b * ∏ x < b, (1 + -f x))
⊢ ∏' (i : ι), (1 + -f i) = 1 + -∑' (i : ι), f i * ∏ i < i, (1 + -f i)
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
α : Type u_4
f : ι → α
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : IsTopologicalAddGroup α
hsum : Summable fun i ↦ f i * ∏ x < i, (1 + -f x)
hprod : Multipliable fun x ↦ 1 + -f x
hsum' : Summable fun b ↦ -f b * ∏ x < b, (1 + -f x)
⊢ ∏' (i : ι), (1 + -f i) = 1 + -∑' (i : ι), f i * ∏ i < i, (1 + -f i)

Tactic:
[

Goal state after:
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
α : Type u_4
f : ι → α
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : IsTopologicalAddGroup α
hsum : Summable fun i ↦ f i * ∏ x < i, (1 + -f x)
hprod : Multipliable fun x ↦ 1 + -f x
hsum' : Summable fun b ↦ -f b * ∏ x < b, (1 + -f x)
⊢ ∏' (i : ι), (1 + -f i) = 1 + -∑' (i : ι), f i * ∏ i < i, (1 + -f i)
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: α : Type u_3
f : α → ℝ≥0
⊢ Tendsto (fun s ↦ ∑' (b : { x // x ∉ s }), f ↑b) atTop (𝓝 0)

Tactic:
[

Goal state after:
α : Type u_3
f : α → ℝ≥0
⊢ Tendsto (fun s ↦ ∑' (b : { x // x ∉ s }), f ↑b) atTop (𝓝 0)
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u
β : Type v
γ : Type w
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
ι' : Type u_3
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
Y : ι → Type u_4
inst✝ : (j : ι) → PseudoEMetricSpace (Y j)
e : ι ≃ ι'
x1 x2 : (i : ι) → Y i
⊢ edist ((Equiv.piCongrLeft' Y e).toFun x1) ((Equiv.piCongrLeft' Y e).toFun x2) = edist x1 x2

Tactic:
[

Goal state after:
F : Type u_1
ι : Type u_2
α : Type u
β : Type v
γ : Type w
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
ι' : Type u_3
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
Y : ι → Type u_4
inst✝ : (j : ι) → PseudoEMetricSpace (Y j)
e : ι ≃ ι'
x1 x2 : (i : ι) → Y i
⊢ edist ((Equiv.piCongrLeft' Y e).toFun x1) ((Equiv.piCongrLeft' Y e).toFun x2) = edist x1 x2
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
m n : ℕ
x✝¹ x✝ : (Fin m → α) × (Fin n → α)
⊢ edist ((Fin.appendEquiv m n).toFun x✝¹) ((Fin.appendEquiv m n).toFun x✝) = edist x✝¹ x✝

Tactic:
[

Goal state after:
F : Type u_1
ι : Type u_2
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
m n : ℕ
x✝¹ x✝ : (Fin m → α) × (Fin n → α)
⊢ edist ((Fin.appendEquiv m n).toFun x✝¹) ((Fin.appendEquiv m n).toFun x✝) = edist x✝¹ x✝
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
m n : ℕ
x✝¹ x✝ : (Fin m → α) × (Fin n → α)
⊢ edist ((Fin.appendEquiv m n).toFun x✝¹) ((Fin.appendEquiv m n).toFun x✝) = edist x✝¹ x✝

Tactic:
by simp_rw [Fin.appendEquiv, Fin.edist_append_eq_max_edist, Prod.edist_eq]

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case inl
xt : 0 ≠ ∞
⊢ (𝓝 0).HasBasis (fun x ↦ x ≠ 0) fun ε ↦ Icc (0 - ε) (0 + ε)

Tactic:
[

Goal state after:
case inl
xt : 0 ≠ ∞
⊢ (𝓝 0).HasBasis (fun x ↦ x ≠ 0) fun ε ↦ Icc (0 - ε) (0 + ε)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case inr.refine_1.refine_1
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + ↑δ < (a, b).2
⊢ (a, b).1 < x - min ε ↑δ

Tactic:
exact lt_tsub_comm.2 ((min_le_left _ _).trans_lt hε)

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
⊢ {x | ‖x⁻¹ * a‖ < b 0} ∈ 𝓝 a

Tactic:
[

Goal state after:
E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
⊢ {x | ‖x⁻¹ * a‖ < b 0} ∈ 𝓝 a
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝¹ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
a : α
⊢ pkg.extend (pkg'.coe ∘ f) (pkg.coe a) = g (pkg.coe a)

Tactic:
[

Goal state after:
α : Type uα
inst✝¹ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
a : α
⊢ pkg.extend (pkg'.coe ∘ f) (pkg.coe a) = g (pkg.coe a)
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: case hh
α : Type u
inst✝ : UniformSpace α
⊢ Monotone fun s ↦ s ○ s

Tactic:
exact monotone_id.relComp monotone_id

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: case hg
α : Type u
inst✝ : UniformSpace α
⊢ Monotone fun s ↦ s ○ s

Tactic:
exact monotone_id.relComp monotone_id

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case succ
n : ℕ
IH : Continuous fun a ↦ a ^ n
⊢ Continuous fun a ↦ a ^ (n + 1)

Tactic:
[

Goal state after:
case succ
n : ℕ
IH : Continuous fun a ↦ a ^ n
⊢ Continuous fun a ↦ a ^ (n + 1)
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: case refine_2
α : Type u
inst✝ : UniformSpace α
f : CauchyFilter α
h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y, (f, pureCauchy y) ∈ s
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ 𝓤 (CauchyFilter α)
⊢ (range pureCauchy ∩ UniformSpace.ball f s).Nonempty

Tactic:
let ⟨y, hy⟩ := h_ex s hs
    have : pureCauchy y ∈ range pureCauchy ∩ { y : CauchyFilter α | (f, y) ∈ s } :=
      ⟨mem_range_self y, hy⟩
    exact ⟨_, this⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: E : Type u_7
inst✝ : NormedCommGroup E
a : E
⊢ Tendsto (fun x ↦ ‖x / a‖) (𝓝[≠] a) (𝓝[>] 0)

Tactic:
[

Goal state after:
E : Type u_7
inst✝ : NormedCommGroup E
a : E
⊢ Tendsto (fun x ↦ ‖x / a‖) (𝓝[≠] a) (𝓝[>] 0)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
⊢ (∃ b, (∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)) →
    ∀ ε > 0, ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε

Tactic:
rintro ⟨b, ⟨b_bound, b_lim⟩⟩ ε εpos

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
b : β → ℝ≥0∞
b_bound : ∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (s m) (s n) < ε