awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, Subtype.mk (p := fun (x : G) ↦ x ∈ s) g hg))).Nonempty
I : (interior (HSMul.hSMul (β := Set X) (g • V) {x})).Nonempty
g' : G
hg' : g' ∈ V
hy : g' • x ∈ interior (HSMul.hSMul (β := Set X) V {x})
J : HSMul.hSMul (β := Set X) (g'⁻¹ • V) {x} ∈ 𝓝 x
⊢ V⁻¹ • V ⊆ U
have rw : V • V ⊆ U
Tactic: rw [V_symm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (hypothesis)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
U : Set G
hU : Membership.mem (γ := Filter G) (𝓝 1) U
x : X
V : Set G
V_mem : Membership.mem (γ := Filter G) (𝓝 1) V
V_closed : IsClosed[inst] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : Eq.{u_1 + 1} (α := Set G) (⋃ g ∈ s, g • V) univ
K : ℕ → Set G := compactCovering G
F : ℕ × (↑s : Type u_1) → Set X := fun (p : ℕ × (↑s : Type u_1)) ↦ HSMul.hSMul (β := Set X) (K p.1 ∩ (↑p.2 : G) • V) {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, Subtype.mk (p := fun (x : G) ↦ x ∈ s) g hg))).Nonempty
I : (interior (HSMul.hSMul (β := Set X) (g • V) {x})).Nonempty
g' : G
hg' : g' ∈ V
hy : g' • x ∈ interior (HSMul.hSMul (β := Set X) V {x})
J : HSMul.hSMul (β := Set X) (g'⁻¹ • V) {x} ∈ 𝓝 x
⊢ HSMul.hSMul (β := Set X) U {x} ∈ 𝓝 x
have this : HSMul.hSMul (β := Set X) (g'⁻¹ • V) {x} ⊆ HSMul.hSMul (β := Set X) U {x}
Tactic: have : (g'⁻¹ • V) • {x} ⊆ U • ({x} : Set X) := by
    apply smul_subset_smul_right
    apply Subset.trans (smul_set_subset_smul (inv_mem_inv.2 hg')) ?_
    rw [V_symm]
    exact VU
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
x : X
⊢ IsOpenMap.{u_1, u_2} (Y := X) fun (g : G) ↦ g • x
have simp_rw : ∀ (x_1 : G), ∀ s ∈ 𝓝 x_1, (fun (g : G) ↦ g • x) '' s ∈ 𝓝 (x_1 • x)
Tactic: simp_rw [isOpenMap_iff_nhds_le, Filter.le_map_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
x : X
g : G
U : Set G
hU : U ∈ 𝓝 g
⊢ Eq (α := G → X) (fun (x_1 : G) ↦ x_1 • x) ((fun (x_1 : G) ↦ x_1 • g • x) ∘ fun (x : G) ↦ x * g⁻¹)
have h : ∀ (g_1 : G), g_1 • x = ((fun (x_1 : G) ↦ x_1 • g • x) ∘ fun (x : G) ↦ x * g⁻¹) g_1
Tactic: ext g
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (hypothesis)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
x : X
g : G
U : Set G
hU : U ∈ 𝓝 g
⊢ (fun (g : G) ↦ g • x) '' U ∈ 𝓝 (g • x)
have this : Eq (α := G → X) (fun (x_1 : G) ↦ x_1 • x) ((fun (x_1 : G) ↦ x_1 • g • x) ∘ fun (x : G) ↦ x * g⁻¹)
Tactic: have : (· • x) = (· • (g • x)) ∘ (· * g⁻¹) := by
    ext g
    simp [smul_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
x : X
g : G
U : Set G
hU : U ∈ 𝓝 g
this : Eq (α := G → X) (fun (x_1 : G) ↦ x_1 • x) ((fun (x_1 : G) ↦ x_1 • g • x) ∘ fun (x : G) ↦ x * g⁻¹)
⊢ (fun (g : G) ↦ g • x) '' U ∈ 𝓝 (g • x)
have rw : HSMul.hSMul (α := Set G) (β := Set X) ((fun (x : G) ↦ x * g⁻¹) '' U) {g • x} ∈ 𝓝 (g • x)
Tactic: rw [this, image_comp, ← smul_singleton]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace G
inst_1 : TopologicalSpace X
inst_2 : Group G
inst_3 : IsTopologicalGroup G
inst_4 : MulAction G X
inst_5 : SigmaCompactSpace G
inst_6 : BaireSpace X
inst_7 : T2Space X
inst_8 : ContinuousSMul G X
inst_9 : IsPretransitive G X
x : X
g : G
U : Set G
hU : U ∈ 𝓝 g
this : Eq (α := G → X) (fun (x_1 : G) ↦ x_1 • x) ((fun (x_1 : G) ↦ x_1 • g • x) ∘ fun (x : G) ↦ x * g⁻¹)
⊢ HSMul.hSMul (α := Set G) (β := Set X) ((fun (x : G) ↦ x * g⁻¹) '' U) {g • x} ∈ 𝓝 (g • x)
have hU₁ : Membership.mem (γ := Filter G) (𝓝 1) ((fun (x : G) ↦ x * g⁻¹) '' U)
Tactic: apply smul_singleton_mem_nhds_of_sigmaCompact
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : SigmaCompactSpace G
H : Type u_3
inst_4 : Group H
inst_5 : TopologicalSpace H
inst_6 : BaireSpace H
inst_7 : T2Space H
inst_8 : ContinuousMul H
f : G →* H
hf : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
h'f : Continuous[inst, inst_5] (⇑f : (a : G) → H)
A : MulAction G H := MulAction.compHom H f
⊢ IsOpenMap.{u_1, u_3} (X := G) (Y := H) (⇑f : (a : G) → H)
have this : ContinuousSMul G H
Tactic: have : ContinuousSMul G H := continuousSMul_compHom h'f
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : SigmaCompactSpace G
H : Type u_3
inst_4 : Group H
inst_5 : TopologicalSpace H
inst_6 : BaireSpace H
inst_7 : T2Space H
inst_8 : ContinuousMul H
f : G →* H
hf : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
h'f : Continuous[inst, inst_5] (⇑f : (a : G) → H)
A : MulAction G H := MulAction.compHom H f
this : ContinuousSMul G H
⊢ IsOpenMap.{u_1, u_3} (X := G) (Y := H) (⇑f : (a : G) → H)
have this₁ : IsPretransitive G H
Tactic: have : IsPretransitive G H := isPretransitive_compHom hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (hypothesis)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : SigmaCompactSpace G
H : Type u_3
inst_4 : Group H
inst_5 : TopologicalSpace H
inst_6 : BaireSpace H
inst_7 : T2Space H
inst_8 : ContinuousMul H
f : G →* H
hf : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
h'f : Continuous[inst, inst_5] (⇑f : (a : G) → H)
A : MulAction G H := MulAction.compHom H f
this_1 : ContinuousSMul G H
this : IsPretransitive G H
⊢ IsOpenMap.{u_1, u_3} (X := G) (Y := H) (⇑f : (a : G) → H)
have this₁ : Eq (α := (a : G) → H) (⇑f : (a : G) → H) fun (g : G) ↦ HSMul.hSMul (β := H) g 1
Tactic: have : f = (fun (g : G) ↦ g • (1 : H)) := by simp [A, MulAction.compHom_smul_def]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.OpenMapping (goal)
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : SigmaCompactSpace G
H : Type u_3
inst_4 : Group H
inst_5 : TopologicalSpace H
inst_6 : BaireSpace H
inst_7 : T2Space H
inst_8 : ContinuousMul H
f : G →* H
hf : Surjective.{u_1 + 1, u_3 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
h'f : Continuous[inst, inst_5] (⇑f : (a : G) → H)
A : MulAction G H := MulAction.compHom H f
this_1 : ContinuousSMul G H
this_2 : IsPretransitive G H
this : Eq (α := (a : G) → H) (⇑f : (a : G) → H) fun (g : G) ↦ HSMul.hSMul (β := H) g 1
⊢ IsOpenMap.{u_1, u_3} (X := G) (Y := H) (⇑f : (a : G) → H)
have rw : IsOpenMap.{u_1, u_3} (Y := H) fun (g : G) ↦ HSMul.hSMul (β := H) g 1
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (hypothesis)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Group α
inst_3 : MulAction α β
inst_4 : ContinuousInv α
inst_5 : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed[inst_1] t
hs : IsCompact s
Φ : Prod.{u, v} (↑s : Type u) β ≃ₜ Prod.{u, v} (↑s : Type u) β :=
  { toFun := fun (gx : Prod.{u, v} (↑s : Type u) β) ↦ (gx.1, (↑gx.1 : α) • gx.2),
    invFun := fun (gx : Prod.{u, v} (↑s : Type u) β) ↦ (gx.1, (↑gx.1 : α)⁻¹ • gx.2), left_inv := ⋯, right_inv := ⋯,
    continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ IsClosed[inst_1] (s • t)
have this : s • t =
  image (α := Prod.{u, v} (↑s : Type u) β)
    (comp (β := Prod.{u, v} (↑s : Type u) β) snd (⇑Φ : (a : (↑s : Type u) × β) → (↑s : Type u) × β)) (snd ⁻¹' t)
Tactic: have : s • t = (snd ∘ Φ) '' snd ⁻¹' t :=
    subset_antisymm
      (smul_subset_iff.mpr fun g hg x hx ↦ mem_image_of_mem (snd ∘ Φ) (x := ⟨⟨g, hg⟩, x⟩) hx)
      (image_subset_iff.mpr fun ⟨⟨g, hg⟩, x⟩ hx ↦ smul_mem_smul hg hx)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Group α
inst_3 : MulAction α β
inst_4 : ContinuousInv α
inst_5 : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed[inst_1] t
hs : IsCompact s
Φ : Prod.{u, v} (↑s : Type u) β ≃ₜ Prod.{u, v} (↑s : Type u) β :=
  { toFun := fun (gx : Prod.{u, v} (↑s : Type u) β) ↦ (gx.1, (↑gx.1 : α) • gx.2),
    invFun := fun (gx : Prod.{u, v} (↑s : Type u) β) ↦ (gx.1, (↑gx.1 : α)⁻¹ • gx.2), left_inv := ⋯, right_inv := ⋯,
    continuous_toFun := ⋯, continuous_invFun := ⋯ }
this :
  s • t =
    image (α := Prod.{u, v} (↑s : Type u) β)
      (comp (β := Prod.{u, v} (↑s : Type u) β) snd (⇑Φ : (a : (↑s : Type u) × β) → (↑s : Type u) × β)) (snd ⁻¹' t)
⊢ IsClosed[inst_1] (s • t)
have rw : IsClosed[inst_1]
  (image (α := Prod.{u, v} (↑s : Type u) β)
    (comp (β := Prod.{u, v} (↑s : Type u) β) snd (⇑Φ : (a : (↑s : Type u) × β) → (↑s : Type u) × β)) (snd ⁻¹' t))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (hypothesis)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Group α
inst_3 : MulAction α β
inst_4 : ContinuousInv α
inst_5 : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed[inst_1] t
hs : IsCompact s
Φ : Prod.{u, v} (↑s : Type u) β ≃ₜ Prod.{u, v} (↑s : Type u) β :=
  { toFun := fun (gx : Prod.{u, v} (↑s : Type u) β) ↦ (gx.1, (↑gx.1 : α) • gx.2),
    invFun := fun (gx : Prod.{u, v} (↑s : Type u) β) ↦ (gx.1, (↑gx.1 : α)⁻¹ • gx.2), left_inv := ⋯, right_inv := ⋯,
    continuous_toFun := ⋯, continuous_invFun := ⋯ }
this :
  s • t =
    image (α := Prod.{u, v} (↑s : Type u) β)
      (comp (β := Prod.{u, v} (↑s : Type u) β) snd (⇑Φ : (a : (↑s : Type u) × β) → (↑s : Type u) × β)) (snd ⁻¹' t)
⊢ IsClosed[inst_1]
    (image (α := Prod.{u, v} (↑s : Type u) β)
      (comp (β := Prod.{u, v} (↑s : Type u) β) snd (⇑Φ : (a : (↑s : Type u) × β) → (↑s : Type u) × β)) (snd ⁻¹' t))
have this₁ : CompactSpace.{u} (↑s : Type u)
Tactic: have : CompactSpace s := isCompact_iff_compactSpace.mp hs
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Group α
inst_3 : MulAction α β
inst_4 : ContinuousInv α
inst_5 : ContinuousSMul α β
inst_6 : CompactSpace α
t : Set β
ht : IsClosed[inst_1] t
⊢ IsClosed[instTopologicalSpaceQuotient] (Quotient.mk' '' t)
have rw : IsClosed[inst_1] (⋃ (g : α), (fun (x : β) ↦ g • x) '' t)
Tactic: rw [← isQuotientMap_quotient_mk'.isClosed_preimage,
    MulAction.quotient_preimage_image_eq_union_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Group α
inst_3 : MulAction α β
inst_4 : ContinuousInv α
inst_5 : ContinuousSMul α β
inst_6 : CompactSpace α
t : Set β
ht : IsClosed[inst_1] t
⊢ IsClosed[inst_1] (⋃ (g : α), (fun (x : β) ↦ g • x) '' t)
have h : ⋃ (g : α), (fun (x : β) ↦ g • x) '' t = HSMul.hSMul.{u, v, v} (α := Set α) univ t
Tactic: convert! ht.smul_left_of_isCompact (isCompact_univ (X := α))
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Group α
inst_3 : MulAction α β
inst_4 : ContinuousInv α
inst_5 : ContinuousSMul α β
inst_6 : CompactSpace α
t : Set β
ht : IsClosed[inst_1] t
⊢ ⋃ (g : α), (fun (x : β) ↦ g • x) '' t = HSMul.hSMul.{u, v, v} (α := Set α) univ t
have h : Eq.{v + 1} (α := Set β) (⋃ (x : α), ⋃ (_ : Membership.mem (γ := Set α) univ x), (fun (x_1 : β) ↦ x • x_1) '' t)
  (⋃ (a : α), ⋃ (_ : Membership.mem (γ := Set α) univ a), a • t)
Tactic: rw [← biUnion_univ, ← iUnion_smul_left_image]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : ContinuousConstSMul α α
s : Set α
a b : α
h : s ∈ 𝓝 b
⊢ {a} * s ∈ 𝓝 (a * b)
have rwa : {a} * s ∈ 𝓝 (a • b)
Tactic: rwa [← smul_eq_mul, ← smul_eq_mul, singleton_smul, smul_mem_nhds_smul_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : ContinuousConstSMul α α
s : Set α
a b : α
h : s ∈ 𝓝 b
rwa : {a} * s ∈ 𝓝 (a • b)
⊢ {a} * s ∈ 𝓝 (a * b)
have rwa₁ : HSMul.hSMul (α := Set α) {a} s ∈ 𝓝 (a • b)
Tactic: rwa [← smul_eq_mul, ← smul_eq_mul, singleton_smul, smul_mem_nhds_smul_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : ContinuousConstSMul α α
s : Set α
a b : α
h : s ∈ 𝓝 b
rwa : {a} * s ∈ 𝓝 (a • b)
rwa₁ : HSMul.hSMul (α := Set α) {a} s ∈ 𝓝 (a • b)
⊢ {a} * s ∈ 𝓝 (a * b)
have rwa₂ : a • s ∈ 𝓝 (a • b)
Tactic: rwa [← smul_eq_mul, ← smul_eq_mul, singleton_smul, smul_mem_nhds_smul_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : ContinuousConstSMul αᵐᵒᵖ α
s t : Set α
hs : IsOpen[inst] s
⊢ IsOpen[inst] (s * t)
have rw : IsOpen[inst] (op '' t • s)
Tactic: rw [← image_op_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Group α
inst_2 : ContinuousConstSMul αᵐᵒᵖ α
s : Set α
a b : α
h : s ∈ 𝓝 b
⊢ s * {a} ∈ 𝓝 (b * a)
have rw : (fun (x : α) ↦ x * a) '' s ∈ 𝓝 (b * a)
Tactic: rw [mul_singleton]
-- 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 t : Set G
ht : IsOpen[inst] t
⊢ IsOpen[inst] (s / t)
have rw : IsOpen[inst] (⋃ a ∈ s, (fun (x : G) ↦ a / x) '' t)
Tactic: rw [← iUnion_div_left_image]
-- 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 t : Set G
hs : IsOpen[inst] s
⊢ IsOpen[inst] (s / t)
have rw : IsOpen[inst] (⋃ a ∈ t, (fun (x : G) ↦ x / a) '' s)
Tactic: rw [← iUnion_div_right_image]
-- 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 : Set G
hs : IsOpen[inst] s
t : Set G
⊢ s * closure[inst] t = s * t
have refine : ∀ (a : G) (ha : a ∈ s) (b : G) (hb : b ∈ closure[inst] t), a * b ∈ s * t
Tactic: refine (mul_subset_iff.2 fun a ha b hb => ?_).antisymm (mul_subset_mul_left subset_closure)
-- 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 : Set G
hs : IsOpen[inst] s
t : Set G
a : G
ha : a ∈ s
b : G
hb : b ∈ closure[inst] t
⊢ a * b ∈ s * t
have hb₁ : ∀ (o : Set G), IsOpen[inst] o → b ∈ o → (o ∩ t).Nonempty
Tactic: rw [mem_closure_iff] at hb
Cleared hypotheses: hb
-- 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 : Set G
hs : IsOpen[inst] s
t : Set G
a : G
ha : a ∈ s
b : G
hb : ∀ (o : Set G), IsOpen[inst] o → b ∈ o → (o ∩ t).Nonempty
⊢ a * b ∈ s * t
have hbU : b ∈ s⁻¹ * {a * b}
Tactic: have hbU : b ∈ s⁻¹ * {a * b} := ⟨a⁻¹, Set.inv_mem_inv.2 ha, a * b, rfl, inv_mul_cancel_left _ _⟩
-- 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 : Set G
hs : IsOpen[inst] s
t : Set G
a : G
ha : a ∈ s
b : G
hb : ∀ (o : Set G), IsOpen[inst] o → b ∈ o → (o ∩ t).Nonempty
hbU : b ∈ s⁻¹ * {a * b}
⊢ a * b ∈ s * t
have obtain : ∀ (c : G) (hc : c ∈ s⁻¹) (hcs : (fun (x1 x2 : G) ↦ x1 * x2) c (a * b) ∈ t), a * b ∈ s * t
Tactic: obtain ⟨_, ⟨c, hc, d, rfl : d = _, rfl⟩, hcs⟩ := hb _ hs.inv.mul_right hbU
-- 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 : IsOpen[inst] t
s : Set G
⊢ closure[inst] s * t = s * t
have rw : (closure[inst] s * t)⁻¹⁻¹ = s * t
Tactic: rw [← inv_inv (closure s * t), mul_inv_rev, inv_closure, ht.inv.mul_closure, mul_inv_rev, inv_inv,
    inv_inv]
-- 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 : IsOpen[inst] t
s : Set G
rw : (closure[inst] s * t)⁻¹⁻¹ = s * t
⊢ closure[inst] s * t = s * t
have rw₁ : (t⁻¹ * (closure[inst] s)⁻¹)⁻¹ = s * t
Tactic: rw [← inv_inv (closure s * t), mul_inv_rev, inv_closure, ht.inv.mul_closure, mul_inv_rev, inv_inv,
    inv_inv]
-- 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 : IsOpen[inst] t
s : Set G
rw : (closure[inst] s * t)⁻¹⁻¹ = s * t
rw₁ : (t⁻¹ * (closure[inst] s)⁻¹)⁻¹ = s * t
⊢ closure[inst] s * t = s * t
have rw₂ : (t⁻¹ * closure[inst] s⁻¹)⁻¹ = s * t
Tactic: rw [← inv_inv (closure s * t), mul_inv_rev, inv_closure, ht.inv.mul_closure, mul_inv_rev, inv_inv,
    inv_inv]
-- 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 : IsOpen[inst] t
s : Set G
rw : (closure[inst] s * t)⁻¹⁻¹ = s * t
rw₁ : (t⁻¹ * (closure[inst] s)⁻¹)⁻¹ = s * t
rw₂ : (t⁻¹ * closure[inst] s⁻¹)⁻¹ = s * t
⊢ closure[inst] s * t = s * t
have rw₃ : (t⁻¹ * s⁻¹)⁻¹ = s * t
Tactic: rw [← inv_inv (closure s * t), mul_inv_rev, inv_closure, ht.inv.mul_closure, mul_inv_rev, inv_inv,
    inv_inv]
-- 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 : IsOpen[inst] t
s : Set G
rw : (closure[inst] s * t)⁻¹⁻¹ = s * t
rw₁ : (t⁻¹ * (closure[inst] s)⁻¹)⁻¹ = s * t
rw₂ : (t⁻¹ * closure[inst] s⁻¹)⁻¹ = s * t
rw₃ : (t⁻¹ * s⁻¹)⁻¹ = s * t
⊢ closure[inst] s * t = s * t
have rw₄ : s⁻¹⁻¹ * t⁻¹⁻¹ = s * t
Tactic: rw [← inv_inv (closure s * t), mul_inv_rev, inv_closure, ht.inv.mul_closure, mul_inv_rev, inv_inv,
    inv_inv]
-- 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 : IsOpen[inst] t
s : Set G
rw : (closure[inst] s * t)⁻¹⁻¹ = s * t
rw₁ : (t⁻¹ * (closure[inst] s)⁻¹)⁻¹ = s * t
rw₂ : (t⁻¹ * closure[inst] s⁻¹)⁻¹ = s * t
rw₃ : (t⁻¹ * s⁻¹)⁻¹ = s * t
rw₄ : s⁻¹⁻¹ * t⁻¹⁻¹ = s * t
⊢ closure[inst] s * t = s * t
have rw₅ : s * t⁻¹⁻¹ = s * t
Tactic: rw [← inv_inv (closure s * t), mul_inv_rev, inv_closure, ht.inv.mul_closure, mul_inv_rev, inv_inv,
    inv_inv]
-- 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 : IsOpen[inst] t
s : Set G
rw : (closure[inst] s * t)⁻¹⁻¹ = s * t
rw₁ : (t⁻¹ * (closure[inst] s)⁻¹)⁻¹ = s * t
rw₂ : (t⁻¹ * closure[inst] s⁻¹)⁻¹ = s * t
rw₃ : (t⁻¹ * s⁻¹)⁻¹ = s * t
rw₄ : s⁻¹⁻¹ * t⁻¹⁻¹ = s * t
rw₅ : s * t⁻¹⁻¹ = s * t
⊢ closure[inst] s * t = s * t
have rw₆ : s * t = s * t
Tactic: rw [← inv_inv (closure s * t), mul_inv_rev, inv_closure, ht.inv.mul_closure, mul_inv_rev, inv_inv,
    inv_inv]
-- 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 : Set G
hs : IsOpen[inst] s
t : Set G
⊢ s / closure[inst] t = s / t
have simp_rw : s * (closure[inst] t)⁻¹ = s * t⁻¹
Tactic: simp_rw [div_eq_mul_inv, inv_closure, hs.mul_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
s : Set G
hs : IsOpen[inst] s
t : Set G
simp_rw : s * (closure[inst] t)⁻¹ = s * t⁻¹
⊢ s / closure[inst] t = s / t
have simp_rw₁ : s * closure[inst] t⁻¹ = s * t⁻¹
Tactic: simp_rw [div_eq_mul_inv, inv_closure, hs.mul_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
t : Set G
ht : IsOpen[inst] t
s : Set G
⊢ closure[inst] s / t = s / t
have simp_rw : closure[inst] s * t⁻¹ = s * t⁻¹
Tactic: simp_rw [div_eq_mul_inv, ht.inv.closure_mul]
-- 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 t : Set G
ht : IsClosed[inst] t
hs : IsCompact s
⊢ IsClosed[inst] (t * s)
have rw : IsClosed[inst] (op '' s • t)
Tactic: rw [← image_op_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Pointwise (hypothesis)
Goal:
G : Type u_1
inst : MulOneClass G
inst_1 : TopologicalSpace G
s : Set G
⊢ s ⊆ s * closure[inst_1] {1}
have this : s ⊆ s * {1}
Tactic: have : s ⊆ s * ({1} : Set G) := 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
K : Set G
hK : IsCompact K
⊢ K * closure[inst] {1} = closure[inst] K
have apply : K * closure[inst] {1} ⊆ closure[inst] K
Tactic: apply Subset.antisymm ?_ ?_
-- 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
apply : K * closure[inst] {1} ⊆ closure[inst] K
⊢ K * closure[inst] {1} = closure[inst] K
have apply₁ : closure[inst] K ⊆ K * closure[inst] {1}
Tactic: apply Subset.antisymm ?_ ?_
-- 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
⊢ K * closure[inst] {1} ⊆ closure[inst] K
have K₁ : closure[inst] (K * {1}) = closure[inst] K
Tactic: calc
    K * (closure {1} : Set G) ⊆ closure K * (closure {1} : Set G) :=
      smul_subset_smul_right subset_closure
    _ ⊆ closure (K * ({1} : Set G)) := smul_set_closure_subset _ _
    _ = closure K := 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
K : Set G
hK : IsCompact K
⊢ closure[inst] K ⊆ K * closure[inst] {1}
have this : IsClosed[inst] (K * closure[inst] {1})
Tactic: have : IsClosed (K * (closure {1} : Set G)) :=
      IsClosed.smul_left_of_isCompact isClosed_closure hK