awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
⊢ IsProperMap f

Tactic:
IsClosedEmbedding.isProperMap ⟨isEmbedding_prodMkRight 1, ?_⟩

Premises used: Topology.IsClosedEmbedding.isProperMap, OfNat.ofNat, Topology.IsClosedEmbedding.mk, isEmbedding_prodMkRight
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
refine : IsClosed[instTopologicalSpaceProd] (range f)
⊢ IsProperMap f

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

Premises used: Topology.IsClosedEmbedding.isProperMap, OfNat.ofNat, Topology.IsClosedEmbedding.mk, isEmbedding_prodMkRight
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
⊢ range f = SProd.sprod (α := Set G) (β := Set X) {1} univ

Tactic:
simp [f, Set.singleton_prod]

Premises used: Set.singleton_prod
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
⊢ range f = SProd.sprod (α := Set G) (β := Set X) {1} univ

Tactic:
have : range f = ({1} ×ˢ univ) := by simp [f, Set.singleton_prod]
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
this : range f = SProd.sprod (α := Set G) (β := Set X) {1} univ
rw : IsClosed[instTopologicalSpaceProd] (SProd.sprod (α := Set G) (β := Set X) {1} univ)
⊢ IsClosed[instTopologicalSpaceProd] (range f)

Tactic:
rw [this]
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
this : range f = SProd.sprod (α := Set G) (β := Set X) {1} univ
⊢ IsClosed[instTopologicalSpaceProd] (SProd.sprod (α := Set G) (β := Set X) {1} univ)

Tactic:
isClosed_singleton.prod isClosed_univ

Premises used: isClosed_univ, IsClosed.prod, isClosed_singleton
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
this : range f = SProd.sprod (α := Set G) (β := Set X) {1} univ
⊢ IsClosed[instTopologicalSpaceProd] (SProd.sprod (α := Set G) (β := Set X) {1} univ)

Tactic:
exact isClosed_singleton.prod isClosed_univ

Premises used: isClosed_univ, IsClosed.prod, isClosed_singleton
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
⊢ IsProperMap f

Tactic:
have proper_f : IsProperMap f := by
    refine IsClosedEmbedding.isProperMap ⟨isEmbedding_prodMkRight 1, ?_⟩
    have : range f = ({1} ×ˢ univ) := by simp [f, Set.singleton_prod]
    rw [this]
    exact isClosed_singleton.prod isClosed_univ
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
proper_f : IsProperMap f
rw : IsClosed[instTopologicalSpaceProd] (diagonal X)
⊢ T2Space X

Tactic:
rw [t2_iff_isClosed_diagonal]

Premises used: t2_iff_isClosed_diagonal
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
proper_f : IsProperMap f
g : (gx : G × X) → X × X := fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
⊢ IsProperMap g

Tactic:
have proper_g : IsProperMap g := (properSMul_iff G X).1 h_proper
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
proper_f : IsProperMap f
g : (gx : G × X) → X × X := fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
proper_g : IsProperMap g
h : ∀ (x : X), ((g ∘ f) x).1 = (x, x).1
h₁ : ∀ (x : X), ((g ∘ f) x).2 = (x, x).2
⊢ g ∘ f = fun (x : X) ↦ (x, x)

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
proper_f : IsProperMap f
g : (gx : G × X) → X × X := fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
proper_g : IsProperMap g
x : X
⊢ ((g ∘ f) x).1 = (x, x).1

Tactic:
simp [f, g]
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
proper_f : IsProperMap f
g : (gx : G × X) → X × X := fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
proper_g : IsProperMap g
x : X
⊢ ((g ∘ f) x).2 = (x, x).2

Tactic:
simp [f, g]
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
proper_f : IsProperMap f
g : (gx : G × X) → X × X := fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
proper_g : IsProperMap g
⊢ g ∘ f = fun (x : X) ↦ (x, x)

Tactic:
have : g ∘ f = fun x ↦ (x, x) := by ext x <;> simp [f, g]
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
proper_f : IsProperMap f
g : (gx : G × X) → X × X := fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
proper_g : IsProperMap g
this : g ∘ f = fun (x : X) ↦ (x, x)
⊢ range (g ∘ f) = diagonal X

Tactic:
simp [this]
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
proper_f : IsProperMap f
g : (gx : G × X) → X × X := fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
proper_g : IsProperMap g
this : g ∘ f = fun (x : X) ↦ (x, x)
⊢ range (g ∘ f) = diagonal X

Tactic:
have range_gf : range (g ∘ f) = diagonal X := by simp [this]
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
proper_f : IsProperMap f
g : (gx : G × X) → X × X := fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
proper_g : IsProperMap g
this : g ∘ f = fun (x : X) ↦ (x, x)
range_gf : range (g ∘ f) = diagonal X
rw : IsClosed[instTopologicalSpaceProd] (range (g ∘ f))
⊢ IsClosed[instTopologicalSpaceProd] (diagonal X)

Tactic:
rw [← range_gf]
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
proper_f : IsProperMap f
g : (gx : G × X) → X × X := fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
proper_g : IsProperMap g
this : g ∘ f = fun (x : X) ↦ (x, x)
range_gf : range (g ∘ f) = diagonal X
⊢ IsClosed[instTopologicalSpaceProd] (range (g ∘ f))

Tactic:
(proper_g.comp proper_f).isClosed_range

Premises used: IsProperMap.isClosed_range, IsProperMap.comp
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
h_proper : ProperSMul G X
inst_4 : T1Space G
f : (x : X) → G × X := fun (x : X) ↦ (1, x)
proper_f : IsProperMap f
g : (gx : G × X) → X × X := fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
proper_g : IsProperMap g
this : g ∘ f = fun (x : X) ↦ (x, x)
range_gf : range (g ∘ f) = diagonal X
⊢ IsClosed[instTopologicalSpaceProd] (range (g ∘ f))

Tactic:
exact (proper_g.comp proper_f).isClosed_range

Premises used: IsProperMap.isClosed_range, IsProperMap.comp
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
H : Type u_3
inst_4 : Group H
inst_5 : MulAction H X
inst_6 : TopologicalSpace H
inst_7 : ProperSMul G X
f : H →* G
f_clemb : IsClosedEmbedding.{u_3, u_1} (X := H) (Y := G) (⇑f : (a : H) → G)
f_compat : ∀ (h : H) (x : X), HSMul.hSMul.{u_1, u_2, u_2} (α := G) ((f : (a : H) → G) h : G) x = h • x
⊢ IsProperMap (X := H × X) (Y := G × X) (Prod.map (⇑f : (a : H) → G) fun (x : X) ↦ x)

Tactic:
have h : IsProperMap (Prod.map f (fun x : X ↦ x)) := f_clemb.isProperMap.prodMap isProperMap_id
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
H : Type u_3
inst_4 : Group H
inst_5 : MulAction H X
inst_6 : TopologicalSpace H
inst_7 : ProperSMul G X
f : H →* G
f_clemb : IsClosedEmbedding.{u_3, u_1} (X := H) (Y := G) (⇑f : (a : H) → G)
f_compat : ∀ (h : H) (x : X), HSMul.hSMul.{u_1, u_2, u_2} (α := G) ((f : (a : H) → G) h : G) x = h • x
h : IsProperMap (X := H × X) (Y := G × X) (Prod.map (⇑f : (a : H) → G) fun (x : X) ↦ x)
⊢ Eq (α := (hx : H × X) → X × X) (fun (hx : H × X) ↦ (hx.1 • hx.2, hx.2)) fun (hx : H × X) ↦
    (HSMul.hSMul.{u_1, u_2, u_2} (α := G) ((f : (a : H) → G) hx.1 : G) hx.2, hx.2)

Tactic:
simp [f_compat]
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
H : Type u_3
inst_4 : Group H
inst_5 : MulAction H X
inst_6 : TopologicalSpace H
inst_7 : ProperSMul G X
f : H →* G
f_clemb : IsClosedEmbedding.{u_3, u_1} (X := H) (Y := G) (⇑f : (a : H) → G)
f_compat : ∀ (h : H) (x : X), HSMul.hSMul.{u_1, u_2, u_2} (α := G) ((f : (a : H) → G) h : G) x = h • x
h : IsProperMap (X := H × X) (Y := G × X) (Prod.map (⇑f : (a : H) → G) fun (x : X) ↦ x)
⊢ Eq (α := (hx : H × X) → X × X) (fun (hx : H × X) ↦ (hx.1 • hx.2, hx.2)) fun (hx : H × X) ↦
    (HSMul.hSMul.{u_1, u_2, u_2} (α := G) ((f : (a : H) → G) hx.1 : G) hx.2, hx.2)

Tactic:
have : (fun hx : H × X ↦ (hx.1 • hx.2, hx.2)) = (fun hx ↦ (f hx.1 • hx.2, hx.2)) := by
      simp [f_compat]
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
H : Type u_3
inst_4 : Group H
inst_5 : MulAction H X
inst_6 : TopologicalSpace H
inst_7 : ProperSMul G X
f : H →* G
f_clemb : IsClosedEmbedding.{u_3, u_1} (X := H) (Y := G) (⇑f : (a : H) → G)
f_compat : ∀ (h : H) (x : X), HSMul.hSMul.{u_1, u_2, u_2} (α := G) ((f : (a : H) → G) h : G) x = h • x
h : IsProperMap (X := H × X) (Y := G × X) (Prod.map (⇑f : (a : H) → G) fun (x : X) ↦ x)
this :
  Eq (α := (hx : H × X) → X × X) (fun (hx : H × X) ↦ (hx.1 • hx.2, hx.2)) fun (hx : H × X) ↦
    (HSMul.hSMul.{u_1, u_2, u_2} (α := G) ((f : (a : H) → G) hx.1 : G) hx.2, hx.2)
rw :
  IsProperMap (Y := X × X) fun (hx : H × X) ↦
    (HSMul.hSMul.{u_1, u_2, u_2} (α := G) ((f : (a : H) → G) hx.1 : G) hx.2, hx.2)
⊢ IsProperMap (Y := X × X) fun (gx : H × X) ↦ (gx.1 • gx.2, gx.2)

Tactic:
rw [this]
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
H : Type u_3
inst_4 : Group H
inst_5 : MulAction H X
inst_6 : TopologicalSpace H
inst_7 : ProperSMul G X
f : H →* G
f_clemb : IsClosedEmbedding.{u_3, u_1} (X := H) (Y := G) (⇑f : (a : H) → G)
f_compat : ∀ (h : H) (x : X), HSMul.hSMul.{u_1, u_2, u_2} (α := G) ((f : (a : H) → G) h : G) x = h • x
h : IsProperMap (X := H × X) (Y := G × X) (Prod.map (⇑f : (a : H) → G) fun (x : X) ↦ x)
this :
  Eq (α := (hx : H × X) → X × X) (fun (hx : H × X) ↦ (hx.1 • hx.2, hx.2)) fun (hx : H × X) ↦
    (HSMul.hSMul.{u_1, u_2, u_2} (α := G) ((f : (a : H) → G) hx.1 : G) hx.2, hx.2)
⊢ IsProperMap (Y := X × X) fun (hx : H × X) ↦
    (HSMul.hSMul.{u_1, u_2, u_2} (α := G) ((f : (a : H) → G) hx.1 : G) hx.2, hx.2)

Tactic:
ProperSMul.isProperMap_smul_pair.comp h

Premises used: ProperSMul.isProperMap_smul_pair, IsProperMap.comp
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
H : Type u_3
inst_4 : Group H
inst_5 : MulAction H X
inst_6 : TopologicalSpace H
inst_7 : ProperSMul G X
f : H →* G
f_clemb : IsClosedEmbedding.{u_3, u_1} (X := H) (Y := G) (⇑f : (a : H) → G)
f_compat : ∀ (h : H) (x : X), HSMul.hSMul.{u_1, u_2, u_2} (α := G) ((f : (a : H) → G) h : G) x = h • x
h : IsProperMap (X := H × X) (Y := G × X) (Prod.map (⇑f : (a : H) → G) fun (x : X) ↦ x)
this :
  Eq (α := (hx : H × X) → X × X) (fun (hx : H × X) ↦ (hx.1 • hx.2, hx.2)) fun (hx : H × X) ↦
    (HSMul.hSMul.{u_1, u_2, u_2} (α := G) ((f : (a : H) → G) hx.1 : G) hx.2, hx.2)
⊢ IsProperMap (Y := X × X) fun (hx : H × X) ↦
    (HSMul.hSMul.{u_1, u_2, u_2} (α := G) ((f : (a : H) → G) hx.1 : G) hx.2, hx.2)

Tactic:
exact ProperSMul.isProperMap_smul_pair.comp h

Premises used: ProperSMul.isProperMap_smul_pair, IsProperMap.comp
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
H : Subgroup G
inst_4 : ProperSMul G X
H_closed : IsClosed[inst_2] (↑H : Set G)
⊢ ProperSMul.{u_1, u_2} (↥H) X

Tactic:
properSMul_of_isClosedEmbedding H.subtype H_closed.isClosedEmbedding_subtypeVal fun _ _ ↦ rfl

Premises used: Subgroup.subtype, properSMul_of_isClosedEmbedding, IsClosed.isClosedEmbedding_subtypeVal, rfl
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : IsTopologicalGroup G
x : G × G
⊢ (fun (gh : G × G) ↦ (gh.1 * gh.2⁻¹, gh.2)) ((fun (gh : G × G) ↦ (gh.1 * gh.2, gh.2)) x) = x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : IsTopologicalGroup G
x : G × G
⊢ (fun (gh : G × G) ↦ (gh.1 * gh.2, gh.2)) ((fun (gh : G × G) ↦ (gh.1 * gh.2⁻¹, gh.2)) x) = x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : IsTopologicalGroup G
Φ : G × G ≃ₜ G × G :=
  { toFun := fun (gh : G × G) ↦ (gh.1 * gh.2, gh.2), invFun := fun (gh : G × G) ↦ (gh.1 * gh.2⁻¹, gh.2), left_inv := ⋯,
    right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ IsProperMap (Y := G × G) fun (gx : G × G) ↦ (gx.1 • gx.2, gx.2)

Tactic:
Φ.isProperMap

Premises used: Homeomorph.isProperMap
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : IsTopologicalGroup G
Φ : G × G ≃ₜ G × G :=
  { toFun := fun (gh : G × G) ↦ (gh.1 * gh.2, gh.2), invFun := fun (gh : G × G) ↦ (gh.1 * gh.2⁻¹, gh.2), left_inv := ⋯,
    right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ IsProperMap (Y := G × G) fun (gx : G × G) ↦ (gx.1 • gx.2, gx.2)

Tactic:
exact Φ.isProperMap

Premises used: Homeomorph.isProperMap
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : IsTopologicalGroup G
x : Gᵐᵒᵖ × G
⊢ (fun (gh : G × G) ↦ (op (gh.2⁻¹ * gh.1), gh.2)) ((fun (gh : Gᵐᵒᵖ × G) ↦ (gh.2 * unop gh.1, gh.2)) x) = x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : IsTopologicalGroup G
x : G × G
⊢ (fun (gh : Gᵐᵒᵖ × G) ↦ (gh.2 * unop gh.1, gh.2)) ((fun (gh : G × G) ↦ (op (gh.2⁻¹ * gh.1), gh.2)) x) = x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : IsTopologicalGroup G
Φ : Gᵐᵒᵖ × G ≃ₜ G × G :=
  { toFun := fun (gh : Gᵐᵒᵖ × G) ↦ (gh.2 * unop gh.1, gh.2), invFun := fun (gh : G × G) ↦ (op (gh.2⁻¹ * gh.1), gh.2),
    left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ IsProperMap (Y := G × G) fun (gx : Gᵐᵒᵖ × G) ↦ (gx.1 • gx.2, gx.2)

Tactic:
Φ.isProperMap

Premises used: Homeomorph.isProperMap
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : IsTopologicalGroup G
Φ : Gᵐᵒᵖ × G ≃ₜ G × G :=
  { toFun := fun (gh : Gᵐᵒᵖ × G) ↦ (gh.2 * unop gh.1, gh.2), invFun := fun (gh : G × G) ↦ (op (gh.2⁻¹ * gh.1), gh.2),
    left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ IsProperMap (Y := G × G) fun (gx : Gᵐᵒᵖ × G) ↦ (gx.1 • gx.2, gx.2)

Tactic:
exact Φ.isProperMap

Premises used: Homeomorph.isProperMap
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : IsTopologicalGroup G
H : Subgroup G
H_closed : IsClosed[inst_2] (↑H : Set G)
⊢ ProperSMul (↥H.op) G

Tactic:
have : IsClosed (H.op : Set Gᵐᵒᵖ) := H_closed.preimage MulOpposite.continuous_unop
  inferInstance

Premises used: inferInstance, MulOpposite.continuous_unop, IsClosed.preimage
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : IsTopologicalGroup G
H : Subgroup G
inst_5 : IsClosed[inst_2] (↑H : Set G)
⊢ T2Space.{u_1} (G ⧸ H)

Tactic:
t2Space_quotient_mulAction_of_properSMul

Premises used: t2Space_quotient_mulAction_of_properSMul
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : ProperSMul G X
t : Set X
Φ : G × X → X × X := fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
⊢ IsProperMap Φ

Tactic:
have Φ_proper : IsProperMap Φ := ProperSMul.isProperMap_smul_pair
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : ProperSMul G X
t : Set X
Φ : G × X → X × X := fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
Φ_proper : IsProperMap Φ
h : ∀ (x : G × X), x ∈ SProd.sprod (α := Set G) univ t ↔ x ∈ Φ ⁻¹' snd ⁻¹' t
⊢ SProd.sprod (α := Set G) univ t = Φ ⁻¹' snd ⁻¹' t

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : ProperSMul G X
t : Set X
Φ : G × X → X × X := fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
Φ_proper : IsProperMap Φ
x : G × X
⊢ x ∈ SProd.sprod (α := Set G) univ t ↔ x ∈ Φ ⁻¹' snd ⁻¹' t

Tactic:
simp [Φ]
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : ProperSMul G X
t : Set X
Φ : G × X → X × X := fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
Φ_proper : IsProperMap Φ
α : Prod.{u_1, u_2} G (↑t : Type u_2) ≃ₜ (↑(Φ ⁻¹' snd ⁻¹' t) : Type (max u_1 u_2)) :=
  have this : SProd.sprod (α := Set G) univ t = Φ ⁻¹' snd ⁻¹' t := ⋯;
  Homeomorph.trans
    (Homeomorph.trans (Homeomorph.prodCongr (Homeomorph.symm (Homeomorph.Set.univ G)) (Homeomorph.refl (↑t : Type u_2)))
      (Homeomorph.symm (Homeomorph.Set.prod univ t)))
    (Homeomorph.setCongr (s := SProd.sprod (α := Set G) univ t) (t := Φ ⁻¹' snd ⁻¹' t) this)
β : X × (↑t : Type u_2) ≃ₜ (↑(snd ⁻¹' t) : Type u_2) :=
  Homeomorph.trans
    (Homeomorph.trans (Homeomorph.prodCongr (Homeomorph.symm (Homeomorph.Set.univ X)) (Homeomorph.refl (↑t : Type u_2)))
      (Homeomorph.symm (Homeomorph.Set.prod univ t)))
    (Homeomorph.setCongr (s := SProd.sprod (α := Set X) univ t) (t := snd ⁻¹' t) ⋯)
⊢ IsProperMap (Y := X × (↑t : Type u_2)) fun (gx : Prod.{u_1, u_2} G (↑t : Type u_2)) ↦ (gx.1 • (↑gx.2 : X), gx.2)

Tactic:
β.symm.isProperMap.comp (Φ_proper.restrictPreimage (snd ⁻¹' t)) |>.comp α.isProperMap

Premises used: Homeomorph.isProperMap, Prod.map, Set.preimage, Homeomorph.symm, IsProperMap.restrictPreimage, Prod.snd, IsProperMap.comp
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : ProperSMul G X
t : Set X
Φ : G × X → X × X := fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
Φ_proper : IsProperMap Φ
α : Prod.{u_1, u_2} G (↑t : Type u_2) ≃ₜ (↑(Φ ⁻¹' snd ⁻¹' t) : Type (max u_1 u_2)) :=
  have this : SProd.sprod (α := Set G) univ t = Φ ⁻¹' snd ⁻¹' t := ⋯;
  Homeomorph.trans
    (Homeomorph.trans (Homeomorph.prodCongr (Homeomorph.symm (Homeomorph.Set.univ G)) (Homeomorph.refl (↑t : Type u_2)))
      (Homeomorph.symm (Homeomorph.Set.prod univ t)))
    (Homeomorph.setCongr (s := SProd.sprod (α := Set G) univ t) (t := Φ ⁻¹' snd ⁻¹' t) this)
β : X × (↑t : Type u_2) ≃ₜ (↑(snd ⁻¹' t) : Type u_2) :=
  Homeomorph.trans
    (Homeomorph.trans (Homeomorph.prodCongr (Homeomorph.symm (Homeomorph.Set.univ X)) (Homeomorph.refl (↑t : Type u_2)))
      (Homeomorph.symm (Homeomorph.Set.prod univ t)))
    (Homeomorph.setCongr (s := SProd.sprod (α := Set X) univ t) (t := snd ⁻¹' t) ⋯)
⊢ IsProperMap (Y := X × (↑t : Type u_2)) fun (gx : Prod.{u_1, u_2} G (↑t : Type u_2)) ↦ (gx.1 • (↑gx.2 : X), gx.2)

Tactic:
exact β.symm.isProperMap.comp (Φ_proper.restrictPreimage (snd ⁻¹' t)) |>.comp α.isProperMap

Premises used: Homeomorph.isProperMap, Set.preimage, Homeomorph.symm, IsProperMap.restrictPreimage, Prod.snd, IsProperMap.comp
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : ProperSMul G X
s : Set G
t : Set X
hs : IsClosed[inst_2] s
ht : IsCompact t
Ψ : Prod.{u_1, u_2} G (↑t : Type u_2) → X × (↑t : Type u_2) :=
  fun (gx : Prod.{u_1, u_2} G (↑t : Type u_2)) ↦ (gx.1 • (↑gx.2 : X), gx.2)
⊢ IsProperMap Ψ

Tactic:
have Ψ_proper : IsProperMap Ψ := ProperSMul.isProperMap_smul_pair_set