awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
Goal:
P : ProfiniteGrp.{u}
rw :
  Function.Bijective (α :=
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (β :=
    (↑((limit P.diagram).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : ProfiniteGrp.{u}) ↦
          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) →ₜ*
            (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
          (CC := fun (X : ProfiniteGrp.{u}) ↦
          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
          P.toLimit) :
      (a : (↑P.toProfinite.toTop : Type u)) → (↑(limit P.diagram).toProfinite.toTop : Type u))
⊢ IsIso P.toLimit

Tactic:
rw [CategoryTheory.ConcreteCategory.isIso_iff_bijective]

Premises used: CategoryTheory.ConcreteCategory.isIso_iff_bijective
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
Goal:
P : ProfiniteGrp.{u}
⊢ Function.Bijective (α :=
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (β :=
    (↑((limit P.diagram).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : ProfiniteGrp.{u}) ↦
          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) →ₜ*
            (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
          (CC := fun (X : ProfiniteGrp.{u}) ↦
          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
          P.toLimit) :
      (a : (↑P.toProfinite.toTop : Type u)) → (↑(limit P.diagram).toProfinite.toTop : Type u))

Tactic:
⟨toLimit_injective P, toLimit_surjective P⟩

Premises used: ProfiniteGrp.toLimit_surjective, ProfiniteGrp.toLimit_injective, And.intro, Function.Bijective
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
Goal:
P : ProfiniteGrp.{u}
⊢ Function.Bijective (α :=
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (β :=
    (↑((limit P.diagram).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : ProfiniteGrp.{u}) ↦
          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) →ₜ*
            (↑(Y.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
          (CC := fun (X : ProfiniteGrp.{u}) ↦
          (↑(X.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
          P.toLimit) :
      (a : (↑P.toProfinite.toTop : Type u)) → (↑(limit P.diagram).toProfinite.toTop : Type u))

Tactic:
exact ⟨toLimit_injective P, toLimit_surjective P⟩
-- Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
Goal:
P : ProfiniteGrp.{u}
U :
  OpenNormalSubgroup
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
⊢ Continuous (X :=
    (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (Y :=
    (↑((P.diagram.obj U).toProfinite.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u))
    (Function.comp (β :=
      (↑((Functor.obj
                  (Functor.obj
                    (Functor.const
                      (OpenNormalSubgroup
                        (↑(P.toProfinite.toTop (P := fun (X : TopCat.{u}) ↦
                              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                          Type u)))
                    (limitCone P.diagram).pt)
                  U).toProfinite.toTop
            (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u))
      (⇑(Hom.hom ((limitCone P.diagram).π.app U)) :
        (a :
            (↑(((Functor.const (OpenNormalSubgroup (↑P.toProfinite.toTop : Type u))).obj (limitCone P.diagram).pt).obj
                      U).toProfinite.toTop :
              Type u)) →
          (↑(P.diagram.obj U).toProfinite.toTop : Type u))
      (⇑(Hom.hom P.toLimit) : (a : (↑P.toProfinite.toTop : Type u)) → (↑(limit P.diagram).toProfinite.toTop : Type u)))

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
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 : ∀ (H : OpenSubgroup G) (hH : (↑H : Set G) ⊆ W), ∃ (H : OpenNormalSubgroup G), (↑H : Set G) ⊆ W
⊢ ∃ (H : OpenNormalSubgroup G), (↑H : Set G) ⊆ W

Tactic:
rcases exist_openSubgroup_sub_clopen_nhds_of_one WClopen einW with ⟨H, hH⟩

Premises used: IsTopologicalGroup.exist_openSubgroup_sub_clopen_nhds_of_one
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
H : OpenSubgroup G
hH : (↑H : Set G) ⊆ W
⊢ (↑H : Subgroup G).FiniteIndex

Tactic:
have : Subgroup.FiniteIndex H.toSubgroup := H.finiteIndex_of_finite_quotient
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
H : OpenSubgroup G
hH : (↑H : Set G) ⊆ W
this : (↑H : Subgroup G).FiniteIndex
h :
  (↑(let __Subgroup := (↑H : Subgroup G).normalCore;
        { toSubgroup := __Subgroup, isOpen' := ⋯, isNormal' := ⋯ : OpenNormalSubgroup G }) :
      Set G) ⊆
    W
⊢ ∃ (H : OpenNormalSubgroup G), (↑H : Set G) ⊆ W

Tactic:
use { toSubgroup := Subgroup.normalCore H
        isOpen' := Subgroup.isOpen_of_isClosed_of_finiteIndex _ (H.normalCore_isClosed H.isClosed) }
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
H : OpenSubgroup G
hH : (↑H : Set G) ⊆ W
this : (↑H : Subgroup G).FiniteIndex
⊢ (↑(let __Subgroup := (↑H : Subgroup G).normalCore;
        { toSubgroup := __Subgroup, isOpen' := ⋯, isNormal' := ⋯ : OpenNormalSubgroup G }) :
      Set G) ⊆
    W

Tactic:
fun _ b ↦ hH (H.normalCore_le b)

Premises used: Set.Subset, Subgroup.normalCore_le, OpenSubgroup.toSubgroup
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
H : OpenSubgroup G
hH : (↑H : Set G) ⊆ W
this : (↑H : Subgroup G).FiniteIndex
⊢ (↑(let __Subgroup := (↑H : Subgroup G).normalCore;
        { toSubgroup := __Subgroup, isOpen' := ⋯, isNormal' := ⋯ : OpenNormalSubgroup G }) :
      Set G) ⊆
    W

Tactic:
exact fun _ b ↦ hH (H.normalCore_le b)

Premises used: Subgroup.normalCore_le, OpenSubgroup.toSubgroup
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
U : Set G
UOpen : IsOpen U
einU : 1 ∈ U
w : Set G
h : U ⊆ U ∧ IsOpen U ∧ 1 ∈ U
⊢ ∃ t ⊆ U, IsOpen t ∧ 1 ∈ t

Tactic:
use U
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
U : Set G
UOpen : IsOpen U
einU : 1 ∈ U
rcases : ∀ (W : Set G) (hW : 1 ∈ W ∧ IsClopen W) (h : id W ⊆ U), ∃ (H : OpenNormalSubgroup G), (↑H : Set G) ⊆ U
⊢ ∃ (H : OpenNormalSubgroup G), (↑H : Set G) ⊆ U

Tactic:
rcases ((Filter.HasBasis.mem_iff' ((nhds_basis_clopen (1 : G))) U).mp <|
    mem_nhds_iff.mpr (by use U)) with ⟨W, hW, h⟩

Premises used: Iff.mpr, mem_nhds_iff, nhds_basis_clopen, Iff.mp, Filter.HasBasis.mem_iff', OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
U : Set G
UOpen : IsOpen U
einU : 1 ∈ U
W : Set G
hW : 1 ∈ W ∧ IsClopen W
h : id W ⊆ U
rcases : ∀ (H : OpenNormalSubgroup G) (hH : (↑H : Set G) ⊆ W), ∃ (H : OpenNormalSubgroup G), (↑H : Set G) ⊆ U
⊢ ∃ (H : OpenNormalSubgroup G), (↑H : Set G) ⊆ U

Tactic:
rcases IsTopologicalGroup.exist_openNormalSubgroup_sub_clopen_nhds_of_one hW.2 hW.1 with ⟨H, hH⟩

Premises used: IsTopologicalGroup.exist_openNormalSubgroup_sub_clopen_nhds_of_one, And.right, And.left
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
U : Set G
UOpen : IsOpen U
einU : 1 ∈ U
W : Set G
hW : 1 ∈ W ∧ IsClopen W
h : id W ⊆ U
H : OpenNormalSubgroup G
hH : (↑H : Set G) ⊆ W
⊢ ∃ (H : OpenNormalSubgroup G), (↑H : Set G) ⊆ U

Tactic:
⟨H, fun _ a ↦ h (hH a)⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
U : Set G
UOpen : IsOpen U
einU : 1 ∈ U
W : Set G
hW : 1 ∈ W ∧ IsClopen W
h : id W ⊆ U
H : OpenNormalSubgroup G
hH : (↑H : Set G) ⊆ W
⊢ ∃ (H : OpenNormalSubgroup G), (↑H : Set G) ⊆ U

Tactic:
exact ⟨H, fun _ a ↦ h (hH a)⟩
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
a : (↑H : Subgroup G) ≤ sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}
a₁ : sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N} ≤ (↑H : Subgroup G)
⊢ (↑H : Subgroup G) = sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
⊢ (↑H : Subgroup G) ≤ sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}

Tactic:
le_sInf fun N hN ↦ hN.2

Premises used: Set.Mem, And.right, le_sInf
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
⊢ (↑H : Subgroup G) ≤ sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}

Tactic:
exact le_sInf fun N hN ↦ hN.2

Premises used: le_sInf
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
a : ∀ (hg_not : g ∉ (↑H : Subgroup G)), False
⊢ g ∈ (↑H : Subgroup G)

Tactic:
by_contra hg_not
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
hg_not : g ∉ (↑H : Subgroup G)
U : Set G := (g • (↑H : Set G))ᶜ
⊢ IsOpen U

Tactic:
have UOpen : IsOpen U :=
      ((Homeomorph.mulLeft g).isClosedMap _ H.isClosed').isOpen_compl
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
hg_not : g ∉ (↑H : Subgroup G)
U : Set G := (g • (↑H : Set G))ᶜ
UOpen : IsOpen U
⊢ 1 ∈ U

Tactic:
Set.mem_compl (fun ⟨l, hl, (hgl : g * l = 1)⟩ ↦ ?_)

Premises used: False, Set.Mem, _private.0.ProfiniteGrp.closedSubgroup_eq_sInf_open.match_1, Set.mem_compl
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
hg_not : g ∉ (↑H : Subgroup G)
U : Set G := (g • (↑H : Set G))ᶜ
UOpen : IsOpen U
refine : 1 ∈ g • (↑H : Set G) → ∀ (l : G) (hl : l ∈ (↑H : Set G)) (hgl : g * l = 1), False
⊢ 1 ∈ U

Tactic:
refine Set.mem_compl (fun ⟨l, hl, (hgl : g * l = 1)⟩ ↦ ?_)
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
hg_not : g ∉ (↑H : Subgroup G)
U : Set G := (g • (↑H : Set G))ᶜ
UOpen : IsOpen U
h : 1 ∈ g • (↑H : Set G)
l : G
hl : l ∈ (↑H : Set G)
hgl : g * l = 1
⊢ g⁻¹ = l

Tactic:
rw [← inv_eq_iff_mul_eq_one] at hgl

Premises used: inv_eq_iff_mul_eq_one
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
hg_not : g ∉ (↑H : Subgroup G)
U : Set G := (g • (↑H : Set G))ᶜ
UOpen : IsOpen U
h : 1 ∈ g • (↑H : Set G)
l : G
hl : l ∈ (↑H : Set G)
hgl : g⁻¹ = l
⊢ False

Tactic:
hg_not <| inv_mem_iff.mp (hgl ▸ hl)

Premises used: inv_mem_iff, Iff.mp
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
hg_not : g ∉ (↑H : Subgroup G)
U : Set G := (g • (↑H : Set G))ᶜ
UOpen : IsOpen U
h : 1 ∈ g • (↑H : Set G)
l : G
hl : l ∈ (↑H : Set G)
hgl : g⁻¹ = l
⊢ False

Tactic:
exact hg_not <| inv_mem_iff.mp (hgl ▸ hl)

Premises used: inv_mem_iff, Iff.mp
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
hg_not : g ∉ (↑H : Subgroup G)
U : Set G := (g • (↑H : Set G))ᶜ
UOpen : IsOpen U
⊢ 1 ∈ U

Tactic:
have einU : 1 ∈ U := by
      refine Set.mem_compl (fun ⟨l, hl, (hgl : g * l = 1)⟩ ↦ ?_)
      rw [← inv_eq_iff_mul_eq_one] at hgl
      exact hg_not <| inv_mem_iff.mp (hgl ▸ hl)
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
hg_not : g ∉ (↑H : Subgroup G)
U : Set G := (g • (↑H : Set G))ᶜ
UOpen : IsOpen U
einU : 1 ∈ U
a : ∀ (N : OpenNormalSubgroup G) (hN : (↑N : Set G) ⊆ U), False
⊢ False

Tactic:
obtain ⟨N, hN⟩ := exist_openNormalSubgroup_sub_open_nhds_of_one UOpen einU

Premises used: ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
hg_not : g ∉ (↑H : Subgroup G)
U : Set G := (g • (↑H : Set G))ᶜ
UOpen : IsOpen U
einU : 1 ∈ U
N : OpenNormalSubgroup G
hN : (↑N : Set G) ⊆ U
NH : Subgroup G := (↑N.toOpenSubgroup : Subgroup G) ⊔ (↑H : Subgroup G)
by_contra : ∀ (hg' : g ∈ NH), False
⊢ g ∉ NH

Tactic:
by_contra hg'
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
hg_not : g ∉ (↑H : Subgroup G)
U : Set G := (g • (↑H : Set G))ᶜ
UOpen : IsOpen U
einU : 1 ∈ U
N : OpenNormalSubgroup G
hN : (↑N : Set G) ⊆ U
NH : Subgroup G := (↑N.toOpenSubgroup : Subgroup G) ⊔ (↑H : Subgroup G)
hg' : g ∈ NH
rcases :
  ∀ (y : G) (hy : y ∈ (↑N.toOpenSubgroup : Subgroup G)) (z : G) (hz : z ∈ (↑H : Subgroup G)) (hyz : y * z = g), False
⊢ False

Tactic:
rcases Subgroup.mem_sup_of_normal_left.mp hg' with ⟨y, hy, z, hz, hyz⟩

Premises used: Iff.mp, Subgroup.mem_sup_of_normal_left
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
hg_not : g ∉ (↑H : Subgroup G)
U : Set G := (g • (↑H : Set G))ᶜ
UOpen : IsOpen U
einU : 1 ∈ U
N : OpenNormalSubgroup G
hN : (↑N : Set G) ⊆ U
NH : Subgroup G := (↑N.toOpenSubgroup : Subgroup G) ⊔ (↑H : Subgroup G)
hg' : g ∈ NH
y : G
hy : y ∈ (↑N.toOpenSubgroup : Subgroup G)
z : G
hz : z ∈ (↑H : Subgroup G)
hyz : y * z = g
⊢ y = g * z⁻¹

Tactic:
rw [← eq_mul_inv_iff_mul_eq] at hyz

Premises used: eq_mul_inv_iff_mul_eq
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
hg_not : g ∉ (↑H : Subgroup G)
U : Set G := (g • (↑H : Set G))ᶜ
UOpen : IsOpen U
einU : 1 ∈ U
N : OpenNormalSubgroup G
hN : (↑N : Set G) ⊆ U
NH : Subgroup G := (↑N.toOpenSubgroup : Subgroup G) ⊔ (↑H : Subgroup G)
hg' : g ∈ NH
y : G
hy : y ∈ (↑N.toOpenSubgroup : Subgroup G)
z : G
hz : z ∈ (↑H : Subgroup G)
hyz : y = g * z⁻¹
⊢ False

Tactic:
hN (hyz ▸ hy) <| mem_leftCoset g (inv_mem_iff.mpr hz)

Premises used: Iff.mpr, inv_mem_iff, mem_leftCoset
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
hg_not : g ∉ (↑H : Subgroup G)
U : Set G := (g • (↑H : Set G))ᶜ
UOpen : IsOpen U
einU : 1 ∈ U
N : OpenNormalSubgroup G
hN : (↑N : Set G) ⊆ U
NH : Subgroup G := (↑N.toOpenSubgroup : Subgroup G) ⊔ (↑H : Subgroup G)
hg' : g ∈ NH
y : G
hy : y ∈ (↑N.toOpenSubgroup : Subgroup G)
z : G
hz : z ∈ (↑H : Subgroup G)
hyz : y = g * z⁻¹
⊢ False

Tactic:
exact hN (hyz ▸ hy) <| mem_leftCoset g (inv_mem_iff.mpr hz)

Premises used: Iff.mpr, inv_mem_iff, mem_leftCoset
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
hg_not : g ∉ (↑H : Subgroup G)
U : Set G := (g • (↑H : Set G))ᶜ
UOpen : IsOpen U
einU : 1 ∈ U
N : OpenNormalSubgroup G
hN : (↑N : Set G) ⊆ U
NH : Subgroup G := (↑N.toOpenSubgroup : Subgroup G) ⊔ (↑H : Subgroup G)
⊢ g ∉ NH

Tactic:
have hg_not' : g ∉ NH := by
      by_contra hg'
      rcases Subgroup.mem_sup_of_normal_left.mp hg' with ⟨y, hy, z, hz, hyz⟩
      rw [← eq_mul_inv_iff_mul_eq] at hyz
      exact hN (hyz ▸ hy) <| mem_leftCoset g (inv_mem_iff.mpr hz)
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
hg_not : g ∉ (↑H : Subgroup G)
U : Set G := (g • (↑H : Set G))ᶜ
UOpen : IsOpen U
einU : 1 ∈ U
N : OpenNormalSubgroup G
hN : (↑N : Set G) ⊆ U
NH : Subgroup G := (↑N.toOpenSubgroup : Subgroup G) ⊔ (↑H : Subgroup G)
hg_not' : g ∉ NH
⊢ False

Tactic:
hg_not' <|
      Subgroup.mem_sInf.mp hg _ ⟨Subgroup.isOpen_mono le_sup_left N.isOpen, le_sup_right⟩

Premises used: OpenSubgroup.isOpen, le_sup_left, Subgroup.isOpen_mono, le_sup_right, Subgroup.mem_sInf, And.intro, Iff.mp, OpenNormalSubgroup.toOpenSubgroup
-- Module: Mathlib.Topology.Algebra.ClopenNhdofOne
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
inst_4 : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : Membership.mem (γ := Subgroup G) (sInf {N : Subgroup G | IsOpen (↑N : Set G) ∧ (↑H : Subgroup G) ≤ N}) g
hg_not : g ∉ (↑H : Subgroup G)
U : Set G := (g • (↑H : Set G))ᶜ
UOpen : IsOpen U
einU : 1 ∈ U
N : OpenNormalSubgroup G
hN : (↑N : Set G) ⊆ U
NH : Subgroup G := (↑N.toOpenSubgroup : Subgroup G) ⊔ (↑H : Subgroup G)
hg_not' : g ∉ NH
⊢ False

Tactic:
exact hg_not' <|
      Subgroup.mem_sInf.mp hg _ ⟨Subgroup.isOpen_mono le_sup_left N.isOpen, le_sup_right⟩

Premises used: OpenSubgroup.isOpen, le_sup_left, Subgroup.isOpen_mono, le_sup_right, Subgroup.mem_sInf, And.intro, Iff.mp, OpenNormalSubgroup.toOpenSubgroup
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : SMul M α
inst_2 : ContinuousConstSMul M α
⊢ ContinuousConstSMul (ULift.{u_4, u_1} M) α

Tactic:
⟨fun γ ↦ continuous_const_smul (ULift.down γ)⟩

Premises used: ContinuousConstSMul.continuous_const_smul, ContinuousConstSMul.mk, ULift.down
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : SMul M α
inst_2 : ContinuousConstSMul M α
f : β → α
l : Filter β
a : α
hf : Tendsto f l (𝓝 a)
c : M
⊢ Tendsto (fun (x : β) ↦ c • f x) l (𝓝 (c • a))

Tactic:
((continuous_const_smul _).tendsto _).comp hf

Premises used: ContinuousConstSMul.continuous_const_smul, Continuous.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : SMul M α
inst_2 : ContinuousConstSMul M α
inst_3 : TopologicalSpace β
g : β → α
b : β
s : Set β
hg : ContinuousWithinAt g s b
c : M
⊢ ContinuousWithinAt.{u_3, u_2} (Y := α) (fun (x : β) ↦ c • g x) s b

Tactic:
hg.const_smul c

Premises used: ContinuousWithinAt, Filter.Tendsto.const_smul
-- Module: Mathlib.Topology.Algebra.ConstMulAction
Goal:
M : Type u_1
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : SMul M α
inst_2 : ContinuousConstSMul M α
inst_3 : TopologicalSpace β
g : β → α
b : β
hg : ContinuousAt g b
c : M
⊢ ContinuousAt.{u_3, u_2} (Y := α) (fun (x : β) ↦ c • g x) b

Tactic:
hg.const_smul c

Premises used: ContinuousAt, Filter.Tendsto.const_smul