awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.CompactOpen (goal)
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
inst_8 : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : Filter.HasBasis (𝓝 1) (fun (x : ℕ) ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : Membership.mem (γ := Filter X) (𝓝 1) U0
U_aux : ℕ → (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7) :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7))
      (Subtype.mk (p := fun (x : Set X) ↦
        Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x) U0 hU0o)
      (fun (x : ℕ) (S : (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7)) ↦
        let h := ⋯;
        Subtype.mk (p := fun (x : Set X) ↦
          Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x)
          (Classical.choose (p := fun (x : Set X) ↦
            Membership.mem (γ := Filter X) (𝓝 1) x ∧ IsClosed[inst] x ∧ x⁻¹ = x ∧ x * x ⊆ (↑S : Set X)) h)
          ⋯)
      t
U : ℕ → Set X := fun (n : ℕ) ↦ (↑(U_aux n) : Set X)
hU1 : ∀ (n : ℕ), Membership.mem (γ := Filter X) (𝓝 1) (U n)
hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n
hU4 : ∀ (f : X →* Y), Set.MapsTo (⇑f : (a : X) → Y) (U 0) (V 0) → ∀ (n : ℕ), Set.MapsTo (⇑f : (a : X) → Y) (U n) (V n)
⊢ LocallyCompactSpace (X →ₜ* Y)
have apply : EquicontinuousAt (X := X) (α := Y)
  (fun (f : (↑{f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) (U 0) (V 0)} : Type (max u_7 u_8))) ↦
    (⇑(↑f : X →* Y) : (a : X) → Y))
  1
Tactic: apply locallyCompactSpace_of_equicontinuousAt (U 0) (V 0) hU0c (hVo.mem_of_mem trivial)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.CompactOpen (goal)
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
inst_8 : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : Filter.HasBasis (𝓝 1) (fun (x : ℕ) ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : Membership.mem (γ := Filter X) (𝓝 1) U0
U_aux : ℕ → (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7) :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7))
      (Subtype.mk (p := fun (x : Set X) ↦
        Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x) U0 hU0o)
      (fun (x : ℕ) (S : (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7)) ↦
        let h := ⋯;
        Subtype.mk (p := fun (x : Set X) ↦
          Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x)
          (Classical.choose (p := fun (x : Set X) ↦
            Membership.mem (γ := Filter X) (𝓝 1) x ∧ IsClosed[inst] x ∧ x⁻¹ = x ∧ x * x ⊆ (↑S : Set X)) h)
          ⋯)
      t
U : ℕ → Set X := fun (n : ℕ) ↦ (↑(U_aux n) : Set X)
hU1 : ∀ (n : ℕ), Membership.mem (γ := Filter X) (𝓝 1) (U n)
hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n
hU4 : ∀ (f : X →* Y), Set.MapsTo (⇑f : (a : X) → Y) (U 0) (V 0) → ∀ (n : ℕ), Set.MapsTo (⇑f : (a : X) → Y) (U n) (V n)
⊢ EquicontinuousAt (X := X) (α := Y)
    (fun (f : (↑{f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) (U 0) (V 0)} : Type (max u_7 u_8))) ↦
      (⇑(↑f : X →* Y) : (a : X) → Y))
    1
have rw : ∀ (k : ℕ),
  True →
    ∀ᶠ (x : X) in 𝓝 1,
      ∀ (i : (↑{f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) (U 0) (V 0)} : Type (max u_7 u_8))),
        Membership.mem.{u_8, u_8} (α := Y × Y) (γ := Set (Y × Y)) {x : Y × Y | x.2 / x.1 ∈ V k}
          ((((↑i : X →* Y) : (a : X) → Y) 1, ((↑i : X →* Y) : (a : X) → Y) x) : Y × Y)
Tactic: rw [hVo.uniformity_of_nhds_one.equicontinuousAt_iff_right]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.CompactOpen (goal)
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
inst_8 : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : Filter.HasBasis (𝓝 1) (fun (x : ℕ) ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : Membership.mem (γ := Filter X) (𝓝 1) U0
U_aux : ℕ → (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7) :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7))
      (Subtype.mk (p := fun (x : Set X) ↦
        Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x) U0 hU0o)
      (fun (x : ℕ) (S : (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7)) ↦
        let h := ⋯;
        Subtype.mk (p := fun (x : Set X) ↦
          Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x)
          (Classical.choose (p := fun (x : Set X) ↦
            Membership.mem (γ := Filter X) (𝓝 1) x ∧ IsClosed[inst] x ∧ x⁻¹ = x ∧ x * x ⊆ (↑S : Set X)) h)
          ⋯)
      t
U : ℕ → Set X := fun (n : ℕ) ↦ (↑(U_aux n) : Set X)
hU1 : ∀ (n : ℕ), Membership.mem (γ := Filter X) (𝓝 1) (U n)
hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n
hU4 : ∀ (f : X →* Y), Set.MapsTo (⇑f : (a : X) → Y) (U 0) (V 0) → ∀ (n : ℕ), Set.MapsTo (⇑f : (a : X) → Y) (U n) (V n)
⊢ ∀ (k : ℕ),
    True →
      ∀ᶠ (x : X) in 𝓝 1,
        ∀ (i : (↑{f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) (U 0) (V 0)} : Type (max u_7 u_8))),
          Membership.mem.{u_8, u_8} (α := Y × Y) (γ := Set (Y × Y)) {x : Y × Y | x.2 / x.1 ∈ V k}
            ((((↑i : X →* Y) : (a : X) → Y) 1, ((↑i : X →* Y) : (a : X) → Y) x) : Y × Y)
have refine : ∀ (n : ℕ),
  True →
    ∀ (x : X) (hx : x ∈ U n) (x_1 : (↑{f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) (U 0) (V 0)} : Type (max u_7 u_8)))
      (f : X →* Y) (hf : Membership.mem (γ := Set (X →* Y)) {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) (U 0) (V 0)} f),
      Membership.mem.{u_8, u_8} (α := Y × Y) (γ := Set (Y × Y)) {x : Y × Y | x.2 / x.1 ∈ V n}
        ((((↑(Subtype.mk (p := fun (x : X →* Y) ↦
                      Membership.mem (γ := Set (X →* Y)) {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) (U 0) (V 0)} x) f
                      hf) :
                  X →* Y) :
                (a : X) → Y)
              1,
            ((↑(Subtype.mk (p := fun (x : X →* Y) ↦
                      Membership.mem (γ := Set (X →* Y)) {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) (U 0) (V 0)} x) f
                      hf) :
                  X →* Y) :
                (a : X) → Y)
              x) :
          Y × Y)
Tactic: refine fun n _ ↦ Filter.eventually_iff_exists_mem.mpr ⟨U n, hU1 n, fun x hx ⟨f, hf⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.CompactOpen (goal)
Goal:
X : Type u_7
Y : Type u_8
inst : TopologicalSpace X
inst_1 : Group X
inst_2 : IsTopologicalGroup X
inst_3 : UniformSpace Y
inst_4 : CommGroup Y
inst_5 : IsUniformGroup Y
inst_6 : T0Space Y
inst_7 : CompactSpace Y
inst_8 : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : Filter.HasBasis (𝓝 1) (fun (x : ℕ) ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : Membership.mem (γ := Filter X) (𝓝 1) U0
U_aux : ℕ → (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7) :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7))
      (Subtype.mk (p := fun (x : Set X) ↦
        Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x) U0 hU0o)
      (fun (x : ℕ) (S : (↑{S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} : Type u_7)) ↦
        let h := ⋯;
        Subtype.mk (p := fun (x : Set X) ↦
          Membership.mem (γ := Set (Set X)) {S : Set X | Membership.mem (γ := Filter X) (𝓝 1) S} x)
          (Classical.choose (p := fun (x : Set X) ↦
            Membership.mem (γ := Filter X) (𝓝 1) x ∧ IsClosed[inst] x ∧ x⁻¹ = x ∧ x * x ⊆ (↑S : Set X)) h)
          ⋯)
      t
U : ℕ → Set X := fun (n : ℕ) ↦ (↑(U_aux n) : Set X)
hU1 : ∀ (n : ℕ), Membership.mem (γ := Filter X) (𝓝 1) (U n)
hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n
hU4 : ∀ (f : X →* Y), Set.MapsTo (⇑f : (a : X) → Y) (U 0) (V 0) → ∀ (n : ℕ), Set.MapsTo (⇑f : (a : X) → Y) (U n) (V n)
n : ℕ
h : True
x : X
hx : x ∈ U n
x_1 : (↑{f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) (U 0) (V 0)} : Type (max u_7 u_8))
f : X →* Y
hf : Membership.mem (γ := Set (X →* Y)) {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) (U 0) (V 0)} f
⊢ Membership.mem.{u_8, u_8} (α := Y × Y) (γ := Set (Y × Y)) {x : Y × Y | x.2 / x.1 ∈ V n}
    ((((↑(Subtype.mk (p := fun (x : X →* Y) ↦
                  Membership.mem (γ := Set (X →* Y)) {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) (U 0) (V 0)} x) f hf) :
              X →* Y) :
            (a : X) → Y)
          1,
        ((↑(Subtype.mk (p := fun (x : X →* Y) ↦
                  Membership.mem (γ := Set (X →* Y)) {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) (U 0) (V 0)} x) f hf) :
              X →* Y) :
            (a : X) → Y)
          x) :
      Y × Y)
have rw : Membership.mem (α := Y) (V n)
  ((1,
        ((↑(Subtype.mk (p := fun (x : X →* Y) ↦
                  Membership.mem (γ := Set (X →* Y)) {f : X →* Y | Set.MapsTo (⇑f : (a : X) → Y) (U 0) (V 0)} x) f hf) :
              X →* Y) :
            (a : X) → Y)
          x).2 :
    Y)
Tactic: rw [Set.mem_setOf_eq, map_one, div_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.Defs (goal)
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
have simp : Continuous[instTopologicalSpaceProd, inst_1] fun (p : G × G) ↦ p.1 * p.2⁻¹
Tactic: simp only [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup (goal)
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : SMul Γ α
S : Subgroup Γ
⊢ ProperlyDiscontinuousSMul.{u_1, u_2} (↥S) α ↔
    ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ S ∧ (g • K ∩ L).Nonempty}
have 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}
Tactic: rw [properlyDiscontinuousSMul_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup (goal)
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : SMul Γ α
S : Subgroup Γ
⊢ (∀ {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}
have 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}
Tactic: congr! with K L hK hL
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup (goal)
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} (α := Γ) {g : Γ | g ∈ S ∧ (g • K ∩ L).Nonempty}
have 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})
Tactic: convert! injOn_subtype_val (s := {m : S | (m • K ∩ L).Nonempty}) |>.bijOn_image.finite_iff_finite
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup (goal)
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
⊢ 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})
have 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
Tactic: ext g
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup (goal)
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
⊢ ProperlyDiscontinuousSMul.{u_1, u_2} (↥H) α
have 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}
Tactic: rw [Subgroup.properlyDiscontinuousSMul_iff] at hG ⊢
Cleared hypotheses: hG, hGH
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup (goal)
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) α
have refine : ProperlyDiscontinuousSMul.{u_1, u_2} (↥⊤) α
Tactic: refine Subgroup.properlyDiscontinuousSMul_of_le ?_ le_top
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup (goal)
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} (↥⊤) α
have simp : ∀ {K L : Set α}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := Γ) {g : Γ | (g • K ∩ L).Nonempty}
Tactic: simp only [Subgroup.properlyDiscontinuousSMul_iff, Subgroup.mem_top, true_and]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup (goal)
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
⊢ ProperlyDiscontinuousSMul.{u_1, u_2} (↥G) α
have 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}
Tactic: rw [Subgroup.properlyDiscontinuousSMul_iff] at hH ⊢
Cleared hypotheses: hH, inst_4
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup (hypothesis)
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
⊢ Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ G ∧ (g • K ∩ L).Nonempty}
have this : ∀ (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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup (goal)
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}
⊢ Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ G ∧ (g • K ∩ L).Nonempty}
have obtain : ∀ (S : Set ↥G) (hS : IsComplement (↑(H.subgroupOf G) : Set ↥G) S),
  Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ G ∧ (g • K ∩ L).Nonempty}
Tactic: obtain ⟨S, hS, -⟩ := (H.subgroupOf G).exists_isComplement_right 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup (goal)
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
have have : ∀ (this : Fintype (↥G ⧸ H.subgroupOf G)), (Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S).Finite
Tactic: have : Fintype (G ⧸ H.subgroupOf G) := Subgroup.fintypeQuotientOfFiniteIndex
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup (goal)
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)
⊢ (Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S).Finite
have have : ∀ (this : Fintype (↑S : Type u_1)), (Subtype.val (p := fun (x : Γ) ↦ x ∈ G) '' S).Finite
Tactic: have : Fintype S := .ofEquiv _ hS.rightQuotientEquiv
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup (hypothesis)
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
⊢ Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ G ∧ (g • K ∩ L).Nonempty}
have hT : (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 _
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup (goal)
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
have 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
Tactic: obtain ⟨p, hp⟩ := (hS.existsUnique ⟨g, hg⟩).exists
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup (hypothesis)
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
⊢ Set.Finite.{u_1} (α := Γ) {g : Γ | g ∈ G ∧ (g • K ∩ L).Nonempty}
have hS' : ∀ {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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup (goal)
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}
have 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
Tactic: refine (hT.biUnion <| fun t ht ↦ (this t).map fun g ↦ g * t).subset fun g ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup (goal)
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
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
have simp : g ∈ G →
  (g • K ∩ L).Nonempty →
    ∃ (i : Γ), g * i⁻¹ ∈ H ∧ (∃ (x : i ∈ G), Subtype.mk (p := fun (a : Γ) ↦ a ∈ G) i sorry ∈ S) ∧ (g • K ∩ L).Nonempty
Tactic: simp [mul_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup (hypothesis)
Goal:
Γ : Type u_1
α : Type u_2
inst : Group Γ
inst_1 : TopologicalSpace α
inst_2 : MulAction Γ α
inst_3 : ContinuousConstSMul Γ α
G H : Subgroup Γ
h : G.Commensurable H
⊢ ProperlyDiscontinuousSMul.{u_1, u_2} (↥G) α ↔ ProperlyDiscontinuousSMul.{u_1, u_2} (↥H) α
have this : (G ⊓ H).IsFiniteRelIndex H
Tactic: have : IsFiniteRelIndex (G ⊓ H) H := ⟨Subgroup.inf_relIndex_right G H ▸ h.1⟩