awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Completion
Goal:
G : Type u_1
inst : AddGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformAddGroup G
inst_3 : NonarchimedeanAddGroup G
U : Set (Completion G)
hU : Membership.mem (γ := Filter (Completion G)) (𝓝 0) U
C : Set (Completion G)
C_subset_U : id C ⊆ U
hC : Membership.mem (γ := Filter (Completion G)) (𝓝 0) C
C_closed : IsClosed C
this : Membership.mem (γ := Filter G) (𝓝 0) ((⇑toCompl : (a : G) → Completion G) ⁻¹' C)
W : OpenAddSubgroup G
hCW : (↑W : Set G) ⊆ (⇑toCompl : (a : G) → Completion G) ⁻¹' C
V : Set (Completion G) := (↑(topologicalClosure (map toCompl (↑W : AddSubgroup G))) : Set (Completion G))
⊢ IsOpen V

Tactic:
have : IsOpen V := by
      /- Since `V` is a subgroup of `Completion G`, it suffices to show that it is a neighborhood of
      `0` in `Completion G`. This follows from the fact that `toCompl : G → Completion G` is dense
      inducing and `W` is a neighborhood of `0` in `G`. -/
      apply isOpen_of_mem_nhds (g := 0)
      apply (isDenseInducing_toCompl _).closure_image_mem_nhds
      exact mem_nhds_zero W
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Completion
Goal:
G : Type u_1
inst : AddGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformAddGroup G
inst_3 : NonarchimedeanAddGroup G
U : Set (Completion G)
hU : Membership.mem (γ := Filter (Completion G)) (𝓝 0) U
C : Set (Completion G)
C_subset_U : id C ⊆ U
hC : Membership.mem (γ := Filter (Completion G)) (𝓝 0) C
C_closed : IsClosed C
this_1 : Membership.mem (γ := Filter G) (𝓝 0) ((⇑toCompl : (a : G) → Completion G) ⁻¹' C)
W : OpenAddSubgroup G
hCW : (↑W : Set G) ⊆ (⇑toCompl : (a : G) → Completion G) ⁻¹' C
V : Set (Completion G) := (↑(topologicalClosure (map toCompl (↑W : AddSubgroup G))) : Set (Completion G))
this : IsOpen V
h :
  (↑{ toAddSubgroup := topologicalClosure (map toCompl (↑W : AddSubgroup G)), isOpen' := this :
          OpenAddSubgroup (Completion G) } :
      Set (Completion G)) ⊆
    U
⊢ ∃ (V : OpenAddSubgroup (Completion G)), (↑V : Set (Completion G)) ⊆ U

Tactic:
use ⟨_, this⟩
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Completion
Goal:
G : Type u_1
inst : AddGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformAddGroup G
inst_3 : NonarchimedeanAddGroup G
U : Set (Completion G)
hU : Membership.mem (γ := Filter (Completion G)) (𝓝 0) U
C : Set (Completion G)
C_subset_U : id C ⊆ U
hC : Membership.mem (γ := Filter (Completion G)) (𝓝 0) C
C_closed : IsClosed C
this_1 : Membership.mem (γ := Filter G) (𝓝 0) ((⇑toCompl : (a : G) → Completion G) ⁻¹' C)
W : OpenAddSubgroup G
hCW : (↑W : Set G) ⊆ (⇑toCompl : (a : G) → Completion G) ⁻¹' C
V : Set (Completion G) := (↑(topologicalClosure (map toCompl (↑W : AddSubgroup G))) : Set (Completion G))
this : IsOpen V
h : V ⊆ C
⊢ (↑{ toAddSubgroup := topologicalClosure (map toCompl (↑W : AddSubgroup G)), isOpen' := this :
          OpenAddSubgroup (Completion G) } :
      Set (Completion G)) ⊆
    U

Tactic:
suffices V ⊆ C from this.trans C_subset_U
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Completion
Goal:
G : Type u_1
inst : AddGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformAddGroup G
inst_3 : NonarchimedeanAddGroup G
U : Set (Completion G)
hU : Membership.mem (γ := Filter (Completion G)) (𝓝 0) U
C : Set (Completion G)
C_subset_U : id C ⊆ U
hC : Membership.mem (γ := Filter (Completion G)) (𝓝 0) C
C_closed : IsClosed C
this_1 : Membership.mem (γ := Filter G) (𝓝 0) ((⇑toCompl : (a : G) → Completion G) ⁻¹' C)
W : OpenAddSubgroup G
hCW : (↑W : Set G) ⊆ (⇑toCompl : (a : G) → Completion G) ⁻¹' C
V : Set (Completion G) := (↑(topologicalClosure (map toCompl (↑W : AddSubgroup G))) : Set (Completion G))
this : IsOpen V
⊢ V ⊆ C

Tactic:
closure_minimal (Set.image_subset_iff.mpr hCW) C_closed

Premises used: Iff.mpr, closure_minimal, setOf, closure, Set.image_subset_iff, Set.sInter
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.Completion
Goal:
G : Type u_1
inst : AddGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformAddGroup G
inst_3 : NonarchimedeanAddGroup G
U : Set (Completion G)
hU : Membership.mem (γ := Filter (Completion G)) (𝓝 0) U
C : Set (Completion G)
C_subset_U : id C ⊆ U
hC : Membership.mem (γ := Filter (Completion G)) (𝓝 0) C
C_closed : IsClosed C
this_1 : Membership.mem (γ := Filter G) (𝓝 0) ((⇑toCompl : (a : G) → Completion G) ⁻¹' C)
W : OpenAddSubgroup G
hCW : (↑W : Set G) ⊆ (⇑toCompl : (a : G) → Completion G) ⁻¹' C
V : Set (Completion G) := (↑(topologicalClosure (map toCompl (↑W : AddSubgroup G))) : Set (Completion G))
this : IsOpen V
⊢ V ⊆ C

Tactic:
exact closure_minimal (Set.image_subset_iff.mpr hCW) C_closed

Premises used: Iff.mpr, closure_minimal, Set.image_subset_iff
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
a b : G
h : a ≠ b
obtain :
  ∀ (u v : Set G),
    IsOpen u →
      ∀ (open_v : IsOpen v) (mem_u : a⁻¹ * b ∈ u) (mem_v : 1 ∈ v) (dis : Disjoint u v),
        ∃ (V : OpenSubgroup G), Disjoint (a • (↑V : Set G)) (b • (↑V : Set G))
⊢ ∃ (V : OpenSubgroup G), Disjoint (a • (↑V : Set G)) (b • (↑V : Set G))

Tactic:
obtain ⟨u, v, _, open_v, mem_u, mem_v, dis⟩ := t2_separation (h ∘ inv_mul_eq_one.mp)

Premises used: Function.comp, Iff.mp, t2_separation, inv_mul_eq_one
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
a b : G
h : a ≠ b
u v : Set G
left : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
obtain :
  ∀ (V : OpenSubgroup G) (hV : (↑V : Set G) ⊆ v), ∃ (V : OpenSubgroup G), Disjoint (a • (↑V : Set G)) (b • (↑V : Set G))
⊢ ∃ (V : OpenSubgroup G), Disjoint (a • (↑V : Set G)) (b • (↑V : Set G))

Tactic:
obtain ⟨V, hV⟩ := is_nonarchimedean v (open_v.mem_nhds mem_v)

Premises used: NonarchimedeanGroup.is_nonarchimedean, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
a b : G
h : a ≠ b
u v : Set G
left : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : (↑V : Set G) ⊆ v
h₁ : Disjoint (a • (↑V : Set G)) (b • (↑V : Set G))
⊢ ∃ (V : OpenSubgroup G), Disjoint (a • (↑V : Set G)) (b • (↑V : Set G))

Tactic:
use V
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
a b : G
h : a ≠ b
u v : Set G
left : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : (↑V : Set G) ⊆ v
h₁ : ∀ ⦃x : Set G⦄, x ⊆ a • (↑V : Set G) → x ⊆ b • (↑V : Set G) → x = ∅
⊢ Disjoint (a • (↑V : Set G)) (b • (↑V : Set G))

Tactic:
simp only [Disjoint, Set.le_eq_subset, Set.bot_eq_empty, Set.subset_empty_iff]

Premises used: Set.le_eq_subset, Disjoint, Set.bot_eq_empty, Set.subset_empty_iff
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
a b : G
h : a ≠ b
u v : Set G
left : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : (↑V : Set G) ⊆ v
x : Set G
mem_aV : x ⊆ a • (↑V : Set G)
mem_bV : x ⊆ b • (↑V : Set G)
h₁ : ∀ (s : G) (hs : s ∈ x), False
⊢ x = ∅

Tactic:
by_contra! ⟨s, hs⟩
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
a b : G
h : a ≠ b
u v : Set G
left : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : (↑V : Set G) ⊆ v
x : Set G
mem_aV : x ⊆ a • (↑V : Set G)
mem_bV : x ⊆ b • (↑V : Set G)
s : G
hs : s ∈ x
⊢ s ∈ a • (↑V : Set G)

Tactic:
have hsa : s ∈ a • (V : Set G) := mem_aV hs
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
a b : G
h : a ≠ b
u v : Set G
left : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : (↑V : Set G) ⊆ v
x : Set G
mem_aV : x ⊆ a • (↑V : Set G)
mem_bV : x ⊆ b • (↑V : Set G)
s : G
hs : s ∈ x
hsa : s ∈ a • (↑V : Set G)
⊢ s ∈ b • (↑V : Set G)

Tactic:
have hsb : s ∈ b • (V : Set G) := mem_bV hs
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
a b : G
h : a ≠ b
u v : Set G
left : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : (↑V : Set G) ⊆ v
x : Set G
mem_aV : x ⊆ a • (↑V : Set G)
mem_bV : x ⊆ b • (↑V : Set G)
s : G
hs : s ∈ x
hsa : s ∈ a • (↑V : Set G)
hsb : s ∈ b • (↑V : Set G)
⊢ a⁻¹ * s ∈ (↑V : Set G)

Tactic:
rw [mem_leftCoset_iff] at hsa hsb

Premises used: mem_leftCoset_iff
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
a b : G
h : a ≠ b
u v : Set G
left : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : (↑V : Set G) ⊆ v
x : Set G
mem_aV : x ⊆ a • (↑V : Set G)
mem_bV : x ⊆ b • (↑V : Set G)
s : G
hs : s ∈ x
hsa : s ∈ a • (↑V : Set G)
hsb : s ∈ b • (↑V : Set G)
hsa₁ : a⁻¹ * s ∈ (↑V : Set G)
⊢ b⁻¹ * s ∈ (↑V : Set G)

Tactic:
rw [mem_leftCoset_iff] at hsa hsb

Premises used: mem_leftCoset_iff
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
a b : G
h : a ≠ b
u v : Set G
left : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : (↑V : Set G) ⊆ v
x : Set G
mem_aV : x ⊆ a • (↑V : Set G)
mem_bV : x ⊆ b • (↑V : Set G)
s : G
hs : s ∈ x
hsa : a⁻¹ * s ∈ (↑V : Set G)
hsb : b⁻¹ * s ∈ (↑V : Set G)
⊢ False

Tactic:
dis.subset_compl_right mem_u (hV ?_)

Premises used: Disjoint.subset_compl_right
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
a b : G
h : a ≠ b
u v : Set G
left : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : (↑V : Set G) ⊆ v
x : Set G
mem_aV : x ⊆ a • (↑V : Set G)
mem_bV : x ⊆ b • (↑V : Set G)
s : G
hs : s ∈ x
hsa : a⁻¹ * s ∈ (↑V : Set G)
hsb : b⁻¹ * s ∈ (↑V : Set G)
h₁ : a⁻¹ * b ∈ (↑V : Set G)
⊢ False

Tactic:
refine dis.subset_compl_right mem_u (hV ?_)

Premises used: Disjoint.subset_compl_right
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
a b : G
h : a ≠ b
u v : Set G
left : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : (↑V : Set G) ⊆ v
x : Set G
mem_aV : x ⊆ a • (↑V : Set G)
mem_bV : x ⊆ b • (↑V : Set G)
s : G
hs : s ∈ x
hsa : a⁻¹ * s ∈ (↑V : Set G)
hsb : b⁻¹ * s ∈ (↑V : Set G)
⊢ a⁻¹ * b ∈ (↑V : Set G)

Tactic:
simpa [mul_assoc] using mul_mem hsa (inv_mem hsb)

Premises used: mul_assoc, InvMemClass.inv_mem, MulMemClass.mul_mem
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
x : G
h : Membership.mem (γ := Set G) Set.univ x
y : G
h_1 : Membership.mem (γ := Set G) Set.univ y
hxy : x ≠ y
obtain :
  ∀ (V : OpenSubgroup G) (dxy : Disjoint (x • (↑V : Set G)) (y • (↑V : Set G))),
    ∃ (u : Set G) (v : Set G), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Set.univ ⊆ u ∪ v ∧ Disjoint u v
⊢ ∃ (u : Set G) (v : Set G), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Set.univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
obtain ⟨V, dxy⟩ := exists_openSubgroup_separating hxy

Premises used: NonarchimedeanGroup.exists_openSubgroup_separating
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
x : G
h : Membership.mem (γ := Set G) Set.univ x
y : G
h_1 : Membership.mem (γ := Set G) Set.univ y
hxy : x ≠ y
V : OpenSubgroup G
dxy : Disjoint (x • (↑V : Set G)) (y • (↑V : Set G))
⊢ Set.univ ⊆ x • (↑V : Set G) ∪ (x • (↑V : Set G))ᶜ

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected
Goal:
G : Type u_1
inst : TopologicalSpace G
inst_1 : Group G
inst_2 : NonarchimedeanGroup G
inst_3 : T2Space G
x : G
h : Membership.mem (γ := Set G) Set.univ x
y : G
h_1 : Membership.mem (γ := Set G) Set.univ y
hxy : x ≠ y
V : OpenSubgroup G
dxy : Disjoint (x • (↑V : Set G)) (y • (↑V : Set G))
⊢ ∃ (u : Set G) (v : Set G), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Set.univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
exact ⟨_, _, V.isOpen.smul x, (V.isClosed.smul x).isOpen_compl, mem_own_leftCoset ..,
      dxy.subset_compl_left <| mem_own_leftCoset .., by simp, disjoint_compl_right⟩
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
U : OpenSubgroup G
⊢ (↑(↑U : Opens G) : Set G) = (↑U : Set G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
U : OpenSubgroup G
⊢ (↑(↑U : Subgroup G) : Set G) = (↑U : Set G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
U : OpenSubgroup G
g : G
⊢ g ∈ (↑U : Opens G) ↔ g ∈ U

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
U : OpenSubgroup G
g : G
⊢ g ∈ (↑U : Subgroup G) ↔ g ∈ U

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
U V : OpenSubgroup G
h : ∀ (x : G), x ∈ U ↔ x ∈ V
⊢ U = V

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
U : OpenSubgroup G
⊢ IsOpen[inst_1] (↑U : Set G)

Tactic:
U.isOpen'

Premises used: OpenSubgroup.isOpen'
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
U : OpenSubgroup G
⊢ Membership.mem (γ := Filter G) (𝓝 1) (↑U : Set G)

Tactic:
U.isOpen.mem_nhds U.one_mem

Premises used: OpenSubgroup.isOpen, Subgroup.one_mem, IsOpen.mem_nhds, OpenSubgroup.toSubgroup
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
x : G
⊢ Membership.mem (γ := OpenSubgroup G) ⊤ x

Tactic:
trivial

Premises used: trivial, Set.Mem, Set.univ, setOf
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
⊢ (↑⊤ : Set G) = Set.univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
⊢ Eq.{u_1 + 1} (α := Subgroup G) (↑⊤ : Subgroup G) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
⊢ Eq.{u_1 + 1} (α := Opens G) (↑⊤ : Opens G) ⊤

Tactic:
rfl

Premises used: Set.univ, setOf, OpenSubgroup.toOpens, rfl
-- 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:
have := QuotientGroup.discreteTopology U.isOpen
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
U : OpenSubgroup G
this : DiscreteTopology.{u_1} (G ⧸ (↑U : Subgroup G))
⊢ IsClosed[inst_1] (↑U : Set G)

Tactic:
QuotientGroup.t1Space_iff.mp inferInstance

Premises used: inferInstance, Iff.mp, QuotientGroup.t1Space_iff
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
U : OpenSubgroup G
this : DiscreteTopology.{u_1} (G ⧸ (↑U : Subgroup G))
⊢ IsClosed[inst_1] (↑U : Set G)

Tactic:
exact QuotientGroup.t1Space_iff.mp inferInstance

Premises used: inferInstance, Iff.mp, QuotientGroup.t1Space_iff
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
U : OpenSubgroup G
⊢ IsClopen (↑U : Set G)

Tactic:
⟨U.isClosed, U.isOpen⟩

Premises used: OpenSubgroup.isOpen, And.intro, OpenSubgroup.isClosed, IsClopen
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
H : Type u_2
inst_2 : Group H
inst_3 : TopologicalSpace H
U : OpenSubgroup G
V : OpenSubgroup H
⊢ (↑(U.prod V) : Set (G × H)) = (↑U : Set G) ×ˢ (↑V : Set H)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.prod, rfl
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
H : Type u_2
inst_2 : Group H
inst_3 : TopologicalSpace H
U : OpenSubgroup G
V : OpenSubgroup H
⊢ (↑(U.prod V) : Subgroup (G × H)) = (↑U : Subgroup G).prod (↑V : Subgroup H)

Tactic:
rfl

Premises used: Subgroup.prod, rfl
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
U V : OpenSubgroup G
⊢ (↑(U ⊓ V) : Set G) = (↑U : Set G) ∩ (↑V : Set G)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, rfl
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace 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:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
U V : OpenSubgroup G
⊢ (↑(U ⊓ V) : Opens G) = (↑U : Opens G) ⊓ (↑V : Opens G)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, OpenSubgroup.toOpens, rfl
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
U V : OpenSubgroup G
x : G
⊢ x ∈ U ⊓ V ↔ x ∈ U ∧ x ∈ V

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
U V : OpenSubgroup G
⊢ (↑U : Subgroup G) ≤ (↑V : Subgroup G) ↔ U ≤ V

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
N : Type u_2
inst_2 : Group N
inst_3 : TopologicalSpace N
H : OpenSubgroup N
f : G →* N
hf : Continuous[inst_1, inst_3] (⇑f : (a : G) → N)
⊢ (↑(comap f hf H) : Set G) = (⇑f : (a : G) → N) ⁻¹' (↑H : Set N)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
N : Type u_2
inst_2 : Group N
inst_3 : TopologicalSpace N
H : OpenSubgroup N
f : G →* N
hf : Continuous[inst_1, inst_3] (⇑f : (a : G) → N)
⊢ (↑(comap f hf H) : Subgroup G) = Subgroup.comap f (↑H : Subgroup N)

Tactic:
rfl

Premises used: Subgroup.comap, rfl
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
N : Type u_2
inst_2 : Group N
inst_3 : TopologicalSpace N
H : OpenSubgroup N
f : G →* N
hf : Continuous[inst_1, inst_3] (⇑f : (a : G) → N)
x : G
⊢ x ∈ comap f hf H ↔ Membership.mem (α := N) H ((f : (a : G) → N) x : N)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
N : Type u_2
inst_2 : Group N
inst_3 : TopologicalSpace N
P : Type u_3
inst_4 : Group P
inst_5 : TopologicalSpace P
K : OpenSubgroup P
f₂ : N →* P
hf₂ : Continuous[inst_3, inst_5] (⇑f₂ : (a : N) → P)
f₁ : G →* N
hf₁ : Continuous[inst_1, inst_3] (⇑f₁ : (a : G) → N)
⊢ comap f₁ hf₁ (comap f₂ hf₂ K) = comap (f₂.comp f₁) ⋯ K

Tactic:
rfl

Premises used: Set.Mem, setOf, OpenSubgroup.comap, Set.preimage, Subgroup.comap, rfl
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
H : Subgroup G
g : G
hg : (↑H : Set G) ∈ 𝓝 g
⊢ IsOpen[inst_1] (↑H : Set G)

Tactic:
isOpen_iff_mem_nhds.2 fun x hx ↦ ?_

Premises used: Iff.mpr, isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
H : Subgroup G
g : G
hg : (↑H : Set G) ∈ 𝓝 g
refine : ∀ (x : G) (hx : x ∈ (↑H : Set G)), (↑H : Set G) ∈ 𝓝 x
⊢ IsOpen[inst_1] (↑H : Set G)

Tactic:
refine isOpen_iff_mem_nhds.2 fun x hx ↦ ?_

Premises used: Iff.mpr, isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
H : Subgroup G
g : G
hg : (↑H : Set G) ∈ 𝓝 g
x : G
hx : x ∈ (↑H : Set G)
⊢ g ∈ H

Tactic:
have hg' : g ∈ H := SetLike.mem_coe.1 (mem_of_mem_nhds hg)
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
H : Subgroup G
g : G
hg : (↑H : Set G) ∈ 𝓝 g
x : G
hx : x ∈ (↑H : Set G)
hg' : g ∈ H
⊢ Filter.Tendsto (fun (y : G) ↦ y * (x⁻¹ * g)) (𝓝 x) (𝓝 g)

Tactic:
have : Filter.Tendsto (fun y ↦ y * (x⁻¹ * g)) (𝓝 x) (𝓝 g) :=
    (continuous_id.mul_const _).tendsto' _ _ (mul_inv_cancel_left _ _)
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
H : Subgroup G
g : G
hg : (↑H : Set G) ∈ 𝓝 g
x : G
hx : x ∈ (↑H : Set G)
hg' : g ∈ H
this : Filter.Tendsto (fun (y : G) ↦ y * (x⁻¹ * g)) (𝓝 x) (𝓝 g)
⊢ (↑H : Set G) ∈ 𝓝 x

Tactic:
simpa only [SetLike.mem_coe, Filter.mem_map',
    H.mul_mem_cancel_right (H.mul_mem (H.inv_mem hx) hg')] using this hg

Premises used: Subgroup.mul_mem_cancel_right, Filter.mem_map', Subgroup.inv_mem, SetLike.mem_coe, Subgroup.mul_mem
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
H₁ H₂ : Subgroup G
h : H₁ ≤ H₂
h₁ : IsOpen[inst_1] (↑H₁ : Set G)
⊢ IsOpen[inst_1] (↑H₂ : Set G)

Tactic:
isOpen_of_mem_nhds _ <| Filter.mem_of_superset (h₁.mem_nhds <| one_mem H₁) h

Premises used: Subgroup.isOpen_of_mem_nhds, IsOpen.mem_nhds, OneMemClass.one_mem, Filter.mem_of_superset
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
H : Subgroup G
U : OpenSubgroup G
h : (↑U : Subgroup G) ≤ H
⊢ IsOpen[inst_1] (↑H : Set G)

Tactic:
isOpen_mono h U.isOpen

Premises used: OpenSubgroup.isOpen, Subgroup.isOpen_mono
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
H : Subgroup G
h_1_int : 1 ∈ interior (↑H : Set G)
⊢ IsOpen[inst_1] (↑H : Set G)

Tactic:
isOpen_of_mem_nhds H <| mem_interior_iff_mem_nhds.1 h_1_int

Premises used: Subgroup.isOpen_of_mem_nhds, mem_interior_iff_mem_nhds, Iff.mp
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : SeparatelyContinuousMul G
U : Subgroup G
h : IsOpen[inst_1] (↑U : Set G)
⊢ IsClosed[inst_1] (↑U : Set G)

Tactic:
OpenSubgroup.isClosed ⟨U, h⟩

Premises used: OpenSubgroup.mk, OpenSubgroup.isClosed