awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
f1 : IsOpenEmbedding (Y := H) fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)
⊢ IsOpen[instTopologicalSpaceSubtype] v

Tactic:
have f2 : IsOpen v := VisClopen.2.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
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)
rw₃ rw₄ : Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V = Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V
⊢ Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V = (fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)) '' v

Tactic:
rw [this, image_comp, Subtype.image_preimage_coe, inter_eq_self_of_subset_right V_sub]

Premises used: Subtype.image_preimage_coe, Set.inter_eq_self_of_subset_right, Set.image_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_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

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]
-- 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)
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
rw : IsOpen[inst] ((fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)) '' v)
⊢ IsOpen[inst] (Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V)

Tactic:
rw [f3]
-- 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)
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] ((fun (x : (↑u : Type u_3)) ↦ (↑(↑x : (↑s : Type u_3)) : H)) '' v)

Tactic:
apply f1.isOpenMap v f2

Premises used: Topology.IsOpenEmbedding.isOpenMap
-- 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:
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
-- 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
VisClopen' : IsClopen (Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V)
⊢ (↑x : H) ∈ Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V

Tactic:
simp [Vx]
-- 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
VisClopen' : IsClopen (Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V)
⊢ Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V ⊆ s

Tactic:
simp
-- 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
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
right : Subtype.val (p := fun (x : H) ↦ x ∈ s) '' V ⊆ U
⊢ ∃ (v : Set H), Membership.mem (γ := Set (Set H)) {s : Set H | IsClopen s} v ∧ (↑x : H) ∈ v ∧ v ⊆ U

Tactic:
use (↑) '' V, VisClopen', by simp [Vx], Subset.trans (by simp) sU

Premises used: Set.Subset.trans
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
H : Type u_3
inst : TopologicalSpace H
inst_1 : LocallyCompactSpace H
inst_2 : T2Space H
mp : TotallyDisconnectedSpace H → TotallySeparatedSpace H
mpr : TotallySeparatedSpace H → TotallyDisconnectedSpace H
⊢ TotallyDisconnectedSpace H ↔ TotallySeparatedSpace H

Tactic:
constructor
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
H : Type u_3
inst : TopologicalSpace H
inst_1 : LocallyCompactSpace H
inst_2 : T2Space H
h : TotallyDisconnectedSpace H
⊢ TotallySeparatedSpace H

Tactic:
totallySeparatedSpace_of_t0_of_basis_clopen loc_compact_Haus_tot_disc_of_zero_dim

Premises used: loc_compact_Haus_tot_disc_of_zero_dim, totallySeparatedSpace_of_t0_of_basis_clopen
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
H : Type u_3
inst : TopologicalSpace H
inst_1 : LocallyCompactSpace H
inst_2 : T2Space H
h : TotallyDisconnectedSpace H
⊢ TotallySeparatedSpace H

Tactic:
exact totallySeparatedSpace_of_t0_of_basis_clopen loc_compact_Haus_tot_disc_of_zero_dim

Premises used: loc_compact_Haus_tot_disc_of_zero_dim, totallySeparatedSpace_of_t0_of_basis_clopen
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
H : Type u_3
inst : TopologicalSpace H
inst_1 : LocallyCompactSpace H
inst_2 : T2Space H
⊢ TotallySeparatedSpace H → TotallyDisconnectedSpace H

Tactic:
apply TotallySeparatedSpace.totallyDisconnectedSpace

Premises used: TotallySeparatedSpace.totallyDisconnectedSpace
-- Module: Mathlib.Topology.Separation.Profinite
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
H : Type u_3
inst_1 : TopologicalSpace H
inst_2 : LocallyCompactSpace H
inst_3 : T2Space H
inst_4 : TotallyDisconnectedSpace H
⊢ TotallySeparatedSpace H

Tactic:
loc_compact_t2_tot_disc_iff_tot_sep.mp inferInstance

Premises used: inferInstance, loc_compact_t2_tot_disc_iff_tot_sep, Iff.mp
-- Module: Mathlib.Topology.Separation.Profinite
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
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
⊢ ∃ (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)

Premises used: compact_exists_isClopen_in_isOpen, Subtype.property
-- Module: Mathlib.Topology.Separation.Profinite
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
⊢ 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⟩
-- Module: Mathlib.Topology.Separation.Profinite
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
choose : ∀ (I : Finset (↑Z : Type u_4)) (hI : Z ⊆ ⋃ i ∈ I, V i), ∃ (C : Set X), IsClopen C ∧ Z ⊆ C ∧ C ⊆ U
⊢ ∃ (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

Premises used: IsCompact.elim_finite_subcover, IsClopen.isOpen, And.left, IsClosed.isCompact
-- Module: Mathlib.Topology.Separation.Profinite
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
I : Finset (↑Z : Type u_4)
hI : Z ⊆ ⋃ i ∈ I, V i
⊢ ⋃ i ∈ I, V i ⊆ U

Tactic:
simp_all
-- Module: Mathlib.Topology.Separation.Profinite
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
I : Finset (↑Z : Type u_4)
hI : Z ⊆ ⋃ i ∈ I, V i
⊢ ∃ (C : Set X), IsClopen C ∧ Z ⊆ C ∧ C ⊆ U

Tactic:
exact ⟨⋃ (i ∈ I), V i, I.finite_toSet.isClopen_biUnion (fun i _ ↦ (hV i).1), hI, by simp_all⟩
-- Module: Mathlib.Topology.Separation.Profinite
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
⊢ PairwiseDisjoint (ι := α) univ (Z ∘ (⇑e : (a : α) → β))

Tactic:
simpa [← e.injective.injOn.pairwiseDisjoint_image]

Premises used: Function.Injective.injOn, Set.InjOn.pairwiseDisjoint_image, Equiv.injective
-- Module: Mathlib.Topology.Separation.Profinite
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
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
⊢ ∃ (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])

Premises used: DFunLike.coe
-- Module: Mathlib.Topology.Separation.Profinite
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
i : β
⊢ Z i ⊆ (C ∘ (⇑e.symm : (a : β) → α)) i

Tactic:
simpa using h2 (e.symm i)

Premises used: Equiv.symm, DFunLike.coe
-- Module: Mathlib.Topology.Separation.Profinite
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
i : β
⊢ (C ∘ (⇑e.symm : (a : β) → α)) i ⊆ D i

Tactic:
simpa using h3 (e.symm i)

Premises used: Equiv.symm, DFunLike.coe
-- Module: Mathlib.Topology.Separation.Profinite
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
⊢ PairwiseDisjoint (ι := β) univ (C ∘ (⇑e.symm : (a : β) → α))

Tactic:
simpa [← e.symm.injective.injOn.pairwiseDisjoint_image]

Premises used: Function.Injective.injOn, Set.InjOn.pairwiseDisjoint_image, Equiv.injective, Equiv.symm
-- Module: Mathlib.Topology.Separation.Profinite
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
of_equiv : Subset.{u_4} (α := Set X) (⋃ (i : β), D i) (⋃ (i : β), (C ∘ (⇑e.symm : (a : β) → α)) i)
⊢ ∃ (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:
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]⟩