-- 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)
g : G × X → X := fun gx => gx.2
x : X
⊢ g (f x) = x

Tactic:
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)
proper_f : IsProperMap f
⊢ T2Space X

Tactic:
rw [t2_iff_isClosed_diagonal]

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
⊢ 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)
proper_g : IsProperMap g
this : g ∘ f = fun x => (x, x)
⊢ IsClosed (diagonal X)

Tactic:
have range_gf : range (g ∘ f) = diagonal X := by simp [this]

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
this : g ∘ f = fun x => (x, x)
range_gf : range (g ∘ f) = diagonal X
⊢ 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)
proper_g : IsProperMap g
this : g ∘ f = fun x => (x, x)
range_gf : range (g ∘ f) = diagonal X
⊢ IsClosed (diagonal X)

Tactic:
rw [← range_gf]

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
this : g ∘ f = fun x => (x, x)
range_gf : range (g ∘ f) = diagonal X
⊢ IsClosed (range (g ∘ f))

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)
⊢ IsProperMap f

Tactic:
refine IsClosedEmbedding.isProperMap ⟨?_, ?_⟩

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)
⊢ IsEmbedding f

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)
⊢ IsClosed (range f)

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)
g : G × X → X := fun gx => gx.2
⊢ IsEmbedding f

Tactic:
have : Function.LeftInverse g f := fun x ↦ by simp [f, g]

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
this : Function.LeftInverse g f
⊢ IsEmbedding f

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
this : g ∘ f = fun x => (x, x)
range_gf : range (g ∘ f) = diagonal X
⊢ IsClosed (range (g ∘ f))

Tactic:
exact (proper_f.comp proper_g).isClosed_range

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
g : G × X → X × X := fun gx => (gx.1 • gx.2, gx.2)
proper_g : IsProperMap g
⊢ IsClosed (diagonal X)

Tactic:
have : g ∘ f = fun x ↦ (x, x) := by ext x <;> simp [f, g]

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
this : g ∘ f = fun x => (x, x)
⊢ 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)
g : G × X → X := fun gx => gx.2
this : Function.LeftInverse g f
⊢ Continuous f

Tactic:
fun_prop

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)
g : G × X → X := fun gx => gx.2
this : Function.LeftInverse g f
⊢ IsEmbedding f

Tactic:
exact this.isEmbedding (by fun_prop) (by fun_prop)

Result:
no goals

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)
⊢ IsClosed (range f)

Tactic:
have : range f = ({1} ×ˢ univ) := by simp [f]

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 (range f)

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
this : g ∘ f = fun x => (x, x)
⊢ range (g ∘ f) = diagonal X

Tactic:
simp [this]

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
⊢ T2Space X

Tactic:
let f := fun x : X ↦ ((1 : G), x)

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)
⊢ T2Space X

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 ({1} ×ˢ univ)

Tactic:
exact isClosed_singleton.prod isClosed_univ

Result:
no goals