awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α), D ((e : (a : α) → β) i) ⊆ ⋃ (i : α), C i

Tactic:
simp only [Function.comp_apply, iUnion_subset_iff] at h4

Premises used: Set.iUnion_subset_iff, Function.comp_apply
-- 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
h5 : PairwiseDisjoint univ C
h4 : ∀ (i : α), D ((e : (a : α) → β) i) ⊆ ⋃ (i : α), C i
⊢ Subset.{u_4} (α := Set X) (⋃ (i : β), D i) (⋃ (i : β), (C ∘ (⇑e.symm : (a : β) → α)) i)

Tactic:
simpa [e.symm.surjective.iUnion_comp C] using fun i ↦ h4 (e.symm i)

Premises used: Function.Surjective.iUnion_comp, Equiv.surjective, 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
Z D : PEmpty.{u_5 + 1} → Set X
Z_closed : ∀ (i : PEmpty.{u_5 + 1}), IsClosed[inst] (Z i)
D_clopen : ∀ (i : PEmpty.{u_5 + 1}), IsClopen (D i)
Z_subset_D : ∀ (i : PEmpty.{u_5 + 1}), Z i ⊆ D i
Z_disj : PairwiseDisjoint univ Z
⊢ ∀ (i : PEmpty.{u_5 + 1}), IsClopen.{u_4} (X := X) ((fun (x : PEmpty.{u_5 + 1}) ↦ (univ : Set X)) i)

Tactic:
simp
-- 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
Z D : PEmpty.{u_5 + 1} → Set X
Z_closed : ∀ (i : PEmpty.{u_5 + 1}), IsClosed[inst] (Z i)
D_clopen : ∀ (i : PEmpty.{u_5 + 1}), IsClopen (D i)
Z_subset_D : ∀ (i : PEmpty.{u_5 + 1}), Z i ⊆ D i
Z_disj : PairwiseDisjoint univ Z
⊢ ∀ (i : PEmpty.{u_5 + 1}), Z i ⊆ (fun (x : PEmpty.{u_5 + 1}) ↦ (univ : Set X)) i

Tactic:
simp
-- 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
Z D : PEmpty.{u_5 + 1} → Set X
Z_closed : ∀ (i : PEmpty.{u_5 + 1}), IsClosed[inst] (Z i)
D_clopen : ∀ (i : PEmpty.{u_5 + 1}), IsClopen (D i)
Z_subset_D : ∀ (i : PEmpty.{u_5 + 1}), Z i ⊆ D i
Z_disj : PairwiseDisjoint univ Z
⊢ ∀ (i : PEmpty.{u_5 + 1}), (fun (x : PEmpty.{u_5 + 1}) ↦ (univ : Set X)) i ⊆ D i

Tactic:
simp
-- 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
Z D : PEmpty.{u_5 + 1} → Set X
Z_closed : ∀ (i : PEmpty.{u_5 + 1}), IsClosed[inst] (Z i)
D_clopen : ∀ (i : PEmpty.{u_5 + 1}), IsClopen (D i)
Z_subset_D : ∀ (i : PEmpty.{u_5 + 1}), Z i ⊆ D i
Z_disj : PairwiseDisjoint univ Z
⊢ Subset.{u_4} (α := Set X) (⋃ (i : PEmpty.{u_5 + 1}), D i)
    (⋃ (i : PEmpty.{u_5 + 1}), (fun (x : PEmpty.{u_5 + 1}) ↦ (univ : Set X)) i)

Tactic:
simp
-- 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
Z D : PEmpty.{u_5 + 1} → Set X
Z_closed : ∀ (i : PEmpty.{u_5 + 1}), IsClosed[inst] (Z i)
D_clopen : ∀ (i : PEmpty.{u_5 + 1}), IsClopen (D i)
Z_subset_D : ∀ (i : PEmpty.{u_5 + 1}), Z i ⊆ D i
Z_disj : PairwiseDisjoint univ Z
⊢ ∃ (C : PEmpty.{u_5 + 1} → Set X),
    (∀ (i : PEmpty.{u_5 + 1}), IsClopen (C i)) ∧
      (∀ (i : PEmpty.{u_5 + 1}), Z i ⊆ C i) ∧
        (∀ (i : PEmpty.{u_5 + 1}), C i ⊆ D i) ∧
          Subset.{u_4} (α := Set X) (⋃ (i : PEmpty.{u_5 + 1}), D i) (⋃ (i : PEmpty.{u_5 + 1}), C i) ∧
            PairwiseDisjoint univ C

Tactic:
exact ⟨fun _ ↦ univ, by simp, by simp, by simp, by simp, fun i ↦ PEmpty.elim i⟩
-- Module: Mathlib.Topology.Separation.Profinite
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)
⊢ ∀ (i : I), IsClosed[inst] (Z (some i))

Tactic:
have Z'_closed (i : I) : IsClosed (Z (some i)) := Z_closed (some i)
-- Module: Mathlib.Topology.Separation.Profinite
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))
rw : PairwiseDisjoint (some '' univ) Z
⊢ PairwiseDisjoint univ (Z ∘ some)

Tactic:
rw [← (Option.some_injective _).injOn.pairwiseDisjoint_image]

Premises used: Function.Injective.injOn, Set.InjOn.pairwiseDisjoint_image, Option.some_injective
-- Module: Mathlib.Topology.Separation.Profinite
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))
⊢ Subset.{u_5} (α := Set (Option I)) (some '' univ) univ

Tactic:
simp
-- Module: Mathlib.Topology.Separation.Profinite
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 (some '' univ) Z

Tactic:
exact PairwiseDisjoint.subset Z_disj (by simp)

Premises used: Set.PairwiseDisjoint.subset
-- Module: Mathlib.Topology.Separation.Profinite
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)

Tactic:
have Z'_disj : univ.PairwiseDisjoint (Z ∘ some) := by
      rw [← (Option.some_injective _).injOn.pairwiseDisjoint_image]
      exact PairwiseDisjoint.subset Z_disj (by simp)
-- Module: Mathlib.Topology.Separation.Profinite
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)
⊢ 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)))
-- Module: Mathlib.Topology.Separation.Profinite
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
rw : Z none ⊆ D none ∧ Disjoint (Z none) (⋃ (i : I), Z (some i))
⊢ Z none ⊆ U

Tactic:
rw [subset_diff]

Premises used: Set.subset_diff
-- Module: Mathlib.Topology.Separation.Profinite
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
a₁ : Membership.mem (γ := Set (Option I)) univ (some i)
a₂ : none ≠ some i
⊢ Disjoint (Z none) (Z (some i))

Tactic:
apply Z_disj
-- Module: Mathlib.Topology.Separation.Profinite
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
⊢ Membership.mem (γ := Set (Option I)) univ none

Tactic:
simp
-- Module: Mathlib.Topology.Separation.Profinite
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
⊢ Membership.mem (γ := Set (Option I)) univ (some i)

Tactic:
simp
-- Module: Mathlib.Topology.Separation.Profinite
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
⊢ none ≠ some i

Tactic:
simp
-- Module: Mathlib.Topology.Separation.Profinite
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 ⊆ D none ∧ Disjoint (Z none) (⋃ (i : I), Z (some i))

Tactic:
simpa using ⟨Z_subset_D none, fun i ↦ (by apply Z_disj; all_goals simp)⟩
-- Module: Mathlib.Topology.Separation.Profinite
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

Tactic:
have Z0_subset_U : Z none ⊆ U := by
      rw [subset_diff]
      simpa using ⟨Z_subset_D none, fun i ↦ (by apply Z_disj; all_goals simp)⟩
-- Module: Mathlib.Topology.Separation.Profinite
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
Z0_subset_U : Z none ⊆ U
h_option :
  ∀ (V : Set X) (V_clopen : IsClopen V) (Z0_subset_V : Z none ⊆ V) (V_subset_U : V ⊆ U),
    ∃ (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
⊢ ∃ (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

Tactic:
obtain ⟨V, V_clopen, Z0_subset_V, V_subset_U⟩ :=
      exists_clopen_of_closed_subset_open (Z_closed none) U_open Z0_subset_U

Premises used: Option.none, exists_clopen_of_closed_subset_open
-- Module: Mathlib.Topology.Separation.Profinite
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
Z0_subset_U : Z none ⊆ U
V : Set X
V_clopen : IsClopen V
Z0_subset_V : Z none ⊆ V
V_subset_U : V ⊆ U
⊢ V ⊆ D none

Tactic:
have V_subset_D0 : V ⊆ D none := subset_trans V_subset_U diff_subset