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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
⊢ TendstoIxxClass uIcc l l

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ∈ Icc (x i₀) (y i₀)
⊢ ((univ.pi fun i ↦ Ioc (x i) (update y i₀ m i)) ∪ univ.pi fun i ↦ Ioc (update x i₀ m i) (y i)) =
    univ.pi fun i ↦ Ioc (x i) (y i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' : (i : ι) → α i
⊢ (Icc x y \ univ.pi fun i ↦ Ioo (x' i) (y' i)) ⊆ (⋃ i, Icc x (update y i (x' i))) ∪ ⋃ i, Icc (update x i (y' i)) y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y z : (i : ι) → α i
⊢ (Icc x z \ univ.pi fun i ↦ Ioc (y i) (z i)) ⊆ ⋃ i, Icc x (update z i (y i))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹⁴ : TopologicalSpace α
inst✝¹³ : AddCommGroup α
inst✝¹² : IsTopologicalAddGroup α
inst✝¹¹ : TopologicalSpace β
inst✝¹⁰ : AddCommGroup β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : AddCommGroup γ
inst✝⁷ : IsTopologicalAddGroup γ
inst✝⁶ : TopologicalSpace δ
inst✝⁵ : AddCommGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝⁴.toTopologicalSpace] fun p ↦ (φ p.1) p.2
inst✝² : IsUniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
this :
  map (fun p ↦ (fun p ↦ (φ p.1) p.2) p.2 - (fun p ↦ (φ p.1) p.2) p.1)
      (comap (fun p ↦ ((e p.1.1, f p.1.2), e p.2.1, f p.2.2)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀))) ≤
    𝓝 0
⊢ map (fun p ↦ (φ p.1) p.2) (comap (Prod.map ⇑e ⇑f) (𝓝 (x₀, y₀))) ×ˢ
      map (fun p ↦ (φ p.1) p.2) (comap (Prod.map ⇑e ⇑f) (𝓝 (x₀, y₀))) ≤
    𝓤 G

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a b ε : G
hε : ε > 1
δ : G
hδ₁ : 1 < δ
hδε : δ < ε
c d : G
hc : |(c, d).1 / a|ₘ < δ
hd : |(c, d).2 / b|ₘ < ε / δ
⊢ |c * d / (a * b)|ₘ = |c / a * (d / b)|ₘ

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
⊢ Continuous[instTopologicalSpaceProd, inst✝⁴] fun p ↦ p.1 * p.2

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a ε : G
ε0 : ε > 1
x : G
hx : |x / a|ₘ < ε
⊢ |x⁻¹ / (fun a ↦ a⁻¹) a|ₘ < ε

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
⊢ comap mabs (𝓝 1) = 𝓝 1

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
α : Type u_2
l : Filter α
f : α → G
⊢ Tendsto f l (𝓝 1) ↔ Tendsto (mabs ∘ f) l (𝓝 1)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : Dense (range fun x ↦ a ^ x)
ha₀ : a ≤ 1
this : ∀ {a : G}, Dense (range fun x ↦ a ^ x) → 1 < a → (range fun x ↦ a ^ x) = univ
hlt : a < 1
⊢ (range fun x ↦ a⁻¹ ^ x) = range fun x ↦ a ^ x

Tactic:
by

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

Goal state before:
pp: case inr.inr
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : Dense (range fun x ↦ a ^ x)
ha₀ : a ≤ 1
this : ∀ {a : G}, Dense (range fun x ↦ a ^ x) → 1 < a → (range fun x ↦ a ^ x) = univ
hlt : a < 1
⊢ (range fun x ↦ a ^ x) = univ

Tactic:
have H : range (a⁻¹ ^ · : ℤ → G) = range (a ^ · : ℤ → G) := by
        simpa only [← inv_zpow, zpow_neg, comp_def] using neg_surjective.range_comp (a ^ · : ℤ → G)
      rw [← H]
      apply this <;> simpa only [H, one_lt_inv']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹⁴ : TopologicalSpace α
inst✝¹³ : AddCommGroup α
inst✝¹² : IsTopologicalAddGroup α
inst✝¹¹ : TopologicalSpace β
inst✝¹⁰ : AddCommGroup β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : AddCommGroup γ
inst✝⁷ : IsTopologicalAddGroup γ
inst✝⁶ : TopologicalSpace δ
inst✝⁵ : AddCommGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝⁴.toTopologicalSpace] fun p ↦ (φ p.1) p.2
inst✝² : IsUniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
⊢ Continuous[instTopologicalSpaceProd, inst✝⁴.toTopologicalSpace] (⋯.extend fun p ↦ (φ p.1) p.2)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x ↦ a ^ x
ha₀ : 1 < a
b : G
⊢ b * a ∈ Ioo b (b * a * a)

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 : α
hab : a < b
s : Set α
⊢ s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a

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
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
hx : CauchySeq x
⊢ (𝓤 (G ⧸ N)).HasBasis (fun x ↦ True) fun i ↦ {x | x.2 / x.1 ∈ mk '' u i}

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x ↦ a ^ x
ha₀ : 1 < a
b : G
⊢ ∃ m, a ^ m ∈ Ioo b (b * a * a)

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 : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
⊢ s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
this : (Ioo (a ^ m) (a ^ (m + 1))).Nonempty
l : ℤ
hl : a ^ l ∈ Ioo (a ^ m) (a ^ (m + 1))
⊢ m < l ∧ l < m + 1

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : DenseRange fun x ↦ a ^ x
ha₀ : 1 < a
b : G
m : ℤ
hm : b < a ^ m
hm' : a ^ m < b * a * a
hne : b ≠ a ^ (m - 1)
this : (Ioo (a ^ m) (a ^ (m + 1))).Nonempty
⊢ ∃ a_1, (fun x ↦ a ^ x) a_1 = b

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
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
h𝓤GN : (𝓤 (G ⧸ N)).HasBasis (fun x ↦ True) fun i ↦ {x | x.2 / x.1 ∈ mk '' u i}
hx : ∀ (i : ℕ), ∃ N_1, ∀ (m : ℕ), N_1 ≤ m → ∀ (n : ℕ), N_1 ≤ n → ∃ x_1 ∈ u i, ↑x_1 = x n / x m
i j M : ℕ
hM : ∀ (m : ℕ), M ≤ m → ∀ (n : ℕ), M ≤ n → ∃ x_1 ∈ u i, ↑x_1 = x n / x m
a b : ℕ
ha : max j M + 1 ≤ a
hb : max j M + 1 ≤ b
g : G
hg : x b = ↑g
y : G
y_mem : y ∈ u i
hy : ↑y = x b / x a
⊢ g / (y⁻¹ * g) ∈ u i

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 : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : (∃ u ∈ Ioc a b, Ioo a u ⊆ s) → ∃ u ∈ Ioi a, Ioo a u ⊆ s
tfae_5_to_1 : (∃ u ∈ Ioi a, Ioo a u ⊆ s) → s ∈ 𝓝[>] a
x✝ : s ∈ 𝓝[>] a
h : s ∈ 𝓝[>] a := x✝
⊢ ∃ u ∈ Ioc a b, Ioo a u ⊆ s

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
⊢ (DenseRange fun x ↦ a ^ x) ↔ Surjective fun x ↦ a ^ 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 b : α
hab : a < b
s : Set α
⊢ [s ∈ 𝓝[>] a, s ∈ 𝓝[Ioc a b] a, s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s].TFAE

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
⊢ 𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ b, a ⋖ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
⊢ {x | 𝓝[>] x = ⊥}.Countable

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
H : t.Countable
⊢ {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ⊆ t ∪ {x | IsTop x}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
H : t.Countable
⊢ {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥}.Countable

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
x : α
hx : x ∈ t
⊢ ∃ y > x, s ∩ Ioo x y = ∅

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < 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.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
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 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
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
⊢ ∀ (i : 𝕜), 0 < i ↔ ((fun x ↦ 0 < x) ∘ Inv.inv) i

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : α → α
hy : ∀ x ∈ t, y x > x
h'y : ∀ x ∈ t, s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
H : a < b
this : b < y a
⊢ b ∈ s ∩ Ioo a (y a)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℕ
hn : n ≠ 0
⊢ Tendsto (fun x ↦ x ^ (-↑n)) atTop (𝓝 0)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : α → α
hy : ∀ x ∈ t, y x > x
h'y : ∀ x ∈ t, s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
H : a < b
⊢ y a ≤ b

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
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
hx : CauchySeq x
⊢ ∀ (i j : ℕ), ∃ M, j < M ∧ ∀ (a b : ℕ), M ≤ a → M ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u i ∧ x a = ↑g'

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℤ
hn : n < 0
⊢ Tendsto (fun x ↦ x ^ n) atTop (𝓝 0)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
⊢ {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥}.Countable

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioi a, Ioc a u ⊆ s

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 ∈ 𝓝[Ico a b] b, s ∈ 𝓝[Ioo a b] b, ∃ l ∈ Ico a b, Ioo l b ⊆ s, ∃ l ∈ Iio b, Ioo l b ⊆ s].TFAE

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
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
hx : CauchySeq x
key₀ : ∀ (i j : ℕ), ∃ M, j < M ∧ ∀ (a b : ℕ), M ≤ a → M ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u i ∧ x a = ↑g'
φ : ℕ → ℕ := fun n ↦ Nat.recOn n (Classical.choose ⋯) fun k yk ↦ Classical.choose ⋯
hφ :
  ∀ (n : ℕ),
    φ n < φ (n + 1) ∧
      ∀ (a b : ℕ), φ (n + 1) ≤ a → φ (n + 1) ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u (n + 1) ∧ x a = ↑g'
x' : (n : ℕ) → (g : G) ×' x (φ (n + 1)) = ↑g :=
  fun n ↦ Nat.recOn n ⟨Classical.choose ⋯, ⋯⟩ fun k hk ↦ ⟨Classical.choose ⋯, ⋯⟩
hx' : ∀ (n : ℕ), (x' n).fst / (x' (n + 1)).fst ∈ u (n + 1)
⊢ (𝓤 G).HasBasis (fun x ↦ True) fun i ↦ {x | x.2 / x.1 ∈ u i}

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁵ : Semifield 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
inst✝ : ContinuousMul 𝕜
x : 𝕜
hx : x > 1
y : 𝕜
hy : y ∈ Ioi x⁻¹
⊢ 0 < x

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 α
⊢ s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ico l a ⊆ s

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁵ : Semifield 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
inst✝ : ContinuousMul 𝕜
⊢ (∀ a' < 1, ∀ᶠ (b : 𝕜) in 𝓝 1, a' < b⁻¹) ∧ ∀ a' > 1, ∀ᶠ (b : 𝕜) in 𝓝 1, b⁻¹ < a'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
⊢ 𝓝[<] a = ⊥ ↔ IsBot a ∨ ∃ b, b ⋖ a

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 : α
hab : a < b
s : Set α
⊢ s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a

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 : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
⊢ s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a

Tactic:
by

Goal state after:
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 < ε}
⊢ ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)

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
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
hx : CauchySeq x
key₀ : ∀ (i j : ℕ), ∃ M, j < M ∧ ∀ (a b : ℕ), M ≤ a → M ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u i ∧ x a = ↑g'
φ : ℕ → ℕ := fun n ↦ Nat.recOn n (Classical.choose ⋯) fun k yk ↦ Classical.choose ⋯
hφ :
  ∀ (n : ℕ),
    φ n < φ (n + 1) ∧
      ∀ (a b : ℕ), φ (n + 1) ≤ a → φ (n + 1) ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u (n + 1) ∧ x a = ↑g'
x' : (n : ℕ) → (g : G) ×' x (φ (n + 1)) = ↑g :=
  fun n ↦ Nat.recOn n ⟨Classical.choose ⋯, ⋯⟩ fun k hk ↦ ⟨Classical.choose ⋯, ⋯⟩
hx' : ∀ (n : ℕ), (x' n).fst / (x' (n + 1)).fst ∈ u (n + 1)
h𝓤G : (𝓤 G).HasBasis (fun x ↦ True) fun i ↦ {x | x.2 / x.1 ∈ u i}
m n : ℕ
hmn : n ≥ m
⊢ (x' n).fst / (x' n).fst ∈ u 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 : α
hab : a < b
s : Set α
⊢ [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u ∈ Ioc a b, Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s].TFAE

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
this✝¹ : UniformSpace (G ⧸ N) := IsTopologicalGroup.rightUniformSpace (G ⧸ N)
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : (𝓤 (G ⧸ N)).IsCountablyGenerated
u : ℕ → Set G
hu : (𝓝 1).HasAntitoneBasis u
u_mul : ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
hv : (𝓝 1).HasBasis (fun x ↦ True) fun x ↦ mk '' u x
v_anti : Antitone fun x ↦ mk '' u x
x : ℕ → G ⧸ N
hx : CauchySeq x
key₀ : ∀ (i j : ℕ), ∃ M, j < M ∧ ∀ (a b : ℕ), M ≤ a → M ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u i ∧ x a = ↑g'
φ : ℕ → ℕ := fun n ↦ Nat.recOn n (Classical.choose ⋯) fun k yk ↦ Classical.choose ⋯
hφ :
  ∀ (n : ℕ),
    φ n < φ (n + 1) ∧
      ∀ (a b : ℕ), φ (n + 1) ≤ a → φ (n + 1) ≤ b → ∀ (g : G), x b = ↑g → ∃ g', g / g' ∈ u (n + 1) ∧ x a = ↑g'
x' : (n : ℕ) → (g : G) ×' x (φ (n + 1)) = ↑g :=
  fun n ↦ Nat.recOn n ⟨Classical.choose ⋯, ⋯⟩ fun k hk ↦ ⟨Classical.choose ⋯, ⋯⟩
hx' : ∀ (n : ℕ), (x' n).fst / (x' (n + 1)).fst ∈ u (n + 1)
⊢ CauchySeq fun n ↦ (x' n).fst

Tactic:
by

Goal state after: