awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
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
⊢ (interior (HSMul.hSMul (β := Set X) (g • V) {x})).Nonempty

Tactic:
have I : (interior ((g • V) • {x})).Nonempty := by
    apply hi.mono
    apply interior_mono
    exact smul_subset_smul_right inter_subset_right
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
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 • interior (HSMul.hSMul (β := Set X) V {x})).Nonempty

Tactic:
rw [smul_assoc, interior_smul] at I

Premises used: smul_assoc, interior_smul
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
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 : (g • interior (HSMul.hSMul (β := Set X) V {x})).Nonempty
⊢ (interior (HSMul.hSMul (β := Set X) V {x})).Nonempty

Tactic:
smul_set_nonempty.1 I

Premises used: Set.smul_set_nonempty, Iff.mp
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
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 : (g • interior (HSMul.hSMul (β := Set X) V {x})).Nonempty
⊢ (interior (HSMul.hSMul (β := Set X) V {x})).Nonempty

Tactic:
exact smul_set_nonempty.1 I

Premises used: Set.smul_set_nonempty, Iff.mp
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
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
obtain : ∀ (y : X) (hy : y ∈ interior (HSMul.hSMul (β := Set X) V {x})), HSMul.hSMul (β := Set X) U {x} ∈ 𝓝 x
⊢ HSMul.hSMul (β := Set X) U {x} ∈ 𝓝 x

Tactic:
obtain ⟨y, hy⟩ : (interior (V • ({x} : Set X))).Nonempty := by
    rw [smul_assoc, interior_smul] at I
    exact smul_set_nonempty.1 I

Premises used: Set.Nonempty, interior, HSMul.hSMul, Singleton.singleton
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
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
y : X
hy : y ∈ interior (HSMul.hSMul (β := Set X) V {x})
⊢ ∃ g' ∈ V, g' • x = y

Tactic:
simpa using interior_subset hy

Premises used: interior_subset
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
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
y : X
hy : y ∈ interior (HSMul.hSMul (β := Set X) V {x})
obtain :
  ∀ (g' : G) (hg' : g' ∈ V) (hy : g' • x ∈ interior (HSMul.hSMul (β := Set X) V {x})),
    HSMul.hSMul (β := Set X) U {x} ∈ 𝓝 x
⊢ HSMul.hSMul (β := Set X) U {x} ∈ 𝓝 x

Tactic:
obtain ⟨g', hg', rfl⟩ : ∃ g' ∈ V, g' • x = y := by simpa using interior_subset hy

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
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})
apply : x ∈ interior (HSMul.hSMul (β := Set X) (g'⁻¹ • V) {x})
⊢ HSMul.hSMul (β := Set X) (g'⁻¹ • V) {x} ∈ 𝓝 x

Tactic:
apply mem_interior_iff_mem_nhds.1

Premises used: mem_interior_iff_mem_nhds, Iff.mp
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
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})
rwa : x ∈ interior (g'⁻¹ • HSMul.hSMul (β := Set X) V {x})
rwa₁ : x ∈ g'⁻¹ • interior (HSMul.hSMul (β := Set X) V {x})
rwa₂ rwa₃ rwa₄ rwa₅ : g' • x ∈ interior (HSMul.hSMul (β := Set X) V {x})
⊢ x ∈ interior (HSMul.hSMul (β := Set X) (g'⁻¹ • V) {x})

Tactic:
rwa [smul_assoc, interior_smul, mem_inv_smul_set_iff]

Premises used: smul_assoc, interior_smul, Set.mem_inv_smul_set_iff
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
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})
⊢ HSMul.hSMul (β := Set X) (g'⁻¹ • V) {x} ∈ 𝓝 x

Tactic:
have J : (g'⁻¹ • V) • {x} ∈ 𝓝 x := by
    apply mem_interior_iff_mem_nhds.1
    rwa [smul_assoc, interior_smul, mem_inv_smul_set_iff]
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
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
a : g'⁻¹ • V ⊆ U
⊢ HSMul.hSMul (β := Set X) (g'⁻¹ • V) {x} ⊆ HSMul.hSMul (β := Set X) U {x}

Tactic:
apply smul_subset_smul_right

Premises used: Set.smul_subset_smul_right
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
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
apply : V⁻¹ • V ⊆ U
⊢ g'⁻¹ • V ⊆ U

Tactic:
apply Subset.trans (smul_set_subset_smul (inv_mem_inv.2 hg')) ?_

Premises used: Iff.mpr, Set.Subset.trans, Set.inv_mem_inv, Set.smul_set_subset_smul
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
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
rw : V • V ⊆ U
⊢ V⁻¹ • V ⊆ U

Tactic:
rw [V_symm]
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
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

Tactic:
VU
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
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

Tactic:
exact VU
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
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) (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
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
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
this : HSMul.hSMul (β := Set X) (g'⁻¹ • V) {x} ⊆ HSMul.hSMul (β := Set X) U {x}
⊢ HSMul.hSMul (β := Set X) U {x} ∈ 𝓝 x

Tactic:
Filter.mem_of_superset J this

Premises used: Filter.mem_of_superset
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
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
this : HSMul.hSMul (β := Set X) (g'⁻¹ • V) {x} ⊆ HSMul.hSMul (β := Set X) U {x}
⊢ HSMul.hSMul (β := Set X) U {x} ∈ 𝓝 x

Tactic:
exact Filter.mem_of_superset J this

Premises used: Filter.mem_of_superset
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
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
simp_rw : ∀ (x_1 : G), ∀ s ∈ 𝓝 x_1, (fun (g : G) ↦ g • x) '' s ∈ 𝓝 (x_1 • x)
⊢ IsOpenMap.{u_1, u_2} (Y := X) fun (g : G) ↦ g • x

Tactic:
simp_rw [isOpenMap_iff_nhds_le, Filter.le_map_iff]

Premises used: Filter.le_map_iff, isOpenMap_iff_nhds_le
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
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
h : ∀ (g_1 : G), g_1 • x = ((fun (x_1 : G) ↦ x_1 • g • x) ∘ fun (x : G) ↦ x * g⁻¹) g_1
⊢ Eq (α := G → X) (fun (x_1 : G) ↦ x_1 • x) ((fun (x_1 : G) ↦ x_1 • g • x) ∘ fun (x : G) ↦ x * g⁻¹)

Tactic:
ext g
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
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_1 : G
U : Set G
hU : U ∈ 𝓝 g_1
g : G
⊢ g • x = ((fun (x_1 : G) ↦ x_1 • g_1 • x) ∘ fun (x : G) ↦ x * g_1⁻¹) g

Tactic:
simp [smul_smul]

Premises used: smul_smul
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
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⁻¹)

Tactic:
have : (· • x) = (· • (g • x)) ∘ (· * g⁻¹) := by
    ext g
    simp [smul_smul]
-- Module: Mathlib.Topology.Algebra.Group.OpenMapping
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⁻¹)
rw : HSMul.hSMul (α := Set G) (β := Set X) ((fun (x : G) ↦ x * g⁻¹) '' U) {g • x} ∈ 𝓝 (g • x)
⊢ (fun (g : G) ↦ g • x) '' U ∈ 𝓝 (g • x)

Tactic:
rw [this, image_comp, ← smul_singleton]

Premises used: Set.image_comp, Set.smul_singleton