mathlib-initiative/mathlib-tactics huggingface dataset:
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))
⊢ g.symm (limsup (fun x ↦ g (u x)) f) ≤ limsup u f

Tactic:
hf

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))
⊢ g.symm (limsup (fun x ↦ g (u x)) f) ≤ limsup (fun i ↦ g.symm (g (u i))) f
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case e'_2.e'_6
x : EReal
n : ℕ
ih : n • x = ↑n * x
⊢ x = 1 * x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case succ.convert_4
x : EReal
n : ℕ
ih : n • x = ↑n * x
⊢ 0 ≤ ↑n

Tactic:
simp

Goal state after:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case succ.convert_5
x : EReal
n : ℕ
ih : n • x = ↑n * x
⊢ 0 ≤ 1

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.BigOperators

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset β
t : Finset α
ht : s.preimage g ⋯ ⊆ t
⊢ ∃ u', s ⊆ u' ∧ ∏ x ∈ u', f x = ∏ b ∈ t, f (g b)

Tactic:
refine ⟨t.image g ∪ s, Finset.subset_union_right, ?_⟩

Goal state after:
case a
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset β
t : Finset α
ht : s.preimage g ⋯ ⊆ t
⊢ ∏ x ∈ image g t ∪ s, f x = ∏ b ∈ t, f (g b)
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
bddmax : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
b : β
hb : b > max (limsup u f) (limsup v f)
hu : ∀ᶠ (a : α) in f, u a < b
hv : ∀ᶠ (a : α) in f, v a < b
x✝ : α
⊢ x✝ ∈ {x | (fun a ↦ u a < b) x} ∩ {x | (fun a ↦ v a < b) x} → x✝ ∈ {x | (fun a ↦ max (u a) (v a) < b) x}

Tactic:
simp

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h✝ : f.NeBot
s_nemp : s.Nonempty
⊢ limsup (fun a ↦ s.sup fun i ↦ F i a) f = s.sup fun i ↦ limsup (F i) f

Tactic:
← Finset.sup'_eq_sup s_nemp fun i ↦ limsup (F i) f,

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (F i)
h✝ : f.NeBot
s_nemp : s.Nonempty
⊢ limsup (fun a ↦ s.sup fun i ↦ F i a) f = s.sup' s_nemp fun i ↦ limsup (F i) f
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite
⊢ ↑⋯.toFinset ⊆ L.support

Tactic:
simp

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

Goal state before:
pp: case e'_6.h
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite
⊢ mulSupport (L.support.mulIndicator fun b ↦ f b) ⊆ ↑⋯.toFinset

Tactic:
simp

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
a₁ : α
inst✝¹ : L.LeAtTop
hf : HasProd f a₁ L
b : β
inst✝ : DecidableEq β
a : α
b' : β
h : b' = b
⊢ a = (if b = b then a / f b else 1) * f b

Tactic:
simp

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 : α
s : Set β
⊢ HasProd (f ∘ Subtype.val) a ↔ HasProd (s.mulIndicator f) a

Tactic:
rw [← Set.mulIndicator_range_comp, Subtype.range_coe,
    hasProd_subtype_iff_of_mulSupport_subset Set.mulSupport_mulIndicator_subset]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f g : β → α
hf : Multipliable f
hfg : f =ᶠ[cofinite] g
⊢ ∀ (b : ↑{x | (fun x ↦ f x = g x) x}ᶜᶜ), (f ∘ Subtype.val) b = (g ∘ Subtype.val) b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
L : SummationFilter β
inst✝ : L.HasSupport
h : HasFiniteMulSupport f
⊢ ∀ b ∉ Set.Finite.toFinset h, f b = 1

Tactic:
simp

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 α
f : β → α
a : α
e : γ ≃ β
⊢ ∀ x ∉ Set.range ⇑e, f x = 1

Tactic:
simp

Goal state after:
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 [tprod_bot hL] using
      (MonoidHomClass.toMonoidHom g).map_finprod_of_injective hge.injective _

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

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

Tactic:
simp

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:
simp

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

Goal state before:
pp: case neg
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
f : ℕ → G
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
e : Set G
he : e ∈ 𝓝 1
s : Finset ℕ
hs : ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
t : Set ℕ
h : ¬s.Nonempty
ht : t ⊆ {n | 0 ≤ n}
⊢ ∀ ⦃a : ℕ⦄, a ∈ t → a ∉ ↑s

Tactic:
exact fun _ _ hs ↦ h ⟨_, hs⟩

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

Goal state before:
pp: case inr.inl
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
hβ : Infinite β
⊢ ∏' (x : β), 1 = 1

Tactic:
simp

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

Goal state before:
pp: case inr.inr
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Infinite β
ha : a ≠ 1
⊢ ∏' (x : β), a = 1

Tactic:
apply tprod_eq_one_of_not_multipliable

Goal state after:
case inr.inr
β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
hβ : Infinite β
ha : a ≠ 1
⊢ ¬Multipliable fun b ↦ a
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
inst✝ : Fintype β
f : β → α
⊢ ∀ b ∉ univ, f b = 1

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
b : β
inst✝¹ : DecidablePred fun x ↦ x = b
a : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
⊢ (if b = b then a b else 1) = a b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
b : β
inst✝¹ : DecidablePred fun x ↦ b = x
a : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
⊢ (if b = b then a b else 1) = a b

Tactic:
simp

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
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
u : Finset ℤ
v' : Finset ℕ
hv' : u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯ ⊆ v'
a✝ : ℕ
hx : Int.negSucc a✝ ∈ u
⊢ a✝ ∈ u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯

Tactic:
simpa using Or.inr hx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
b : β
f : β → α
⊢ ∏' (x : ↑{b}), f ↑x = f b

Tactic:
simp

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 g : α → K
inst✝ : SeparatelyContinuousMul K
hf' : ∀ (a : α), f a ≠ 0
hfg : ∀ᶠ (a : α) in cofinite, f a = g a
c : K
hc : HasProd f c
⊢ ∀ i ∉ Set.Finite.toFinset hfg, f i = g i

Tactic:
simp

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

Goal state before:
pp: case codisjoint.ofNat
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n ↦ f ↑n) m
hf₂ : HasProd (fun n ↦ f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
i : ℕ
⊢ Int.ofNat i ∈ ⊤ → Int.ofNat i ∈ Set.range Nat.cast ⊔ Set.range Int.negSucc

Tactic:
simp

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

Goal state before:
pp: case codisjoint.negSucc
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n ↦ f ↑n) m
hf₂ : HasProd (fun n ↦ f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
j : ℕ
⊢ Int.negSucc j ∈ ⊤ → Int.negSucc j ∈ Set.range Nat.cast ⊔ Set.range Int.negSucc

Tactic:
simp

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 α
e : γ ≃ β
f : β → α
⊢ mulSupport f ⊆ Set.range ⇑e

Tactic:
simp

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

Goal state before:
pp: case e_a.refine_1
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x ↦ ↑x) v'
u2 : Finset ℤ := image (fun x ↦ -↑x) v'
A : u ⊆ u1 ∪ u2
⊢ ∀ x ∈ (u1 ∪ u2) \ (u1 ∩ u2), (if x = 0 then f 0 else 1) = 1

pp: case e_a.refine_2
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x ↦ ↑x) v'
u2 : Finset ℤ := image (fun x ↦ -↑x) v'
A : u ⊆ u1 ∪ u2
⊢ ∀ x ∈ u1 ∩ u2, f x = if x = 0 then f 0 else 1

Tactic:
· intro x hx
        suffices x ≠ 0 by simp only [this, if_false]
        rintro rfl
        simp [u1, u2] at hx

Goal state after:
case e_a.refine_2
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x ↦ ↑x) v'
u2 : Finset ℤ := image (fun x ↦ -↑x) v'
A : u ⊆ u1 ∪ u2
⊢ ∀ x ∈ u1 ∩ u2, f x = if x = 0 then f 0 else 1
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
f : β → α
⊢ ∀ (b : ↑s), f ↑b = s.mulIndicator f ↑b

Tactic:
simp

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 α
g : γ → β
f : β → α
hg : Injective g
⊢ ∏' (x : ↑(g '' Set.univ)), f ↑x = ∏' (x : γ), f (g x)

Tactic:
tprod_image f hg.injOn

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.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
g : γ → α
e : ↑(mulSupport f) ≃ ↑(mulSupport g)
he : ∀ (x : ↑(mulSupport f)), g ↑(e x) = f ↑x
⊢ mulSupport g ⊆ Set.range (Subtype.val ∘ ⇑e)

Tactic:
simp

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

Goal state before:
pp: α : Type u_3
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : IsUniformAddGroup α
inst✝ : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Summable fun n ↦ (-1) ^ n * f n

Tactic:
by
  apply Summable.even_add_odd
  · simp only [even_two, Even.mul_right, Even.neg_pow, one_pow, one_mul]
    exact hf.comp_injective (mul_right_injective₀ (two_ne_zero' ℕ))
  · simp only [pow_add, even_two, Even.mul_right, Even.neg_pow, one_pow, pow_one, mul_neg, mul_one,
      neg_mul, one_mul]
    apply Summable.neg
    apply hf.comp_injective
    exact (add_left_injective 1).comp (mul_right_injective₀ (two_ne_zero' ℕ))

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

Goal state before:
pp: case inl
ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
hsum : Summable fun i ↦ f i * ∏ j < i, (1 + f j)
hprod : Multipliable fun x ↦ 1 + f x
h✝ : IsEmpty ι
⊢ ∏' (i : ι), (1 + f i) = 1 + ∑' (i : ι), f i * ∏ j < i, (1 + f j)

Tactic:
simp

Goal state after:
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)
h3 : Multipliable fun n ↦ f ↑↑n
h4 : Multipliable fun n ↦ f (-↑↑n)
this : ∏' (n : ℕ), f ↑n * f (-↑n) = (∏' (n : ℤ), f n) * f 0
⊢ Multipliable ?m.133

Tactic:
by simpa using h1.mul h2

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 α
inst✝² : T2Space α
α' : Type u_4
inst✝¹ : CommMonoid α'
inst✝ : TopologicalSpace α'
e : α' → α
hes : Surjective e
h1 : e 1 = 1
f : β → α
g : γ → α'
h : ∀ {a : α'}, HasProd f (e a) ↔ HasProd g a
hg : ¬Multipliable g
hf : ¬Multipliable f
⊢ ∏' (b : β), f b = e (∏' (c : γ), g c)

Tactic:
simp [tprod_def, hf, hg, h1]

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

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
inst✝⁴ : CommMonoid α
inst✝³ : TopologicalSpace α
f : β → α
L : SummationFilter β
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : L.NeBot
hf : Multipliable f L
⊢ ∏'[L] (b : β), f b ^ 0 = (∏'[L] (b : β), f b) ^ 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoidWithZero α
inst✝² : TopologicalSpace α
L : SummationFilter β
inst✝¹ : Nonempty β
inst✝ : L.LeAtTop
b : β
⊢ 0 = 0

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
inst✝ : L.LeAtTop
hβ : IsEmpty β
⊢ Multipliable (fun x ↦ 0) L

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
x : ℝ≥0
⊢ (toRealHom x).toNNReal = x

Tactic:
simp

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

Goal state before:
pp: f : ℕ → ℝ≥0
h_ant : Antitone f
⊢ BddBelow (range f)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
f : α → β
inst✝ : Subsingleton α
x y : α
⊢ edist (f y) (f y) = edist y y

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → PseudoEMetricSpace (E i)
inst✝ : (i : ι) → Zero (E i)
i : ι
x y : E i
⊢ edist x y ≤ edist (Pi.single i x i) (Pi.single i y i)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: case inl
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → PseudoEMetricSpace (E i)
inst✝ : (i : ι) → Zero (E i)
i : ι
x y : E i
⊢ i ∈ Finset.univ → edist (Pi.single i x i) (Pi.single i y i) ≤ edist x y

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : AddZeroClass α
inst✝ : AddZeroClass β
x y : α
⊢ max (edist ((AddMonoidHom.inl α β) x).1 ((AddMonoidHom.inl α β) y).1)
      (edist ((AddMonoidHom.inl α β) x).2 ((AddMonoidHom.inl α β) y).2) =
    edist x y

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : AddZeroClass α
inst✝ : AddZeroClass β
x y : β
⊢ max (edist ((AddMonoidHom.inr α β) x).1 ((AddMonoidHom.inr α β) y).1)
      (edist ((AddMonoidHom.inr α β) x).2 ((AddMonoidHom.inr α β) y).2) =
    edist x y

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
x y : X
⊢ (zipWith d [x] ([] ++ [y])).sum = d x y

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ range ⇑h = univ

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
⊢ ↑(d x y) ≤ 2 * ↑(⨅ l, (zipWith d (x :: l) (l ++ [y])).sum)

Tactic:
← NNReal.coe_two,

Goal state after:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
⊢ ↑(d x y) ≤ ↑2 * ↑(⨅ l, (zipWith d (x :: l) (l ++ [y])).sum)
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst✝¹] {x m}
j a : ℕ
⊢ (Iic a).Finite

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : SequentialSpace X
h₂ : SequentialSpace X
⊢ SequentialSpace X

Tactic:
rw [sup_eq_iSup]
  exact .iSup <| Bool.forall_bool.2 ⟨h₂, h₁⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DecidableEq β
b : β
a : α
⊢ Pi.mulSingle b a b = a

Tactic:
simp

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

Goal state before:
pp: case e'_3
α : Type u_4
β : Type u_5
M : Type u_6
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
s : Finset α × Finset β
⊢ ((fun x ↦ ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm) s =
    ((fun p ↦ p.1 * p.2) ∘ Prod.map (fun s ↦ ∏ b ∈ s, (f ∘ Sum.inl) b) fun s ↦ ∏ b ∈ s, (f ∘ Sum.inr) b) s

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0
l : Filter α
⊢ (∀ (x : ℝ≥0), ∀ᶠ (a : α) in l, ↑x < ↑(f a)) ↔ ∀ (i : ℝ≥0), True → ∀ᶠ (x : α) in l, f x ∈ Ioi i

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝ : SeminormedGroup E
f : α → E
a : Filter α
⊢ Tendsto (fun e ↦ ‖(f e)⁻¹ * 1‖) a (𝓝 0) ↔ Tendsto (fun x ↦ ‖f x‖) a (𝓝 0)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝ : SeminormedGroup E
f : α → E
a : Filter α
⊢ Tendsto (fun e ↦ ‖(f e)⁻¹ * 1‖ₑ) a (𝓝 0) ↔ Tendsto (fun x ↦ ‖f x‖ₑ) a (𝓝 0)

Tactic:
simp

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

Goal state before:
pp: E : Type u_4
inst✝ : SeminormedGroup E
x : E
⊢ ∀ᶠ (n : E) in 𝓝 x, ‖n⁻¹ * x‖ ∈ Set.Ici 0

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
m : ℕ
hm : Forall (fun x ↦ x = 0) L
hLm : L.length ≤ m
⊢ (x :: l).length = (l ++ [y]).length

Tactic:
simp

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

Goal state before:
pp: E : Type u_4
inst✝ : SeminormedCommGroup E
x : E
⊢ ∀ᶠ (n : E) in 𝓝 x, ‖n / x‖ ∈ Set.Ici 0

Tactic:
simp

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)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
n : ℕ
⊢ {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E

Tactic:
by
    simpa [← dist_eq_norm_inv_mul] using Metric.dist_mem_uniformity (b_pos <| n + 1)

Goal state after: