-- Mathlib/Topology/Algebra/ProperAction/Basic.lean
theorem t2Space_of_properSMul_of_t2Group [h_proper : ProperSMul G X] [T2Space G] : T2Space X

Proof state:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
h_proper : ProperSMul G X
inst✝ : T2Space G
f : X → G × X := fun x => (1, x)
proper_f : IsProperMap f
g : G × X → X × X := fun gx => (gx.1 • gx.2, gx.2)
proper_g : IsProperMap g
⊢ g ∘ f = fun x => (x, x)

Tactic:
ext x <;> simp [f, g]

Result:
no goals

Proof state:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
h_proper : ProperSMul G X
inst✝ : T2Space G
f : X → G × X := fun x => (1, x)
g : G × X → X := fun gx => gx.2
this : Function.LeftInverse g f
⊢ Continuous g

Tactic:
fun_prop

Result:
no goals

Proof state:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
h_proper : ProperSMul G X
inst✝ : T2Space G
f : X → G × X := fun x => (1, x)
proper_f : IsProperMap f
⊢ IsClosed (diagonal X)

Tactic:
let g := fun gx : G × X ↦ (gx.1 • gx.2, gx.2)

Result:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
h_proper : ProperSMul G X
inst✝ : T2Space G
f : X → G × X := fun x => (1, x)
proper_f : IsProperMap f
g : G × X → X × X := fun gx => (gx.1 • gx.2, gx.2)
⊢ IsClosed (diagonal X)

Proof state:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
h_proper : ProperSMul G X
inst✝ : T2Space G
f : X → G × X := fun x => (1, x)
proper_f : IsProperMap f
g : G × X → X × X := fun gx => (gx.1 • gx.2, gx.2)
⊢ IsClosed (diagonal X)

Tactic:
have proper_g : IsProperMap g := (properSMul_iff G X).1 h_proper

Result:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
h_proper : ProperSMul G X
inst✝ : T2Space G
f : X → G × X := fun x => (1, x)
proper_f : IsProperMap f
g : G × X → X × X := fun gx => (gx.1 • gx.2, gx.2)
proper_g : IsProperMap g
⊢ IsClosed (diagonal X)

Proof state:
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
h_proper : ProperSMul G X
inst✝ : T2Space G
f : X → G × X := fun x => (1, x)
⊢ range f = {1} ×ˢ univ

Tactic:
simp [f]

Result:
no goals

Proof state:
case refine_1
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
h_proper : ProperSMul G X
inst✝ : T2Space G
f : X → G × X := fun x => (1, x)
⊢ IsEmbedding f

Tactic:
let g := fun gx : G × X ↦ gx.2

Result:
case refine_1
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
h_proper : ProperSMul G X
inst✝ : T2Space G
f : X → G × X := fun x => (1, x)
g : G × X → X := fun gx => gx.2
⊢ IsEmbedding f

Proof state:
case refine_2
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
h_proper : ProperSMul G X
inst✝ : T2Space G
f : X → G × X := fun x => (1, x)
this : range f = {1} ×ˢ univ
⊢ IsClosed (range f)

Tactic:
rw [this]

Result:
case refine_2
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
h_proper : ProperSMul G X
inst✝ : T2Space G
f : X → G × X := fun x => (1, x)
this : range f = {1} ×ˢ univ
⊢ IsClosed ({1} ×ˢ univ)