-- Mathlib/Topology/Algebra/Group/OpenMapping.lean
theorem MonoidHom.isOpenMap_of_sigmaCompact
    {H : Type*} [Group H] [TopologicalSpace H] [BaireSpace H] [T2Space H] [ContinuousMul H]
    (f : G →* H) (hf : Function.Surjective f) (h'f : Continuous f) :
    IsOpenMap f

Proof state:
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SigmaCompactSpace G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : BaireSpace H
inst✝¹ : T2Space H
inst✝ : ContinuousMul H
f : G →* H
hf : Surjective ⇑f
h'f : Continuous ⇑f
A : MulAction G H := MulAction.compHom H f
this✝ : ContinuousSMul G H
this : IsPretransitive G H
⊢ IsOpenMap ⇑f

Tactic:
have : f = (fun (g : G) ↦ g • (1 : H)) := by simp [A, MulAction.compHom_smul_def]

Result:
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SigmaCompactSpace G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : BaireSpace H
inst✝¹ : T2Space H
inst✝ : ContinuousMul H
f : G →* H
hf : Surjective ⇑f
h'f : Continuous ⇑f
A : MulAction G H := MulAction.compHom H f
this✝¹ : ContinuousSMul G H
this✝ : IsPretransitive G H
this : ⇑f = fun g => g • 1
⊢ IsOpenMap ⇑f

Proof state:
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SigmaCompactSpace G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : BaireSpace H
inst✝¹ : T2Space H
inst✝ : ContinuousMul H
f : G →* H
hf : Surjective ⇑f
h'f : Continuous ⇑f
A : MulAction G H := MulAction.compHom H f
this✝¹ : ContinuousSMul G H
this✝ : IsPretransitive G H
this : ⇑f = fun g => g • 1
⊢ IsOpenMap ⇑f

Tactic:
rw [this]

Result:
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SigmaCompactSpace G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : BaireSpace H
inst✝¹ : T2Space H
inst✝ : ContinuousMul H
f : G →* H
hf : Surjective ⇑f
h'f : Continuous ⇑f
A : MulAction G H := MulAction.compHom H f
this✝¹ : ContinuousSMul G H
this✝ : IsPretransitive G H
this : ⇑f = fun g => g • 1
⊢ IsOpenMap fun g => g • 1

Proof state:
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SigmaCompactSpace G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : BaireSpace H
inst✝¹ : T2Space H
inst✝ : ContinuousMul H
f : G →* H
hf : Surjective ⇑f
h'f : Continuous ⇑f
A : MulAction G H := MulAction.compHom H f
this : ContinuousSMul G H
⊢ IsOpenMap ⇑f

Tactic:
have : IsPretransitive G H := isPretransitive_compHom hf

Result:
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SigmaCompactSpace G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : BaireSpace H
inst✝¹ : T2Space H
inst✝ : ContinuousMul H
f : G →* H
hf : Surjective ⇑f
h'f : Continuous ⇑f
A : MulAction G H := MulAction.compHom H f
this✝ : ContinuousSMul G H
this : IsPretransitive G H
⊢ IsOpenMap ⇑f

Proof state:
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SigmaCompactSpace G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : BaireSpace H
inst✝¹ : T2Space H
inst✝ : ContinuousMul H
f : G →* H
hf : Surjective ⇑f
h'f : Continuous ⇑f
⊢ IsOpenMap ⇑f

Tactic:
let A : MulAction G H := MulAction.compHom _ f

Result:
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SigmaCompactSpace G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : BaireSpace H
inst✝¹ : T2Space H
inst✝ : ContinuousMul H
f : G →* H
hf : Surjective ⇑f
h'f : Continuous ⇑f
A : MulAction G H := MulAction.compHom H f
⊢ IsOpenMap ⇑f

Proof state:
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SigmaCompactSpace G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : BaireSpace H
inst✝¹ : T2Space H
inst✝ : ContinuousMul H
f : G →* H
hf : Surjective ⇑f
h'f : Continuous ⇑f
A : MulAction G H := MulAction.compHom H f
this✝¹ : ContinuousSMul G H
this✝ : IsPretransitive G H
this : ⇑f = fun g => g • 1
⊢ IsOpenMap fun g => g • 1

Tactic:
exact isOpenMap_smul_of_sigmaCompact _

Result:
no goals

Proof state:
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SigmaCompactSpace G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : BaireSpace H
inst✝¹ : T2Space H
inst✝ : ContinuousMul H
f : G →* H
hf : Surjective ⇑f
h'f : Continuous ⇑f
A : MulAction G H := MulAction.compHom H f
this✝ : ContinuousSMul G H
this : IsPretransitive G H
⊢ ⇑f = fun g => g • 1

Tactic:
simp [A, MulAction.compHom_smul_def]

Result:
no goals

Proof state:
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SigmaCompactSpace G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : BaireSpace H
inst✝¹ : T2Space H
inst✝ : ContinuousMul H
f : G →* H
hf : Surjective ⇑f
h'f : Continuous ⇑f
A : MulAction G H := MulAction.compHom H f
⊢ IsOpenMap ⇑f

Tactic:
have : ContinuousSMul G H := continuousSMul_compHom h'f

Result:
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SigmaCompactSpace G
H : Type u_3
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : BaireSpace H
inst✝¹ : T2Space H
inst✝ : ContinuousMul H
f : G →* H
hf : Surjective ⇑f
h'f : Continuous ⇑f
A : MulAction G H := MulAction.compHom H f
this : ContinuousSMul G H
⊢ IsOpenMap ⇑f