awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Group.Defs
Goal:
G : Type u_1
α : Type u_2
inst : TopologicalSpace G
inst_1 : Inv G
inst_2 : ContinuousInv G
f : α → G
l : Filter α
y : G
h : Tendsto f l (𝓝 y)
⊢ Tendsto (fun (x : α) ↦ (f x)⁻¹) l (𝓝 y⁻¹)

Tactic:
(continuous_inv.tendsto y).comp h

Premises used: Continuous.tendsto, Filter.Tendsto.comp, ContinuousInv.continuous_inv
-- Module: Mathlib.Topology.Algebra.Group.Defs
Goal:
G : Type u_1
X : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace G
inst_2 : Inv G
inst_3 : ContinuousInv G
f : X → G
hf : Continuous[inst, inst_1] f
⊢ Continuous[inst, inst_1] fun (x : X) ↦ (f x)⁻¹

Tactic:
continuous_inv.comp hf

Premises used: Continuous.comp, ContinuousInv.continuous_inv
-- Module: Mathlib.Topology.Algebra.Group.Defs
Goal:
G : Type u_1
X : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace G
inst_2 : Inv G
inst_3 : ContinuousInv G
f : X → G
s : Set X
x : X
hf : ContinuousWithinAt f s x
⊢ ContinuousWithinAt.{u_3, u_1} (Y := G) (fun (x : X) ↦ (f x)⁻¹) s x

Tactic:
hf.inv

Premises used: ContinuousWithinAt, Filter.Tendsto.inv
-- Module: Mathlib.Topology.Algebra.Group.Defs
Goal:
G : Type u_1
X : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace G
inst_2 : Inv G
inst_3 : ContinuousInv G
f : X → G
x : X
hf : ContinuousAt f x
⊢ ContinuousAt.{u_3, u_1} (Y := G) (fun (x : X) ↦ (f x)⁻¹) x

Tactic:
hf.inv

Premises used: ContinuousAt, Filter.Tendsto.inv
-- Module: Mathlib.Topology.Algebra.Group.Defs
Goal:
G : Type u_1
X : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace G
inst_2 : Inv G
inst_3 : ContinuousInv G
f : X → G
s : Set X
hf : ContinuousOn f s
⊢ ContinuousOn.{u_3, u_1} (Y := G) (fun (x : X) ↦ (f x)⁻¹) s

Tactic:
fun x hx ↦
  (hf x hx).inv

Premises used: ContinuousWithinAt.inv, ContinuousOn
-- Module: Mathlib.Topology.Algebra.Group.Defs
Goal:
G_1 : Type u_1
α : Type u_2
X : Type u_3
inst : TopologicalSpace X
G : Type u
inst_1 : TopologicalSpace G
inst_2 : Group G
inst_3 : IsTopologicalGroup G
simp : Continuous[instTopologicalSpaceProd, inst_1] fun (p : G × G) ↦ p.1 * p.2⁻¹
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (p : G × G) ↦ p.1 / p.2

Tactic:
simp only [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Topology.Algebra.Group.Defs
Goal:
G_1 : Type u_1
α : Type u_2
X : Type u_3
inst : TopologicalSpace X
G : Type u
inst_1 : TopologicalSpace G
inst_2 : Group G
inst_3 : IsTopologicalGroup G
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (p : G × G) ↦ p.1 * p.2⁻¹

Tactic:
continuous_mul.comp₂ continuous_fst <| continuous_inv.comp continuous_snd

Premises used: Continuous.comp₂, continuous_mul, Continuous.comp, continuous_snd, continuous_fst, ContinuousInv.continuous_inv
-- Module: Mathlib.Topology.Algebra.Group.Defs
Goal:
G_1 : Type u_1
α : Type u_2
X : Type u_3
inst : TopologicalSpace X
G : Type u
inst_1 : TopologicalSpace G
inst_2 : Group G
inst_3 : IsTopologicalGroup G
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (p : G × G) ↦ p.1 * p.2⁻¹

Tactic:
exact continuous_mul.comp₂ continuous_fst <| continuous_inv.comp continuous_snd

Premises used: Continuous.comp₂, continuous_mul, Continuous.comp, continuous_snd, continuous_fst, ContinuousInv.continuous_inv
-- Module: Mathlib.Topology.Algebra.Group.Defs
Goal:
G : Type u_1
α : Type u_2
inst : TopologicalSpace G
inst_1 : Div G
inst_2 : ContinuousDiv G
f g : α → G
l : Filter α
a b : G
hf : Tendsto f l (𝓝 a)
hg : Tendsto g l (𝓝 b)
⊢ Tendsto (fun (x : α) ↦ f x / g x) l (𝓝 (a / b))

Tactic:
(continuous_div'.tendsto (a, b)).comp (hf.prodMk_nhds hg)

Premises used: Prod.mk, ContinuousDiv.continuous_div', Continuous.tendsto, Filter.Tendsto.comp, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Topology.Algebra.Group.Defs
Goal:
G : Type u_1
X : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace G
inst_2 : Div G
inst_3 : ContinuousDiv G
f g : X → G
x : X
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ ContinuousAt.{u_3, u_1} (Y := G) (fun (x : X) ↦ f x / g x) x

Tactic:
hf.div' hg

Premises used: ContinuousAt, Filter.Tendsto.div'
-- Module: Mathlib.Topology.Algebra.Group.Defs
Goal:
G : Type u_1
X : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace G
inst_2 : Div G
inst_3 : ContinuousDiv G
f g : X → G
s : Set X
x : X
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g s x
⊢ ContinuousWithinAt.{u_3, u_1} (Y := G) (fun (x : X) ↦ f x / g x) s x

Tactic:
Filter.Tendsto.div' hf hg

Premises used: ContinuousWithinAt, Filter.Tendsto.div'
-- Module: Mathlib.Topology.Algebra.Group.Defs
Goal:
G : Type u_1
X : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace G
inst_2 : Div G
inst_3 : ContinuousDiv G
f g : X → G
s : Set X
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ ContinuousOn.{u_3, u_1} (Y := G) (fun (x : X) ↦ f x / g x) s

Tactic:
fun x hx => (hf x hx).div' (hg x hx)

Premises used: ContinuousWithinAt.div', ContinuousOn
-- Module: Mathlib.Topology.Algebra.Group.Defs
Goal:
G : Type u_1
X : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace G
inst_2 : Div G
inst_3 : ContinuousDiv G
f g : X → G
hf : Continuous[inst, inst_1] f
hg : Continuous[inst, inst_1] g
⊢ Continuous[inst, inst_1] fun (x : X) ↦ f x / g x

Tactic:
continuous_div'.comp₂ hf hg

Premises used: Continuous.comp₂, ContinuousDiv.continuous_div'
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : SMul Γ α
S : Subgroup Γ
rw :
  (∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := ↥S) {m : ↥S | (m • K ∩ L).Nonempty}) ↔
    ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ S ∧ (g • K ∩ L).Nonempty}
⊢ ProperlyDiscontinuousSMul.{u_1, u_2} (↥S) α ↔
    ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ S ∧ (g • K ∩ L).Nonempty}

Tactic:
rw [properlyDiscontinuousSMul_iff]

Premises used: properlyDiscontinuousSMul_iff
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : SMul Γ α
S : Subgroup Γ
a :
  ∀ (K L : Set α) (hK : IsCompact K) (hL : IsCompact L),
    Set.Finite.{u_1} (α := ↥S) {m : ↥S | (m • K ∩ L).Nonempty} ↔
      Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ S ∧ (g • K ∩ L).Nonempty}
⊢ (∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := ↥S) {m : ↥S | (m • K ∩ L).Nonempty}) ↔
    ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ S ∧ (g • K ∩ L).Nonempty}

Tactic:
congr! with K L hK hL
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : SMul Γ α
S : Subgroup Γ
K L : Set α
hK : IsCompact K
hL : IsCompact L
⊢ Set.Finite.{u_1} (α := ↥S) {m : ↥S | (m • K ∩ L).Nonempty} ↔
    Set.Finite.{u_1} (α := Γ) (image (α := ↥S) (Subtype.val (p := fun (x : Γ) ↦ x ∈ S)) {m : ↥S | (m • K ∩ L).Nonempty})

Tactic:
injOn_subtype_val (s := {m : S | (m • K ∩ L).Nonempty}) |>.bijOn_image.finite_iff_finite

Premises used: Set.BijOn.finite_iff_finite, Set.InjOn.bijOn_image, Set.injOn_subtype_val
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : SMul Γ α
S : Subgroup Γ
K L : Set α
hK : IsCompact K
hL : IsCompact L
h :
  Eq.{u_1 + 1} (α := Set Γ) {g : Γ | g ∈ S ∧ (g • K ∩ L).Nonempty}
    (image (α := ↥S) (Subtype.val (p := fun (x : Γ) ↦ x ∈ S)) {m : ↥S | (m • K ∩ L).Nonempty})
⊢ Set.Finite.{u_1} (α := ↥S) {m : ↥S | (m • K ∩ L).Nonempty} ↔
    Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ S ∧ (g • K ∩ L).Nonempty}

Tactic:
convert! injOn_subtype_val (s := {m : S | (m • K ∩ L).Nonempty}) |>.bijOn_image.finite_iff_finite

Premises used: Set.BijOn.finite_iff_finite, Set.InjOn.bijOn_image, Set.injOn_subtype_val
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : SMul Γ α
S : Subgroup Γ
K L : Set α
hK : IsCompact K
hL : IsCompact L
h :
  ∀ (g : Γ),
    Membership.mem (γ := Set Γ) {g : Γ | g ∈ S ∧ (g • K ∩ L).Nonempty} g ↔
      Membership.mem (γ := Set Γ)
        (image (α := ↥S) (Subtype.val (p := fun (x : Γ) ↦ x ∈ S)) {m : ↥S | (m • K ∩ L).Nonempty}) g
⊢ Eq.{u_1 + 1} (α := Set Γ) {g : Γ | g ∈ S ∧ (g • K ∩ L).Nonempty}
    (image (α := ↥S) (Subtype.val (p := fun (x : Γ) ↦ x ∈ S)) {m : ↥S | (m • K ∩ L).Nonempty})

Tactic:
ext g
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : SMul Γ α
S : Subgroup Γ
K L : Set α
hK : IsCompact K
hL : IsCompact L
g : Γ
⊢ Membership.mem (γ := Set Γ) {g : Γ | g ∈ S ∧ (g • K ∩ L).Nonempty} g ↔
    Membership.mem (γ := Set Γ)
      (image (α := ↥S) (Subtype.val (p := fun (x : Γ) ↦ x ∈ S)) {m : ↥S | (m • K ∩ L).Nonempty}) g

Tactic:
simp [Set.subtype_smul_set, and_comm]

Premises used: and_comm, Set.subtype_smul_set
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : SMul Γ α
G H : Subgroup Γ
hG : ProperlyDiscontinuousSMul.{u_1, u_2} (↥G) α
hGH : H ≤ G
rw :
  ∀ (hG : ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ G ∧ (g • K ∩ L).Nonempty})
    (hGH : H ≤ G) {K L : Set α},
    IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • K ∩ L).Nonempty}
⊢ ProperlyDiscontinuousSMul.{u_1, u_2} (↥H) α

Tactic:
rw [Subgroup.properlyDiscontinuousSMul_iff] at hG ⊢

Premises used: Subgroup.properlyDiscontinuousSMul_iff
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : SMul Γ α
G H : Subgroup Γ
hG : ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ G ∧ (g • K ∩ L).Nonempty}
hGH : H ≤ G
K L : Set α
hK : IsCompact K
hL : IsCompact L
⊢ Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • K ∩ L).Nonempty}

Tactic:
(hG hK hL).subset fun _ ⟨hg, hg'⟩ ↦ ⟨hGH hg, hg'⟩

Premises used: setOf, Membership.mem, Set.Finite.subset, Inter.inter, And, Set.Nonempty, And.intro, HSMul.hSMul, _private.0.Subgroup.properlyDiscontinuousSMul_of_le.match_1
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : SMul Γ α
G H : Subgroup Γ
hG : ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ G ∧ (g • K ∩ L).Nonempty}
hGH : H ≤ G
K L : Set α
hK : IsCompact K
hL : IsCompact L
⊢ Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • K ∩ L).Nonempty}

Tactic:
exact (hG hK hL).subset fun _ ⟨hg, hg'⟩ ↦ ⟨hGH hg, hg'⟩
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : SMul Γ α
inst_3 : ProperlyDiscontinuousSMul Γ α
G : Subgroup Γ
⊢ ProperlyDiscontinuousSMul.{u_1, u_2} (↥G) α

Tactic:
Subgroup.properlyDiscontinuousSMul_of_le ?_ le_top

Premises used: Subgroup.properlyDiscontinuousSMul_of_le, le_top
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : SMul Γ α
inst_3 : ProperlyDiscontinuousSMul Γ α
G : Subgroup Γ
refine : ProperlyDiscontinuousSMul.{u_1, u_2} (↥⊤) α
⊢ ProperlyDiscontinuousSMul.{u_1, u_2} (↥G) α

Tactic:
refine Subgroup.properlyDiscontinuousSMul_of_le ?_ le_top

Premises used: Subgroup.properlyDiscontinuousSMul_of_le, le_top
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : SMul Γ α
inst_3 : ProperlyDiscontinuousSMul Γ α
G : Subgroup Γ
simp : ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | (g • K ∩ L).Nonempty}
⊢ ProperlyDiscontinuousSMul.{u_1, u_2} (↥⊤) α

Tactic:
simp only [Subgroup.properlyDiscontinuousSMul_iff, Subgroup.mem_top, true_and]

Premises used: Subgroup.properlyDiscontinuousSMul_iff, Subgroup.mem_top, true_and
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : SMul Γ α
inst_3 : ProperlyDiscontinuousSMul Γ α
G : Subgroup Γ
K L : Set α
⊢ IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | (g • K ∩ L).Nonempty}

Tactic:
finite_disjoint_inter_image

Premises used: setOf, ProperlyDiscontinuousSMul.finite_disjoint_inter_image
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : SMul Γ α
inst_3 : ProperlyDiscontinuousSMul Γ α
G : Subgroup Γ
⊢ ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | (g • K ∩ L).Nonempty}

Tactic:
exact finite_disjoint_inter_image
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : MulAction Γ α
inst_3 : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ProperlyDiscontinuousSMul.{u_1, u_2} (↥H) α
inst_4 : H.IsFiniteRelIndex G
rw :
  ∀ (hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • K ∩ L).Nonempty})
    [H.IsFiniteRelIndex G] {K L : Set α},
    IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ G ∧ (g • K ∩ L).Nonempty}
⊢ ProperlyDiscontinuousSMul.{u_1, u_2} (↥G) α

Tactic:
rw [Subgroup.properlyDiscontinuousSMul_iff] at hH ⊢

Premises used: Subgroup.properlyDiscontinuousSMul_iff
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : MulAction Γ α
inst_3 : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • K ∩ L).Nonempty}
inst_4 : H.IsFiniteRelIndex G
K L : Set α
hK : IsCompact K
hL : IsCompact L
⊢ ∀ (t : Γ), Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • t • K ∩ L).Nonempty}

Tactic:
have (t : Γ) : {g | g ∈ H ∧ (g • t • K ∩ L).Nonempty}.Finite :=
    hH (hK.image <| continuous_const_smul t) hL
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : MulAction Γ α
inst_3 : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • K ∩ L).Nonempty}
inst_4 : H.IsFiniteRelIndex G
K L : Set α
hK : IsCompact K
hL : IsCompact L
this : ∀ (t : Γ), Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • t • K ∩ L).Nonempty}
obtain :
  ∀ (S : Set ↥G) (hS : IsComplement (↑(H.subgroupOf G) : Set ↥G) S),
    Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ G ∧ (g • K ∩ L).Nonempty}
⊢ Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ G ∧ (g • K ∩ L).Nonempty}

Tactic:
obtain ⟨S, hS, -⟩ := (H.subgroupOf G).exists_isComplement_right 1

Premises used: Subgroup.subgroupOf, OfNat.ofNat, Subgroup.exists_isComplement_right
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : MulAction Γ α
inst_3 : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • K ∩ L).Nonempty}
inst_4 : H.IsFiniteRelIndex G
K L : Set α
hK : IsCompact K
hL : IsCompact L
this : ∀ (t : Γ), Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • t • K ∩ L).Nonempty}
S : Set ↥G
hS : IsComplement (↑(H.subgroupOf G) : Set ↥G) S
have : ∀ (this : Fintype (↥G ⧸ H.subgroupOf G)), (Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S).Finite
⊢ (Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S).Finite

Tactic:
have : Fintype (G ⧸ H.subgroupOf G) := Subgroup.fintypeQuotientOfFiniteIndex
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : MulAction Γ α
inst_3 : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • K ∩ L).Nonempty}
inst_4 : H.IsFiniteRelIndex G
K L : Set α
hK : IsCompact K
hL : IsCompact L
this_1 : ∀ (t : Γ), Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • t • K ∩ L).Nonempty}
S : Set ↥G
hS : IsComplement (↑(H.subgroupOf G) : Set ↥G) S
this : Fintype (↥G ⧸ H.subgroupOf G)
have : ∀ (this : Fintype (↑S : Type u_1)), (Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S).Finite
⊢ (Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S).Finite

Tactic:
have : Fintype S := .ofEquiv _ hS.rightQuotientEquiv
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : MulAction Γ α
inst_3 : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • K ∩ L).Nonempty}
inst_4 : H.IsFiniteRelIndex G
K L : Set α
hK : IsCompact K
hL : IsCompact L
this_1 : ∀ (t : Γ), Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • t • K ∩ L).Nonempty}
S : Set ↥G
hS : IsComplement (↑(H.subgroupOf G) : Set ↥G) S
this_2 : Fintype (↥G ⧸ H.subgroupOf G)
this : Fintype (↑S : Type u_1)
⊢ (Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S).Finite

Tactic:
(toFinite S).image _

Premises used: Set.Finite.image, Set.toFinite
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : MulAction Γ α
inst_3 : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • K ∩ L).Nonempty}
inst_4 : H.IsFiniteRelIndex G
K L : Set α
hK : IsCompact K
hL : IsCompact L
this_1 : ∀ (t : Γ), Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • t • K ∩ L).Nonempty}
S : Set ↥G
hS : IsComplement (↑(H.subgroupOf G) : Set ↥G) S
this_2 : Fintype (↥G ⧸ H.subgroupOf G)
this : Fintype (↑S : Type u_1)
⊢ (Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S).Finite

Tactic:
exact (toFinite S).image _

Premises used: Set.Finite.image, Set.toFinite
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : MulAction Γ α
inst_3 : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • K ∩ L).Nonempty}
inst_4 : H.IsFiniteRelIndex G
K L : Set α
hK : IsCompact K
hL : IsCompact L
this : ∀ (t : Γ), Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • t • K ∩ L).Nonempty}
S : Set ↥G
hS : IsComplement (↑(H.subgroupOf G) : Set ↥G) S
⊢ (Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S).Finite

Tactic:
have hT : (Subtype.val '' S).Finite := by
    have : Fintype (G ⧸ H.subgroupOf G) := Subgroup.fintypeQuotientOfFiniteIndex
    have : Fintype S := .ofEquiv _ hS.rightQuotientEquiv
    exact (toFinite S).image _
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : MulAction Γ α
inst_3 : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • K ∩ L).Nonempty}
inst_4 : H.IsFiniteRelIndex G
K L : Set α
hK : IsCompact K
hL : IsCompact L
this : ∀ (t : Γ), Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • t • K ∩ L).Nonempty}
S : Set ↥G
hS : IsComplement (↑(H.subgroupOf G) : Set ↥G) S
hT : (Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S).Finite
g : Γ
hg : g ∈ G
obtain :
  ∀ (p : (↑(↑(H.subgroupOf G) : Set ↥G) : Type u_1) × (↑S : Type u_1))
    (hp : (↑p.1 : ↥G) * (↑p.2 : ↥G) = Subtype.mk (p := fun (x : Γ) ↦ x ∈ G) g hg),
    ∃ t ∈ Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S, g * t⁻¹ ∈ H
⊢ ∃ t ∈ Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S, g * t⁻¹ ∈ H

Tactic:
obtain ⟨p, hp⟩ := (hS.existsUnique ⟨g, hg⟩).exists

Premises used: ExistsUnique.exists, Subgroup.IsComplement.existsUnique, Subtype.mk
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : MulAction Γ α
inst_3 : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • K ∩ L).Nonempty}
inst_4 : H.IsFiniteRelIndex G
K L : Set α
hK : IsCompact K
hL : IsCompact L
this : ∀ (t : Γ), Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • t • K ∩ L).Nonempty}
S : Set ↥G
hS : IsComplement (↑(H.subgroupOf G) : Set ↥G) S
hT : (Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S).Finite
g : Γ
hg : g ∈ G
p : (↑(↑(H.subgroupOf G) : Set ↥G) : Type u_1) × (↑S : Type u_1)
hp : (↑p.1 : ↥G) * (↑p.2 : ↥G) = Subtype.mk (p := fun (x : Γ) ↦ x ∈ G) g hg
⊢ ∃ t ∈ Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S, g * t⁻¹ ∈ H

Tactic:
aesop
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : MulAction Γ α
inst_3 : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • K ∩ L).Nonempty}
inst_4 : H.IsFiniteRelIndex G
K L : Set α
hK : IsCompact K
hL : IsCompact L
this : ∀ (t : Γ), Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • t • K ∩ L).Nonempty}
S : Set ↥G
hS : IsComplement (↑(H.subgroupOf G) : Set ↥G) S
hT : (Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S).Finite
⊢ ∀ {g : Γ} (hg : g ∈ G), ∃ t ∈ Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S, g * t⁻¹ ∈ H

Tactic:
have hS' {g : Γ} (hg : g ∈ G) : ∃ t ∈ Subtype.val '' S, g * t⁻¹ ∈ H := by
    obtain ⟨p, hp⟩ := (hS.existsUnique ⟨g, hg⟩).exists
    aesop
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : MulAction Γ α
inst_3 : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • K ∩ L).Nonempty}
inst_4 : H.IsFiniteRelIndex G
K L : Set α
hK : IsCompact K
hL : IsCompact L
this : ∀ (t : Γ), Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • t • K ∩ L).Nonempty}
S : Set ↥G
hS : IsComplement (↑(H.subgroupOf G) : Set ↥G) S
hT : (Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S).Finite
hS' : ∀ {g : Γ} (hg : g ∈ G), ∃ t ∈ Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S, g * t⁻¹ ∈ H
⊢ Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ G ∧ (g • K ∩ L).Nonempty}

Tactic:
(hT.biUnion <| fun t ht ↦ (this t).map fun g ↦ g * t).subset fun g ↦ ?_

Premises used: HMul.hMul, Set.Finite.subset, Set.Finite.map, Set.Finite.biUnion
-- Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : MulAction Γ α
inst_3 : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • K ∩ L).Nonempty}
inst_4 : H.IsFiniteRelIndex G
K L : Set α
hK : IsCompact K
hL : IsCompact L
this : ∀ (t : Γ), Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ H ∧ (g • t • K ∩ L).Nonempty}
S : Set ↥G
hS : IsComplement (↑(H.subgroupOf G) : Set ↥G) S
hT : (Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S).Finite
hS' : ∀ {g : Γ} (hg : g ∈ G), ∃ t ∈ Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S, g * t⁻¹ ∈ H
refine :
  ∀ (g : Γ),
    Membership.mem (γ := Set Γ) {g : Γ | g ∈ G ∧ (g • K ∩ L).Nonempty} g →
      Membership.mem (γ := Set Γ)
        (⋃ i ∈ Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S,
          (fun (g : Γ) ↦ g * i) <$> {g : Γ | g ∈ H ∧ (g • i • K ∩ L).Nonempty})
        g
⊢ Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ G ∧ (g • K ∩ L).Nonempty}

Tactic:
refine (hT.biUnion <| fun t ht ↦ (this t).map fun g ↦ g * t).subset fun g ↦ ?_

Premises used: HMul.hMul, Set.Finite.subset, Set.Finite.map, Set.Finite.biUnion