mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : IsUniformGroup α
hom : Type u_3
inst✝⁴ : UniformSpace β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
h : Tendsto (⇑f) (𝓝 1) (𝓝 1)
this : ((fun x ↦ x.2 / x.1) ∘ fun x ↦ (f x.1, f x.2)) = fun x ↦ f (x.2 / x.1)
⊢ Tendsto ((fun x ↦ x.2 / x.1) ∘ fun x ↦ (f x.1, f x.2)) (comap (fun x ↦ x.2 / x.1) (𝓝 1)) (𝓝 1)

Tactic:
this

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : IsUniformGroup α
hom : Type u_3
inst✝⁴ : UniformSpace β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
h : Tendsto (⇑f) (𝓝 1) (𝓝 1)
this : ((fun x ↦ x.2 / x.1) ∘ fun x ↦ (f x.1, f x.2)) = fun x ↦ f (x.2 / x.1)
⊢ Tendsto (fun x ↦ f (x.2 / x.1)) (comap (fun x ↦ x.2 / x.1) (𝓝 1)) (𝓝 1)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this :
  (fun x ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹)) = (fun p ↦ p.1 * p.2⁻¹) ∘ fun p ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)
⊢ Tendsto (fun x ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹)) (comap (fun p ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) (𝓝 (1, 1)))
    (𝓝 1)

Tactic:
this

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this :
  (fun x ↦ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹)) = (fun p ↦ p.1 * p.2⁻¹) ∘ fun p ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)
⊢ Tendsto ((fun p ↦ p.1 * p.2⁻¹) ∘ fun p ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹))
    (comap (fun p ↦ (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) (𝓝 (1, 1))) (𝓝 1)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
H : Type x
inst✝⁴ : Group G
inst✝³ : Monoid H
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace H
inst✝ : ContinuousInv G
f : G →* Hˣ
hf : Continuous[inst✝², inst✝¹] ⇑((Units.coeHom H).comp f)
⊢ Continuous[inst✝², instTopologicalSpaceMulOpposite] fun x ↦ op ↑(f x)⁻¹

Tactic:
[

Goal state after:
G : Type w
H : Type x
inst✝⁴ : Group G
inst✝³ : Monoid H
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace H
inst✝ : ContinuousInv G
f : G →* Hˣ
hf : Continuous[inst✝², inst✝¹] ⇑((Units.coeHom H).comp f)
⊢ Continuous[inst✝², instTopologicalSpaceMulOpposite] fun x ↦ op ↑(f x)⁻¹
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_3
inst✝³ : Group G
inst✝² : UniformSpace G
inst✝¹ : IsRightUniformGroup G
inst✝ : WeaklyLocallyCompactSpace G
f : Filter G
hf : Cauchy f
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : K ∈ 𝓝 1
x : G
hx : ∀ᶠ (y : G) in f, y / x ∈ K
⊢ ∃ x, f ≤ 𝓝 x

Tactic:
[

Goal state after:
G : Type u_3
inst✝³ : Group G
inst✝² : UniformSpace G
inst✝¹ : IsRightUniformGroup G
inst✝ : WeaklyLocallyCompactSpace G
f : Filter G
hf : Cauchy f
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : K ∈ 𝓝 1
x : G
hx : ∀ᶠ (y : G) in f, y / x ∈ K
⊢ ∃ x, f ≤ 𝓝 x
Module: Mathlib.Topology.Algebra.GroupWithZero

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : ContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt ↿h (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
hga : g a = 0
⊢ Tendsto (↿h ∘ fun x ↦ (x, f x / g x)) (𝓝 a) (𝓝 ((↿h ∘ fun x ↦ (x, f x / g x)) a))

Tactic:
[

Goal state after:
case pos
α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : ContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt ↿h (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
hga : g a = 0
⊢ Tendsto (↿h ∘ fun x ↦ (x, f x / g x)) (𝓝 a) (𝓝 ((↿h ∘ fun x ↦ (x, f x / g x)) a))
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : 𝓝 1 = comap (⇑opHomeomorph) (𝓝 1)
⊢ comap (fun x ↦ (op x.1, op x.2)) (comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1)) = comap (fun p ↦ p.1⁻¹ * p.2) (𝓝 1)

Tactic:
[

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : 𝓝 1 = comap (⇑opHomeomorph) (𝓝 1)
⊢ comap (fun x ↦ (op x.1, op x.2)) (comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1)) = comap (fun p ↦ p.1⁻¹ * p.2) (𝓝 1)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : 𝓝 1 = comap (⇑opHomeomorph) (𝓝 1)
⊢ comap (fun x ↦ (op x.1, op x.2)) (comap (fun p ↦ p.1⁻¹ * p.2) (𝓝 1)) = comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1)

Tactic:
[

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : 𝓝 1 = comap (⇑opHomeomorph) (𝓝 1)
⊢ comap (fun x ↦ (op x.1, op x.2)) (comap (fun p ↦ p.1⁻¹ * p.2) (𝓝 1)) = comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : 𝓝 1 = comap (⇑(Homeomorph.inv G)) (𝓝 1)
⊢ comap (fun x ↦ ((Equiv.inv G) x.1, (Equiv.inv G) x.2)) (comap (fun p ↦ p.1⁻¹ * p.2) (𝓝 1)) =
    comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1)

Tactic:
this

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : 𝓝 1 = comap (⇑(Homeomorph.inv G)) (𝓝 1)
⊢ comap (fun x ↦ ((Equiv.inv G) x.1, (Equiv.inv G) x.2))
      (comap (fun p ↦ p.1⁻¹ * p.2) (comap (⇑(Homeomorph.inv G)) (𝓝 1))) =
    comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝¹.toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
lim1 : Tendsto (fun a ↦ (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 (0, y₁))
lim2 : Tendsto (fun p ↦ (φ p.1) p.2) (𝓝 (0, y₁)) (𝓝 0)
lim :
  ∀ W ∈ 𝓝 0,
    ∃ U ∈ comap (⇑e) Nx, ∀ (x x' : β), x ∈ U → x' ∈ U → ((fun p ↦ (φ p.1) p.2) ∘ fun a ↦ (a.2 - a.1, y₁)) (x, x') ∈ W
⊢ ∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (φ (x' - x)) y₁ ∈ W'

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝¹.toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
lim1 : Tendsto (fun a ↦ (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 (0, y₁))
lim2 : Tendsto (fun p ↦ (φ p.1) p.2) (𝓝 (0, y₁)) (𝓝 0)
lim :
  ∀ W ∈ 𝓝 0,
    ∃ U ∈ comap (⇑e) Nx, ∀ (x x' : β), x ∈ U → x' ∈ U → ((fun p ↦ (φ p.1) p.2) ∘ fun a ↦ (a.2 - a.1, y₁)) (x, x') ∈ W
⊢ ∃ U₂ ∈ comap (⇑e) (𝓝 x₀), ∀ x ∈ U₂, ∀ x' ∈ U₂, (φ (x' - x)) y₁ ∈ W'
Module: Mathlib.Topology.Algebra.Field

Goal state before:
pp: K : Type u_1
inst✝⁷ : DivisionRing K
inst✝⁶ : TopologicalSpace K
R : Type u_2
inst✝⁵ : DivisionSemiring R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : PosMulReflectLT R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousInv₀ R
⊢ Continuous (unitsEquivPos R).invFun

Tactic:
rw [Units.continuous_iff]
    refine ⟨by fun_prop, ?_⟩
    suffices Continuous fun (x : { r : R // 0 < r }) ↦ (x⁻¹ : R) by
      simpa [Topology.IsEmbedding.subtypeVal.continuous_iff, Function.comp_def]
    rw [continuous_iff_continuousAt]
    exact fun x ↦ ContinuousAt.inv₀ (by fun_prop) x.2.ne'

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
this : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
⊢ (univ.pi fun i ↦ Ioc (update x i₀ m i) (y i)) = {z | m < z i₀} ∩ univ.pi fun i ↦ Ioc (x i) (y i)

Tactic:
[

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
this : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
⊢ (univ.pi fun i ↦ Ioc (update x i₀ m i) (y i)) = {z | m < z i₀} ∩ univ.pi fun i ↦ Ioc (x i) (y i)
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
this : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
⊢ ({x | x i₀ ∈ Ioc m (y i₀)} ∩ {i₀}ᶜ.pi fun j ↦ Ioc (x j) (y j)) =
    {z | m < z i₀} ∩ {x_1 | x_1 i₀ ∈ Ioc (x i₀) (y i₀)} ∩ {i₀}ᶜ.pi fun j ↦ Ioc (x j) (y j)

Tactic:
this

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : x i₀ ≤ m
this : Ioc m (y i₀) = Ioi m ∩ Ioc (x i₀) (y i₀)
⊢ ({x_1 | x_1 i₀ ∈ Ioi m ∩ Ioc (x i₀) (y i₀)} ∩ {i₀}ᶜ.pi fun j ↦ Ioc (x j) (y j)) =
    {z | m < z i₀} ∩ {x_1 | x_1 i₀ ∈ Ioc (x i₀) (y i₀)} ∩ {i₀}ᶜ.pi fun j ↦ Ioc (x j) (y j)
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
this : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
⊢ (univ.pi fun i ↦ Ioc (x i) (update y i₀ m i)) = {z | z i₀ ≤ m} ∩ univ.pi fun i ↦ Ioc (x i) (y i)

Tactic:
[

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
this : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
⊢ (univ.pi fun i ↦ Ioc (x i) (update y i₀ m i)) = {z | z i₀ ≤ m} ∩ univ.pi fun i ↦ Ioc (x i) (y i)
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
this : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
⊢ ({x_1 | x_1 i₀ ∈ Ioc (x i₀) m} ∩ {i₀}ᶜ.pi fun j ↦ Ioc (x j) (y j)) =
    {z | z i₀ ≤ m} ∩ {x_1 | x_1 i₀ ∈ Ioc (x i₀) (y i₀)} ∩ {i₀}ᶜ.pi fun j ↦ Ioc (x j) (y j)

Tactic:
this

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : DecidableEq ι
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ≤ y i₀
this : Ioc (x i₀) m = Iic m ∩ Ioc (x i₀) (y i₀)
⊢ ({x_1 | x_1 i₀ ∈ Iic m ∩ Ioc (x i₀) (y i₀)} ∩ {i₀}ᶜ.pi fun j ↦ Ioc (x j) (y j)) =
    {z | z i₀ ≤ m} ∩ {x_1 | x_1 i₀ ∈ Ioc (x i₀) (y i₀)} ∩ {i₀}ᶜ.pi fun j ↦ Ioc (x j) (y j)
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Lattice (α i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
i : ι
a b : α i
⊢ Icc (update f i (a ⊓ b)) (update f i (a ⊔ b)) = uIcc (update f i a) (update f i b)

Tactic:
[

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Lattice (α i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
i : ι
a b : α i
⊢ Icc (update f i (a ⊓ b)) (update f i (a ⊔ b)) = uIcc (update f i a) (update f i b)
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:
[

Goal state after:
ι : 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)
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 : 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)
hlt : a ^ (m - 1) < b
⊢ (Ioo (a ^ m) (a ^ (m + 1))).Nonempty

Tactic:
· use b * a
    simp only [mem_Ioo, zpow_add, zpow_sub, zpow_one, ← div_eq_mul_inv,
      mul_lt_mul_iff_right] at hlt ⊢
    exact ⟨div_lt_iff_lt_mul.1 hlt, hm⟩

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

Goal state before:
pp: case refine_1
𝕜 : 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
x' : 𝕜
h₀ : 0 < x'
hxx' : x ≤ x'
h₁ : x' < 1
⊢ ∀ᶠ (b : 𝕜) in 𝓝 1, x < b⁻¹

Tactic:
filter_upwards [Ioo_mem_nhds one_pos ((one_lt_inv₀ h₀).2 h₁)] with y hy

Goal state after:
𝕜 : 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
x' : 𝕜
h₀ : 0 < x'
hxx' : x ≤ x'
h₁ : x' < 1
y : 𝕜
hy : y ∈ Ioo 0 x'⁻¹
⊢ x < y⁻¹
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:
simpa using nhds_basis_abs_sub_lt (0 : 𝕜)

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)
⊢ 0 = |C * 0|

Tactic:
[

Goal state after:
𝕜 : 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)
⊢ 0 = |C * 0|
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
  convert! nhds_basis_mabs_div_lt a
  simp only [Ioo, mabs_lt, ← div_lt_iff_lt_mul, inv_lt_div_iff_lt_mul, div_lt_comm]

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

Goal state after:
α : Type u_1
inst✝ : Preorder α
⊢ generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a} = generateFrom {s | ∃ a, s = Iio a ∨ s = Ioi a}
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝ : Preorder α
t : OrderTopology α
⊢ OrderDual.instTopologicalSpace = Preorder.topology αᵒᵈ

Tactic:
[

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝ : Preorder α
t : OrderTopology α
⊢ OrderDual.instTopologicalSpace = Preorder.topology αᵒᵈ
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace β
f : β → α
⊢ Continuous[inst✝, ts] f ↔ ∀ (a : α), IsOpen[inst✝] (f ⁻¹' Ioi a) ∧ IsOpen[inst✝] (f ⁻¹' Iio a)

Tactic:
[

Goal state after:
α : Type u
β : Type v
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace β
f : β → α
⊢ Continuous[inst✝, ts] f ↔ ∀ (a : α), IsOpen[inst✝] (f ⁻¹' Ioi a) ∧ IsOpen[inst✝] (f ⁻¹' Iio a)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ ⨅ s ∈ {s | a ∈ s ∧ s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}}, 𝓟 s = (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)

Tactic:
[

Goal state after:
α : Type u
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ ⨅ s ∈ {s | a ∈ s ∧ s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}}, 𝓟 s = (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ (e.trans f).source = (e'.trans f').source

Tactic:
trans_source'',

Goal state after:
case left
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ ↑e.symm '' (e.target ∩ f.source) = (e'.trans f').source
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ ↑e.symm '' (e.target ∩ f.source) = (e'.trans f').source

Tactic:
trans_source'',

Goal state after:
case left
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ ↑e.symm '' (e.target ∩ f.source) = ↑e'.symm '' (e'.target ∩ f'.source)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
⊢ ∃ b c, a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s

Tactic:
by
  rcases exists_Icc_mem_subset_of_mem_nhdsLE (nhdsWithin_le_nhds hs) with
    ⟨b, hba, hb_nhds, hbs⟩
  rcases exists_Icc_mem_subset_of_mem_nhdsGE (nhdsWithin_le_nhds hs) with
    ⟨c, hac, hc_nhds, hcs⟩
  refine ⟨b, c, ⟨hba, hac⟩, ?_⟩
  rw [← Icc_union_Icc_eq_Icc hba hac, ← nhdsLE_sup_nhdsGE]
  exact ⟨union_mem_sup hb_nhds hc_nhds, union_subset hbs hcs⟩

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
⊢ x ∈ Ioc (a + toIocDiv hp a x • p) (a + p + toIocDiv hp a x • p)

Tactic:
rw [← sub_mem_Ioc_iff_left, ← toIocDiv_eq_iff]

Goal state after:
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
r : R
c : A →ₗ[R] CharacterModule B
x : A ⊗[R] B
⊢ (liftAddHom (r • c).toAddMonoidHom ⋯) 0 = ((RingHom.id R) r • liftAddHom c.toAddMonoidHom ⋯) 0

Tactic:
[

Goal state after:
R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
r : R
c : A →ₗ[R] CharacterModule B
x : A ⊗[R] B
⊢ (liftAddHom (r • c).toAddMonoidHom ⋯) 0 = ((RingHom.id R) r • liftAddHom c.toAddMonoidHom ⋯) 0
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx✝ : ↑y ∈ {x | n • x = 0}
hx : n • y ∈ zmultiples p
m' : ℤ
this : NeZero n
m : ℤ × Fin n := (Int.divModEquiv n) m'
hm : (fun x ↦ x • p) (m.1 * ↑n + ↑↑m.2) = n • y
⊢ ↑(y - m.1 • p) = ↑y ∧ n • (y - m.1 • p) = ↑m.2 • p

Tactic:
[

Goal state after:
case h
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx✝ : ↑y ∈ {x | n • x = 0}
hx : n • y ∈ zmultiples p
m' : ℤ
this : NeZero n
m : ℤ × Fin n := (Int.divModEquiv n) m'
hm : (fun x ↦ x • p) (m.1 * ↑n + ↑↑m.2) = n • y
⊢ ↑(y - m.1 • p) = ↑y ∧ n • (y - m.1 • p) = ↑m.2 • p
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := ⋯
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := ⋯
z : α → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint fun x ↦ Ioc (z x) x
x : α
hx : x ∈ t
⊢ Ioo (z x) (y x) ⊆ Ioc (z x) x

Tactic:
[

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := ⋯
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := ⋯
z : α → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint fun x ↦ Ioc (z x) x
x : α
hx : x ∈ t
⊢ Ioo (z x) (y x) ⊆ Ioc (z x) x
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
⊢ QuotientAddGroup.mk '' Ico a (a + p) = univ

Tactic:
by
  rw [image_eq_range]
  exact (equivIco p a).symm.range_eq_univ

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

Goal state before:
pp: case inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SeparableSpace α
h : {x | IsTop x} = ∅
s : Set α
s_count : s.Countable
hs : Dense s
this : atTop = generate (Ici '' s)
⊢ atTop.IsCountablyGenerated

Tactic:
this

Goal state after:
case inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SeparableSpace α
h : {x | IsTop x} = ∅
s : Set α
s_count : s.Countable
hs : Dense s
this : atTop = generate (Ici '' s)
⊢ (generate (Ici '' s)).IsCountablyGenerated
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inr
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SeparableSpace α
x : α
hx : x ∈ {x | IsTop x}
⊢ (pure x).IsCountablyGenerated

Tactic:
exact isCountablyGenerated_pure x

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

Goal state before:
pp: X : Type u_1
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
Y : Type u_2
inst✝² : ConditionallyCompleteLinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
x : X
hf : LeftOrdContinuous f
⊢ Tendsto f (𝓝[≤] x) (𝓝 (f x))

Tactic:
[

Goal state after:
X : Type u_1
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
Y : Type u_2
inst✝² : ConditionallyCompleteLinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
x : X
hf : LeftOrdContinuous f
⊢ Tendsto f (𝓝[≤] x) (𝓝 (f x))
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
⊢ n • ↑(p / ↑n) = 0

Tactic:
simp only [Ne, ← coe_nsmul, nsmul_eq_mul]

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
⊢ ↑(↑n * (p / ↑n)) = 0