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
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)
Ψ_proper : IsProperMap Ψ
⊢ s • t = fst ∘ Ψ '' fst ⁻¹' s

Tactic:
have : s • t = (fst ∘ Ψ) '' fst ⁻¹' s :=
    subset_antisymm
      (smul_subset_iff.mpr fun g hg x hx ↦ mem_image_of_mem (fst ∘ Ψ) (x := ⟨g, ⟨x, hx⟩⟩) hg)
      (image_subset_iff.mpr fun ⟨g, ⟨x, hx⟩⟩ hg ↦ smul_mem_smul hg hx)
-- 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)
Ψ_proper : IsProperMap Ψ
this : s • t = fst ∘ Ψ '' fst ⁻¹' s
rw : IsClosed[inst_3] (fst ∘ Ψ '' fst ⁻¹' s)
⊢ IsClosed[inst_3] (s • t)

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
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)
Ψ_proper : IsProperMap Ψ
this : s • t = fst ∘ Ψ '' fst ⁻¹' s
⊢ CompactSpace.{u_2} (↑t : Type u_2)

Tactic:
have : CompactSpace t := isCompact_iff_compactSpace.mp ht
-- 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)
Ψ_proper : IsProperMap Ψ
this_1 : s • t = fst ∘ Ψ '' fst ⁻¹' s
this : CompactSpace.{u_2} (↑t : Type u_2)
⊢ IsClosed[inst_3] (fst ∘ Ψ '' fst ⁻¹' s)

Tactic:
(isProperMap_fst_of_compactSpace.comp Ψ_proper).isClosedMap _ (hs.preimage continuous_fst)

Premises used: IsProperMap.isClosedMap, isProperMap_fst_of_compactSpace, continuous_fst, IsClosed.preimage, 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)
Ψ_proper : IsProperMap Ψ
this_1 : s • t = fst ∘ Ψ '' fst ⁻¹' s
this : CompactSpace.{u_2} (↑t : Type u_2)
⊢ IsClosed[inst_3] (fst ∘ Ψ '' fst ⁻¹' s)

Tactic:
exact (isProperMap_fst_of_compactSpace.comp Ψ_proper).isClosedMap _ (hs.preimage continuous_fst)

Premises used: IsProperMap.isClosedMap, isProperMap_fst_of_compactSpace, continuous_fst, IsClosed.preimage, IsProperMap.comp
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
X : Type u_2
inst : TopologicalSpace X
G : Type u_3
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : TopologicalSpace G
inst_4 : ProperSMul G X
U V : Set X
hU : IsCompact U
hV : IsCompact V
⊢ IsCompact.{u_3} (X := G) (image (α := G × X) fst ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' V ×ˢ U))

Tactic:
((ProperSMul.isProperMap_smul_pair (G := G)).isCompact_preimage (hV.prod hU)).image
      continuous_fst

Premises used: IsCompact.prod, ProperSMul.isProperMap_smul_pair, continuous_fst, IsProperMap.isCompact_preimage, IsCompact.image
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
X : Type u_2
inst : TopologicalSpace X
G : Type u_3
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : TopologicalSpace G
inst_4 : ProperSMul G X
U V : Set X
hU : IsCompact U
hV : IsCompact V
h :
  Eq.{u_3 + 1} (α := Set G) {g : G | (g • U ∩ V).Nonempty}
    (image (α := G × X) fst ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' V ×ˢ U))
⊢ IsCompact.{u_3} (X := G) {g : G | (g • U ∩ V).Nonempty}

Tactic:
convert!
    ((ProperSMul.isProperMap_smul_pair (G := G)).isCompact_preimage (hV.prod hU)).image
      continuous_fst

Premises used: IsCompact.prod, ProperSMul.isProperMap_smul_pair, continuous_fst, IsProperMap.isCompact_preimage, IsCompact.image
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
X : Type u_2
inst : TopologicalSpace X
G : Type u_3
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : TopologicalSpace G
inst_4 : ProperSMul G X
U V : Set X
hU : IsCompact U
hV : IsCompact V
h :
  ∀ (g : G),
    Membership.mem (γ := Set G) {g : G | (g • U ∩ V).Nonempty} g ↔
      Membership.mem (γ := Set G) (image (α := G × X) fst ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' V ×ˢ U)) g
⊢ Eq.{u_3 + 1} (α := Set G) {g : G | (g • U ∩ V).Nonempty}
    (image (α := G × X) fst ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' V ×ˢ U))

Tactic:
ext g
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
X : Type u_2
inst : TopologicalSpace X
G : Type u_3
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : TopologicalSpace G
inst_4 : ProperSMul G X
U V : Set X
hU : IsCompact U
hV : IsCompact V
g : G
this : (∃ v ∈ g • U, v ∈ V) ↔ ∃ (u : X), g • u ∈ V ∧ u ∈ U
⊢ Membership.mem (γ := Set G) {g : G | (g • U ∩ V).Nonempty} g ↔
    Membership.mem (γ := Set G) (image (α := G × X) fst ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' V ×ˢ U)) g

Tactic:
simpa
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
X : Type u_2
inst : TopologicalSpace X
G : Type u_3
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : TopologicalSpace G
inst_4 : ProperSMul G X
U V : Set X
hU : IsCompact U
hV : IsCompact V
g : G
h : (∃ v ∈ g • U, v ∈ V) ↔ ∃ (u : X), g • u ∈ V ∧ u ∈ U
⊢ Membership.mem (γ := Set G) {g : G | (g • U ∩ V).Nonempty} g ↔
    Membership.mem (γ := Set G) (image (α := G × X) fst ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' V ×ˢ U)) g

Tactic:
suffices (∃ v, v ∈ g • U ∧ v ∈ V) ↔ ∃ u, g • u ∈ V ∧ u ∈ U by simpa
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
X : Type u_2
inst : TopologicalSpace X
G : Type u_3
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : TopologicalSpace G
inst_4 : ProperSMul G X
U V : Set X
hU : IsCompact U
hV : IsCompact V
g : G
h :
  (∃ (a : X),
      Membership.mem (α := X) (g • U) ((MulAction.toPerm g : (a : X) → X) a : X) ∧
        Membership.mem (α := X) V ((MulAction.toPerm g : (a : X) → X) a : X)) ↔
    ∃ (u : X), g • u ∈ V ∧ u ∈ U
⊢ (∃ v ∈ g • U, v ∈ V) ↔ ∃ (u : X), g • u ∈ V ∧ u ∈ U

Tactic:
rw [← (MulAction.toPerm g).exists_congr_right]

Premises used: Equiv.exists_congr_right, MulAction.toPerm
-- Module: Mathlib.Topology.Algebra.ProperAction.Basic
Goal:
X : Type u_2
inst : TopologicalSpace X
G : Type u_3
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : TopologicalSpace G
inst_4 : ProperSMul G X
U V : Set X
hU : IsCompact U
hV : IsCompact V
g : G
⊢ (∃ (a : X),
      Membership.mem (α := X) (g • U) ((MulAction.toPerm g : (a : X) → X) a : X) ∧
        Membership.mem (α := X) V ((MulAction.toPerm g : (a : X) → X) a : X)) ↔
    ∃ (u : X), g • u ∈ V ∧ u ∈ U

Tactic:
simp [and_comm]

Premises used: and_comm
-- 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 : ContinuousSMul G X
inst_5 : IsTopologicalGroup G
inst_6 : IsPretransitive G X
x : X
hx : IsProperMap.{u_1, u_2} (Y := X) fun (g : G) ↦ g • x
isProperMap_smul_pair : IsProperMap (Y := X × X) fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
⊢ ProperSMul G X

Tactic:
constructor
-- 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 : ContinuousSMul G X
inst_5 : IsTopologicalGroup G
inst_6 : IsPretransitive G X
x : X
hx : IsProperMap.{u_1, u_2} (Y := X) fun (g : G) ↦ g • x
f : G × G → G × X := Prod.map id fun (g : G) ↦ g • x
⊢ Function.Surjective f

Tactic:
have hfsurj : f.Surjective := Function.surjective_id.prodMap (surjective_smul G 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
inst_4 : ContinuousSMul G X
inst_5 : IsTopologicalGroup G
inst_6 : IsPretransitive G X
x : X
hx : IsProperMap.{u_1, u_2} (Y := X) fun (g : G) ↦ g • x
f : G × G → G × X := Prod.map id fun (g : G) ↦ g • x
hfsurj : Function.Surjective f
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] f

Tactic:
fun_prop
-- 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 : ContinuousSMul G X
inst_5 : IsTopologicalGroup G
inst_6 : IsPretransitive G X
x : X
hx : IsProperMap.{u_1, u_2} (Y := X) fun (g : G) ↦ g • x
f : G × G → G × X := Prod.map id fun (g : G) ↦ g • x
hfsurj : Function.Surjective f
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)

Tactic:
fun_prop
-- 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 : ContinuousSMul G X
inst_5 : IsTopologicalGroup G
inst_6 : IsPretransitive G X
x : X
hx : IsProperMap.{u_1, u_2} (Y := X) fun (g : G) ↦ g • x
f : G × G → G × X := Prod.map id fun (g : G) ↦ g • x
hfsurj : Function.Surjective f
isProperMap_smul_pair : IsProperMap.{u_1, u_2} (Y := X × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ∘ f)
⊢ IsProperMap (Y := X × X) fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)

Tactic:
refine isProperMap_of_comp_of_surj (by fun_prop) (by fun_prop) ?_ hfsurj

Premises used: isProperMap_of_comp_of_surj
-- 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 : ContinuousSMul G X
inst_5 : IsTopologicalGroup G
inst_6 : IsPretransitive G X
x : X
hx : IsProperMap.{u_1, u_2} (Y := X) fun (g : G) ↦ g • x
f : G × G → G × X := Prod.map id fun (g : G) ↦ g • x
hfsurj : Function.Surjective f
⊢ IsProperMap.{u_1, u_2} (Y := X × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ∘ f)

Tactic:
simpa [Function.comp_def, Prod.map_apply, mul_smul]
    using (hx.prodMap hx).comp (ProperSMul.isProperMap_smul_pair (G := G))

Premises used: ProperSMul.isProperMap_smul_pair, Function.comp_def, IsProperMap.prodMap, Prod.map_apply, SemigroupAction.mul_smul, IsProperMap.comp
-- Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : ContinuousSMul G X
⊢ ProperSMul G X ↔ ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}

Tactic:
⟨fun h ↦ ProperSMul.isCompact_setOf_inter_nonempty, fun h ↦ ⟨?_⟩⟩

Premises used: ProperSMul.mk, Iff.intro, ProperSMul.isCompact_setOf_inter_nonempty
-- Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : ContinuousSMul G X
refine :
  ∀ (h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}),
    IsProperMap (Y := X × X) fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
⊢ ProperSMul G X ↔ ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}

Tactic:
refine ⟨fun h ↦ ProperSMul.isCompact_setOf_inter_nonempty, fun h ↦ ⟨?_⟩⟩
-- Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}
⊢ Continuous (Y := X × X) fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}
refine : ∀ {K : Set (X × X)} (hK : IsCompact K), IsCompact (X := G × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' K)
⊢ IsProperMap (Y := X × X) fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)

Tactic:
refine isProperMap_iff_isCompact_preimage.mpr ⟨by fun_prop, fun {K} hK ↦ ?_⟩

Premises used: Iff.mpr, isProperMap_iff_isCompact_preimage, And.intro
-- Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
⊢ IsCompact U

Tactic:
have hU : IsCompact U := hK.image continuous_fst
-- Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
hU : IsCompact U
⊢ IsCompact V

Tactic:
have hV : IsCompact V := hK.image continuous_snd
-- Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
hU : IsCompact U
hV : IsCompact V
this : IsCompact (X := G × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)
⊢ Continuous (Y := X × X) fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
hU : IsCompact U
hV : IsCompact V
this : IsCompact (X := G × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)
apply :
  Subset (α := Set (G × X)) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' K)
    ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)
⊢ IsCompact (X := G × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' K)

Tactic:
apply this.of_isClosed_subset (hK.isClosed.preimage <| by fun_prop)

Premises used: IsCompact.of_isClosed_subset, IsClosed.preimage, IsCompact.isClosed
-- Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
hU : IsCompact U
hV : IsCompact V
this : IsCompact (X := G × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)
⊢ Subset (α := Set (G × X)) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' K)
    ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)

Tactic:
Set.preimage_mono Set.subset_fst_image_prod_snd_image

Premises used: Set.subset_fst_image_prod_snd_image, Set.preimage_mono
-- Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
hU : IsCompact U
hV : IsCompact V
this : IsCompact (X := G × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)
⊢ Subset (α := Set (G × X)) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' K)
    ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)

Tactic:
exact Set.preimage_mono Set.subset_fst_image_prod_snd_image

Premises used: Set.subset_fst_image_prod_snd_image, Set.preimage_mono
-- Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
hU : IsCompact U
hV : IsCompact V
suffices : IsCompact (X := G × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)
⊢ IsCompact (X := G × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' K)

Tactic:
suffices IsCompact ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' (U ×ˢ V)) by
    apply this.of_isClosed_subset (hK.isClosed.preimage <| by fun_prop)
    exact Set.preimage_mono Set.subset_fst_image_prod_snd_image
-- Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
hU : IsCompact U
hV : IsCompact V
ht : IsClosed (X := G × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)
h₁ : (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V ⊆ SProd.sprod (α := Set G) {g : G | (g • V ∩ U).Nonempty} V
⊢ IsCompact (X := G × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)

Tactic:
apply ((h hV hU).prod hV).of_isClosed_subset

Premises used: IsCompact.prod, IsCompact.of_isClosed_subset
-- Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
hU : IsCompact U
hV : IsCompact V
⊢ Continuous (Y := X × X) fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
hU : IsCompact U
hV : IsCompact V
⊢ IsClosed (X := G × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)

Tactic:
exact (hU.prod hV).isClosed.preimage (by fun_prop)

Premises used: IsCompact.prod, IsClosed.preimage, IsCompact.isClosed
-- Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
hU : IsCompact U
hV : IsCompact V
⊢ (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V ⊆ SProd.sprod (α := Set G) {g : G | (g • V ∩ U).Nonempty} V

Tactic:
fun ⟨g, x⟩ ⟨hgx, hgx'⟩ ↦ ⟨⟨g • x, smul_mem_smul_set hgx', hgx⟩, hgx'⟩

Premises used: _private.0.MulAction.properSMul_iff_isCompact_setOf_inter_nonempty.match_2, _private.0.MulAction.properSMul_iff_isCompact_setOf_inter_nonempty.match_1, SProd.sprod, setOf, Membership.mem, Prod.mk, Set.Subset, Inter.inter, Set.Nonempty, And.intro, Exists.intro, HSMul.hSMul, Set.smul_mem_smul_set
-- Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
hU : IsCompact U
hV : IsCompact V
⊢ (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V ⊆ SProd.sprod (α := Set G) {g : G | (g • V ∩ U).Nonempty} V

Tactic:
exact fun ⟨g, x⟩ ⟨hgx, hgx'⟩ ↦ ⟨⟨g • x, smul_mem_smul_set hgx', hgx⟩, hgx'⟩
-- Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : DiscreteTopology G
inst_7 : ContinuousConstSMul G X
⊢ ContinuousSMul G X

Tactic:
have : ContinuousSMul G X := ⟨continuous_prod_of_discrete_left.mpr continuous_const_smul⟩
-- Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : DiscreteTopology G
inst_7 : ContinuousConstSMul G X
this : ContinuousSMul G X
simp :
  ProperlyDiscontinuousSMul G X ↔
    ∀ {U V : Set X}, IsCompact U → IsCompact V → Set.Finite.{u_1} (α := G) {g : G | (g • U ∩ V).Nonempty}
⊢ ProperlyDiscontinuousSMul G X ↔ ProperSMul G X

Tactic:
simp only [MulAction.properSMul_iff_isCompact_setOf_inter_nonempty, isCompact_iff_finite]

Premises used: isCompact_iff_finite, MulAction.properSMul_iff_isCompact_setOf_inter_nonempty