awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hx : Eq (α := Set X) (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X)) {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s : Set X // IsClopen s ∧ x ∈ s }
this : Nonempty N
hNcl : ∀ (s : N), IsClosed[inst] (↑s : Set X)
hdir : Directed (α := Set X) Superset fun (s : N) ↦ (↑s : Set X)
h_nhds : ∀ (y : X), Membership.mem (γ := Set X) (⋂ (s : N), (↑s : Set X)) y → U ∈ 𝓝 y
⊢ ∃ (s : N), (↑s : Set X) ⊆ U

Tactic:
exists_subset_nhds_of_compactSpace hdir hNcl h_nhds

Premises used: exists_subset_nhds_of_compactSpace
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hx : Eq (α := Set X) (⋂ (s : { s : Set X // IsClopen s ∧ x ∈ s }), (↑s : Set X)) {x}
hU : U ∈ 𝓝 x
N : Type (max 0 u_1) := { s : Set X // IsClopen s ∧ x ∈ s }
this : Nonempty N
hNcl : ∀ (s : N), IsClosed[inst] (↑s : Set X)
hdir : Directed (α := Set X) Superset fun (s : N) ↦ (↑s : Set X)
h_nhds : ∀ (y : X), Membership.mem (γ := Set X) (⋂ (s : N), (↑s : Set X)) y → U ∈ 𝓝 y
⊢ ∃ (s : N), (↑s : Set X) ⊆ U

Tactic:
exact exists_subset_nhds_of_compactSpace hdir hNcl h_nhds

Premises used: exists_subset_nhds_of_compactSpace
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U V : Set X
hUV : V ⊆ U
hxV : x ∈ V
V_op : IsOpen[inst] V
mpr : ∃ t ⊆ U, IsOpen[inst] t ∧ x ∈ t
⊢ U ∈ 𝓝 x

Tactic:
rw [mem_nhds_iff]

Premises used: mem_nhds_iff
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U V : Set X
hUV : V ⊆ U
hxV : x ∈ V
V_op : IsOpen[inst] V
⊢ ∃ t ⊆ U, IsOpen[inst] t ∧ x ∈ t

Tactic:
⟨V, hUV, V_op, hxV⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U V : Set X
hUV : V ⊆ U
hxV : x ∈ V
V_op : IsOpen[inst] V
⊢ ∃ t ⊆ U, IsOpen[inst] t ∧ x ∈ t

Tactic:
exact ⟨V, hUV, V_op, hxV⟩
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
apply :
  ∀ (a : X) (u : Set X),
    a ∈ u →
      IsOpen[inst] u →
        ∃ (v : Set X),
          Membership.mem (γ := Set (Set X)) (fun (U : Set X) ↦ IsClosed[inst] U ∧ IsOpen[inst] U) v ∧ a ∈ v ∧ v ⊆ u
⊢ IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}

Tactic:
apply isTopologicalBasis_of_isOpen_of_nhds fun U (hU : IsClopen U) => hU.2

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds, And.right
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hxU : x ∈ U
U_op : IsOpen[inst] U
⊢ U ∈ 𝓝 x

Tactic:
have : U ∈ 𝓝 x := IsOpen.mem_nhds U_op hxU
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hxU : x ∈ U
U_op : IsOpen[inst] U
this : U ∈ 𝓝 x
rcases :
  ∀ (V : Set X) (hVU : V ⊆ U) (hxV : x ∈ V) (hV : IsClopen V),
    ∃ (v : Set X),
      Membership.mem (γ := Set (Set X)) (fun (U : Set X) ↦ IsClosed[inst] U ∧ IsOpen[inst] U) v ∧ x ∈ v ∧ v ⊆ U
⊢ ∃ (v : Set X),
    Membership.mem (γ := Set (Set X)) (fun (U : Set X) ↦ IsClosed[inst] U ∧ IsOpen[inst] U) v ∧ x ∈ v ∧ v ⊆ U

Tactic:
rcases (nhds_basis_clopen x).mem_iff.mp this with ⟨V, ⟨hxV, hV⟩, hVU : V ⊆ U⟩

Premises used: Filter.HasBasis.mem_iff, nhds_basis_clopen, Iff.mp
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hxU : x ∈ U
U_op : IsOpen[inst] U
this : U ∈ 𝓝 x
V : Set X
hVU : V ⊆ U
hxV : x ∈ V
hV : IsClopen V
h : Membership.mem (γ := Set (Set X)) (fun (U : Set X) ↦ IsClosed[inst] U ∧ IsOpen[inst] U) V ∧ x ∈ V ∧ V ⊆ U
⊢ ∃ (v : Set X),
    Membership.mem (γ := Set (Set X)) (fun (U : Set X) ↦ IsClosed[inst] U ∧ IsOpen[inst] U) v ∧ x ∈ v ∧ v ⊆ U

Tactic:
use V
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
hxU : x ∈ U
U_op : IsOpen[inst] U
this : U ∈ 𝓝 x
V : Set X
hVU : V ⊆ U
hxV : x ∈ V
hV : IsClopen V
h : Membership.mem (γ := Set (Set X)) (fun (U : Set X) ↦ IsClosed[inst] U ∧ IsOpen[inst] U) V
h₁ : x ∈ V
h₂ : V ⊆ U
⊢ Membership.mem (γ := Set (Set X)) (fun (U : Set X) ↦ IsClosed[inst] U ∧ IsOpen[inst] U) V ∧ x ∈ V ∧ V ⊆ U

Tactic:
tauto
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
x : X
U : Set X
is_open : IsOpen[inst] U
memU : x ∈ U
⊢ ∃ (V : Set X), IsClopen V ∧ x ∈ V ∧ V ⊆ U

Tactic:
isTopologicalBasis_isClopen.mem_nhds_iff.1 (is_open.mem_nhds memU)

Premises used: Set.Mem, setOf, isTopologicalBasis_isClopen, IsOpen.mem_nhds, Iff.mp, IsClopen, TopologicalSpace.IsTopologicalBasis.mem_nhds_iff
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
H : Type u_3
inst : TopologicalSpace H
inst_1 : LocallyCompactSpace H
inst_2 : T2Space H
inst_3 : TotallyDisconnectedSpace H
⊢ IsTopologicalBasis.{u_3} (α := H) {s : Set H | IsClopen s}

Tactic:
isTopologicalBasis_of_isOpen_of_nhds (fun u hu => hu.2) fun x U memU hU => ?_

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds, And.right
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
H : Type u_3
inst : TopologicalSpace H
inst_1 : LocallyCompactSpace H
inst_2 : T2Space H
inst_3 : TotallyDisconnectedSpace H
refine :
  ∀ (x : H) (U : Set H) (memU : x ∈ U) (hU : IsOpen[inst] U),
    ∃ (v : Set H), Membership.mem (γ := Set (Set H)) {s : Set H | IsClopen s} v ∧ x ∈ v ∧ v ⊆ U
⊢ IsTopologicalBasis.{u_3} (α := H) {s : Set H | IsClopen s}

Tactic:
refine isTopologicalBasis_of_isOpen_of_nhds (fun u hu => hu.2) fun x U memU hU => ?_

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
H : Type u_3
inst : TopologicalSpace H
inst_1 : LocallyCompactSpace H
inst_2 : T2Space H
inst_3 : TotallyDisconnectedSpace H
x : H
U : Set H
memU : x ∈ U
hU : IsOpen[inst] U
obtain :
  ∀ (s : Set H) (comp : IsCompact s) (xs : x ∈ interior s) (sU : s ⊆ U),
    ∃ (v : Set H), Membership.mem (γ := Set (Set H)) {s : Set H | IsClopen s} v ∧ x ∈ v ∧ v ⊆ U
⊢ ∃ (v : Set H), Membership.mem (γ := Set (Set H)) {s : Set H | IsClopen s} v ∧ x ∈ v ∧ v ⊆ U

Tactic:
obtain ⟨s, comp, xs, sU⟩ := exists_compact_subset hU memU

Premises used: Function.comp, exists_compact_subset
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
H : Type u_3
inst : TopologicalSpace H
inst_1 : LocallyCompactSpace H
inst_2 : T2Space H
inst_3 : TotallyDisconnectedSpace H
x : H
U : Set H
memU : x ∈ U
hU : IsOpen[inst] U
s : Set H
comp : IsCompact s
xs : x ∈ interior s
sU : s ⊆ U
u : Set (↑s : Type u_3) := Subtype.val (p := fun (x : H) ↦ x ∈ s) ⁻¹' interior s
⊢ IsOpen[instTopologicalSpaceSubtype] u

Tactic:
have u_open_in_s : IsOpen u := isOpen_interior.preimage continuous_subtype_val
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
H : Type u_3
inst : TopologicalSpace H
inst_1 : LocallyCompactSpace H
inst_2 : T2Space H
inst_3 : TotallyDisconnectedSpace H
x : H
U : Set H
memU : x ∈ U
hU : IsOpen[inst] U
s : Set H
comp : IsCompact s
xs : x ∈ interior s
sU : s ⊆ U
u : Set (↑s : Type u_3) := Subtype.val (p := fun (x : H) ↦ x ∈ s) ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
⊢ x ∈ s

Tactic:
interior_subset xs

Premises used: interior_subset
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
H : Type u_3
inst : TopologicalSpace H
inst_1 : LocallyCompactSpace H
inst_2 : T2Space H
inst_3 : TotallyDisconnectedSpace H
x : H
U : Set H
memU : x ∈ U
hU : IsOpen[inst] U
s : Set H
comp : IsCompact s
xs : x ∈ interior s
sU : s ⊆ U
u : Set (↑s : Type u_3) := Subtype.val (p := fun (x : H) ↦ x ∈ s) ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
lift :
  ∀ (x : { x : H // x ∈ s }) (memU : (↑x : H) ∈ U) (xs : (↑x : H) ∈ interior s),
    ∃ (v : Set H), Membership.mem (γ := Set (Set H)) {s : Set H | IsClopen s} v ∧ (↑x : H) ∈ v ∧ v ⊆ U
⊢ ∃ (v : Set H), Membership.mem (γ := Set (Set H)) {s : Set H | IsClopen s} v ∧ x ∈ v ∧ v ⊆ U

Tactic:
lift x to s using interior_subset xs

Premises used: interior_subset
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
H : Type u_3
inst : TopologicalSpace H
inst_1 : LocallyCompactSpace H
inst_2 : T2Space H
inst_3 : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set (↑s : Type u_3) := Subtype.val (p := fun (x : H) ↦ x ∈ s) ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x : H // x ∈ s }
memU : (↑x : H) ∈ U
xs : (↑x : H) ∈ interior s
⊢ CompactSpace.{u_3} (↑s : Type u_3)

Tactic:
haveI : CompactSpace s := isCompact_iff_compactSpace.1 comp
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
H : Type u_3
inst : TopologicalSpace H
inst_1 : LocallyCompactSpace H
inst_2 : T2Space H
inst_3 : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set (↑s : Type u_3) := Subtype.val (p := fun (x : H) ↦ x ∈ s) ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x : H // x ∈ s }
memU : (↑x : H) ∈ U
xs : (↑x : H) ∈ interior s
this : CompactSpace.{u_3} (↑s : Type u_3)
obtain :
  ∀ (V : Set (↑s : Type u_3)) (VisClopen : IsClopen V) (Vx : x ∈ V) (V_sub : V ⊆ u),
    ∃ (v : Set H), Membership.mem (γ := Set (Set H)) {s : Set H | IsClopen s} v ∧ (↑x : H) ∈ v ∧ v ⊆ U
⊢ ∃ (v : Set H), Membership.mem (γ := Set (Set H)) {s : Set H | IsClopen s} v ∧ (↑x : H) ∈ v ∧ v ⊆ U

Tactic:
obtain ⟨V : Set s, VisClopen, Vx, V_sub⟩ := compact_exists_isClopen_in_isOpen u_open_in_s xs

Premises used: Set.Elem, compact_exists_isClopen_in_isOpen, Set
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
H : Type u_3
inst : TopologicalSpace H
inst_1 : LocallyCompactSpace H
inst_2 : T2Space H
inst_3 : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set (↑s : Type u_3) := Subtype.val (p := fun (x : H) ↦ x ∈ s) ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x : H // x ∈ s }
memU : (↑x : H) ∈ U
xs : (↑x : H) ∈ interior s
this : CompactSpace.{u_3} (↑s : Type u_3)
V : Set (↑s : Type u_3)
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
⊢ IsClopen (Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V)

Tactic:
⟨comp.isClosed.isClosedEmbedding_subtypeVal.isClosed_iff_image_isClosed.1 VisClopen.1,
      ?_⟩

Premises used: And.left, Topology.IsClosedEmbedding.isClosed_iff_image_isClosed, And.intro, Iff.mp, IsClosed.isClosedEmbedding_subtypeVal, IsClopen, IsCompact.isClosed
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
H : Type u_3
inst : TopologicalSpace H
inst_1 : LocallyCompactSpace H
inst_2 : T2Space H
inst_3 : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set (↑s : Type u_3) := Subtype.val (p := fun (x : H) ↦ x ∈ s) ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x : H // x ∈ s }
memU : (↑x : H) ∈ U
xs : (↑x : H) ∈ interior s
this : CompactSpace.{u_3} (↑s : Type u_3)
V : Set (↑s : Type u_3)
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
refine : IsOpen[inst] (Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V)
⊢ IsClopen (Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V)

Tactic:
refine ⟨comp.isClosed.isClosedEmbedding_subtypeVal.isClosed_iff_image_isClosed.1 VisClopen.1,
      ?_⟩
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
H : Type u_3
inst : TopologicalSpace H
inst_1 : LocallyCompactSpace H
inst_2 : T2Space H
inst_3 : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set (↑s : Type u_3) := Subtype.val (p := fun (x : H) ↦ x ∈ s) ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x : H // x ∈ s }
memU : (↑x : H) ∈ U
xs : (↑x : H) ∈ interior s
this : CompactSpace.{u_3} (↑s : Type u_3)
V : Set (↑s : Type u_3)
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set (↑u : Type u_3) := Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u) ⁻¹' V
⊢ Eq.{u_3 + 1} (α := (x : (↑u : Type u_3)) → H) (fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H))
    (Subtype.val (p := fun (x : H) ↦ x ∈ s) ∘ Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u))

Tactic:
have : ((↑) : u → H) = ((↑) : s → H) ∘ ((↑) : u → s) := rfl
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
H : Type u_3
inst : TopologicalSpace H
inst_1 : LocallyCompactSpace H
inst_2 : T2Space H
inst_3 : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set (↑s : Type u_3) := Subtype.val (p := fun (x : H) ↦ x ∈ s) ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x : H // x ∈ s }
memU : (↑x : H) ∈ U
xs : (↑x : H) ∈ interior s
this_1 : CompactSpace.{u_3} (↑s : Type u_3)
V : Set (↑s : Type u_3)
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set (↑u : Type u_3) := Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u) ⁻¹' V
this :
  Eq.{u_3 + 1} (α := (x : (↑u : Type u_3)) → H) (fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H))
    (Subtype.val (p := fun (x : H) ↦ x ∈ s) ∘ Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u))
⊢ IsEmbedding (Y := H) fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)

Tactic:
have f0 : IsEmbedding ((↑) : u → H) := IsEmbedding.subtypeVal.comp IsEmbedding.subtypeVal
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
H : Type u_3
inst : TopologicalSpace H
inst_1 : LocallyCompactSpace H
inst_2 : T2Space H
inst_3 : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set (↑s : Type u_3) := Subtype.val (p := fun (x : H) ↦ x ∈ s) ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x : H // x ∈ s }
memU : (↑x : H) ∈ U
xs : (↑x : H) ∈ interior s
this_1 : CompactSpace.{u_3} (↑s : Type u_3)
V : Set (↑s : Type u_3)
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set (↑u : Type u_3) := Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u) ⁻¹' V
this :
  Eq.{u_3 + 1} (α := (x : (↑u : Type u_3)) → H) (fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H))
    (Subtype.val (p := fun (x : H) ↦ x ∈ s) ∘ Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u))
f0 : IsEmbedding (Y := H) fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)
⊢ IsOpenEmbedding (Y := H) fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)

Tactic:
⟨f0, ?_⟩

Premises used: Topology.IsOpenEmbedding.mk
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
H : Type u_3
inst : TopologicalSpace H
inst_1 : LocallyCompactSpace H
inst_2 : T2Space H
inst_3 : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set (↑s : Type u_3) := Subtype.val (p := fun (x : H) ↦ x ∈ s) ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x : H // x ∈ s }
memU : (↑x : H) ∈ U
xs : (↑x : H) ∈ interior s
this_1 : CompactSpace.{u_3} (↑s : Type u_3)
V : Set (↑s : Type u_3)
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set (↑u : Type u_3) := Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u) ⁻¹' V
this :
  Eq.{u_3 + 1} (α := (x : (↑u : Type u_3)) → H) (fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H))
    (Subtype.val (p := fun (x : H) ↦ x ∈ s) ∘ Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u))
f0 : IsEmbedding (Y := H) fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)
refine : IsOpen[inst] (range fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H))
⊢ IsOpenEmbedding (Y := H) fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)

Tactic:
refine ⟨f0, ?_⟩
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
H : Type u_3
inst : TopologicalSpace H
inst_1 : LocallyCompactSpace H
inst_2 : T2Space H
inst_3 : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set (↑s : Type u_3) := Subtype.val (p := fun (x : H) ↦ x ∈ s) ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x : H // x ∈ s }
memU : (↑x : H) ∈ U
xs : (↑x : H) ∈ interior s
this_1 : CompactSpace.{u_3} (↑s : Type u_3)
V : Set (↑s : Type u_3)
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set (↑u : Type u_3) := Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u) ⁻¹' V
this :
  Eq.{u_3 + 1} (α := (x : (↑u : Type u_3)) → H) (fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H))
    (Subtype.val (p := fun (x : H) ↦ x ∈ s) ∘ Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u))
f0 : IsEmbedding (Y := H) fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)
rw : s ∩ interior s = interior s
⊢ (range fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)) = interior s

Tactic:
rw [this, Set.range_comp, Subtype.range_coe, Subtype.image_preimage_coe]

Premises used: Set.range_comp, Subtype.image_preimage_coe, Subtype.range_coe
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
H : Type u_3
inst : TopologicalSpace H
inst_1 : LocallyCompactSpace H
inst_2 : T2Space H
inst_3 : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set (↑s : Type u_3) := Subtype.val (p := fun (x : H) ↦ x ∈ s) ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x : H // x ∈ s }
memU : (↑x : H) ∈ U
xs : (↑x : H) ∈ interior s
this_1 : CompactSpace.{u_3} (↑s : Type u_3)
V : Set (↑s : Type u_3)
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set (↑u : Type u_3) := Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u) ⁻¹' V
this :
  Eq.{u_3 + 1} (α := (x : (↑u : Type u_3)) → H) (fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H))
    (Subtype.val (p := fun (x : H) ↦ x ∈ s) ∘ Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u))
f0 : IsEmbedding (Y := H) fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)
⊢ s ∩ interior s = interior s

Tactic:
apply Set.inter_eq_self_of_subset_right interior_subset

Premises used: interior_subset, Set.inter_eq_self_of_subset_right
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
H : Type u_3
inst : TopologicalSpace H
inst_1 : LocallyCompactSpace H
inst_2 : T2Space H
inst_3 : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set (↑s : Type u_3) := Subtype.val (p := fun (x : H) ↦ x ∈ s) ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x : H // x ∈ s }
memU : (↑x : H) ∈ U
xs : (↑x : H) ∈ interior s
this_1 : CompactSpace.{u_3} (↑s : Type u_3)
V : Set (↑s : Type u_3)
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set (↑u : Type u_3) := Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u) ⁻¹' V
this :
  Eq.{u_3 + 1} (α := (x : (↑u : Type u_3)) → H) (fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H))
    (Subtype.val (p := fun (x : H) ↦ x ∈ s) ∘ Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u))
f0 : IsEmbedding (Y := H) fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)
⊢ (range fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)) = interior s

Tactic:
have : Set.range ((↑) : u → H) = interior s := by
          rw [this, Set.range_comp, Subtype.range_coe, Subtype.image_preimage_coe]
          apply Set.inter_eq_self_of_subset_right interior_subset
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
H : Type u_3
inst : TopologicalSpace H
inst_1 : LocallyCompactSpace H
inst_2 : T2Space H
inst_3 : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set (↑s : Type u_3) := Subtype.val (p := fun (x : H) ↦ x ∈ s) ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x : H // x ∈ s }
memU : (↑x : H) ∈ U
xs : (↑x : H) ∈ interior s
this_1 : CompactSpace.{u_3} (↑s : Type u_3)
V : Set (↑s : Type u_3)
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set (↑u : Type u_3) := Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u) ⁻¹' V
this_2 :
  Eq.{u_3 + 1} (α := (x : (↑u : Type u_3)) → H) (fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H))
    (Subtype.val (p := fun (x : H) ↦ x ∈ s) ∘ Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u))
f0 : IsEmbedding (Y := H) fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)
this : (range fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)) = interior s
rw : IsOpen[inst] (interior s)
⊢ IsOpen[inst] (range fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H))

Tactic:
rw [this]
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
H : Type u_3
inst : TopologicalSpace H
inst_1 : LocallyCompactSpace H
inst_2 : T2Space H
inst_3 : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set (↑s : Type u_3) := Subtype.val (p := fun (x : H) ↦ x ∈ s) ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x : H // x ∈ s }
memU : (↑x : H) ∈ U
xs : (↑x : H) ∈ interior s
this_1 : CompactSpace.{u_3} (↑s : Type u_3)
V : Set (↑s : Type u_3)
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set (↑u : Type u_3) := Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u) ⁻¹' V
this_2 :
  Eq.{u_3 + 1} (α := (x : (↑u : Type u_3)) → H) (fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H))
    (Subtype.val (p := fun (x : H) ↦ x ∈ s) ∘ Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u))
f0 : IsEmbedding (Y := H) fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)
this : (range fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)) = interior s
⊢ IsOpen[inst] (interior s)

Tactic:
apply isOpen_interior

Premises used: isOpen_interior
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
H : Type u_3
inst : TopologicalSpace H
inst_1 : LocallyCompactSpace H
inst_2 : T2Space H
inst_3 : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen[inst] U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set (↑s : Type u_3) := Subtype.val (p := fun (x : H) ↦ x ∈ s) ⁻¹' interior s
u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
x : { x : H // x ∈ s }
memU : (↑x : H) ∈ U
xs : (↑x : H) ∈ interior s
this_1 : CompactSpace.{u_3} (↑s : Type u_3)
V : Set (↑s : Type u_3)
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
v : Set (↑u : Type u_3) := Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u) ⁻¹' V
this :
  Eq.{u_3 + 1} (α := (x : (↑u : Type u_3)) → H) (fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H))
    (Subtype.val (p := fun (x : H) ↦ x ∈ s) ∘ Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u))
f0 : IsEmbedding (Y := H) fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)
⊢ IsOpenEmbedding (Y := H) fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)

Tactic:
have f1 : IsOpenEmbedding ((↑) : u → H) := by
      refine ⟨f0, ?_⟩
      · have : Set.range ((↑) : u → H) = interior s := by
          rw [this, Set.range_comp, Subtype.range_coe, Subtype.image_preimage_coe]
          apply Set.inter_eq_self_of_subset_right interior_subset
        rw [this]
        apply isOpen_interior