mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
hs : s ∈ 𝓝 1
this : (fun p ↦ p.1 * p.2⁻¹) ⁻¹' s ∈ 𝓝 (1, 1)
⊢ ∃ V ∈ 𝓝 1, ∀ v ∈ V, ∀ w ∈ V, v / w ∈ s

Tactic:
simpa only [div_eq_mul_inv, nhds_prod_eq, mem_prod_self_iff, prod_subset_iff, mem_preimage] using
    this

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

Goal state before:
pp: case refine_1
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
⊢ IsCompact ((y * x⁻¹) • K)

pp: case refine_2
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
⊢ (y * x⁻¹) • K ∈ 𝓝 y

Tactic:
·

Goal state after:
case refine_1
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
⊢ IsCompact ((y * x⁻¹) • K)
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: case refine_2
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
⊢ (y * x⁻¹) • K ∈ 𝓝 y

Tactic:
·

Goal state after:
case refine_2
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
⊢ (y * x⁻¹) • K ∈ 𝓝 y
Module: Mathlib.Order.Filter.AtTopBot.Monoid

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l f
hfg : Tendsto (fun x ↦ f x * g x) l atTop
⊢ Tendsto g l atTop

Tactic:
obtain ⟨C, hC⟩ := hf

Goal state after:
α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedCancelMonoid M
l : Filter α
f g : α → M
hfg : Tendsto (fun x ↦ f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map f l, (fun x1 x2 ↦ x1 ≤ x2) x C
⊢ Tendsto g l atTop
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case mp
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousMul A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen[inst✝⁵] U
x : A
⊢ x ∈ ⇑φ ⁻¹' ⇑φ '' U → x ∈ ⋃ k ∈ (↑φ).ker, (fun x ↦ x * k) ⁻¹' U

pp: case mpr
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousMul A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen[inst✝⁵] U
x : A
⊢ x ∈ ⋃ k ∈ (↑φ).ker, (fun x ↦ x * k) ⁻¹' U → x ∈ ⇑φ ⁻¹' ⇑φ '' U

Tactic:
·

Goal state after:
case mp
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousMul A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen[inst✝⁵] U
x : A
⊢ x ∈ ⇑φ ⁻¹' ⇑φ '' U → x ∈ ⋃ k ∈ (↑φ).ker, (fun x ↦ x * k) ⁻¹' U
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case mpr
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousMul A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen[inst✝⁵] U
x : A
⊢ x ∈ ⋃ k ∈ (↑φ).ker, (fun x ↦ x * k) ⁻¹' U → x ∈ ⇑φ ⁻¹' ⇑φ '' U

Tactic:
·

Goal state after:
case mpr
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousMul A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen[inst✝⁵] U
x : A
⊢ x ∈ ⋃ k ∈ (↑φ).ker, (fun x ↦ x * k) ⁻¹' U → x ∈ ⇑φ ⁻¹' ⇑φ '' U
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: case refine_1
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto (fun x ↦ x.1.1⁻¹ * x.1.2) (𝓤 β ×ˢ 𝓤 β) (𝓝 1)

pp: case refine_2
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto (fun x ↦ x.2.2⁻¹ * x.2.1) (𝓤 β ×ˢ 𝓤 β) (𝓝 1)

Tactic:
·

Goal state after:
case refine_1
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto (fun x ↦ x.1.1⁻¹ * x.1.2) (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: case refine_2
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto (fun x ↦ x.2.2⁻¹ * x.2.1) (𝓤 β ×ˢ 𝓤 β) (𝓝 1)

Tactic:
·

Goal state after:
case refine_2
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto (fun x ↦ x.2.2⁻¹ * x.2.1) (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
c : α
n : ℕ
h : Tendsto (fun x ↦ c * x ^ n) atTop atTop
⊢ n ≠ 0

pp: case refine_2
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
c : α
n : ℕ
h : Tendsto (fun x ↦ c * x ^ n) atTop atTop
⊢ 0 < c

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
c : α
n : ℕ
h : Tendsto (fun x ↦ c * x ^ n) atTop atTop
⊢ n ≠ 0
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
c : α
n : ℕ
h : Tendsto (fun x ↦ c * x ^ n) atTop atTop
⊢ 0 < c

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
c : α
n : ℕ
h : Tendsto (fun x ↦ c * x ^ n) atTop atTop
⊢ 0 < c
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
hr : r < 0
⊢ Tendsto (fun x ↦ r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
inst✝ : l.NeBot
⊢ Tendsto (fun x ↦ 0 * f x) l atTop ↔ 0 < 0 ∧ Tendsto f l atTop ∨ 0 < 0 ∧ Tendsto f l atBot

pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
hr : 0 < r
⊢ Tendsto (fun x ↦ r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
hr : r < 0
⊢ Tendsto (fun x ↦ r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
inst✝ : l.NeBot
⊢ Tendsto (fun x ↦ 0 * f x) l atTop ↔ 0 < 0 ∧ Tendsto f l atTop ∨ 0 < 0 ∧ Tendsto f l atBot

pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
hr : 0 < r
⊢ Tendsto (fun x ↦ r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
inst✝ : l.NeBot
⊢ Tendsto (fun x ↦ 0 * f x) l atTop ↔ 0 < 0 ∧ Tendsto f l atTop ∨ 0 < 0 ∧ Tendsto f l atBot
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝⁸ : UniformSpace α
inst✝⁷ : Group α
inst✝⁶ : IsUniformGroup α
hom : Type u_3
inst✝⁵ : UniformSpace β
inst✝⁴ : DiscreteTopology β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
hf : UniformContinuous ⇑f
⊢ IsOpen[inst✝⁸.toTopologicalSpace] ↑(↑f).ker

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁸ : UniformSpace α
inst✝⁷ : Group α
inst✝⁶ : IsUniformGroup α
hom : Type u_3
inst✝⁵ : UniformSpace β
inst✝⁴ : DiscreteTopology β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
hf : IsOpen[inst✝⁸.toTopologicalSpace] ↑(↑f).ker
⊢ UniformContinuous ⇑f

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁸ : UniformSpace α
inst✝⁷ : Group α
inst✝⁶ : IsUniformGroup α
hom : Type u_3
inst✝⁵ : UniformSpace β
inst✝⁴ : DiscreteTopology β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
hf : UniformContinuous ⇑f
⊢ IsOpen[inst✝⁸.toTopologicalSpace] ↑(↑f).ker
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
hr : 0 < r
⊢ Tendsto (fun x ↦ r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot

Tactic:
·

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
hr : 0 < r
⊢ Tendsto (fun x ↦ r * f x) l atTop ↔ 0 < r ∧ Tendsto f l atTop ∨ r < 0 ∧ Tendsto f l atBot
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁸ : UniformSpace α
inst✝⁷ : Group α
inst✝⁶ : IsUniformGroup α
hom : Type u_3
inst✝⁵ : UniformSpace β
inst✝⁴ : DiscreteTopology β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
hf : IsOpen[inst✝⁸.toTopologicalSpace] ↑(↑f).ker
⊢ UniformContinuous ⇑f

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁸ : UniformSpace α
inst✝⁷ : Group α
inst✝⁶ : IsUniformGroup α
hom : Type u_3
inst✝⁵ : UniformSpace β
inst✝⁴ : DiscreteTopology β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
hf : IsOpen[inst✝⁸.toTopologicalSpace] ↑(↑f).ker
⊢ UniformContinuous ⇑f
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case refine_1
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∃ V ∈ 𝓝 1, ∅ * V ⊆ U

pp: case refine_2
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∀ ⦃s t : Set G⦄, s ⊆ t → (∃ V ∈ 𝓝 1, t * V ⊆ U) → ∃ V ∈ 𝓝 1, s * V ⊆ U

pp: case refine_3
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∀ ⦃s t : Set G⦄, (∃ V ∈ 𝓝 1, s * V ⊆ U) → (∃ V ∈ 𝓝 1, t * V ⊆ U) → ∃ V ∈ 𝓝 1, (s ∪ t) * V ⊆ U

pp: case refine_4
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Tactic:
·

Goal state after:
case refine_1
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∃ V ∈ 𝓝 1, ∅ * V ⊆ U
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case refine_2
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∀ ⦃s t : Set G⦄, s ⊆ t → (∃ V ∈ 𝓝 1, t * V ⊆ U) → ∃ V ∈ 𝓝 1, s * V ⊆ U

pp: case refine_3
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∀ ⦃s t : Set G⦄, (∃ V ∈ 𝓝 1, s * V ⊆ U) → (∃ V ∈ 𝓝 1, t * V ⊆ U) → ∃ V ∈ 𝓝 1, (s ∪ t) * V ⊆ U

pp: case refine_4
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Tactic:
·

Goal state after:
case refine_2
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∀ ⦃s t : Set G⦄, s ⊆ t → (∃ V ∈ 𝓝 1, t * V ⊆ U) → ∃ V ∈ 𝓝 1, s * V ⊆ U
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case refine_3
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∀ ⦃s t : Set G⦄, (∃ V ∈ 𝓝 1, s * V ⊆ U) → (∃ V ∈ 𝓝 1, t * V ⊆ U) → ∃ V ∈ 𝓝 1, (s ∪ t) * V ⊆ U

pp: case refine_4
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Tactic:
·

Goal state after:
case refine_3
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∀ ⦃s t : Set G⦄, (∃ V ∈ 𝓝 1, s * V ⊆ U) → (∃ V ∈ 𝓝 1, t * V ⊆ U) → ∃ V ∈ 𝓝 1, (s ∪ t) * V ⊆ U
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case refine_4
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Tactic:
·

Goal state after:
case refine_4
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case refine_1
G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : L ∈ 𝓝 1
⊢ ∀ (n : ℕ), IsCompact ((fun n ↦ (fun x ↦ x * denseSeq G n) ⁻¹' L) n)

pp: case refine_2
G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : L ∈ 𝓝 1
⊢ ⋃ n, (fun n ↦ (fun x ↦ x * denseSeq G n) ⁻¹' L) n = univ

Tactic:
·

Goal state after:
case refine_1
G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : L ∈ 𝓝 1
⊢ ∀ (n : ℕ), IsCompact ((fun n ↦ (fun x ↦ x * denseSeq G n) ⁻¹' L) n)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case refine_2
G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : L ∈ 𝓝 1
⊢ ⋃ n, (fun n ↦ (fun x ↦ x * denseSeq G n) ⁻¹' L) n = univ

Tactic:
·

Goal state after:
case refine_2
G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : L ∈ 𝓝 1
⊢ ⋃ n, (fun n ↦ (fun x ↦ x * denseSeq G n) ⁻¹' L) n = univ
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
⊢ ContinuousAt (↿h ∘ fun x ↦ (x, f x / g x)) a

pp: case neg
α : 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
⊢ ContinuousAt (↿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
⊢ ContinuousAt (↿h ∘ fun x ↦ (x, f x / g x)) a
Module: Mathlib.Topology.Algebra.GroupWithZero

Goal state before:
pp: case neg
α : 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
⊢ ContinuousAt (↿h ∘ fun x ↦ (x, f x / g x)) a

Tactic:
·

Goal state after:
case neg
α : 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
⊢ ContinuousAt (↿h ∘ fun x ↦ (x, f x / g x)) a
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: case refine_1
G✝ : Type u_1
inst✝⁵ : Group G✝
inst✝⁴ : TopologicalSpace G✝
inst✝³ : IsTopologicalGroup G✝
G : Type u_2
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : UniformSpace Gᵐᵒᵖ := IsTopologicalGroup.leftUniformSpace Gᵐᵒᵖ
⊢ UniformContinuous opEquiv.toFun

pp: case refine_2
G✝ : Type u_1
inst✝⁵ : Group G✝
inst✝⁴ : TopologicalSpace G✝
inst✝³ : IsTopologicalGroup G✝
G : Type u_2
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : UniformSpace Gᵐᵒᵖ := IsTopologicalGroup.leftUniformSpace Gᵐᵒᵖ
⊢ UniformContinuous opEquiv.invFun

Tactic:
·

Goal state after:
case refine_1
G✝ : Type u_1
inst✝⁵ : Group G✝
inst✝⁴ : TopologicalSpace G✝
inst✝³ : IsTopologicalGroup G✝
G : Type u_2
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : UniformSpace Gᵐᵒᵖ := IsTopologicalGroup.leftUniformSpace Gᵐᵒᵖ
⊢ UniformContinuous opEquiv.toFun
Module: Mathlib.Topology.Algebra.GroupWithZero

Goal state before:
pp: case ofNat
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : ContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.ofNat m
⊢ ContinuousAt (fun x ↦ x ^ Int.ofNat m) x

pp: case negSucc
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : ContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
⊢ ContinuousAt (fun x ↦ x ^ Int.negSucc m) x

Tactic:
·

Goal state after:
case ofNat
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : ContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.ofNat m
⊢ ContinuousAt (fun x ↦ x ^ Int.ofNat m) x
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: case refine_2
G✝ : Type u_1
inst✝⁵ : Group G✝
inst✝⁴ : TopologicalSpace G✝
inst✝³ : IsTopologicalGroup G✝
G : Type u_2
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : UniformSpace Gᵐᵒᵖ := IsTopologicalGroup.leftUniformSpace Gᵐᵒᵖ
⊢ UniformContinuous opEquiv.invFun

Tactic:
·

Goal state after:
case refine_2
G✝ : Type u_1
inst✝⁵ : Group G✝
inst✝⁴ : TopologicalSpace G✝
inst✝³ : IsTopologicalGroup G✝
G : Type u_2
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : UniformSpace Gᵐᵒᵖ := IsTopologicalGroup.leftUniformSpace Gᵐᵒᵖ
⊢ UniformContinuous opEquiv.invFun
Module: Mathlib.Topology.Algebra.GroupWithZero

Goal state before:
pp: case negSucc
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : ContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
⊢ ContinuousAt (fun x ↦ x ^ Int.negSucc m) x

Tactic:
·

Goal state after:
case negSucc
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : ContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
⊢ ContinuousAt (fun x ↦ x ^ Int.negSucc m) x