-- 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:
case mpr.finite_disjoint_inter_image
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
⊢ {γ | ((fun x => γ • x) '' K ∩ L).Nonempty}.Finite

Tactic:
apply IsCompact.finite_of_discrete

Result:
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
⊢ IsCompact {γ | ((fun x => γ • x) '' K ∩ L).Nonempty}

Proof state:
case mpr
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)
⊢ ProperSMul G X → ProperlyDiscontinuousSMul G X

Tactic:
intro h

Result:
case mpr
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
⊢ ProperlyDiscontinuousSMul 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 : 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').1 • (g, g⁻¹ • x').2 ∈ K'

Tactic:
simpa

Result:
no goals

Proof state:
case mpr
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
⊢ ProperlyDiscontinuousSMul G X

Tactic:
constructor

Result:
case mpr.finite_disjoint_inter_image
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}, IsCompact K → IsCompact L → {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}.Finite

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
⊢ IsCompact {γ | ((fun x => γ • x) '' K ∩ L).Nonempty}

Tactic:
have : IsProperMap (fun gx : G × X ↦ (gx.1⁻¹ • gx.2, gx.2)) :=
  (IsProperMap.prodMap (Homeomorph.isProperMap (Homeomorph.inv G)) isProperMap_id).comp <|
    ProperSMul.isProperMap_smul_pair

Result:
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)
⊢ IsCompact {γ | ((fun x => γ • x) '' K ∩ L).Nonempty}

Proof state:
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.1 • gx.2 ∈ K' ∧ gx.2 ∈ K' ↔
    ∃ i ∈ K', ∃ i_1, i_1 • i ∈ K' ∧ ∃ x, ((∃ x_1 ∈ K', i_1⁻¹ • x_1 = x) ∧ x ∈ K') ∧ (i_1, x) = gx

Tactic:
constructor

Result:
case h.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
gx : G × X
⊢ gx.1 • gx.2 ∈ K' ∧ gx.2 ∈ K' →
    ∃ i ∈ K', ∃ i_1, i_1 • i ∈ K' ∧ ∃ x, ((∃ x_1 ∈ K', i_1⁻¹ • x_1 = x) ∧ x ∈ K') ∧ (i_1, x) = gx

case h.mpr
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
⊢ (∃ i ∈ K', ∃ i_1, i_1 • i ∈ K' ∧ ∃ x, ((∃ x_1 ∈ K', i_1⁻¹ • x_1 = x) ∧ x ∈ K') ∧ (i_1, x) = gx) →
    gx.1 • gx.2 ∈ K' ∧ gx.2 ∈ K'

Proof state:
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')

Tactic:
simp only [mem_preimage, mem_prod, nonempty_def, mem_inter_iff, mem_image,
  exists_exists_and_eq_and, mem_setOf_eq, singleton_prod, iUnion_exists, biUnion_and',
  mem_iUnion, exists_prop, E]

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.1 • gx.2 ∈ K' ∧ gx.2 ∈ K' ↔
    ∃ i ∈ K', ∃ i_1, i_1 • i ∈ K' ∧ ∃ x, ((∃ x_1 ∈ K', i_1⁻¹ • x_1 = x) ∧ x ∈ K') ∧ (i_1, x) = gx

Proof state:
case h.mpr.intro.intro
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
⊢ gx.1 ∈ {g | ∃ x, x ∈ (fun x => g • x) '' K ∩ L}

Tactic:
exact ⟨gx.2, ⟨gx.1⁻¹ • gx.2, hgx.1, by simp⟩, hgx.2⟩

Result:
no goals