awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
a : G
s : Set G
hs : s ∈ 𝓝 a
this : Tendsto (fun (p : G × G) ↦ p.1 * p.2) (𝓝 (a, 1)) (𝓝 a)
U : Set G
hU : U ∈ 𝓝 a
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 1) V
hUV : image2 HMul.hMul U V ⊆ s
⊢ U * interior V ⊆ U * V

Tactic:
mul_subset_mul_left interior_subset

Premises used: interior_subset, Set.mul_subset_mul_left
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
a : G
s : Set G
hs : s ∈ 𝓝 a
this : Tendsto (fun (p : G × G) ↦ p.1 * p.2) (𝓝 (a, 1)) (𝓝 a)
U : Set G
hU : U ∈ 𝓝 a
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 1) V
hUV : image2 HMul.hMul U V ⊆ s
⊢ U * V ⊆ s

Tactic:
hUV
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
a : G
s : Set G
hs : s ∈ 𝓝 a
this : Tendsto (fun (p : G × G) ↦ p.1 * p.2) (𝓝 (a, 1)) (𝓝 a)
U : Set G
hU : U ∈ 𝓝 a
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 1) V
hUV : image2 HMul.hMul U V ⊆ s
⊢ closure[inst] U ⊆ s

Tactic:
calc
    closure U ⊆ closure U * interior V := subset_mul_left _ (mem_interior_iff_mem_nhds.2 hV)
    _ = U * interior V := isOpen_interior.closure_mul U
    _ ⊆ U * V := mul_subset_mul_left interior_subset
    _ ⊆ s := hUV

Premises used: Iff.mpr, mem_interior_iff_mem_nhds, interior_subset, isOpen_interior, closure, interior, Set.mul_subset_mul_left, IsOpen.closure_mul, Set.subset_mul_left
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
x y : G
rw :
  Inseparable (X := G) ((Homeomorph.mulRight y⁻¹ : (a : G) → G) x : G) ((Homeomorph.mulRight y⁻¹ : (a : G) → G) y : G) ↔
    Inseparable (x / y) 1
⊢ Inseparable x y ↔ Membership.mem (γ := Set G) (closure[inst] 1) (x / y)

Tactic:
rw [← singleton_one, ← specializes_iff_mem_closure, specializes_comm, specializes_iff_inseparable,
    ← (Homeomorph.mulRight y⁻¹).isEmbedding.inseparable_iff]

Premises used: Homeomorph.isEmbedding, Homeomorph.mulRight, specializes_iff_mem_closure, Inv.inv, specializes_iff_inseparable, Topology.IsEmbedding.toIsInducing, specializes_comm, Set.singleton_one, Topology.IsInducing.inseparable_iff
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
x y : G
⊢ Inseparable (X := G) ((Homeomorph.mulRight y⁻¹ : (a : G) → G) x : G) ((Homeomorph.mulRight y⁻¹ : (a : G) → G) y : G) ↔
    Inseparable (x / y) 1

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
⊢ T2Space G ↔ IsClosed[inst] {1}

Tactic:
⟨fun _ ↦ isClosed_singleton, fun h ↦
    have := IsTopologicalGroup.t1Space G h; inferInstance⟩

Premises used: IsTopologicalGroup.t1Space, inferInstance, Iff.intro, isClosed_singleton
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ (U : Set G), Membership.mem (γ := Filter G) (𝓝 1) U ∧ x ∉ U
suffices : T1Space G
⊢ T2Space G

Tactic:
suffices T1Space G from inferInstance
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ (U : Set G), Membership.mem (γ := Filter G) (𝓝 1) U ∧ x ∉ U
⊢ T1Space G

Tactic:
t1Space_iff_specializes_imp_eq.2 fun x y hspec ↦ by_contra fun hne ↦ ?_

Premises used: t1Space_iff_specializes_imp_eq, Iff.mpr, by_contra
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ (U : Set G), Membership.mem (γ := Filter G) (𝓝 1) U ∧ x ∉ U
refine : ∀ (x y : G) (hspec : x ⤳ y) (hne : ¬x = y), False
⊢ T1Space G

Tactic:
refine t1Space_iff_specializes_imp_eq.2 fun x y hspec ↦ by_contra fun hne ↦ ?_

Premises used: t1Space_iff_specializes_imp_eq, Iff.mpr, by_contra
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ (U : Set G), Membership.mem (γ := Filter G) (𝓝 1) U ∧ x ∉ U
x y : G
hspec : x ⤳ y
hne : ¬x = y
rwa : ¬x * y⁻¹ = 1
rwa₁ rwa₂ rwa₃ rwa₄ : ¬x = y
⊢ x * y⁻¹ ≠ 1

Tactic:
rwa [Ne, mul_inv_eq_one]

Premises used: mul_inv_eq_one, Ne
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ (U : Set G), Membership.mem (γ := Filter G) (𝓝 1) U ∧ x ∉ U
x y : G
hspec : x ⤳ y
hne : ¬x = y
rcases : ∀ (U : Set G) (hU₁ : Membership.mem (γ := Filter G) (𝓝 1) U) (hU : x * y⁻¹ ∉ U), False
⊢ False

Tactic:
rcases H (x * y⁻¹) (by rwa [Ne, mul_inv_eq_one]) with ⟨U, hU₁, hU⟩

Premises used: HMul.hMul, Inv.inv
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ (U : Set G), Membership.mem (γ := Filter G) (𝓝 1) U ∧ x ∉ U
x y : G
hspec : x ⤳ y
hne : ¬x = y
U : Set G
hU₁ : Membership.mem (γ := Filter G) (𝓝 1) U
hU : x * y⁻¹ ∉ U
rwa rwa₁ rwa₂ rwa₃ : Membership.mem (γ := Filter G) (𝓝 1) U
⊢ U ∈ 𝓝 (y * y⁻¹)

Tactic:
rwa [mul_inv_cancel]

Premises used: mul_inv_cancel
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ (U : Set G), Membership.mem (γ := Filter G) (𝓝 1) U ∧ x ∉ U
x y : G
hspec : x ⤳ y
hne : ¬x = y
U : Set G
hU₁ : Membership.mem (γ := Filter G) (𝓝 1) U
hU : x * y⁻¹ ∉ U
⊢ False

Tactic:
exact hU <| mem_of_mem_nhds <| hspec.map (continuous_mul_const y⁻¹) (by rwa [mul_inv_cancel])

Premises used: mem_of_mem_nhds, Inv.inv, Specializes.map, continuous_mul_const
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
rcases :
  ∀ (V : Set G) (V_open : IsOpen[inst] V) (V_mem : 1 ∈ V) (hV : V * V ⊆ U),
    ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ IsClosed[inst] V ∧ V⁻¹ = V ∧ V * V ⊆ U
⊢ ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ IsClosed[inst] V ∧ V⁻¹ = V ∧ V * V ⊆ U

Tactic:
rcases exists_open_nhds_one_mul_subset hU with ⟨V, V_open, V_mem, hV⟩

Premises used: exists_open_nhds_one_mul_subset
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
V : Set G
V_open : IsOpen[inst] V
V_mem : 1 ∈ V
hV : V * V ⊆ U
rcases :
  ∀ (W : Set G) (W_mem : Membership.mem (γ := Filter G) (𝓝 1) W) (W_closed : IsClosed[inst] W) (hW : W ⊆ V),
    ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ IsClosed[inst] V ∧ V⁻¹ = V ∧ V * V ⊆ U
⊢ ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ IsClosed[inst] V ∧ V⁻¹ = V ∧ V * V ⊆ U

Tactic:
rcases exists_mem_nhds_isClosed_subset (V_open.mem_nhds V_mem) with ⟨W, W_mem, W_closed, hW⟩

Premises used: IsOpen.mem_nhds, exists_mem_nhds_isClosed_subset
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
V : Set G
V_open : IsOpen[inst] V
V_mem : 1 ∈ V
hV : V * V ⊆ U
W : Set G
W_mem : Membership.mem (γ := Filter G) (𝓝 1) W
W_closed : IsClosed[inst] W
hW : W ⊆ V
⊢ (W ∩ W⁻¹)⁻¹ = W ∩ W⁻¹

Tactic:
simp [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
V : Set G
V_open : IsOpen[inst] V
V_mem : 1 ∈ V
hV : V * V ⊆ U
W : Set G
W_mem : Membership.mem (γ := Filter G) (𝓝 1) W
W_closed : IsClosed[inst] W
hW : W ⊆ V
refine : W ∩ W⁻¹ * (W ∩ W⁻¹) ⊆ U
⊢ ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ IsClosed[inst] V ∧ V⁻¹ = V ∧ V * V ⊆ U

Tactic:
refine ⟨W ∩ W⁻¹, Filter.inter_mem W_mem (inv_mem_nhds_one G W_mem), W_closed.inter W_closed.inv,
    by simp [inter_comm], ?_⟩
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
V : Set G
V_open : IsOpen[inst] V
V_mem : 1 ∈ V
hV : V * V ⊆ U
W : Set G
W_mem : Membership.mem (γ := Filter G) (𝓝 1) W
W_closed : IsClosed[inst] W
hW : W ⊆ V
⊢ W ∩ W⁻¹ * (W ∩ W⁻¹) ⊆ W * W

Tactic:
mul_subset_mul inter_subset_left inter_subset_left

Premises used: Set.inter_subset_left, Set.mul_subset_mul
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
V : Set G
V_open : IsOpen[inst] V
V_mem : 1 ∈ V
hV : V * V ⊆ U
W : Set G
W_mem : Membership.mem (γ := Filter G) (𝓝 1) W
W_closed : IsClosed[inst] W
hW : W ⊆ V
⊢ W * W ⊆ V * V

Tactic:
mul_subset_mul hW hW

Premises used: Set.mul_subset_mul
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
V : Set G
V_open : IsOpen[inst] V
V_mem : 1 ∈ V
hV : V * V ⊆ U
W : Set G
W_mem : Membership.mem (γ := Filter G) (𝓝 1) W
W_closed : IsClosed[inst] W
hW : W ⊆ V
⊢ V * V ⊆ U

Tactic:
hV
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
V : Set G
V_open : IsOpen[inst] V
V_mem : 1 ∈ V
hV : V * V ⊆ U
W : Set G
W_mem : Membership.mem (γ := Filter G) (𝓝 1) W
W_closed : IsClosed[inst] W
hW : W ⊆ V
⊢ W ∩ W⁻¹ * (W ∩ W⁻¹) ⊆ U

Tactic:
calc
  W ∩ W⁻¹ * (W ∩ W⁻¹)
    ⊆ W * W := mul_subset_mul inter_subset_left inter_subset_left
  _ ⊆ V * V := mul_subset_mul hW hW
  _ ⊆ U := hV

Premises used: Set.inter_subset_left, Inter.inter, Inv.inv, Set.mul_subset_mul
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : IsDiscrete (↑S : Set G)
obtain :
  ∀ (V : Set G) (hV : Membership.mem (γ := Filter G) (𝓝 1) V ∧ V ∩ (↑S : Set G) = {1}),
    ∃ (U : Set G),
      Membership.mem (γ := Filter G) (𝓝 1) U ∧ U⁻¹ = U ∧ ∀ g ∈ S, ((fun (x : G) ↦ g * x) '' U ∩ U).Nonempty → g = 1
⊢ ∃ (U : Set G),
    Membership.mem (γ := Filter G) (𝓝 1) U ∧ U⁻¹ = U ∧ ∀ g ∈ S, ((fun (x : G) ↦ g * x) '' U ∩ U).Nonempty → g = 1

Tactic:
obtain ⟨V, hV⟩ := nhds_inter_eq_singleton_of_mem_discrete hS S.one_mem

Premises used: nhds_inter_eq_singleton_of_mem_discrete, Subgroup.one_mem
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : IsDiscrete (↑S : Set G)
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 1) V ∧ V ∩ (↑S : Set G) = {1}
obtain :
  ∀ (U : Set G) (hU : Membership.mem (γ := Filter G) (𝓝 1) U) (hUinv : U⁻¹ = U) (hUV : U * U ⊆ V),
    ∃ (U : Set G),
      Membership.mem (γ := Filter G) (𝓝 1) U ∧ U⁻¹ = U ∧ ∀ g ∈ S, ((fun (x : G) ↦ g * x) '' U ∩ U).Nonempty → g = 1
⊢ ∃ (U : Set G),
    Membership.mem (γ := Filter G) (𝓝 1) U ∧ U⁻¹ = U ∧ ∀ g ∈ S, ((fun (x : G) ↦ g * x) '' U ∩ U).Nonempty → g = 1

Tactic:
obtain ⟨U, hU, -, hUinv, hUV⟩ := exists_closed_nhds_one_inv_eq_mul_subset hV.1

Premises used: exists_closed_nhds_one_inv_eq_mul_subset, And.left
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : IsDiscrete (↑S : Set G)
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 1) V ∧ V ∩ (↑S : Set G) = {1}
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
hUinv : U⁻¹ = U
hUV : U * U ⊆ V
⊢ ∃ (U : Set G),
    Membership.mem (γ := Filter G) (𝓝 1) U ∧ U⁻¹ = U ∧ ∀ g ∈ S, ((fun (x : G) ↦ g * x) '' U ∩ U).Nonempty → g = 1

Tactic:
⟨U, hU, hUinv, fun g hgS ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : IsDiscrete (↑S : Set G)
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 1) V ∧ V ∩ (↑S : Set G) = {1}
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
hUinv : U⁻¹ = U
hUV : U * U ⊆ V
refine : ∀ (g : G) (hgS : g ∈ S), ((fun (x : G) ↦ g * x) '' U ∩ U).Nonempty → g = 1
⊢ ∃ (U : Set G),
    Membership.mem (γ := Filter G) (𝓝 1) U ∧ U⁻¹ = U ∧ ∀ g ∈ S, ((fun (x : G) ↦ g * x) '' U ∩ U).Nonempty → g = 1

Tactic:
refine ⟨U, hU, hUinv, fun g hgS ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : IsDiscrete (↑S : Set G)
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 1) V ∧ V ∩ (↑S : Set G) = {1}
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
hUinv : U⁻¹ = U
hUV : U * U ⊆ V
g : G
hgS : g ∈ S
x : G
hx : x ∈ U
hgx : (fun (x : G) ↦ g * x) x ∈ U
⊢ g = 1

Tactic:
hV.2.subset ⟨hUV ?_, hgS⟩

Premises used: Set.Mem, setOf, Eq.subset, And.right, And.intro, Set.singleton
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : IsDiscrete (↑S : Set G)
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 1) V ∧ V ∩ (↑S : Set G) = {1}
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
hUinv : U⁻¹ = U
hUV : U * U ⊆ V
g : G
hgS : g ∈ S
x : G
hx : x ∈ U
hgx : (fun (x : G) ↦ g * x) x ∈ U
refine : g ∈ U * U
⊢ g = 1

Tactic:
refine hV.2.subset ⟨hUV ?_, hgS⟩

Premises used: Eq.subset, And.right, And.intro
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : IsDiscrete (↑S : Set G)
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 1) V ∧ V ∩ (↑S : Set G) = {1}
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
hUinv : U⁻¹ = U
hUV : U * U ⊆ V
g : G
hgS : g ∈ S
x : G
hx : x ∈ U
hgx : (fun (x : G) ↦ g * x) x ∈ U
⊢ x ∈ U⁻¹

Tactic:
rw [← hUinv] at hx
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : IsDiscrete (↑S : Set G)
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 1) V ∧ V ∩ (↑S : Set G) = {1}
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
hUinv : U⁻¹ = U
hUV : U * U ⊆ V
g : G
hgS : g ∈ S
x : G
hx : x ∈ U
hgx : (fun (x : G) ↦ g * x) x ∈ U
hx₁ : x ∈ U⁻¹
⊢ (fun (x : G) ↦ g * x) x ∈ U

Tactic:
rw [← hUinv] at hx
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : IsDiscrete (↑S : Set G)
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 1) V ∧ V ∩ (↑S : Set G) = {1}
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
hUinv : U⁻¹ = U
hUV : U * U ⊆ V
g : G
hgS : g ∈ S
x : G
hx : x ∈ U⁻¹
hgx : (fun (x : G) ↦ g * x) x ∈ U
⊢ (fun (x1 x2 : G) ↦ x1 * x2) ((fun (x : G) ↦ g * x) x) x⁻¹ = g

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : IsDiscrete (↑S : Set G)
V : Set G
hV : Membership.mem (γ := Filter G) (𝓝 1) V ∧ V ∩ (↑S : Set G) = {1}
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
hUinv : U⁻¹ = U
hUV : U * U ⊆ V
g : G
hgS : g ∈ S
x : G
hx : x ∈ U⁻¹
hgx : (fun (x : G) ↦ g * x) x ∈ U
⊢ g ∈ U * U

Tactic:
exact ⟨_, hgx, _, hx, by simp⟩
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : IsDiscrete (↑S : Set G)
have :
  ∀ (U : Set G) (hU : Membership.mem (γ := Filter G) (𝓝 1) U) (hUinv : U⁻¹ = U)
    (h : ∀ g ∈ S, ((fun (x : G) ↦ g * x) '' U ∩ U).Nonempty → g = 1),
    ∃ (U : Set G),
      Membership.mem (γ := Filter G) (𝓝 1) U ∧ U⁻¹ = U ∧ ∀ g ∈ S, ((fun (x : G) ↦ x * g) '' U ∩ U).Nonempty → g = 1
⊢ ∃ (U : Set G),
    Membership.mem (γ := Filter G) (𝓝 1) U ∧ U⁻¹ = U ∧ ∀ g ∈ S, ((fun (x : G) ↦ x * g) '' U ∩ U).Nonempty → g = 1

Tactic:
have ⟨U, hU, hUinv, h⟩ := hS.exists_nhds_eq_one_of_image_mulLeft_inter_nonempty
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : IsDiscrete (↑S : Set G)
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
hUinv : U⁻¹ = U
h : ∀ g ∈ S, ((fun (x : G) ↦ g * x) '' U ∩ U).Nonempty → g = 1
⊢ ∃ (U : Set G),
    Membership.mem (γ := Filter G) (𝓝 1) U ∧ U⁻¹ = U ∧ ∀ g ∈ S, ((fun (x : G) ↦ x * g) '' U ∩ U).Nonempty → g = 1

Tactic:
⟨U, hU, hUinv, fun g hgS hgU ↦ inv_eq_one.mp (h _ (S.inv_mem hgS) ?_)⟩

Premises used: inv_eq_one, Inv.inv, Subgroup.inv_mem, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : IsDiscrete (↑S : Set G)
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
hUinv : U⁻¹ = U
h : ∀ g ∈ S, ((fun (x : G) ↦ g * x) '' U ∩ U).Nonempty → g = 1
refine :
  ∀ (g : G) (hgS : g ∈ S) (hgU : ((fun (x : G) ↦ x * g) '' U ∩ U).Nonempty), ((fun (x : G) ↦ g⁻¹ * x) '' U ∩ U).Nonempty
⊢ ∃ (U : Set G),
    Membership.mem (γ := Filter G) (𝓝 1) U ∧ U⁻¹ = U ∧ ∀ g ∈ S, ((fun (x : G) ↦ x * g) '' U ∩ U).Nonempty → g = 1

Tactic:
refine ⟨U, hU, hUinv, fun g hgS hgU ↦ inv_eq_one.mp (h _ (S.inv_mem hgS) ?_)⟩
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
S : Subgroup G
hS : IsDiscrete (↑S : Set G)
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
hUinv : U⁻¹ = U
h : ∀ g ∈ S, ((fun (x : G) ↦ g * x) '' U ∩ U).Nonempty → g = 1
g : G
hgS : g ∈ S
hgU : ((fun (x : G) ↦ x * g) '' U ∩ U).Nonempty
rwa : ((fun (x : G) ↦ x * g) '' U⁻¹ ∩ U⁻¹).Nonempty
rwa₁ rwa₂ rwa₃ rwa₄ : ((fun (x : G) ↦ x * g) '' U ∩ U).Nonempty
⊢ ((fun (x : G) ↦ g⁻¹ * x) '' U ∩ U).Nonempty

Tactic:
rwa [Set.nonempty_image_mulLeft_inv_inter_iff, hUinv]

Premises used: Set.nonempty_image_mulLeft_inv_inter_iff
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
suffices : WeaklyLocallyCompactSpace G
⊢ LocallyCompactSpace G

Tactic:
suffices WeaklyLocallyCompactSpace G from inferInstance
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
⊢ WeaklyLocallyCompactSpace G

Tactic:
⟨fun y ↦ ⟨(y * x⁻¹) • K, ?_, ?_⟩⟩

Premises used: WeaklyLocallyCompactSpace.mk, HMul.hMul, Inv.inv, And.intro, Exists.intro, HSMul.hSMul
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
refine_1 : ∀ (y : G), IsCompact ((y * x⁻¹) • K)
refine_2 : ∀ (y : G), (y * x⁻¹) • K ∈ 𝓝 y
⊢ WeaklyLocallyCompactSpace G

Tactic:
refine ⟨fun y ↦ ⟨(y * x⁻¹) • K, ?_, ?_⟩⟩
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
⊢ IsCompact ((y * x⁻¹) • K)

Tactic:
hK.smul _

Premises used: IsCompact.smul
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
⊢ IsCompact ((y * x⁻¹) • K)

Tactic:
exact hK.smul _

Premises used: IsCompact.smul
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
refine_2 : (fun (x_1 : G) ↦ (y * x⁻¹)⁻¹ • x_1) ⁻¹' K ∈ 𝓝 y
⊢ (y * x⁻¹) • K ∈ 𝓝 y

Tactic:
rw [← preimage_smul_inv]

Premises used: Set.preimage_smul_inv
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
⊢ K ∈ 𝓝 ((y * x⁻¹)⁻¹ • y)

Tactic:
simpa using h
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
⊢ (fun (x_1 : G) ↦ (y * x⁻¹)⁻¹ • x_1) ⁻¹' K ∈ 𝓝 y

Tactic:
exact (continuous_const_smul _).continuousAt.preimage_mem_nhds (by simpa using h)

Premises used: ContinuousConstSMul.continuous_const_smul, ContinuousAt.preimage_mem_nhds, Continuous.continuousAt
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : TopologicalSpace α
inst_4 : Zero α
inst_5 : T1Space α
f : G → α
k : Set G
hk : IsCompact k
hf : support f ⊆ k
h'f : Continuous[inst, inst_3] f
⊢ f = 0 ∨ LocallyCompactSpace G

Tactic:
or_iff_not_imp_left.mpr fun h => ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_left
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : TopologicalSpace α
inst_4 : Zero α
inst_5 : T1Space α
f : G → α
k : Set G
hk : IsCompact k
hf : support f ⊆ k
h'f : Continuous[inst, inst_3] f
refine : ∀ (h : ¬f = 0), LocallyCompactSpace G
⊢ f = 0 ∨ LocallyCompactSpace G

Tactic:
refine or_iff_not_imp_left.mpr fun h => ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_left
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : TopologicalSpace α
inst_4 : Zero α
inst_5 : T1Space α
f : G → α
k : Set G
hk : IsCompact k
hf : support f ⊆ k
h'f : Continuous[inst, inst_3] f
h : ¬f = 0
⊢ ¬∀ (x : G), f x = 0

Tactic:
simp_rw [funext_iff, Pi.zero_apply] at h

Premises used: funext_iff, Pi.zero_apply
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : TopologicalSpace α
inst_4 : Zero α
inst_5 : T1Space α
f : G → α
k : Set G
hk : IsCompact k
hf : support f ⊆ k
h'f : Continuous[inst, inst_3] f
h : ¬∀ (x : G), f x = 0
⊢ ∃ (x : G), f x ≠ 0

Tactic:
push Not at h

Premises used: Not
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : TopologicalSpace α
inst_4 : Zero α
inst_5 : T1Space α
f : G → α
k : Set G
hk : IsCompact k
hf : support f ⊆ k
h'f : Continuous[inst, inst_3] f
h : ∃ (x : G), f x ≠ 0
⊢ ∃ (x : G), f x ≠ 0

Tactic:
h
-- Module: Mathlib.Topology.Algebra.Group.Pointwise
Goal:
G : Type w
α : Type u
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : TopologicalSpace α
inst_4 : Zero α
inst_5 : T1Space α
f : G → α
k : Set G
hk : IsCompact k
hf : support f ⊆ k
h'f : Continuous[inst, inst_3] f
h : ∃ (x : G), f x ≠ 0
obtain : ∀ (x : G) (hx : f x ≠ 0), LocallyCompactSpace G
⊢ LocallyCompactSpace G

Tactic:
obtain ⟨x, hx⟩ : ∃ x, f x ≠ 0 := h