-- Mathlib/Topology/Algebra/Group/OpenMapping.lean
theorem isOpenMap_smul_of_sigmaCompact (x : X) : IsOpenMap (fun (g : G) ↦ g • x)

Proof state:
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
x : X
⊢ ∀ (x_1 : G), ∀ s ∈ 𝓝 x_1, (fun g => g • x) '' s ∈ 𝓝 (x_1 • x)

Tactic:
intro g U hU

Result:
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
x : X
g : G
U : Set G
hU : U ∈ 𝓝 g
⊢ (fun g => g • x) '' U ∈ 𝓝 (g • x)

Proof state:
case h
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
x : X
g✝ : G
U : Set G
hU : U ∈ 𝓝 g✝
g : G
⊢ g • x = ((fun x_1 => x_1 • g✝ • x) ∘ fun x => x * g✝⁻¹) g

Tactic:
simp [smul_smul]

Result:
no goals

Proof state:
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
x : X
g : G
U : Set G
hU : U ∈ 𝓝 g
this : (fun x_1 => x_1 • x) = (fun x_1 => x_1 • g • x) ∘ fun x => x * g⁻¹
⊢ (fun x => x * g⁻¹) '' U • {g • x} ∈ 𝓝 (g • x)

Tactic:
apply smul_singleton_mem_nhds_of_sigmaCompact

Result:
case hU
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
x : X
g : G
U : Set G
hU : U ∈ 𝓝 g
this : (fun x_1 => x_1 • x) = (fun x_1 => x_1 • g • x) ∘ fun x => x * g⁻¹
⊢ (fun x => x * g⁻¹) '' U ∈ 𝓝 1

Proof state:
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
x : X
g : G
U : Set G
hU : U ∈ 𝓝 g
⊢ (fun x_1 => x_1 • x) = (fun x_1 => x_1 • g • x) ∘ fun x => x * g⁻¹

Tactic:
ext g

Result:
case h
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
x : X
g✝ : G
U : Set G
hU : U ∈ 𝓝 g✝
g : G
⊢ g • x = ((fun x_1 => x_1 • g✝ • x) ∘ fun x => x * g✝⁻¹) g

Proof state:
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
x : X
g : G
U : Set G
hU : U ∈ 𝓝 g
this : (fun x_1 => x_1 • x) = (fun x_1 => x_1 • g • x) ∘ fun x => x * g⁻¹
⊢ (fun g => g • x) '' U ∈ 𝓝 (g • x)

Tactic:
rw [this, image_comp, ← smul_singleton]

Result:
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
x : X
g : G
U : Set G
hU : U ∈ 𝓝 g
this : (fun x_1 => x_1 • x) = (fun x_1 => x_1 • g • x) ∘ fun x => x * g⁻¹
⊢ (fun x => x * g⁻¹) '' U • {g • x} ∈ 𝓝 (g • x)

Proof state:
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
x : X
⊢ IsOpenMap fun g => g • x

Tactic:
simp_rw [isOpenMap_iff_nhds_le, Filter.le_map_iff]

Result:
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
x : X
⊢ ∀ (x_1 : G), ∀ s ∈ 𝓝 x_1, (fun g => g • x) '' s ∈ 𝓝 (x_1 • x)

Proof state:
case hU
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
x : X
g : G
U : Set G
hU : U ∈ 𝓝 g
this : (fun x_1 => x_1 • x) = (fun x_1 => x_1 • g • x) ∘ fun x => x * g⁻¹
⊢ (fun x => x * g⁻¹) '' U ∈ 𝓝 1

Tactic:
simpa using isOpenMap_mul_right g⁻¹ |>.image_mem_nhds hU

Result:
no goals