awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : CompactSpace X
inst_3 : TotallyDisconnectedSpace X
⊢ IsTopologicalBasis.{u_1} (α := X) {s : Set X | IsClopen s}
have 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
Tactic: apply isTopologicalBasis_of_isOpen_of_nhds fun U (hU : IsClopen U) => hU.2
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (hypothesis)
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
⊢ ∃ (v : Set X),
    Membership.mem (γ := Set (Set X)) (fun (U : Set X) ↦ IsClosed[inst] U ∧ IsOpen[inst] U) v ∧ x ∈ v ∧ v ⊆ U
have this : U ∈ 𝓝 x
Tactic: have : U ∈ 𝓝 x := IsOpen.mem_nhds U_op hxU
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
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),
    Membership.mem (γ := Set (Set X)) (fun (U : Set X) ↦ IsClosed[inst] U ∧ IsOpen[inst] U) v ∧ x ∈ v ∧ v ⊆ U
have 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
Tactic: rcases (nhds_basis_clopen x).mem_iff.mp this with ⟨V, ⟨hxV, hV⟩, hVU : V ⊆ U⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
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
⊢ ∃ (v : Set X),
    Membership.mem (γ := Set (Set X)) (fun (U : Set X) ↦ IsClosed[inst] U ∧ IsOpen[inst] U) v ∧ x ∈ v ∧ v ⊆ U
have h : Membership.mem (γ := Set (Set X)) (fun (U : Set X) ↦ IsClosed[inst] U ∧ IsOpen[inst] U) V ∧ x ∈ V ∧ V ⊆ U
Tactic: use V
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
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
⊢ Membership.mem (γ := Set (Set X)) (fun (U : Set X) ↦ IsClosed[inst] U ∧ IsOpen[inst] U) V ∧ x ∈ V ∧ V ⊆ U
have h : Membership.mem (γ := Set (Set X)) (fun (U : Set X) ↦ IsClosed[inst] U ∧ IsOpen[inst] U) V
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
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}
have 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
Tactic: refine isTopologicalBasis_of_isOpen_of_nhds (fun u hu => hu.2) fun x U memU hU => ?_
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
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
⊢ ∃ (v : Set H), Membership.mem (γ := Set (Set H)) {s : Set H | IsClopen s} v ∧ x ∈ v ∧ v ⊆ U
have 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
Tactic: obtain ⟨s, comp, xs, sU⟩ := exists_compact_subset hU memU
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (hypothesis)
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
⊢ ∃ (v : Set H), Membership.mem (γ := Set (Set H)) {s : Set H | IsClopen s} v ∧ x ∈ v ∧ v ⊆ U
have u_open_in_s : IsOpen[instTopologicalSpaceSubtype] u
Tactic: have u_open_in_s : IsOpen u := isOpen_interior.preimage continuous_subtype_val
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
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
⊢ ∃ (v : Set H), Membership.mem (γ := Set (Set H)) {s : Set H | IsClopen s} v ∧ x ∈ v ∧ v ⊆ U
have 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
Tactic: lift x to s using interior_subset xs
Cleared hypotheses: x, memU, xs
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (hypothesis)
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
⊢ ∃ (v : Set H), Membership.mem (γ := Set (Set H)) {s : Set H | IsClopen s} v ∧ (↑x : H) ∈ v ∧ v ⊆ U
have this : CompactSpace.{u_3} (↑s : Type u_3)
Tactic: haveI : CompactSpace s := isCompact_iff_compactSpace.1 comp
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
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 H), Membership.mem (γ := Set (Set H)) {s : Set H | IsClopen s} v ∧ (↑x : H) ∈ v ∧ v ⊆ U
have 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
Tactic: obtain ⟨V : Set s, VisClopen, Vx, V_sub⟩ := compact_exists_isClopen_in_isOpen u_open_in_s xs
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
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)
have refine : IsOpen[inst] (Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V)
Tactic: refine ⟨comp.isClosed.isClosedEmbedding_subtypeVal.isClosed_iff_image_isClosed.1 VisClopen.1,
      ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (hypothesis)
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
⊢ IsOpen[inst] (Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V)
have 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))
Tactic: have : ((↑) : u → H) = ((↑) : s → H) ∘ ((↑) : u → s) := rfl
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (hypothesis)
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))
⊢ IsOpen[inst] (Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V)
have f0 : 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
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
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)
have refine : IsOpen[inst] (range fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H))
Tactic: refine ⟨f0, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
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
have rw : s ∩ interior s = interior s
Tactic: rw [this, Set.range_comp, Subtype.range_coe, Subtype.image_preimage_coe]
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (hypothesis)
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)
⊢ IsOpen[inst] (range fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H))
have this₁ : (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
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
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] (range fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H))
have rw : IsOpen[inst] (interior s)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (hypothesis)
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)
⊢ IsOpen[inst] (Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V)
have f1 : 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
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (hypothesis)
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)
f1 : IsOpenEmbedding (Y := H) fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)
⊢ IsOpen[inst] (Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V)
have f2 : IsOpen[instTopologicalSpaceSubtype] v
Tactic: have f2 : IsOpen v := VisClopen.2.preimage continuous_subtype_val
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
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)
f1 : IsOpenEmbedding (Y := H) fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)
f2 : IsOpen[instTopologicalSpaceSubtype] v
⊢ Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V = (fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)) '' v
have rw : Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V =
  Subtype.val (p := fun (x : H) ↦ x ∈ s) ∘ Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u) '' v
Tactic: rw [this, image_comp, Subtype.image_preimage_coe, inter_eq_self_of_subset_right V_sub]
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
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)
f1 : IsOpenEmbedding (Y := H) fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)
f2 : IsOpen[instTopologicalSpaceSubtype] v
rw :
  Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V =
    Subtype.val (p := fun (x : H) ↦ x ∈ s) ∘ Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u) '' v
⊢ Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V = (fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)) '' v
have rw₁ : Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V =
  Subtype.val (p := fun (x : H) ↦ x ∈ s) '' Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u) '' v
Tactic: rw [this, image_comp, Subtype.image_preimage_coe, inter_eq_self_of_subset_right V_sub]
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
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)
f1 : IsOpenEmbedding (Y := H) fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)
f2 : IsOpen[instTopologicalSpaceSubtype] v
rw :
  Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V =
    Subtype.val (p := fun (x : H) ↦ x ∈ s) ∘ Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u) '' v
rw₁ :
  Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V =
    Subtype.val (p := fun (x : H) ↦ x ∈ s) '' Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u) '' v
⊢ Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V = (fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)) '' v
have rw₂ : Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V = Subtype.val (p := fun (x : H) ↦ x ∈ s) '' (u ∩ V)
Tactic: rw [this, image_comp, Subtype.image_preimage_coe, inter_eq_self_of_subset_right V_sub]
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
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)
f1 : IsOpenEmbedding (Y := H) fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)
f2 : IsOpen[instTopologicalSpaceSubtype] v
rw :
  Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V =
    Subtype.val (p := fun (x : H) ↦ x ∈ s) ∘ Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u) '' v
rw₁ :
  Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V =
    Subtype.val (p := fun (x : H) ↦ x ∈ s) '' Subtype.val (p := fun (x : (↑s : Type u_3)) ↦ x ∈ u) '' v
rw₂ : Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V = Subtype.val (p := fun (x : H) ↦ x ∈ s) '' (u ∩ V)
⊢ Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V = (fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)) '' v
have rw₃ : Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V = Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V
Tactic: rw [this, image_comp, Subtype.image_preimage_coe, inter_eq_self_of_subset_right V_sub]