awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
f2 : IsOpen[instTopologicalSpaceSubtype] v
⊢ IsOpen[inst] (Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V)
have f3 : Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V = (fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)) '' v
Tactic: have f3 : ((↑) : s → H) '' V = ((↑) : u → H) '' v := by
      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
f3 : Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V = (fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)) '' v
⊢ IsOpen[inst] (Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V)
have rw : IsOpen[inst] ((fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)) '' v)
Tactic: rw [f3]
-- 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 H), Membership.mem (γ := Set (Set H)) {s : Set H | IsClopen s} v ∧ (↑x : H) ∈ v ∧ v ⊆ U
have VisClopen' : IsClopen (Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V)
Tactic: have VisClopen' : IsClopen (((↑) : s → H) '' V) := by
    refine ⟨comp.isClosed.isClosedEmbedding_subtypeVal.isClosed_iff_image_isClosed.1 VisClopen.1,
      ?_⟩
    let v : Set u := ((↑) : u → s) ⁻¹' V
    have : ((↑) : u → H) = ((↑) : s → H) ∘ ((↑) : u → s) := rfl
    have f0 : IsEmbedding ((↑) : u → H) := IsEmbedding.subtypeVal.comp IsEmbedding.subtypeVal
    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
    have f2 : IsOpen v := VisClopen.2.preimage continuous_subtype_val
    have f3 : ((↑) : s → H) '' V = ((↑) : u → H) '' v := by
      rw [this, image_comp, Subtype.image_preimage_coe, inter_eq_self_of_subset_right V_sub]
    rw [f3]
    apply f1.isOpenMap v f2
-- 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
VisClopen' : IsClopen (Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V)
w : Set H
⊢ ∃ (v : Set H), Membership.mem (γ := Set (Set H)) {s : Set H | IsClopen s} v ∧ (↑x : H) ∈ v ∧ v ⊆ U
have left : Membership.mem (γ := Set (Set H)) {s : Set H | IsClopen s} (Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V)
Tactic: use (↑) '' V, VisClopen', by simp [Vx], Subset.trans (by simp) sU
-- 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
VisClopen' : IsClopen (Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V)
w : Set H
left : Membership.mem (γ := Set (Set H)) {s : Set H | IsClopen s} (Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V)
⊢ ∃ (v : Set H), Membership.mem (γ := Set (Set H)) {s : Set H | IsClopen s} v ∧ (↑x : H) ∈ v ∧ v ⊆ U
have left₁ : (↑x : H) ∈ Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V
Tactic: use (↑) '' V, VisClopen', by simp [Vx], Subset.trans (by simp) sU
-- 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
VisClopen' : IsClopen (Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V)
w : Set H
left : Membership.mem (γ := Set (Set H)) {s : Set H | IsClopen s} (Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V)
left₁ : (↑x : H) ∈ Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V
⊢ ∃ (v : Set H), Membership.mem (γ := Set (Set H)) {s : Set H | IsClopen s} v ∧ (↑x : H) ∈ v ∧ v ⊆ U
have right : Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V ⊆ U
Tactic: use (↑) '' V, VisClopen', by simp [Vx], Subset.trans (by simp) sU
-- 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
⊢ TotallyDisconnectedSpace H ↔ TotallySeparatedSpace H
have mp : TotallyDisconnectedSpace H → TotallySeparatedSpace H
Tactic: constructor
-- 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
mp : TotallyDisconnectedSpace H → TotallySeparatedSpace H
⊢ TotallyDisconnectedSpace H ↔ TotallySeparatedSpace H
have mpr : TotallySeparatedSpace H → TotallyDisconnectedSpace H
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
Goal:
X : Type u_4
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
Z U : Set X
hZ : IsClosed[inst] Z
hU : IsOpen[inst] U
hZU : Z ⊆ U
⊢ ∃ (C : Set X), IsClopen C ∧ Z ⊆ C ∧ C ⊆ U
have choose : ∀ (V : (z : (↑Z : Type u_4)) → Set X) (hV : ∀ (z : (↑Z : Type u_4)), IsClopen (V z) ∧ (↑z : X) ∈ V z ∧ V z ⊆ U),
  ∃ (C : Set X), IsClopen C ∧ Z ⊆ C ∧ C ⊆ U
Tactic: choose V hV using fun (z : Z) ↦ compact_exists_isClopen_in_isOpen hU (hZU z.property)
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (hypothesis)
Goal:
X : Type u_4
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
Z U : Set X
hZ : IsClosed[inst] Z
hU : IsOpen[inst] U
hZU : Z ⊆ U
V : (z : (↑Z : Type u_4)) → Set X
hV : ∀ (z : (↑Z : Type u_4)), IsClopen (V z) ∧ (↑z : X) ∈ V z ∧ V z ⊆ U
⊢ ∃ (C : Set X), IsClopen C ∧ Z ⊆ C ∧ C ⊆ U
have V_cover : Z ⊆ ⋃ (z : (↑Z : Type u_4)), V z
Tactic: have V_cover : Z ⊆ ⋃ z, V z := fun z hz ↦ mem_iUnion.mpr ⟨⟨z, hz⟩, (hV ⟨z, hz⟩).2.1⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
Goal:
X : Type u_4
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
Z U : Set X
hZ : IsClosed[inst] Z
hU : IsOpen[inst] U
hZU : Z ⊆ U
V : (z : (↑Z : Type u_4)) → Set X
hV : ∀ (z : (↑Z : Type u_4)), IsClopen (V z) ∧ (↑z : X) ∈ V z ∧ V z ⊆ U
V_cover : Z ⊆ ⋃ (z : (↑Z : Type u_4)), V z
⊢ ∃ (C : Set X), IsClopen C ∧ Z ⊆ C ∧ C ⊆ U
have choose : ∀ (I : Finset (↑Z : Type u_4)) (hI : Z ⊆ ⋃ i ∈ I, V i), ∃ (C : Set X), IsClopen C ∧ Z ⊆ C ∧ C ⊆ U
Tactic: choose I hI using hZ.isCompact.elim_finite_subcover V (fun z ↦ (hV z).1.isOpen) V_cover
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
Goal:
X : Type u_4
I : Type u_5
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
inst_4 : Finite I
α β : Type u_5
e : α ≃ β
IH :
  ∀ {Z D : α → Set X} (Z_closed : ∀ (i : α), IsClosed[inst] (Z i)) (D_clopen : ∀ (i : α), IsClopen (D i))
    (Z_subset_D : ∀ (i : α), Z i ⊆ D i) (Z_disj : PairwiseDisjoint univ Z),
    ∃ (C : α → Set X),
      (∀ (i : α), IsClopen (C i)) ∧
        (∀ (i : α), Z i ⊆ C i) ∧
          (∀ (i : α), C i ⊆ D i) ∧ Subset.{u_4} (α := Set X) (⋃ (i : α), D i) (⋃ (i : α), C i) ∧ PairwiseDisjoint univ C
Z D : β → Set X
Z_closed : ∀ (i : β), IsClosed[inst] (Z i)
D_clopen : ∀ (i : β), IsClopen (D i)
Z_subset_D : ∀ (i : β), Z i ⊆ D i
Z_disj : PairwiseDisjoint univ Z
⊢ ∃ (C : β → Set X),
    (∀ (i : β), IsClopen (C i)) ∧
      (∀ (i : β), Z i ⊆ C i) ∧
        (∀ (i : β), C i ⊆ D i) ∧ Subset.{u_4} (α := Set X) (⋃ (i : β), D i) (⋃ (i : β), C i) ∧ PairwiseDisjoint univ C
have of_equiv : ∀ (C : α → Set X) (h1 : ∀ (i : α), IsClopen (C i)) (h2 : ∀ (i : α), (Z ∘ (⇑e : (a : α) → β)) i ⊆ C i)
  (h3 : ∀ (i : α), C i ⊆ (D ∘ (⇑e : (a : α) → β)) i)
  (h4 : Subset.{u_4} (α := Set X) (⋃ (i : α), (D ∘ (⇑e : (a : α) → β)) i) (⋃ (i : α), C i))
  (h5 : PairwiseDisjoint univ C),
  ∃ (C : β → Set X),
    (∀ (i : β), IsClopen (C i)) ∧
      (∀ (i : β), Z i ⊆ C i) ∧
        (∀ (i : β), C i ⊆ D i) ∧ Subset.{u_4} (α := Set X) (⋃ (i : β), D i) (⋃ (i : β), C i) ∧ PairwiseDisjoint univ C
Tactic: obtain ⟨C, h1, h2, h3, h4, h5⟩ := IH (Z := Z ∘ e) (D := D ∘ e)
      (fun i ↦ Z_closed (e i)) (fun i ↦ D_clopen (e i))
      (fun i ↦ Z_subset_D (e i)) (by simpa [← e.injective.injOn.pairwiseDisjoint_image])
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
Goal:
X : Type u_4
I : Type u_5
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
inst_4 : Finite I
α β : Type u_5
e : α ≃ β
IH :
  ∀ {Z D : α → Set X} (Z_closed : ∀ (i : α), IsClosed[inst] (Z i)) (D_clopen : ∀ (i : α), IsClopen (D i))
    (Z_subset_D : ∀ (i : α), Z i ⊆ D i) (Z_disj : PairwiseDisjoint univ Z),
    ∃ (C : α → Set X),
      (∀ (i : α), IsClopen (C i)) ∧
        (∀ (i : α), Z i ⊆ C i) ∧
          (∀ (i : α), C i ⊆ D i) ∧ Subset.{u_4} (α := Set X) (⋃ (i : α), D i) (⋃ (i : α), C i) ∧ PairwiseDisjoint univ C
Z D : β → Set X
Z_closed : ∀ (i : β), IsClosed[inst] (Z i)
D_clopen : ∀ (i : β), IsClopen (D i)
Z_subset_D : ∀ (i : β), Z i ⊆ D i
Z_disj : PairwiseDisjoint univ Z
C : α → Set X
h1 : ∀ (i : α), IsClopen (C i)
h2 : ∀ (i : α), (Z ∘ (⇑e : (a : α) → β)) i ⊆ C i
h3 : ∀ (i : α), C i ⊆ (D ∘ (⇑e : (a : α) → β)) i
h4 : Subset.{u_4} (α := Set X) (⋃ (i : α), (D ∘ (⇑e : (a : α) → β)) i) (⋃ (i : α), C i)
h5 : PairwiseDisjoint univ C
⊢ ∃ (C : β → Set X),
    (∀ (i : β), IsClopen (C i)) ∧
      (∀ (i : β), Z i ⊆ C i) ∧
        (∀ (i : β), C i ⊆ D i) ∧ Subset.{u_4} (α := Set X) (⋃ (i : β), D i) (⋃ (i : β), C i) ∧ PairwiseDisjoint univ C
have of_equiv : Subset.{u_4} (α := Set X) (⋃ (i : β), D i) (⋃ (i : β), (C ∘ (⇑e.symm : (a : β) → α)) i)
Tactic: refine ⟨C ∘ e.symm, fun i ↦ h1 (e.symm i), fun i ↦ by simpa using h2 (e.symm i),
      fun i ↦ by simpa using h3 (e.symm i), ?_,
      by simpa [← e.symm.injective.injOn.pairwiseDisjoint_image]⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (hypothesis)
Goal:
X : Type u_4
I : Type u_5
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
inst_4 : Finite I
α β : Type u_5
e : α ≃ β
IH :
  ∀ {Z D : α → Set X} (Z_closed : ∀ (i : α), IsClosed[inst] (Z i)) (D_clopen : ∀ (i : α), IsClopen (D i))
    (Z_subset_D : ∀ (i : α), Z i ⊆ D i) (Z_disj : PairwiseDisjoint univ Z),
    ∃ (C : α → Set X),
      (∀ (i : α), IsClopen (C i)) ∧
        (∀ (i : α), Z i ⊆ C i) ∧
          (∀ (i : α), C i ⊆ D i) ∧ Subset.{u_4} (α := Set X) (⋃ (i : α), D i) (⋃ (i : α), C i) ∧ PairwiseDisjoint univ C
Z D : β → Set X
Z_closed : ∀ (i : β), IsClosed[inst] (Z i)
D_clopen : ∀ (i : β), IsClopen (D i)
Z_subset_D : ∀ (i : β), Z i ⊆ D i
Z_disj : PairwiseDisjoint univ Z
C : α → Set X
h1 : ∀ (i : α), IsClopen (C i)
h2 : ∀ (i : α), (Z ∘ (⇑e : (a : α) → β)) i ⊆ C i
h3 : ∀ (i : α), C i ⊆ (D ∘ (⇑e : (a : α) → β)) i
h4 : Subset.{u_4} (α := Set X) (⋃ (i : α), (D ∘ (⇑e : (a : α) → β)) i) (⋃ (i : α), C i)
h5 : PairwiseDisjoint univ C
⊢ Subset.{u_4} (α := Set X) (⋃ (i : β), D i) (⋃ (i : β), (C ∘ (⇑e.symm : (a : β) → α)) i)
have h4₁ : ∀ (i : α), D ((e : (a : α) → β) i) ⊆ ⋃ (i : α), C i
Tactic: simp only [Function.comp_apply, iUnion_subset_iff] at h4
Cleared hypotheses: h4
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (hypothesis)
Goal:
X : Type u_4
I_1 : Type u_5
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
inst_4 : Finite I_1
I : Type u_5
inst_5 : Fintype I
IH :
  ∀ {Z D : I → Set X} (Z_closed : ∀ (i : I), IsClosed[inst] (Z i)) (D_clopen : ∀ (i : I), IsClopen (D i))
    (Z_subset_D : ∀ (i : I), Z i ⊆ D i) (Z_disj : PairwiseDisjoint univ Z),
    ∃ (C : I → Set X),
      (∀ (i : I), IsClopen (C i)) ∧
        (∀ (i : I), Z i ⊆ C i) ∧
          (∀ (i : I), C i ⊆ D i) ∧ Subset.{u_4} (α := Set X) (⋃ (i : I), D i) (⋃ (i : I), C i) ∧ PairwiseDisjoint univ C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : PairwiseDisjoint univ Z
Z' : I → Set X := fun (i : I) ↦ Z (some i)
⊢ ∃ (C : Option I → Set X),
    (∀ (i : Option I), IsClopen (C i)) ∧
      (∀ (i : Option I), Z i ⊆ C i) ∧
        (∀ (i : Option I), C i ⊆ D i) ∧
          Subset.{u_4} (α := Set X) (⋃ (i : Option I), D i) (⋃ (i : Option I), C i) ∧ PairwiseDisjoint univ C
have Z'_closed : ∀ (i : I), IsClosed[inst] (Z (some i))
Tactic: have Z'_closed (i : I) : IsClosed (Z (some i)) := Z_closed (some i)
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
Goal:
X : Type u_4
I_1 : Type u_5
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
inst_4 : Finite I_1
I : Type u_5
inst_5 : Fintype I
IH :
  ∀ {Z D : I → Set X} (Z_closed : ∀ (i : I), IsClosed[inst] (Z i)) (D_clopen : ∀ (i : I), IsClopen (D i))
    (Z_subset_D : ∀ (i : I), Z i ⊆ D i) (Z_disj : PairwiseDisjoint univ Z),
    ∃ (C : I → Set X),
      (∀ (i : I), IsClopen (C i)) ∧
        (∀ (i : I), Z i ⊆ C i) ∧
          (∀ (i : I), C i ⊆ D i) ∧ Subset.{u_4} (α := Set X) (⋃ (i : I), D i) (⋃ (i : I), C i) ∧ PairwiseDisjoint univ C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : PairwiseDisjoint univ Z
Z' : I → Set X := fun (i : I) ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst] (Z (some i))
⊢ PairwiseDisjoint univ (Z ∘ some)
have rw : PairwiseDisjoint (some '' univ) Z
Tactic: rw [← (Option.some_injective _).injOn.pairwiseDisjoint_image]
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (hypothesis)
Goal:
X : Type u_4
I_1 : Type u_5
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
inst_4 : Finite I_1
I : Type u_5
inst_5 : Fintype I
IH :
  ∀ {Z D : I → Set X} (Z_closed : ∀ (i : I), IsClosed[inst] (Z i)) (D_clopen : ∀ (i : I), IsClopen (D i))
    (Z_subset_D : ∀ (i : I), Z i ⊆ D i) (Z_disj : PairwiseDisjoint univ Z),
    ∃ (C : I → Set X),
      (∀ (i : I), IsClopen (C i)) ∧
        (∀ (i : I), Z i ⊆ C i) ∧
          (∀ (i : I), C i ⊆ D i) ∧ Subset.{u_4} (α := Set X) (⋃ (i : I), D i) (⋃ (i : I), C i) ∧ PairwiseDisjoint univ C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : PairwiseDisjoint univ Z
Z' : I → Set X := fun (i : I) ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst] (Z (some i))
⊢ ∃ (C : Option I → Set X),
    (∀ (i : Option I), IsClopen (C i)) ∧
      (∀ (i : Option I), Z i ⊆ C i) ∧
        (∀ (i : Option I), C i ⊆ D i) ∧
          Subset.{u_4} (α := Set X) (⋃ (i : Option I), D i) (⋃ (i : Option I), C i) ∧ PairwiseDisjoint univ C
have Z'_disj : PairwiseDisjoint univ (Z ∘ some)
Tactic: have Z'_disj : univ.PairwiseDisjoint (Z ∘ some) := by
      rw [← (Option.some_injective _).injOn.pairwiseDisjoint_image]
      exact PairwiseDisjoint.subset Z_disj (by simp)
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (hypothesis)
Goal:
X : Type u_4
I_1 : Type u_5
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
inst_4 : Finite I_1
I : Type u_5
inst_5 : Fintype I
IH :
  ∀ {Z D : I → Set X} (Z_closed : ∀ (i : I), IsClosed[inst] (Z i)) (D_clopen : ∀ (i : I), IsClopen (D i))
    (Z_subset_D : ∀ (i : I), Z i ⊆ D i) (Z_disj : PairwiseDisjoint univ Z),
    ∃ (C : I → Set X),
      (∀ (i : I), IsClopen (C i)) ∧
        (∀ (i : I), Z i ⊆ C i) ∧
          (∀ (i : I), C i ⊆ D i) ∧ Subset.{u_4} (α := Set X) (⋃ (i : I), D i) (⋃ (i : I), C i) ∧ PairwiseDisjoint univ C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : PairwiseDisjoint univ Z
Z' : I → Set X := fun (i : I) ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst] (Z (some i))
Z'_disj : PairwiseDisjoint univ (Z ∘ some)
U : Set X := D none \ ⋃ (i : I), Z (some i)
⊢ ∃ (C : Option I → Set X),
    (∀ (i : Option I), IsClopen (C i)) ∧
      (∀ (i : Option I), Z i ⊆ C i) ∧
        (∀ (i : Option I), C i ⊆ D i) ∧
          Subset.{u_4} (α := Set X) (⋃ (i : Option I), D i) (⋃ (i : Option I), C i) ∧ PairwiseDisjoint univ C
have U_open : IsOpen[inst] U
Tactic: have U_open : IsOpen U := IsOpen.sdiff (D_clopen none).2
      (isClosed_iUnion_of_finite (fun i ↦ Z_closed (some i)))
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
Goal:
X : Type u_4
I_1 : Type u_5
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
inst_4 : Finite I_1
I : Type u_5
inst_5 : Fintype I
IH :
  ∀ {Z D : I → Set X} (Z_closed : ∀ (i : I), IsClosed[inst] (Z i)) (D_clopen : ∀ (i : I), IsClopen (D i))
    (Z_subset_D : ∀ (i : I), Z i ⊆ D i) (Z_disj : PairwiseDisjoint univ Z),
    ∃ (C : I → Set X),
      (∀ (i : I), IsClopen (C i)) ∧
        (∀ (i : I), Z i ⊆ C i) ∧
          (∀ (i : I), C i ⊆ D i) ∧ Subset.{u_4} (α := Set X) (⋃ (i : I), D i) (⋃ (i : I), C i) ∧ PairwiseDisjoint univ C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : PairwiseDisjoint univ Z
Z' : I → Set X := fun (i : I) ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst] (Z (some i))
Z'_disj : PairwiseDisjoint univ (Z ∘ some)
U : Set X := D none \ ⋃ (i : I), Z (some i)
U_open : IsOpen[inst] U
⊢ Z none ⊆ U
have rw : Z none ⊆ D none ∧ Disjoint (Z none) (⋃ (i : I), Z (some i))
Tactic: rw [subset_diff]
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
Goal:
X : Type u_4
I_1 : Type u_5
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
inst_4 : Finite I_1
I : Type u_5
inst_5 : Fintype I
IH :
  ∀ {Z D : I → Set X} (Z_closed : ∀ (i : I), IsClosed[inst] (Z i)) (D_clopen : ∀ (i : I), IsClopen (D i))
    (Z_subset_D : ∀ (i : I), Z i ⊆ D i) (Z_disj : PairwiseDisjoint univ Z),
    ∃ (C : I → Set X),
      (∀ (i : I), IsClopen (C i)) ∧
        (∀ (i : I), Z i ⊆ C i) ∧
          (∀ (i : I), C i ⊆ D i) ∧ Subset.{u_4} (α := Set X) (⋃ (i : I), D i) (⋃ (i : I), C i) ∧ PairwiseDisjoint univ C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : PairwiseDisjoint univ Z
Z' : I → Set X := fun (i : I) ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst] (Z (some i))
Z'_disj : PairwiseDisjoint univ (Z ∘ some)
U : Set X := D none \ ⋃ (i : I), Z (some i)
U_open : IsOpen[inst] U
i : I
⊢ Disjoint (Z none) (Z (some i))
have a : Membership.mem (γ := Set (Option I)) univ none
Tactic: apply Z_disj
-- Lean 4 proof step from Mathlib.Topology.Separation.Profinite (goal)
Goal:
X : Type u_4
I_1 : Type u_5
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
inst_4 : Finite I_1
I : Type u_5
inst_5 : Fintype I
IH :
  ∀ {Z D : I → Set X} (Z_closed : ∀ (i : I), IsClosed[inst] (Z i)) (D_clopen : ∀ (i : I), IsClopen (D i))
    (Z_subset_D : ∀ (i : I), Z i ⊆ D i) (Z_disj : PairwiseDisjoint univ Z),
    ∃ (C : I → Set X),
      (∀ (i : I), IsClopen (C i)) ∧
        (∀ (i : I), Z i ⊆ C i) ∧
          (∀ (i : I), C i ⊆ D i) ∧ Subset.{u_4} (α := Set X) (⋃ (i : I), D i) (⋃ (i : I), C i) ∧ PairwiseDisjoint univ C
Z D : Option I → Set X
Z_closed : ∀ (i : Option I), IsClosed[inst] (Z i)
D_clopen : ∀ (i : Option I), IsClopen (D i)
Z_subset_D : ∀ (i : Option I), Z i ⊆ D i
Z_disj : PairwiseDisjoint univ Z
Z' : I → Set X := fun (i : I) ↦ Z (some i)
Z'_closed : ∀ (i : I), IsClosed[inst] (Z (some i))
Z'_disj : PairwiseDisjoint univ (Z ∘ some)
U : Set X := D none \ ⋃ (i : I), Z (some i)
U_open : IsOpen[inst] U
i : I
a : Membership.mem (γ := Set (Option I)) univ none
⊢ Disjoint (Z none) (Z (some i))
have a₁ : Membership.mem (γ := Set (Option I)) univ (some i)
Tactic: apply Z_disj