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

Goal state before:
pp: R : Type u_1
𝕜 : Type u_2
inst✝⁵ : NonUnitalNonAssocRing R
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : (𝓝 0).HasBasis (fun x ↦ 0 < x) fun ε ↦ {x | norm x < ε}
⊢ IsTopologicalRing R

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
⊢ (𝓝 0).HasBasis (fun x ↦ 0 < x) fun ε ↦ {x | |x| < ε}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a u' : α
s : Set α
hu' : a < u'
⊢ [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a u'] a, s ∈ 𝓝[Ico a u'] a, ∃ u ∈ Ioc a u', Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s][0]? =
    some (s ∈ 𝓝[≥] a)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x ↦ f x * g x) l atBot

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
⊢ Tendsto (fun x ↦ f x * g x) l atBot

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a u' : α
s : Set α
hu' : a < u'
⊢ [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a u'] a, s ∈ 𝓝[Ico a u'] a, ∃ u ∈ Ioc a u', Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s][3]? =
    some (∃ u ∈ Ioc a u', Ico a u ⊆ s)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x ↦ f x * g x) l atBot

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x ↦ f x * g x) l atTop

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atBot
⊢ Tendsto (fun x ↦ f x * g x) l atBot

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atBot
⊢ Tendsto (fun x ↦ f x * g x) l atTop

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a u' : α
s : Set α
hu' : a < u'
⊢ [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a u'] a, s ∈ 𝓝[Ico a u'] a, ∃ u ∈ Ioc a u', Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s][4]? =
    some (∃ u ∈ Ioi a, Ico a u ⊆ s)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
⊢ ∀ (i : 𝕜), i < 0 ↔ ((fun x ↦ x < 0) ∘ Inv.inv) i

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
a : 𝕜
ha : a < 0
⊢ Ioo a 0 = ((fun i ↦ Inv.inv '' Iio i) ∘ Inv.inv) a

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
⊢ (𝓝[<] 0)⁻¹ = atBot

Tactic:
by

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

Goal state before:
pp: G : Type u
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : FirstCountableTopology G
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : CompleteSpace G
⊢ CompleteSpace (G ⧸ N)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
h : a < b
s : Set α
⊢ [s ∈ 𝓝[≤] b, s ∈ 𝓝[Icc a b] b, s ∈ 𝓝[Ioc a b] b, ∃ l ∈ Ico a b, Ioc l b ⊆ s, ∃ l ∈ Iio b, Ioc l b ⊆ s].TFAE

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsRightUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
⊢ IsTopologicalGroup.rightUniformSpace G = us

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
h : Tendsto (fun x ↦ f x⁻¹) atBot l
⊢ Tendsto f (𝓝[<] 0) l

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a l' : α
s : Set α
hl' : l' < a
⊢ [s ∈ 𝓝[≤] a, s ∈ 𝓝[Icc l' a] a, s ∈ 𝓝[Ioc l' a] a, ∃ l ∈ Ico l' a, Ioc l a ⊆ s, ∃ l ∈ Iio a, Ioc l a ⊆ s][0]? =
    some (s ∈ 𝓝[≤] a)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsRightUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
⊢ CompleteSpace (G ⧸ N)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atTop
⊢ Tendsto (fun x ↦ f x / g x) l (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a l' : α
s : Set α
hl' : l' < a
⊢ [s ∈ 𝓝[≤] a, s ∈ 𝓝[Icc l' a] a, s ∈ 𝓝[Ioc l' a] a, ∃ l ∈ Ico l' a, Ioc l a ⊆ s, ∃ l ∈ Iio a, Ioc l a ⊆ s][3]? =
    some (∃ l ∈ Ico l' a, Ioc l a ⊆ s)

Tactic:
by

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

Goal state before:
pp: G : Type u
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
⊢ CompleteSpace (G ⧸ N)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atBot
⊢ Tendsto (fun x ↦ f x / g x) l (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a l' : α
s : Set α
hl' : l' < a
⊢ [s ∈ 𝓝[≤] a, s ∈ 𝓝[Icc l' a] a, s ∈ 𝓝[Ioc l' a] a, ∃ l ∈ Ico l' a, Ioc l a ⊆ s, ∃ l ∈ Iio a, Ioc l a ⊆ s][4]? =
    some (∃ l ∈ Iio a, Ioc l a ⊆ s)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsLeftUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
⊢ IsTopologicalGroup.leftUniformSpace G = us

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMinOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ (∃ u, toDual a < toDual u ∧ Icc (toDual a) (toDual u) ⊆ ⇑ofDual ⁻¹' s) ↔ ∃ l < a, Icc l a ⊆ s

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsLeftUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
⊢ CompleteSpace (G ⧸ N)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
⊢ Tendsto (fun x ↦ |C * g x|) l (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
a : α
⊢ 𝓝 a = ⨅ r, ⨅ (_ : r > 1), 𝓟 {b | |a / b|ₘ < r}

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
x : α
y : β
hx : x ∈ e.source
hy : y ∈ e.target
h : ↑e.symm y = x
⊢ y = ↑e x

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
x : α
y : β
hx : x ∈ e.source
hy : y ∈ e.target
h : y = ↑e x
⊢ ↑e.symm y = x

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
x : α
y : β
hx : x ∈ e.source
hy : y ∈ e.target
⊢ x = ↑e.symm y ↔ ↑e x = y

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : PartialEquiv α β
e' : PartialEquiv β γ
e : α ≃ β
s : Set α
t : Set β
h : ⇑e '' s = t
x : β
hx : x ∈ t
⊢ e.symm x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e✝ : PartialEquiv α β
e' : PartialEquiv β γ
e : α ≃ β
⊢ ⇑e '' univ = univ

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
f : α → β
hf : ↑e = f
g : β → α
hg : ↑e.symm = g
s : Set α
hs : e.source = s
t : Set β
ht : e.target = t
⊢ e.copy f hf g hg s hs t ht = e

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ ∀ (x : ↑e.source), e.source.domRestrict (↑e) x ∈ e.target

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ ∀ (x : ↑e.target), e.target.domRestrict e.invFun x ∈ e.source

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ ⇑e.toEquiv.symm = codRestrict (e.target.domRestrict e.invFun) e.source ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
p : β → Prop
⊢ (∀ (y : β), y ∈ e.target → p y) ↔ ∀ (x : α), x ∈ e.source → p (↑e x)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
p : β → Prop
⊢ (∃ y, y ∈ e.target ∧ p y) ↔ ∃ x, x ∈ e.source ∧ p (↑e x)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
h : e.IsImage s t
x : α
hx : x ∈ e.source
⊢ ↑e.symm (↑e x) ∈ s ↔ ↑e x ∈ t

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
⊢ e.IsImage s t ↔ e.source ∩ ↑e ⁻¹' t = e.source ∩ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedMonoid α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ r, ⨅ (_ : r > 1), 𝓟 {b | |a / b|ₘ < r}
⊢ OrderTopology α

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
f : β → α
x : Filter β
a : α
⊢ Tendsto f x (𝓝 a) ↔ ∀ ε > 1, ∀ᶠ (b : β) in x, |f b / a|ₘ < ε

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
a ε : α
hε : 1 < ε
⊢ {x | (fun x ↦ |x / a|ₘ < ε) x} ∈ 𝓟 {b | |a / b|ₘ < ε}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
⊢ Tendsto (fun x ↦ f x * g x) l atTop

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
⊢ Tendsto (fun x ↦ f x * g x) l (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x ↦ f x * g x) l atTop

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x ↦ f x * g x) l atBot

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a : α
⊢ (𝓝 a).HasBasis (fun ε ↦ 1 < ε) fun ε ↦ {b | |b / a|ₘ < ε}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a : α
⊢ (𝓝 a).HasBasis (fun ε ↦ 1 < ε) fun ε ↦ Ioo (a / ε) (a * ε)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : CommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : IsOrderedMonoid α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a _ε : α
ε₁ : 1 < _ε
δ : α
δ₁ : 1 < δ
δε : δ < _ε
⊢ a / _ε < a / δ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : CommGroup α
inst✝⁴ : LinearOrder α
inst✝³ : IsOrderedMonoid α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a _ε : α
ε₁ : 1 < _ε
δ : α
δ₁ : 1 < δ
δε : δ < _ε
⊢ a * δ < a * _ε

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
inst✝¹ : (i : α) → Decidable (i ∈ s)
inst✝ : (i : β) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
⊢ LeftInvOn (t.piecewise ↑e.symm ↑e'.symm) (s.piecewise ↑e ↑e') (s.ite e.source e'.source)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
⊢ (𝓝 1).HasBasis (fun ε ↦ 1 < ε) fun ε ↦ {b | |b|ₘ < ε}

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l (𝓝 0)
⊢ Tendsto (fun x ↦ f x * g x) l (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a : α
ha : 1 < a
ε : α
hε : 1 < ε
⊢ Ioo (a / min a ε) (a * min a ε) ⊆ Ioo (a / ε) (a * ε)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b B : 𝕜
hb : ∀ᶠ (x : α) in l, b ≤ f x
hB : ∀ᶠ (x : α) in l, f x ≤ B
hg : Tendsto g l atTop
⊢ Tendsto (fun x ↦ f x / g x) l (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
h' : e'.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
⊢ e.target ∩ t = e'.target ∩ t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Defs

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e✝ : PartialHomeomorph X Y
e : X ≃ₜ Y
⊢ ⇑e '' univ = univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
e' : PartialEquiv X Y
h : e.toPartialEquiv = e'
⊢ e.replacePartialEquiv e' h = e

Tactic:
by

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Defs

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X Y
e : X ≃ₜ Y
s : Set X
hs : IsOpen[inst✝⁵] s
t : Set Y
h : ⇑e '' s = t
⊢ IsOpen[inst✝³] (e.toPartialHomeomorphOfImageEq s t h).target

Tactic:
by

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Defs

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X Y
e : X ≃ₜ Y
⊢ ⇑e '' univ = univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
e' : PartialEquiv X Y
h : e.toPartialEquiv = e'
⊢ e.replacePartialEquiv e' h = e

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
c d : 𝕜
⊢ Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
c d : 𝕜
hc : c ≠ 0
⊢ Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d) ↔ n = 0 ∧ c = d

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
⊢ EqOn (↑e.symm) (↑e'.symm) (e.target ∩ t)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
x : α
hx : x ∈ e.source
⊢ ↑e x ∈ e.target ↔ x ∈ e.source

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
⊢ Tendsto (fun x ↦ c * x ^ n) atTop (𝓝 d) ↔ n = 0 ∧ c = d ∨ n < 0 ∧ d = 0

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
hs : Disjoint e.source e'.source
ht : Disjoint e.target e'.target
⊢ ↑e '' (e.source ∩ e'.source) = e.target ∩ e'.target

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
⊢ ↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a} = generateFrom {s | ∃ a, s = Iio a ∨ s = Ioi a}

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
hx : 0 < x
⊢ comap (fun x_1 ↦ x * x_1) (𝓝[>] 0) = 𝓝[>] 0

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
⊢ ↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
h : s ⊆ e.source
⊢ ↑e '' s = e.target ∩ ↑e.symm ⁻¹' s

Tactic:
by

Goal state after: