-- Mathlib/Topology/Algebra/ProperAction/ProperlyDiscontinuous.lean
theorem properlyDiscontinuousSMul_iff_properSMul [T2Space X] [DiscreteTopology G]
    [ContinuousConstSMul G X] [CompactlyGeneratedSpace (X × X)] :
    ProperlyDiscontinuousSMul G X ↔ ProperSMul G X

Proof state:
G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : DiscreteTopology G
inst✝¹ : ContinuousConstSMul G X
inst✝ : CompactlyGeneratedSpace (X × X)
h : ProperSMul G X
K L : Set X
hK : IsCompact K
hL : IsCompact L
this : IsProperMap fun gx => (gx.1⁻¹ • gx.2, gx.2)
gx : G × X
hgx : gx ∈ (fun gx => (gx.1⁻¹ • gx.2, gx.2)) ⁻¹' K ×ˢ L
⊢ (fun x => gx.1 • x) (gx.1⁻¹ • gx.2) = gx.2

Tactic:
simp

Result:
no goals

Proof state:
case mp
G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : DiscreteTopology G
inst✝¹ : ContinuousConstSMul G X
inst✝ : CompactlyGeneratedSpace (X × X)
h : ProperlyDiscontinuousSMul G X
K : Set (X × X)
hK : IsCompact K
K' : Set X := fst '' K ∪ snd '' K
hK' : IsCompact K'
E : Set G := {g | ((fun x => g • x) '' K' ∩ K').Nonempty}
fin : E.Finite
this : (fun gx => (gx.1 • gx.2, gx.2)) ⁻¹' K' ×ˢ K' = ⋃ g ∈ E, {g} ×ˢ ((fun x => g⁻¹ • x) '' K' ∩ K')
⊢ IsCompact ((fun gx => (gx.1 • gx.2, gx.2)) ⁻¹' K)

Tactic:
have : IsCompact ((fun gx : G × X ↦ (gx.1 • gx.2, gx.2)) ⁻¹' (K' ×ˢ K')) :=
  this ▸ fin.isCompact_biUnion fun g hg ↦
    isCompact_singleton.prod <| (hK'.image <| continuous_const_smul _).inter hK'

Result:
case mp
G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : DiscreteTopology G
inst✝¹ : ContinuousConstSMul G X
inst✝ : CompactlyGeneratedSpace (X × X)
h : ProperlyDiscontinuousSMul G X
K : Set (X × X)
hK : IsCompact K
K' : Set X := fst '' K ∪ snd '' K
hK' : IsCompact K'
E : Set G := {g | ((fun x => g • x) '' K' ∩ K').Nonempty}
fin : E.Finite
this✝ : (fun gx => (gx.1 • gx.2, gx.2)) ⁻¹' K' ×ˢ K' = ⋃ g ∈ E, {g} ×ˢ ((fun x => g⁻¹ • x) '' K' ∩ K')
this : IsCompact ((fun gx => (gx.1 • gx.2, gx.2)) ⁻¹' K' ×ˢ K')
⊢ IsCompact ((fun gx => (gx.1 • gx.2, gx.2)) ⁻¹' K)

Proof state:
G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : DiscreteTopology G
inst✝¹ : ContinuousConstSMul G X
inst✝ : CompactlyGeneratedSpace (X × X)
h : ProperlyDiscontinuousSMul G X
K : Set (X × X)
hK : IsCompact K
K' : Set X := fst '' K ∪ snd '' K
hK' : IsCompact K'
E : Set G := {g | ((fun x => g • x) '' K' ∩ K').Nonempty}
fin : E.Finite
gx : G × X
x✝ : gx.1 • gx.2 ∈ K' ∧ gx.2 ∈ K'
gx_mem : gx.1 • gx.2 ∈ K'
x_mem : gx.2 ∈ K'
⊢ gx.1⁻¹ • gx.1 • gx.2 = gx.2

Tactic:
simp

Result:
no goals

Proof state:
case mp
G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : DiscreteTopology G
inst✝¹ : ContinuousConstSMul G X
inst✝ : CompactlyGeneratedSpace (X × X)
h : ProperlyDiscontinuousSMul G X
K : Set (X × X)
hK : IsCompact K
K' : Set X := fst '' K ∪ snd '' K
hK' : IsCompact K'
E : Set G := {g | ((fun x => g • x) '' K' ∩ K').Nonempty}
⊢ IsCompact ((fun gx => (gx.1 • gx.2, gx.2)) ⁻¹' K)

Tactic:
have fin : Set.Finite E := by
  simp_rw [E, nonempty_iff_ne_empty]
  exact h.finite_disjoint_inter_image hK' hK'

Result:
case mp
G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : DiscreteTopology G
inst✝¹ : ContinuousConstSMul G X
inst✝ : CompactlyGeneratedSpace (X × X)
h : ProperlyDiscontinuousSMul G X
K : Set (X × X)
hK : IsCompact K
K' : Set X := fst '' K ∪ snd '' K
hK' : IsCompact K'
E : Set G := {g | ((fun x => g • x) '' K' ∩ K').Nonempty}
fin : E.Finite
⊢ IsCompact ((fun gx => (gx.1 • gx.2, gx.2)) ⁻¹' K)

Proof state:
G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : DiscreteTopology G
inst✝¹ : ContinuousConstSMul G X
inst✝ : CompactlyGeneratedSpace (X × X)
h : ProperlyDiscontinuousSMul G X
K : Set (X × X)
hK : IsCompact K
K' : Set X := fst '' K ∪ snd '' K
hK' : IsCompact K'
E : Set G := {g | ((fun x => g • x) '' K' ∩ K').Nonempty}
fin : E.Finite
⊢ (fun gx => (gx.1 • gx.2, gx.2)) ⁻¹' K' ×ˢ K' = ⋃ g ∈ E, {g} ×ˢ ((fun x => g⁻¹ • x) '' K' ∩ K')

Tactic:
ext gx

Result:
case h
G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : DiscreteTopology G
inst✝¹ : ContinuousConstSMul G X
inst✝ : CompactlyGeneratedSpace (X × X)
h : ProperlyDiscontinuousSMul G X
K : Set (X × X)
hK : IsCompact K
K' : Set X := fst '' K ∪ snd '' K
hK' : IsCompact K'
E : Set G := {g | ((fun x => g • x) '' K' ∩ K').Nonempty}
fin : E.Finite
gx : G × X
⊢ gx ∈ (fun gx => (gx.1 • gx.2, gx.2)) ⁻¹' K' ×ˢ K' ↔ gx ∈ ⋃ g ∈ E, {g} ×ˢ ((fun x => g⁻¹ • x) '' K' ∩ K')

Proof state:
case mpr.finite_disjoint_inter_image.hs
G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : DiscreteTopology G
inst✝¹ : ContinuousConstSMul G X
inst✝ : CompactlyGeneratedSpace (X × X)
h : ProperSMul G X
K L : Set X
hK : IsCompact K
hL : IsCompact L
this : IsProperMap fun gx => (gx.1⁻¹ • gx.2, gx.2)
eq : {g | ((fun x => g • x) '' K ∩ L).Nonempty} = fst '' ((fun gx => (gx.1⁻¹ • gx.2, gx.2)) ⁻¹' K ×ˢ L)
⊢ IsCompact {γ | ((fun x => γ • x) '' K ∩ L).Nonempty}

Tactic:
exact eq ▸ IsCompact.image (this.isCompact_preimage <| hK.prod hL) continuous_fst

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
inst✝³ : T2Space X
inst✝² : DiscreteTopology G
inst✝¹ : ContinuousConstSMul G X
inst✝ : CompactlyGeneratedSpace (X × X)
h : ProperlyDiscontinuousSMul G X
K : Set (X × X)
hK : IsCompact K
K' : Set X := fst '' K ∪ snd '' K
hK' : IsCompact K'
E : Set G := {g | ((fun x => g • x) '' K' ∩ K').Nonempty}
fin : E.Finite
x : X
g : G
x' : X
x'_mem : x' ∈ K'
ginvx'_mem : g⁻¹ • x' ∈ K'
⊢ (g, g⁻¹ • x').2 ∈ K'

Tactic:
simpa

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
inst✝³ : T2Space X
inst✝² : DiscreteTopology G
inst✝¹ : ContinuousConstSMul G X
inst✝ : CompactlyGeneratedSpace (X × X)
h : ProperlyDiscontinuousSMul G X
K : Set (X × X)
hK : IsCompact K
K' : Set X := fst '' K ∪ snd '' K
hK' : IsCompact K'
E : Set G := {g | ((fun x => g • x) '' K' ∩ K').Nonempty}
⊢ E.Finite

Tactic:
simp_rw [E, nonempty_iff_ne_empty]

Result:
G : Type u_1
X : Type u_2
inst✝⁷ : Group G
inst✝⁶ : MulAction G X
inst✝⁵ : TopologicalSpace G
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : DiscreteTopology G
inst✝¹ : ContinuousConstSMul G X
inst✝ : CompactlyGeneratedSpace (X × X)
h : ProperlyDiscontinuousSMul G X
K : Set (X × X)
hK : IsCompact K
K' : Set X := fst '' K ∪ snd '' K
hK' : IsCompact K'
E : Set G := {g | ((fun x => g • x) '' K' ∩ K').Nonempty}
⊢ {g | (fun x => g • x) '' K' ∩ K' ≠ ∅}.Finite