-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem Subgroup.properlyDiscontinuousSMul_of_tendsto_cofinite (S : Subgroup G)
    (hS : Tendsto S.subtype cofinite (cocompact G)) : ProperlyDiscontinuousSMul S G :=
  { finite_disjoint_inter_image

Proof state:
case h.e'_2.h
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : (⇑S.subtype ⁻¹' ((fun p => p.1 / p.2) '' L ×ˢ K)).Finite
x : ↥S
⊢ x ∈ {γ | (fun x => γ • x) '' K ∩ L ≠ ∅} ↔ x ∈ ⇑S.subtype ⁻¹' ((fun p => p.1 / p.2) '' L ×ˢ K)

Tactic:
simp only [image_smul, mem_setOf_eq, coe_subtype, mem_preimage, mem_image, Prod.exists]

Result:
case h.e'_2.h
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : (⇑S.subtype ⁻¹' ((fun p => p.1 / p.2) '' L ×ˢ K)).Finite
x : ↥S
⊢ x • K ∩ L ≠ ∅ ↔ ∃ a b, (a, b) ∈ L ×ˢ K ∧ a / b = ↑x

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
⊢ {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}.Finite

Tactic:
have H : Set.Finite _ := hS ((hL.prod hK).image continuous_div').compl_mem_cocompact

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : (⇑S.subtype ⁻¹' ((fun p => p.1 / p.2) '' L ×ˢ K)ᶜ)ᶜ.Finite
⊢ {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}.Finite

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : (⇑S.subtype ⁻¹' ((fun p => p.1 / p.2) '' L ×ˢ K)ᶜ)ᶜ.Finite
⊢ {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}.Finite

Tactic:
rw [preimage_compl, compl_compl] at H

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : (⇑S.subtype ⁻¹' ((fun p => p.1 / p.2) '' L ×ˢ K)).Finite
⊢ {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}.Finite

Proof state:
case h.e'_2
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : (⇑S.subtype ⁻¹' ((fun p => p.1 / p.2) '' L ×ˢ K)).Finite
⊢ {γ | (fun x => γ • x) '' K ∩ L ≠ ∅} = ⇑S.subtype ⁻¹' ((fun p => p.1 / p.2) '' L ×ˢ K)

Tactic:
ext x

Result:
case h.e'_2.h
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : (⇑S.subtype ⁻¹' ((fun p => p.1 / p.2) '' L ×ˢ K)).Finite
x : ↥S
⊢ x ∈ {γ | (fun x => γ • x) '' K ∩ L ≠ ∅} ↔ x ∈ ⇑S.subtype ⁻¹' ((fun p => p.1 / p.2) '' L ×ˢ K)

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : (⇑S.subtype ⁻¹' ((fun p => p.1 / p.2) '' L ×ˢ K)).Finite
⊢ {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}.Finite

Tactic:
convert H

Result:
case h.e'_2
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : (⇑S.subtype ⁻¹' ((fun p => p.1 / p.2) '' L ×ˢ K)).Finite
⊢ {γ | (fun x => γ • x) '' K ∩ L ≠ ∅} = ⇑S.subtype ⁻¹' ((fun p => p.1 / p.2) '' L ×ˢ K)

Proof state:
case h.e'_2.h
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : (⇑S.subtype ⁻¹' ((fun p => p.1 / p.2) '' L ×ˢ K)).Finite
x : ↥S
⊢ x • K ∩ L ≠ ∅ ↔ ∃ a b, (a, b) ∈ L ×ˢ K ∧ a / b = ↑x

Tactic:
exact Set.smul_inter_ne_empty_iff'

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
⊢ ∀ {K L : Set G}, IsCompact K → IsCompact L → {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}.Finite

Tactic:
intro K L hK hL

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
⊢ {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}.Finite