-- 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 ≠ ∅}.Finite

Tactic:
simp_rw [← nonempty_iff_ne_empty]

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

Proof state:
case h.mpr.intro.intro.intro.intro.intro.intro.intro.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 : 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' ∧ (g, g⁻¹ • x').2 ∈ K'

Tactic:
exact ⟨by simpa, by simpa⟩

Result:
no goals

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

Tactic:
rintro ⟨x, -, g, -, ⟨-, ⟨⟨x', x'_mem, rfl⟩, ginvx'_mem⟩, rfl⟩⟩

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

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
⊢ ProperSMul G X

Tactic:
rw [properSMul_iff]

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
⊢ IsProperMap fun gx => (gx.1 • gx.2, gx.2)

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)
⊢ ProperlyDiscontinuousSMul G X → ProperSMul G X

Tactic:
intro h

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
⊢ ProperSMul G X

Proof state:
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 : ProperSMul G X
K L : Set X
hK : IsCompact K
hL : IsCompact L
this : IsProperMap fun gx => (gx.1⁻¹ • gx.2, gx.2)
g : G
⊢ g ∈ {g | ∃ x, x ∈ (fun x => g • x) '' K ∩ L} → g ∈ fst '' ((fun gx => (gx.1⁻¹ • gx.2, gx.2)) ⁻¹' K ×ˢ L)

Tactic:
exact fun ⟨_, ⟨x, x_mem, rfl⟩, hx⟩ ↦ ⟨(g, g • x), ⟨by simpa, hx⟩, rfl⟩

Result:
no goals

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

Tactic:
intro K L hK hL

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
hK : IsCompact K
hL : IsCompact L
⊢ {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}.Finite

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
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')
⊢ Continuous snd

Tactic:
fun_prop

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
⊢ IsProperMap fun gx => (gx.1 • gx.2, gx.2)

Tactic:
refine isProperMap_iff_isCompact_preimage.2
  ⟨(continuous_prod_of_discrete_left.2 continuous_const_smul).prod_mk (by fun_prop),
  fun K 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
⊢ 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 : ProperSMul G X
K L : Set X
hK : IsCompact K
hL : IsCompact L
this : IsProperMap fun gx => (gx.1⁻¹ • gx.2, gx.2)
g : G
x✝ : g ∈ {g | ∃ x, x ∈ (fun x => g • x) '' K ∩ L}
x : X
x_mem : x ∈ K
hx : (fun x => g • x) x ∈ L
⊢ ((fun gx => (gx.1⁻¹ • gx.2, gx.2)) (g, g • x)).1 ∈ K

Tactic:
simpa

Result:
no goals