awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
U K : Subgroup G
h : IsOpen[inst_1] (↑K : Set G)
⊢ IsOpen[instTopologicalSpaceSubtype] (↑(K.subgroupOf U) : Set ↥U)

Tactic:
Continuous.isOpen_preimage (continuous_iff_le_induced.mpr fun _ ↦ id) _ h

Premises used: Iff.mpr, Set.Mem, setOf, id, continuous_iff_le_induced, Set.preimage, Continuous.isOpen_preimage
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
U : OpenSubgroup G
⊢ DiscreteTopology.{u_1} (G ⧸ (↑U : Subgroup G))

Tactic:
QuotientGroup.discreteTopology U.isOpen

Premises used: QuotientGroup.discreteTopology, OpenSubgroup.isOpen
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
inst_3 : CompactSpace G
U : Subgroup G
h : IsOpen[inst_1] (↑U : Set G)
⊢ Finite.{u_1 + 1} (G ⧸ U)

Tactic:
have : DiscreteTopology (G ⧸ U) := QuotientGroup.discreteTopology h
  finite_of_compact_of_discrete

Premises used: QuotientGroup.discreteTopology, finite_of_compact_of_discrete
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
inst_3 : CompactSpace G
U : OpenSubgroup G
⊢ Finite.{u_1 + 1} (G ⧸ (↑U : Subgroup G))

Tactic:
quotient_finite_of_isOpen U.toSubgroup U.isOpen

Premises used: OpenSubgroup.isOpen, Subgroup.quotient_finite_of_isOpen, OpenSubgroup.toSubgroup
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
U : Subgroup G
K : Subgroup ↥U
hUopen : IsOpen[inst_1] (↑U : Set G)
hKopen : IsOpen[instTopologicalSpaceSubtype] (↑K : Set ↥U)
⊢ Finite.{u_1 + 1} (↥U ⧸ K)

Tactic:
have : CompactSpace U := isCompact_iff_compactSpace.mp <| IsClosed.isCompact <|
    U.isClosed_of_isOpen hUopen
  K.quotient_finite_of_isOpen hKopen

Premises used: isCompact_iff_compactSpace, Subgroup.isClosed_of_isOpen, IsClosed.isCompact, Iff.mp, Subgroup.quotient_finite_of_isOpen
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
U : OpenSubgroup G
K : OpenSubgroup ↥U
⊢ Finite.{u_1 + 1} (↥U ⧸ (↑K : Subgroup ↥U))

Tactic:
quotient_finite_of_isOpen' U.toSubgroup K.toSubgroup U.isOpen K.isOpen

Premises used: OpenSubgroup.isOpen, Set.Mem, Subgroup.quotient_finite_of_isOpen', OpenSubgroup.toSubgroup
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
U V : OpenSubgroup G
⊢ (↑(U ⊔ V) : Subgroup G) = (↑U : Subgroup G) ⊔ (↑V : Subgroup G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : TopologicalSpace M
inst_3 : IsTopologicalAddGroup M
inst_4 : Module R M
U P : Submodule R M
h : U ≤ P
hU : IsOpen[inst_2] (↑U : Set M)
⊢ IsOpen[inst_2] (↑P : Set M)

Tactic:
@AddSubgroup.isOpen_mono M _ _ _ U.toAddSubgroup P.toAddSubgroup h hU

Premises used: AddSubgroup.isOpen_mono
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
U I : Ideal R
h : U ≤ I
hU : IsOpen[inst_1] (↑U : Set R)
⊢ IsOpen[inst_1] (↑I : Set R)

Tactic:
@Submodule.isOpen_mono R R _ _ _ _ Semiring.toModule _ _ h hU

Premises used: Submodule.isOpen_mono
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
H : OpenNormalSubgroup G
⊢ (↑H.toOpenSubgroup : Subgroup G).Normal

Tactic:
H.isNormal'

Premises used: OpenNormalSubgroup.isNormal'
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
A B : OpenNormalSubgroup G
h :
  Eq.{u + 1} (α := Subgroup G) ((fun (H : OpenNormalSubgroup G) ↦ (↑H.toOpenSubgroup : Subgroup G)) A)
    ((fun (H : OpenNormalSubgroup G) ↦ (↑H.toOpenSubgroup : Subgroup G)) B)
carrier : ∀ (x : G), x ∈ (↑A.toOpenSubgroup : Subgroup G).carrier ↔ x ∈ (↑B.toOpenSubgroup : Subgroup G).carrier
⊢ A = B

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u
inst : Group G
inst_1 : TopologicalSpace G
A B : OpenNormalSubgroup G
h : (↑A.toOpenSubgroup : Subgroup G) = (↑B.toOpenSubgroup : Subgroup G)
x : G
carrier carrier₁ : x ∈ (↑B.toOpenSubgroup : Subgroup G).carrier ↔ x ∈ (↑B.toOpenSubgroup : Subgroup G).carrier
⊢ x ∈ (↑A.toOpenSubgroup : Subgroup G).carrier ↔ x ∈ (↑B.toOpenSubgroup : Subgroup G).carrier

Tactic:
rw [h]
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
⊢ Membership.mem (γ := Filter G) (𝓝 1) univ ∧ HMul.hMul (α := Set G) ∅ univ ⊆ W

Tactic:
simp only [univ_mem, empty_mul, empty_subset, and_self]

Premises used: and_self, Set.empty_mul, Set.empty_subset, Filter.univ_mem
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
U V : Set G
h : (fun (S : Set G) ↦ ∃ (T : Set G), Membership.mem (γ := Filter G) (𝓝 1) T ∧ S * T ⊆ W) U
h_1 : (fun (S : Set G) ↦ ∃ (T : Set G), Membership.mem (γ := Filter G) (𝓝 1) T ∧ S * T ⊆ W) V
T₁ : Set G
hT₁ : Membership.mem (γ := Filter G) (𝓝 1) T₁
mem1 : U * T₁ ⊆ W
T₂ : Set G
hT₂ : Membership.mem (γ := Filter G) (𝓝 1) T₂
mem2 : V * T₂ ⊆ W
rw : U * (T₁ ∩ T₂) ∪ V * (T₁ ∩ T₂) ⊆ W
⊢ (U ∪ V) * (T₁ ∩ T₂) ⊆ W

Tactic:
rw [union_mul]

Premises used: Set.union_mul
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
U V : Set G
h : (fun (S : Set G) ↦ ∃ (T : Set G), Membership.mem (γ := Filter G) (𝓝 1) T ∧ S * T ⊆ W) U
h_1 : (fun (S : Set G) ↦ ∃ (T : Set G), Membership.mem (γ := Filter G) (𝓝 1) T ∧ S * T ⊆ W) V
T₁ : Set G
hT₁ : Membership.mem (γ := Filter G) (𝓝 1) T₁
mem1 : U * T₁ ⊆ W
T₂ : Set G
hT₂ : Membership.mem (γ := Filter G) (𝓝 1) T₂
mem2 : V * T₂ ⊆ W
⊢ U * (T₁ ∩ T₂) ∪ V * (T₁ ∩ T₂) ⊆ W

Tactic:
union_subset (mul_subset_mul_left inter_subset_left |>.trans mem1)
        (mul_subset_mul_left inter_subset_right |>.trans mem2)

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, Set.union_subset, Set.mul_subset_mul_left, Set.inter_subset_right
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
U V : Set G
h : (fun (S : Set G) ↦ ∃ (T : Set G), Membership.mem (γ := Filter G) (𝓝 1) T ∧ S * T ⊆ W) U
h_1 : (fun (S : Set G) ↦ ∃ (T : Set G), Membership.mem (γ := Filter G) (𝓝 1) T ∧ S * T ⊆ W) V
T₁ : Set G
hT₁ : Membership.mem (γ := Filter G) (𝓝 1) T₁
mem1 : U * T₁ ⊆ W
T₂ : Set G
hT₂ : Membership.mem (γ := Filter G) (𝓝 1) T₂
mem2 : V * T₂ ⊆ W
⊢ U * (T₁ ∩ T₂) ∪ V * (T₁ ∩ T₂) ⊆ W

Tactic:
exact union_subset (mul_subset_mul_left inter_subset_left |>.trans mem1)
        (mul_subset_mul_left inter_subset_right |>.trans mem2)

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, Set.union_subset, Set.mul_subset_mul_left, Set.inter_subset_right
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
apply : ∀ x ∈ W, ∃ t ∈ 𝓝[W] x, ∃ (T : Set G), Membership.mem (γ := Filter G) (𝓝 1) T ∧ t * T ⊆ W
⊢ ∃ (T : Set G), Membership.mem (γ := Filter G) (𝓝 1) T ∧ W * T ⊆ W

Tactic:
apply WClopen.isClosed.isCompact.induction_on (p := fun S ↦ ∃ T ∈ 𝓝 (1 : G), S * T ⊆ W)
    ⟨Set.univ, by simp only [univ_mem, empty_mul, empty_subset, and_self]⟩
    (fun _ _ huv ⟨T, hT, mem⟩ ↦ ⟨T, hT, (mul_subset_mul_right huv).trans mem⟩)
    fun U V ⟨T₁, hT₁, mem1⟩ ⟨T₂, hT₂, mem2⟩ ↦ ⟨T₁ ∩ T₂, inter_mem hT₁ hT₂, by
      rw [union_mul]
      exact union_subset (mul_subset_mul_left inter_subset_left |>.trans mem1)
        (mul_subset_mul_left inter_subset_right |>.trans mem2) ⟩

Premises used: HMul.hMul, Set.univ, Filter.inter_mem, Membership.mem, Exists, nhds, HasSubset.Subset.trans, Set.mul_subset_mul_right, HasSubset.Subset, Inter.inter, And, IsClopen.isClosed, And.intro, IsClosed.isCompact, Exists.intro, IsCompact.induction_on, Union.union, OfNat.ofNat, _private.0.IsTopologicalGroup.exist_mul_closure_nhds.match_1
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
x : G
memW : x ∈ W
⊢ Membership.mem (γ := Set (G × G)) ((fun (p : G × G) ↦ p.1 * p.2) ⁻¹' W) (x, 1)

Tactic:
simp [memW]
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
x : G
memW : x ∈ W
⊢ Membership.mem (γ := Set (G × G)) ((fun (p : G × G) ↦ p.1 * p.2) ⁻¹' W) (x, 1)

Tactic:
have : (x, 1) ∈ (fun p ↦ p.1 * p.2) ⁻¹' W := by simp [memW]
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
x : G
memW : x ∈ W
this : Membership.mem (γ := Set (G × G)) ((fun (p : G × G) ↦ p.1 * p.2) ⁻¹' W) (x, 1)
rcases :
  ∀ (U V : Set G) (Uopen : IsOpen[inst] U) (Vopen : IsOpen[inst] V) (xmemU : x ∈ U) (onememV : 1 ∈ V)
    (prodsub : U ×ˢ V ⊆ (fun (p : G × G) ↦ p.1 * p.2) ⁻¹' W),
    ∃ t ∈ 𝓝[W] x, ∃ (T : Set G), Membership.mem (γ := Filter G) (𝓝 1) T ∧ t * T ⊆ W
⊢ ∃ t ∈ 𝓝[W] x, ∃ (T : Set G), Membership.mem (γ := Filter G) (𝓝 1) T ∧ t * T ⊆ W

Tactic:
rcases isOpen_prod_iff.mp (continuous_mul.isOpen_preimage W <| WClopen.2) x 1 this with
    ⟨U, V, Uopen, Vopen, xmemU, onememV, prodsub⟩

Premises used: isOpen_prod_iff, continuous_mul, And.right, Iff.mp, OfNat.ofNat, Continuous.isOpen_preimage
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
x : G
memW : x ∈ W
this : Membership.mem (γ := Set (G × G)) ((fun (p : G × G) ↦ p.1 * p.2) ⁻¹' W) (x, 1)
U V : Set G
Uopen : IsOpen[inst] U
Vopen : IsOpen[inst] V
xmemU : x ∈ U
onememV : 1 ∈ V
prodsub : U ×ˢ V ⊆ (fun (p : G × G) ↦ p.1 * p.2) ⁻¹' W
⊢ U * V ⊆ W

Tactic:
have h6 : U * V ⊆ W := mul_subset_iff.mpr (fun _ hx _ hy ↦ prodsub (mk_mem_prod hx hy))
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
x : G
memW : x ∈ W
this : Membership.mem (γ := Set (G × G)) ((fun (p : G × G) ↦ p.1 * p.2) ⁻¹' W) (x, 1)
U V : Set G
Uopen : IsOpen[inst] U
Vopen : IsOpen[inst] V
xmemU : x ∈ U
onememV : 1 ∈ V
prodsub : U ×ˢ V ⊆ (fun (p : G × G) ↦ p.1 * p.2) ⁻¹' W
h6 : U * V ⊆ W
⊢ ∃ t ∈ 𝓝[W] x, ∃ (T : Set G), Membership.mem (γ := Filter G) (𝓝 1) T ∧ t * T ⊆ W

Tactic:
⟨U ∩ W, ⟨U, Uopen.mem_nhds xmemU, W, fun _ a ↦ a, rfl⟩,
    V, IsOpen.mem_nhds Vopen onememV, fun _ a ↦ h6 ((mul_subset_mul_right inter_subset_left) a)⟩

Premises used: Set.mul_subset_mul_right, Set.inter_subset_left, Inter.inter, And.intro, IsOpen.mem_nhds, Exists.intro, rfl
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
x : G
memW : x ∈ W
this : Membership.mem (γ := Set (G × G)) ((fun (p : G × G) ↦ p.1 * p.2) ⁻¹' W) (x, 1)
U V : Set G
Uopen : IsOpen[inst] U
Vopen : IsOpen[inst] V
xmemU : x ∈ U
onememV : 1 ∈ V
prodsub : U ×ˢ V ⊆ (fun (p : G × G) ↦ p.1 * p.2) ⁻¹' W
h6 : U * V ⊆ W
⊢ ∃ t ∈ 𝓝[W] x, ∃ (T : Set G), Membership.mem (γ := Filter G) (𝓝 1) T ∧ t * T ⊆ W

Tactic:
exact ⟨U ∩ W, ⟨U, Uopen.mem_nhds xmemU, W, fun _ a ↦ a, rfl⟩,
    V, IsOpen.mem_nhds Vopen onememV, fun _ a ↦ h6 ((mul_subset_mul_right inter_subset_left) a)⟩
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
rcases :
  ∀ (S : Set G) (Smemnhds : Membership.mem (γ := Filter G) (𝓝 1) S) (mulclose : W * S ⊆ W),
    ∃ (T : Set G), mulInvClosureNhd T W
⊢ ∃ (T : Set G), mulInvClosureNhd T W

Tactic:
rcases exist_mul_closure_nhds WClopen with ⟨S, Smemnhds, mulclose⟩

Premises used: IsTopologicalGroup.exist_mul_closure_nhds
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : Membership.mem (γ := Filter G) (𝓝 1) S
mulclose : W * S ⊆ W
rcases : ∀ (U : Set G) (UsubS : U ⊆ S) (Uopen : IsOpen[inst] U) (onememU : 1 ∈ U), ∃ (T : Set G), mulInvClosureNhd T W
⊢ ∃ (T : Set G), mulInvClosureNhd T W

Tactic:
rcases mem_nhds_iff.mp Smemnhds with ⟨U, UsubS, Uopen, onememU⟩

Premises used: mem_nhds_iff, Iff.mp
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : Membership.mem (γ := Filter G) (𝓝 1) S
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen[inst] U
onememU : 1 ∈ U
h : mulInvClosureNhd (U ∩ U⁻¹) W
⊢ ∃ (T : Set G), mulInvClosureNhd T W

Tactic:
use U ∩ U⁻¹
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : Membership.mem (γ := Filter G) (𝓝 1) S
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen[inst] U
onememU : 1 ∈ U
h : Membership.mem (γ := Filter G) (𝓝 1) (U ∩ U⁻¹)
h₁ : (U ∩ U⁻¹)⁻¹ = U ∩ U⁻¹
h₂ : IsOpen[inst] (U ∩ U⁻¹)
h₃ : W * (U ∩ U⁻¹) ⊆ W
⊢ mulInvClosureNhd (U ∩ U⁻¹) W

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : Membership.mem (γ := Filter G) (𝓝 1) S
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen[inst] U
onememU : 1 ∈ U
⊢ Membership.mem (γ := Filter G) (𝓝 1) (U ∩ U⁻¹)

Tactic:
simp [Uopen.mem_nhds onememU, inv_mem_nhds_one]

Premises used: inv_mem_nhds_one, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : Membership.mem (γ := Filter G) (𝓝 1) S
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen[inst] U
onememU : 1 ∈ U
⊢ (U ∩ U⁻¹)⁻¹ = U ∩ U⁻¹

Tactic:
simp [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : Membership.mem (γ := Filter G) (𝓝 1) S
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen[inst] U
onememU : 1 ∈ U
⊢ IsOpen[inst] (U ∩ U⁻¹)

Tactic:
Uopen.inter Uopen.inv

Premises used: IsOpen.inter, IsOpen.inv
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : Membership.mem (γ := Filter G) (𝓝 1) S
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen[inst] U
onememU : 1 ∈ U
⊢ IsOpen[inst] (U ∩ U⁻¹)

Tactic:
exact Uopen.inter Uopen.inv

Premises used: IsOpen.inter, IsOpen.inv
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : Membership.mem (γ := Filter G) (𝓝 1) S
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen[inst] U
onememU : 1 ∈ U
⊢ W * (U ∩ U⁻¹) ⊆ W

Tactic:
fun a ha ↦ mulclose (mul_subset_mul_left UsubS (mul_subset_mul_left inter_subset_left ha))

Premises used: Set.inter_subset_left, Set.Subset, Set.mul_subset_mul_left
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
S : Set G
Smemnhds : Membership.mem (γ := Filter G) (𝓝 1) S
mulclose : W * S ⊆ W
U : Set G
UsubS : U ⊆ S
Uopen : IsOpen[inst] U
onememU : 1 ∈ U
⊢ W * (U ∩ U⁻¹) ⊆ W

Tactic:
exact fun a ha ↦ mulclose (mul_subset_mul_left UsubS (mul_subset_mul_left inter_subset_left ha))

Premises used: Set.inter_subset_left, Set.mul_subset_mul_left
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
rcases : ∀ (V : Set G) (hV : mulInvClosureNhd V W), ∃ (H : OpenSubgroup G), (↑H : Set G) ⊆ W
⊢ ∃ (H : OpenSubgroup G), (↑H : Set G) ⊆ W

Tactic:
rcases exists_mulInvClosureNhd WClopen with ⟨V, hV⟩

Premises used: IsTopologicalGroup.exists_mulInvClosureNhd
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
a b : G
ha : Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) a
hb : Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) b
rcases : ∀ (k : ℕ) (hk : a ∈ V ^ (k + 1)), Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) (a * b)
⊢ Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) (a * b)

Tactic:
rcases mem_iUnion.mp ha with ⟨k, hk⟩

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
a b : G
ha : Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) a
hb : Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) b
k : ℕ
hk : a ∈ V ^ (k + 1)
rcases : ∀ (l : ℕ) (hl : b ∈ V ^ (l + 1)), Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) (a * b)
⊢ Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) (a * b)

Tactic:
rcases mem_iUnion.mp hb with ⟨l, hl⟩

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
a b : G
ha : Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) a
hb : Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) b
k : ℕ
hk : a ∈ V ^ (k + 1)
l : ℕ
hl : b ∈ V ^ (l + 1)
apply : ∃ (i : ℕ), a * b ∈ V ^ (i + 1)
⊢ Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) (a * b)

Tactic:
apply mem_iUnion.mpr

Premises used: Iff.mpr, Set.mem_iUnion
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
a b : G
ha : Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) a
hb : Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) b
k : ℕ
hk : a ∈ V ^ (k + 1)
l : ℕ
hl : b ∈ V ^ (l + 1)
h : a * b ∈ V ^ (k + 1 + l + 1)
⊢ ∃ (i : ℕ), a * b ∈ V ^ (i + 1)

Tactic:
use k + 1 + l
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
a b : G
ha : Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) a
hb : Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) b
k : ℕ
hk : a ∈ V ^ (k + 1)
l : ℕ
hl : b ∈ V ^ (l + 1)
h : a * b ∈ V ^ (k + 1) * V ^ (l + 1)
⊢ a * b ∈ V ^ (k + 1 + l + 1)

Tactic:
rw [add_assoc, pow_add]

Premises used: add_assoc, pow_add
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
a b : G
ha : Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) a
hb : Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) b
k : ℕ
hk : a ∈ V ^ (k + 1)
l : ℕ
hl : b ∈ V ^ (l + 1)
⊢ a * b ∈ V ^ (k + 1) * V ^ (l + 1)

Tactic:
Set.mul_mem_mul hk hl

Premises used: Set.Mem, Set.mul_mem_mul
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
a b : G
ha : Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) a
hb : Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) b
k : ℕ
hk : a ∈ V ^ (k + 1)
l : ℕ
hl : b ∈ V ^ (l + 1)
⊢ a * b ∈ V ^ (k + 1) * V ^ (l + 1)

Tactic:
exact Set.mul_mem_mul hk hl

Premises used: Set.mul_mem_mul
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
apply : ∃ (i : ℕ), 1 ∈ V ^ (i + 1)
⊢ Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) 1

Tactic:
apply mem_iUnion.mpr

Premises used: Iff.mpr, Set.mem_iUnion
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
h : 1 ∈ V ^ HAdd.hAdd (α := ℕ) 0 1
⊢ ∃ (i : ℕ), 1 ∈ V ^ (i + 1)

Tactic:
use 0
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
⊢ 1 ∈ V ^ HAdd.hAdd (α := ℕ) 0 1

Tactic:
simp [mem_of_mem_nhds hV.nhds]

Premises used: IsTopologicalGroup.mulInvClosureNhd.nhds, mem_of_mem_nhds
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
x : G
ha : Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) x
rcases : ∀ (k : ℕ) (hk : x ∈ V ^ (k + 1)), Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) x⁻¹
⊢ Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) x⁻¹

Tactic:
rcases mem_iUnion.mp ha with ⟨k, hk⟩

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
x : G
ha : Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) x
k : ℕ
hk : x ∈ V ^ (k + 1)
apply : ∃ (i : ℕ), x⁻¹ ∈ V ^ (i + 1)
⊢ Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) x⁻¹

Tactic:
apply mem_iUnion.mpr

Premises used: Iff.mpr, Set.mem_iUnion
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
x : G
ha : Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) x
k : ℕ
hk : x ∈ V ^ (k + 1)
h : x⁻¹ ∈ V ^ (k + 1)
⊢ ∃ (i : ℕ), x⁻¹ ∈ V ^ (i + 1)

Tactic:
use k