-- 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 : 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

Tactic:
exact h.finite_disjoint_inter_image hK' hK'

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

Tactic:
ext g

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 : 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)

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

Tactic:
constructor

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

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

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 : 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 ∈ fst '' ((fun gx => (gx.1⁻¹ • gx.2, gx.2)) ⁻¹' K ×ˢ L) → g ∈ {g | ∃ x, x ∈ (fun x => g • x) '' K ∩ L}

Tactic:
rintro ⟨gx, hgx, rfl⟩

Result:
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}

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
⊢ IsCompact ((fun gx => (gx.1 • gx.2, gx.2)) ⁻¹' K)

Tactic:
let K' := fst '' K ∪ snd '' K

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
⊢ 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 | ((fun x => g • x) '' K ∩ L).Nonempty} = fst '' ((fun gx => (gx.1⁻¹ • gx.2, gx.2)) ⁻¹' K ×ˢ L)

Tactic:
simp_rw [nonempty_def]

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

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 : 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:
exact fun ⟨gx_mem, x_mem⟩ ↦ ⟨gx.2, x_mem, gx.1, gx_mem,
  ⟨gx.2, ⟨⟨gx.1 • gx.2, gx_mem, by simp⟩, x_mem⟩, rfl⟩⟩

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
⊢ 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
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)

Tactic:
exact this.of_isClosed_subset (hK.isClosed.preimage <|
  (continuous_prod_of_discrete_left.2 continuous_const_smul).prod_mk (by fun_prop)) <|
  preimage_mono fun x hx ↦ ⟨Or.inl ⟨x, hx, rfl⟩, Or.inr ⟨x, hx, rfl⟩⟩

Result:
no goals