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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
x₀ : G
⊢ map ((fun x ↦ x * x₀⁻¹) ∘ fun x ↦ x * x₀) (𝓝 1) = 𝓝 1

Tactic:
]

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
x₀ : G
⊢ map ((fun x ↦ x * x₀⁻¹) ∘ fun x ↦ x * x₀) (𝓝 1) = 𝓝 1
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
x₀ : G
hconj : ∀ (x₀ : G), map (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1) = 𝓝 1
⊢ 𝓝 x₀ = map (fun x ↦ x * x₀) (map (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1))

Tactic:
]

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hinv : Tendsto (fun x ↦ x⁻¹) (𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : G), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
x₀ : G
hconj : ∀ (x₀ : G), map (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1) = 𝓝 1
⊢ 𝓝 x₀ = map (fun x ↦ x * x₀) (map (fun x ↦ x₀ * x * x₀⁻¹) (𝓝 1))
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: β : 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 ψ (𝓤 β ×ˢ 𝓤 β) (𝓝 (1 * 1))

Tactic:
]

Goal state after:
β : 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 ψ (𝓤 β ×ˢ 𝓤 β) (𝓝 (1 * 1))
Module: Mathlib.Order.Filter.AtTopBot.Group

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b x : G
hx : x ≤ a ∧ x ≤ b⁻¹ ∨ a⁻¹ ≤ x ∧ b ≤ x
⊢ x ∈ Iic (a, b).1 ∪ Ici (a, b).2

Tactic:
]

Goal state after:
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b x : G
hx : x ≤ a ∧ x ≤ b⁻¹ ∨ a⁻¹ ≤ x ∧ b ≤ x
⊢ x ∈ Iic (a, b).1 ∪ Ici (a, b).2
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) (comap (fun x ↦ x.1⁻¹ * x.2) (𝓝 1) ×ˢ comap (fun x ↦ x.1⁻¹ * 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) (comap (fun x ↦ x.1⁻¹ * x.2) (𝓝 1) ×ˢ comap (fun x ↦ x.1⁻¹ * x.2) (𝓝 1)) (𝓝 1)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case e'_3
α : Type u
G : Type u_1
inst✝² : GroupWithZero G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
h : Tendsto (fun x ↦ f x / b) l (𝓝 (c / b))
k : α
⊢ f k = f k

Tactic:
]

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

Goal state before:
pp: case e'_5
α : Type u
G : Type u_1
inst✝² : GroupWithZero G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
h : Tendsto (fun x ↦ f x / b) l (𝓝 (c / b))
⊢ c = c

Tactic:
]

Goal state after:
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) (comap (fun x ↦ x.2⁻¹ * x.1) (𝓝 1) ×ˢ comap (fun x ↦ x.2⁻¹ * x.1) (𝓝 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) (comap (fun x ↦ x.2⁻¹ * x.1) (𝓝 1) ×ˢ comap (fun x ↦ x.2⁻¹ * x.1) (𝓝 1)) (𝓝 1)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case e'_3
α : Type u
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousDiv G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun x ↦ f x / b) l (𝓝 (c / b))
k : α
⊢ f k = f k

Tactic:
]

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

Goal state before:
pp: case e'_5
α : Type u
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousDiv G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun x ↦ f x / b) l (𝓝 (c / b))
⊢ c = c

Tactic:
]

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

Goal state before:
pp: case e'_3
G : Type w
α : Type u
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun k ↦ b / f k) l (𝓝 (b / c))
k : α
⊢ f k = f k

Tactic:
]

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

Goal state before:
pp: case e'_5
G : Type w
α : Type u
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun k ↦ b / f k) l (𝓝 (b / c))
⊢ c = c

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k : α
hk : 0 < k
a b : α
x✝ : 1 ≤ b
⊢ a ≤ k * b ↔ a ≤ k * b

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k : α
hk : 0 < k
b : α
x✝ : 1 ≤ b
⊢ b ≤ b

pp: case hb
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k : α
hk : 0 < k
b : α
x✝ : 1 ≤ b
⊢ k ≠ 0

Tactic:
]

Goal state after:
case hb
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k : α
hk : 0 < k
b : α
x✝ : 1 ≤ b
⊢ k ≠ 0
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (Filter.comap (fun x ↦ x.2 / x.1) (𝓝 1)).HasBasis p fun i ↦ {x | x.2 / x.1 ∈ U i}

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (Filter.comap (fun x ↦ x.2 / x.1) (𝓝 1)).HasBasis p fun i ↦ {x | x.2 / x.1 ∈ U i}
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (Filter.comap (fun x ↦ x.1⁻¹ * x.2) (𝓝 1)).HasBasis p fun i ↦ {x | x.1⁻¹ * x.2 ∈ U i}

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (Filter.comap (fun x ↦ x.1⁻¹ * x.2) (𝓝 1)).HasBasis p fun i ↦ {x | x.1⁻¹ * x.2 ∈ U i}
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (Filter.comap (fun x ↦ x.1 / x.2) (𝓝 1)).HasBasis p fun i ↦ {x | x.1 / x.2 ∈ U i}

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (Filter.comap (fun x ↦ x.1 / x.2) (𝓝 1)).HasBasis p fun i ↦ {x | x.1 / x.2 ∈ U i}
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (Filter.comap (fun x ↦ x.2⁻¹ * x.1) (𝓝 1)).HasBasis p fun i ↦ {x | x.2⁻¹ * x.1 ∈ U i}

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (Filter.comap (fun x ↦ x.2⁻¹ * x.1) (𝓝 1)).HasBasis p fun i ↦ {x | x.2⁻¹ * x.1 ∈ U i}
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : (⇑S.subtype ⁻¹' (fun p ↦ p.1 / p.2) '' L ×ˢ K).Finite
⊢ {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty}.Finite

Tactic:
]

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : (⇑S.subtype ⁻¹' (fun p ↦ p.1 / p.2) '' L ×ˢ K).Finite
⊢ {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty}.Finite
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 ↦ f (x.2 / x.1)) (comap (fun x ↦ x.2 / x.1) (𝓝 1)) (𝓝 1)

Tactic:
]

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: 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
⊢ ∀ᶠ (x : α) in 𝓝 1, f x = 1

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
⊢ ∀ᶠ (x : α) in 𝓝 1, f x = 1
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 : Continuous[inst✝⁷.toTopologicalSpace, inst✝⁴.toTopologicalSpace] ⇑f
this : Tendsto (⇑f) (𝓝 1) (𝓝 1)
⊢ Tendsto (⇑f) (𝓝 1) (𝓝 1)

Tactic:
]

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 : Continuous[inst✝⁷.toTopologicalSpace, inst✝⁴.toTopologicalSpace] ⇑f
this : Tendsto (⇑f) (𝓝 1) (𝓝 1)
⊢ Tendsto (⇑f) (𝓝 1) (𝓝 1)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case right
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 V : Set G
V_in : V ∈ 𝓝 1
hV' : s * V ⊆ U
W : Set G
W_in : W ∈ 𝓝 1
hW' : t * W ⊆ U
⊢ s * (V ∩ W) ∪ t * (V ∩ W) ⊆ U

Tactic:
]

Goal state after:
case right
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 V : Set G
V_in : V ∈ 𝓝 1
hV' : s * V ⊆ U
W : Set G
W_in : W ∈ 𝓝 1
hW' : t * W ⊆ U
⊢ s * (V ∩ W) ∪ t * (V ∩ W) ⊆ 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 : G
hx : x ∈ K
this : ∃ t₁ ∈ 𝓝 x, ∃ t₂ ∈ 𝓝 1, t₁ ×ˢ t₂ ⊆ (fun p ↦ p.1 * p.2) ⁻¹' U
⊢ ∃ 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 : G
hx : x ∈ K
this : ∃ t₁ ∈ 𝓝 x, ∃ t₂ ∈ 𝓝 1, t₁ ×ˢ t₂ ⊆ (fun p ↦ p.1 * p.2) ⁻¹' U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, 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 : G
hx : x ∈ K
t : Set G
ht : t ∈ 𝓝 x
s : Set G
hs : s ∈ 𝓝 1
h : t * s ⊆ U
⊢ ∃ 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 : G
hx : x ∈ K
t : Set G
ht : t ∈ 𝓝 x
s : Set G
hs : s ∈ 𝓝 1
h : t * s ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U
Module: Mathlib.Order.Filter.AtTopBot.Field

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

Tactic:
by
  simp [tendsto_const_mul_atBot_iff, h, h.not_tendsto disjoint_atTop_atBot]

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
x : (G × G) × G × G
⊢ x.1.2 * (x.1.1⁻¹ * x.2.1 * x.2.2⁻¹) = x.1.2 * x.1.1⁻¹ * (x.2.1 * x.2.2⁻¹)

Tactic:
]

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
x : (G × G) × G × G
⊢ x.1.2 * (x.1.1⁻¹ * x.2.1 * x.2.2⁻¹) = x.1.2 * x.1.1⁻¹ * (x.2.1 * x.2.2⁻¹)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: 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 : Set Gᵐᵒᵖ
hV : V ∈ 𝓝 (op 1)
hV' : op ⁻¹' V * K ⊆ U
⊢ op ⁻¹' V * K ⊆ U

Tactic:
]

Goal state after:
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 : Set Gᵐᵒᵖ
hV : V ∈ 𝓝 (op 1)
hV' : op ⁻¹' V * K ⊆ U
⊢ op ⁻¹' V * K ⊆ U
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 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)

Tactic:
]

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
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
g : G
x✝ : g ∈ K
⊢ g₀ ∈ interior V

Tactic:
]

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
g : G
x✝ : g ∈ K
⊢ g₀ ∈ interior V
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: G : Type u_2
u : UniformSpace G
inst✝¹ : Group G
inst✝ : IsUniformGroup G
⊢ comap (fun p ↦ p.2 * p.1⁻¹) (𝓝 1) = comap (fun x ↦ x.2 * x.1⁻¹) (𝓝 1)

Tactic:
]

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

Goal state before:
pp: 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
x : G
hL1 : L ∈ 𝓝 ((Homeomorph.mulLeft x) ((Homeomorph.mulLeft x).symm 1))
⊢ (range (denseSeq G) ∩ (fun y ↦ x * y) ⁻¹' L).Nonempty

Tactic:
]

Goal state after:
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
x : G
hL1 : L ∈ 𝓝 ((Homeomorph.mulLeft x) ((Homeomorph.mulLeft x).symm 1))
⊢ (range (denseSeq G) ∩ (fun y ↦ x * y) ⁻¹' L).Nonempty
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
⊢ ∃ g, Disjoint K (g • L)

Tactic:
have A : ¬K * L⁻¹ = univ := (hK.mul hL.inv).ne_univ
  obtain ⟨g, hg⟩ : ∃ g, g ∉ K * L⁻¹ := by
    contrapose! A
    exact eq_univ_iff_forall.2 A
  refine ⟨g, ?_⟩
  refine disjoint_left.2 fun a ha h'a => hg ?_
  rcases h'a with ⟨b, bL, rfl⟩
  refine ⟨g * b, ha, b⁻¹, by simpa only [Set.mem_inv, inv_inv] using bL, ?_⟩
  simp only [mul_inv_cancel_right]

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x y : G
⊢ map₂ (fun a b ↦ x * (a * b * y)) (𝓝 1) (𝓝 1) = map₂ (fun a b ↦ x * (a * b * y)) (𝓝 1) (𝓝 1)

Tactic:
]

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x y : G
⊢ map₂ (fun a b ↦ x * a * (b * y)) (𝓝 1) (𝓝 1) = map₂ (fun a b ↦ x * a * (b * y)) (𝓝 1) (𝓝 1)

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝³ : Monoid α
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ContinuousMul α
⊢ IsClosed[instTopologicalSpaceProd] {p | p.1 * unop p.2 = 1 ∧ unop p.2 * p.1 = 1}

Tactic:
]

Goal state after:
α : Type u
inst✝³ : Monoid α
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ContinuousMul α
⊢ IsClosed[instTopologicalSpaceProd] {p | p.1 * unop p.2 = 1 ∧ unop p.2 * p.1 = 1}
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
ι : Sort u_1
inst✝ : Group G
ts' : ι → TopologicalSpace G
h' : ∀ (i : ι), IsTopologicalGroup G
⊢ IsTopologicalGroup G

Tactic:
]

Goal state after:
G : Type w
ι : Sort u_1
inst✝ : Group G
ts' : ι → TopologicalSpace G
h' : ∀ (i : ι), IsTopologicalGroup G
⊢ IsTopologicalGroup G
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝ : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
⊢ IsTopologicalGroup G

Tactic:
]

Goal state after:
G : Type w
inst✝ : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
⊢ IsTopologicalGroup G
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝ : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
⊢ IsTopologicalGroup G

Tactic:
rw [inf_eq_iInf]
  refine topologicalGroup_iInf fun b => ?_
  cases b <;> assumption

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

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
a : α
⊢ 𝓤 α = 𝓤 α

pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
a : α
⊢ Function.Injective fun x ↦ (x.1 * a, x.2 * a)

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
a : α
⊢ Function.Injective fun x ↦ (x.1 * a, x.2 * a)
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 : Tendsto (fun x ↦ x.2 / x.1) (f ×ˢ f) (𝓝 1)
this : f.NeBot
K : Set G
K_compact : IsCompact K
K_mem : K ∈ 𝓝 1
⊢ ∃ x, ∀ᶠ (y : G) in f, y / x ∈ K

Tactic:
]

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

Goal state before:
pp: α : Type u_1
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : ContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
inst✝ : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
hfg : Tendsto (fun n ↦ f n * g n) l (𝓝 (x * y))
⊢ Tendsto f l (𝓝 (x * y / y))

Tactic:
]

Goal state after:
α : Type u_1
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : ContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
inst✝ : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
hfg : Tendsto (fun n ↦ f n * g n) l (𝓝 (x * y))
⊢ Tendsto f l (𝓝 (x * y / y))
Module: Mathlib.Topology.Algebra.Group.GroupTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝ : Group β
f : α → β
⊢ ∀ t_1 ∈ toTopologicalSpace '' {b | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace}, Continuous[t, _] f

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
inst✝ : Group β
f : α → β
⊢ ∀ t_1 ∈ toTopologicalSpace '' {b | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace}, Continuous[t, _] f