awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
K : Set G
hK : IsCompact K
this : IsClosed[inst] (K * closure[inst] {1})
⊢ closure[inst] K ⊆ K * closure[inst] {1}
have rw : K ⊆ K * closure[inst] {1}
Tactic: rw [IsClosed.closure_subset_iff this]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
F : Set G
hF : IsClosed[inst] F
⊢ F * closure[inst] {1} = F
have refine : F * closure[inst] {1} ⊆ F
Tactic: refine Subset.antisymm ?_ (subset_mul_closure_one F)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
F : Set G
hF : IsClosed[inst] F
⊢ F * closure[inst] {1} = closure[inst] F * closure[inst] {1}
have rw : F * closure[inst] {1} = F * closure[inst] {1}
Tactic: rw [hF.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
F : Set G
hF : IsClosed[inst] F
⊢ F * closure[inst] {1} ⊆ F
have F₁ : F * closure[inst] {1} = closure[inst] F * closure[inst] {1}
Tactic: calc
  F * (closure {1} : Set G) = closure F * closure ({1} : Set G) := by rw [hF.closure_eq]
  _ ⊆ closure (F * ({1} : Set G)) := smul_set_closure_subset _ _
  _ = F := by simp
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
F : Set G
hF : IsClosed[inst] F
F₁ : F * closure[inst] {1} = closure[inst] F * closure[inst] {1}
⊢ F * closure[inst] {1} ⊆ F
have F₂ : closure[inst] (F * {1}) = F
Tactic: calc
  F * (closure {1} : Set G) = closure F * closure ({1} : Set G) := by rw [hF.closure_eq]
  _ ⊆ closure (F * ({1} : Set G)) := smul_set_closure_subset _ _
  _ = F := by simp
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
t : Set G
ht : t * closure[inst] {1} = t
⊢ tᶜ * closure[inst] {1} = tᶜ
have refine : tᶜ * closure[inst] {1} ⊆ tᶜ
Tactic: refine Subset.antisymm ?_ (subset_mul_closure_one tᶜ)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
t : Set G
ht : t * closure[inst] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : Membership.mem (γ := Set G) (closure[inst] {1}) g
⊢ (fun (x1 x2 : G) ↦ x1 * x2) x g ∈ tᶜ
have by_contra : ∀ (H : (fun (x1 x2 : G) ↦ x1 * x2) x g ∉ tᶜ), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
t : Set G
ht : t * closure[inst] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : Membership.mem (γ := Set G) (closure[inst] {1}) g
H : (fun (x1 x2 : G) ↦ x1 * x2) x g ∉ tᶜ
⊢ x ∈ t * closure[inst] {1}
have rw : ∀ (hg : g ∈ (↑(Subgroup.topologicalClosure ⊥) : Set G)) (H : (fun (x1 x2 : G) ↦ x1 * x2) x g ∉ tᶜ),
  x ∈ t * (↑(Subgroup.topologicalClosure ⊥) : Set G)
Tactic: rw [← Subgroup.coe_topologicalClosure_bot G] at hg ⊢
Cleared hypotheses: hg, H
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (hypothesis)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
t : Set G
ht : t * closure[inst] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : g ∈ (↑(Subgroup.topologicalClosure ⊥) : Set G)
H : (fun (x1 x2 : G) ↦ x1 * x2) x g ∉ tᶜ
⊢ x ∈ t * (↑(Subgroup.topologicalClosure ⊥) : Set G)
have H₁ : x * g ∈ t
Tactic: simp only [mem_compl_iff, not_not] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (hypothesis)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
t : Set G
ht : t * closure[inst] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : Membership.mem (γ := Set G) (closure[inst] {1}) g
H : (fun (x1 x2 : G) ↦ x1 * x2) x g ∉ tᶜ
⊢ False
have this : x ∈ t * closure[inst] {1}
Tactic: have : x ∈ t * (closure {1} : Set G) := by
    rw [← Subgroup.coe_topologicalClosure_bot G] at hg ⊢
    simp only [mem_compl_iff, not_not] at H
    exact ⟨x * g, H, g⁻¹, Subgroup.inv_mem _ hg, by simp⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (hypothesis)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
t : Set G
ht : t * closure[inst] {1} = t
x : G
hx : x ∈ tᶜ
g : G
hg : Membership.mem (γ := Set G) (closure[inst] {1}) g
H : (fun (x1 x2 : G) ↦ x1 * x2) x g ∉ tᶜ
this : x ∈ t * closure[inst] {1}
⊢ False
have this₁ : x ∈ t
Tactic: rw [ht] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (hypothesis)
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
x : G
hx : x ∈ closure[inst] U
⊢ x ∈ U * U
have hx₁ : ∀ t ∈ 𝓝 x, (t ∩ U).Nonempty
Tactic: rw [mem_closure_iff_nhds] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (hypothesis)
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
x : G
hx : ∀ t ∈ 𝓝 x, (t ∩ U).Nonempty
⊢ x ∈ U * U
have hkey : (fun (y : G) ↦ x / y) ⁻¹' U ∈ 𝓝 x
Tactic: have hkey : (fun y => x / y) ⁻¹' U ∈ 𝓝 x :=
    ContinuousAt.preimage_mem_nhds (by fun_prop) (by simpa)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
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
x : G
hx : ∀ t ∈ 𝓝 x, (t ∩ U).Nonempty
hkey : (fun (y : G) ↦ x / y) ⁻¹' U ∈ 𝓝 x
⊢ x ∈ U * U
have obtain : ∀ (a : G) (ha_mem : Membership.mem (γ := Set G) ((fun (y : G) ↦ x / y) ⁻¹' U) a) (ha_s : a ∈ U), x ∈ U * U
Tactic: obtain ⟨a, ha_mem, ha_s⟩ := hx _ hkey
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
Goal:
G : Type w
H : Type x
α : Type u
β : Type v
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
⊢ RegularSpace G
have refine : ∀ (a : G) (s : Set G) (hs : s ∈ 𝓝 a), ∃ t ∈ 𝓝 a, IsClosed[inst] t ∧ t ⊆ s
Tactic: refine .of_exists_mem_nhds_isClosed_subset fun a s hs ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (hypothesis)
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
⊢ ∃ t ∈ 𝓝 a, IsClosed[inst] t ∧ t ⊆ s
have this : Tendsto (fun (p : G × G) ↦ p.1 * p.2) (𝓝 (a, 1)) (𝓝 a)
Tactic: have : Tendsto (fun p : G × G => p.1 * p.2) (𝓝 (a, 1)) (𝓝 a) :=
    continuous_mul.tendsto' _ _ (mul_one a)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
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)
⊢ ∃ t ∈ 𝓝 a, IsClosed[inst] t ∧ t ⊆ s
have rcases : ∀ (U : Set G) (hU : U ∈ 𝓝 a) (V : Set G) (hV : Membership.mem (γ := Filter G) (𝓝 1) V)
  (hUV : U ×ˢ V ⊆ (fun (p : G × G) ↦ p.1 * p.2) ⁻¹' s), ∃ t ∈ 𝓝 a, IsClosed[inst] t ∧ t ⊆ s
Tactic: rcases mem_nhds_prod_iff.mp (this hs) with ⟨U, hU, V, hV, hUV⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (hypothesis)
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 : U ×ˢ V ⊆ (fun (p : G × G) ↦ p.1 * p.2) ⁻¹' s
⊢ ∃ t ∈ 𝓝 a, IsClosed[inst] t ∧ t ⊆ s
have hUV₁ : image2 HMul.hMul U V ⊆ s
Tactic: rw [← image_subset_iff, image_prod] at hUV
Cleared hypotheses: hUV
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
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
⊢ ∃ t ∈ 𝓝 a, IsClosed[inst] t ∧ t ⊆ s
have refine : closure[inst] U ⊆ s
Tactic: refine ⟨closure U, mem_of_superset hU subset_closure, isClosed_closure, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
Goal:
G : Type w
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
x y : G
⊢ Inseparable x y ↔ Membership.mem (γ := Set G) (closure[inst] 1) (x / y)
have rw : Inseparable (X := G) ((Homeomorph.mulRight y⁻¹ : (a : G) → G) x : G) ((Homeomorph.mulRight y⁻¹ : (a : G) → G) y : G) ↔
  Inseparable (x / y) 1
Tactic: rw [← singleton_one, ← specializes_iff_mem_closure, specializes_comm, specializes_iff_inseparable,
    ← (Homeomorph.mulRight y⁻¹).isEmbedding.inseparable_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
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
⊢ T2Space G
have suffices : T1Space G
Tactic: suffices T1Space G from inferInstance
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
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
have refine : ∀ (x y : G) (hspec : x ⤳ y) (hne : ¬x = y), False
Tactic: refine t1Space_iff_specializes_imp_eq.2 fun x y hspec ↦ by_contra fun hne ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
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
⊢ x * y⁻¹ ≠ 1
have rwa : ¬x * y⁻¹ = 1
Tactic: rwa [Ne, mul_inv_eq_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
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
⊢ False
have rcases : ∀ (U : Set G) (hU₁ : Membership.mem (γ := Filter G) (𝓝 1) U) (hU : x * y⁻¹ ∉ U), False
Tactic: rcases H (x * y⁻¹) (by rwa [Ne, mul_inv_eq_one]) with ⟨U, hU₁, hU⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
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), Membership.mem (γ := Filter G) (𝓝 1) V ∧ IsClosed[inst] V ∧ V⁻¹ = V ∧ V * V ⊆ U
have 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
Tactic: rcases exists_open_nhds_one_mul_subset hU with ⟨V, V_open, V_mem, hV⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
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
⊢ ∃ (V : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ IsClosed[inst] V ∧ V⁻¹ = V ∧ V * V ⊆ U
have 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
Tactic: rcases exists_mem_nhds_isClosed_subset (V_open.mem_nhds V_mem) with ⟨W, W_mem, W_closed, hW⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
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 : Set G), Membership.mem (γ := Filter G) (𝓝 1) V ∧ IsClosed[inst] V ∧ V⁻¹ = V ∧ V * V ⊆ U
have refine : W ∩ W⁻¹ * (W ∩ W⁻¹) ⊆ 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], ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
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),
    Membership.mem (γ := Filter G) (𝓝 1) U ∧ U⁻¹ = U ∧ ∀ g ∈ S, ((fun (x : G) ↦ g * x) '' U ∩ U).Nonempty → g = 1
have 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
Tactic: obtain ⟨V, hV⟩ := nhds_inter_eq_singleton_of_mem_discrete hS S.one_mem
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
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),
    Membership.mem (γ := Filter G) (𝓝 1) U ∧ U⁻¹ = U ∧ ∀ g ∈ S, ((fun (x : G) ↦ g * x) '' U ∩ U).Nonempty → g = 1
have 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
Tactic: obtain ⟨U, hU, -, hUinv, hUV⟩ := exists_closed_nhds_one_inv_eq_mul_subset hV.1
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
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
have refine : ∀ (g : G) (hgS : g ∈ S), ((fun (x : G) ↦ g * x) '' U ∩ U).Nonempty → g = 1
Tactic: refine ⟨U, hU, hUinv, fun g hgS ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
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
have refine : g ∈ U * U
Tactic: refine hV.2.subset ⟨hUV ?_, hgS⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (hypothesis)
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
have hx₁ : x ∈ U⁻¹
Tactic: rw [← hUinv] at hx
Cleared hypotheses: hx, hgx
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
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),
    Membership.mem (γ := Filter G) (𝓝 1) U ∧ U⁻¹ = U ∧ ∀ g ∈ S, ((fun (x : G) ↦ x * g) '' U ∩ U).Nonempty → g = 1
have 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
Tactic: have ⟨U, hU, hUinv, h⟩ := hS.exists_nhds_eq_one_of_image_mulLeft_inter_nonempty
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
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
have refine : ∀ (g : G) (hgS : g ∈ S) (hgU : ((fun (x : G) ↦ x * g) '' U ∩ U).Nonempty), ((fun (x : G) ↦ g⁻¹ * x) '' U ∩ U).Nonempty
Tactic: refine ⟨U, hU, hUinv, fun g hgS hgU ↦ inv_eq_one.mp (h _ (S.inv_mem hgS) ?_)⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
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
⊢ ((fun (x : G) ↦ g⁻¹ * x) '' U ∩ U).Nonempty
have rwa : ((fun (x : G) ↦ x * g) '' U⁻¹ ∩ U⁻¹).Nonempty
Tactic: rwa [Set.nonempty_image_mulLeft_inv_inter_iff, hUinv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
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
⊢ LocallyCompactSpace G
have suffices : WeaklyLocallyCompactSpace G
Tactic: suffices WeaklyLocallyCompactSpace G from inferInstance
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
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
have refine_1 : ∀ (y : G), IsCompact ((y * x⁻¹) • K)
Tactic: refine ⟨fun y ↦ ⟨(y * x⁻¹) • K, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
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)
⊢ WeaklyLocallyCompactSpace G
have refine_2 : ∀ (y : G), (y * x⁻¹) • K ∈ 𝓝 y
Tactic: refine ⟨fun y ↦ ⟨(y * x⁻¹) • K, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
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
⊢ (y * x⁻¹) • K ∈ 𝓝 y
have refine_2 : (fun (x_1 : G) ↦ (y * x⁻¹)⁻¹ • x_1) ⁻¹' K ∈ 𝓝 y
Tactic: rw [← preimage_smul_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
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
have refine : ∀ (h : ¬f = 0), LocallyCompactSpace G
Tactic: refine or_iff_not_imp_left.mpr fun h => ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (hypothesis)
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
⊢ LocallyCompactSpace G
have h₁ : ¬∀ (x : G), f x = 0
Tactic: simp_rw [funext_iff, Pi.zero_apply] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (hypothesis)
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
⊢ LocallyCompactSpace G
have h₁ : ∃ (x : G), f x ≠ 0
Tactic: push Not at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
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
⊢ LocallyCompactSpace G
have obtain : ∀ (x : G) (hx : f x ≠ 0), LocallyCompactSpace G
Tactic: obtain ⟨x, hx⟩ : ∃ x, f x ≠ 0 := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (hypothesis)
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
x : G
hx : f x ≠ 0
⊢ LocallyCompactSpace G
have this : k ∈ 𝓝 x
Tactic: have : k ∈ 𝓝 x :=
    mem_of_superset (h'f.isOpen_support.mem_nhds hx) hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Quotient (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
N : Subgroup G
s : Set G
⊢ Dense (X := G ⧸ N) (mk '' s) ↔ Dense (s * (↑N : Set G))
have rw : Dense (Set.preimage (β := G ⧸ N) mk (mk '' s)) ↔ Dense (s * (↑N : Set G))
Tactic: rw [← dense_preimage_mk, preimage_image_mk_eq_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Quotient (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
N : Subgroup G
s : Set G
rw : Dense (Set.preimage (β := G ⧸ N) mk (mk '' s)) ↔ Dense (s * (↑N : Set G))
⊢ Dense (X := G ⧸ N) (mk '' s) ↔ Dense (s * (↑N : Set G))
have rw₁ : Dense (s * (↑N : Set G)) ↔ Dense (s * (↑N : Set G))
Tactic: rw [← dense_preimage_mk, preimage_image_mk_eq_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Quotient (goal)
Goal:
G_1 : Type u_1
inst : TopologicalSpace G_1
inst_1 : Group G_1
inst_2 : SeparatelyContinuousMul G_1
N_1 : Subgroup G_1
G : Type u_2
inst_3 : Group G
inst_4 : TopologicalSpace G
inst_5 : ContinuousMul G
N : Subgroup G
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpace N] fun (p : G × G ⧸ N) ↦ p.1 • p.2
have rw : Continuous[instTopologicalSpaceProd, instTopologicalSpace N] ((fun (p : G × G ⧸ N) ↦ p.1 • p.2) ∘ Prod.map id mk)
Tactic: rw [← (IsOpenQuotientMap.id.prodMap isOpenQuotientMap_mk).continuous_comp_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Quotient (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
N : Subgroup G
γ : G
⊢ Continuous[instTopologicalSpace N, instTopologicalSpace N] fun (x : G ⧸ N) ↦ γ • x
have rw : Continuous[inst, instTopologicalSpace N] ((fun (x : G ⧸ N) ↦ γ • x) ∘ mk)
Tactic: rw [← isOpenQuotientMap_mk.continuous_comp_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Quotient (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
N : Subgroup G
⊢ T1Space.{u_1} (G ⧸ N) ↔ IsClosed[inst] (↑N : Set G)
have rw : IsClosed[inst] (Set.preimage (β := G ⧸ N) Quotient.mk' {(↑1 : G ⧸ N)}) ↔
  IsClosed[inst] (Set.preimage (β := G ⧸ N) mk {(↑1 : G ⧸ N)})
Tactic: rw [← QuotientGroup.preimage_mk_one, MulAction.IsPretransitive.t1Space_iff G (mk 1),
      isClosed_coinduced]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Quotient (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : SeparatelyContinuousMul G
N : Subgroup G
⊢ DiscreteTopology.{u_1} (G ⧸ N) ↔ IsOpen[inst] (↑N : Set G)
have rw : IsOpen[inst] (Set.preimage (β := G ⧸ N) Quotient.mk' {(↑1 : G ⧸ N)}) ↔
  IsOpen[inst] (Set.preimage (β := G ⧸ N) mk {(↑1 : G ⧸ N)})
Tactic: rw [← QuotientGroup.preimage_mk_one, MulAction.IsPretransitive.discreteTopology_iff G (mk 1),
      isOpen_coinduced]