awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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_subset_D0 : V ⊆ D none
D' : I → Set X := fun (i : I) ↦ D (some i) \ V
D'_clopen : ∀ (i : I), IsClopen (D' i)
Z'_subset_D' : ∀ (i : I), Z' i ⊆ D' i
C' : I → Set X
C'_clopen : ∀ (i : I), IsClopen (C' i)
Z'_subset_C' : ∀ (i : I), Z (some i) ⊆ C' i
C'_subset_D' : ∀ (i : I), C' i ⊆ D' i
C'_cover_D' : Subset.{u_4} (α := Set X) (⋃ (i : I), D' i) (⋃ (i : I), C' i)
C'_disj : PairwiseDisjoint univ C'
C0 : Set X := D none \ ⋃ (i : I), C' i
this_1 : IsClopen C0
this : Z none ⊆ C0
C : Option I → Set X := fun (i : Option I) ↦ Option.casesOn (motive := fun (x : Option I) ↦ Set X) i C0 C'
x : X
hx : ∃ (i : Option I), x ∈ D i
hx0 : x ∉ C0
hxD : x ∈ D none
hxC' : Membership.mem (γ := Set X) (⋃ (i : I), C' i) x
⊢ ∃ (i : Option I), x ∈ C i
have pos : ∀ (i : I) (hi : x ∈ C' i), ∃ (i : Option I), x ∈ C i
Tactic: obtain ⟨i, hi⟩ := mem_iUnion.mp hxC'
-- 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
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_subset_D0 : V ⊆ D none
D' : I → Set X := fun (i : I) ↦ D (some i) \ V
D'_clopen : ∀ (i : I), IsClopen (D' i)
Z'_subset_D' : ∀ (i : I), Z' i ⊆ D' i
C' : I → Set X
C'_clopen : ∀ (i : I), IsClopen (C' i)
Z'_subset_C' : ∀ (i : I), Z (some i) ⊆ C' i
C'_subset_D' : ∀ (i : I), C' i ⊆ D' i
C'_cover_D' : Subset.{u_4} (α := Set X) (⋃ (i : I), D' i) (⋃ (i : I), C' i)
C'_disj : PairwiseDisjoint univ C'
C0 : Set X := D none \ ⋃ (i : I), C' i
this_1 : IsClopen C0
this : Z none ⊆ C0
C : Option I → Set X := fun (i : Option I) ↦ Option.casesOn (motive := fun (x : Option I) ↦ Set X) i C0 C'
x : X
hx : ∃ (i : Option I), x ∈ D i
hx0 : x ∉ C0
hxD : x ∉ D none
⊢ ∃ (i : Option I), x ∈ C i
have neg : ∀ (hi : x ∈ D none), ∃ (i : Option I), x ∈ C i
Tactic: obtain ⟨none | j, hi⟩ := hx
Cleared hypotheses: hx
-- 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
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_subset_D0 : V ⊆ D none
D' : I → Set X := fun (i : I) ↦ D (some i) \ V
D'_clopen : ∀ (i : I), IsClopen (D' i)
Z'_subset_D' : ∀ (i : I), Z' i ⊆ D' i
C' : I → Set X
C'_clopen : ∀ (i : I), IsClopen (C' i)
Z'_subset_C' : ∀ (i : I), Z (some i) ⊆ C' i
C'_subset_D' : ∀ (i : I), C' i ⊆ D' i
C'_cover_D' : Subset.{u_4} (α := Set X) (⋃ (i : I), D' i) (⋃ (i : I), C' i)
C'_disj : PairwiseDisjoint univ C'
C0 : Set X := D none \ ⋃ (i : I), C' i
this_1 : IsClopen C0
this : Z none ⊆ C0
C : Option I → Set X := fun (i : Option I) ↦ Option.casesOn (motive := fun (x : Option I) ↦ Set X) i C0 C'
x : X
hx : ∃ (i : Option I), x ∈ D i
hx0 : x ∉ C0
hxD : x ∉ D none
neg : ∀ (hi : x ∈ D none), ∃ (i : Option I), x ∈ C i
⊢ ∃ (i : Option I), x ∈ C i
have neg₁ : ∀ (j : I) (hi : x ∈ D (some j)), ∃ (i : Option I), x ∈ C i
Tactic: obtain ⟨none | j, hi⟩ := hx
Cleared hypotheses: hx
-- 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)
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_subset_D0 : V ⊆ D none
D' : I → Set X := fun (i : I) ↦ D (some i) \ V
D'_clopen : ∀ (i : I), IsClopen (D' i)
Z'_subset_D' : ∀ (i : I), Z' i ⊆ D' i
C' : I → Set X
C'_clopen : ∀ (i : I), IsClopen (C' i)
Z'_subset_C' : ∀ (i : I), Z (some i) ⊆ C' i
C'_subset_D' : ∀ (i : I), C' i ⊆ D' i
C'_cover_D' : Subset.{u_4} (α := Set X) (⋃ (i : I), D' i) (⋃ (i : I), C' i)
C'_disj : PairwiseDisjoint univ C'
C0 : Set X := D none \ ⋃ (i : I), C' i
this_1 : IsClopen C0
this : Z none ⊆ C0
C : Option I → Set X := fun (i : Option I) ↦ Option.casesOn (motive := fun (x : Option I) ↦ Set X) i C0 C'
x : X
hx0 : x ∉ C0
hxD : x ∉ D none
j : I
hi : x ∈ D (some j)
⊢ ∃ (i : Option I), x ∈ C i
have hxD' : Membership.mem (γ := Set X) (⋃ (i : I), D' i) x
Tactic: have hxD' : x ∈ ⋃ i, D' i := mem_iUnion.mpr ⟨j, by grind⟩
-- 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
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_subset_D0 : V ⊆ D none
D' : I → Set X := fun (i : I) ↦ D (some i) \ V
D'_clopen : ∀ (i : I), IsClopen (D' i)
Z'_subset_D' : ∀ (i : I), Z' i ⊆ D' i
C' : I → Set X
C'_clopen : ∀ (i : I), IsClopen (C' i)
Z'_subset_C' : ∀ (i : I), Z (some i) ⊆ C' i
C'_subset_D' : ∀ (i : I), C' i ⊆ D' i
C'_cover_D' : Subset.{u_4} (α := Set X) (⋃ (i : I), D' i) (⋃ (i : I), C' i)
C'_disj : PairwiseDisjoint univ C'
C0 : Set X := D none \ ⋃ (i : I), C' i
this_1 : IsClopen C0
this : Z none ⊆ C0
C : Option I → Set X := fun (i : Option I) ↦ Option.casesOn (motive := fun (x : Option I) ↦ Set X) i C0 C'
x : X
hx0 : x ∉ C0
hxD : x ∉ D none
j : I
hi : x ∈ D (some j)
hxD' : Membership.mem (γ := Set X) (⋃ (i : I), D' i) x
⊢ ∃ (i : Option I), x ∈ C i
have neg : ∀ (k : I) (hk : x ∈ C' k), ∃ (i : Option I), x ∈ C i
Tactic: obtain ⟨k, hk⟩ := mem_iUnion.mp <| C'_cover_D' hxD'
-- 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
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_subset_D0 : V ⊆ D none
D' : I → Set X := fun (i : I) ↦ D (some i) \ V
D'_clopen : ∀ (i : I), IsClopen (D' i)
Z'_subset_D' : ∀ (i : I), Z' i ⊆ D' i
C' : I → Set X
C'_clopen : ∀ (i : I), IsClopen (C' i)
Z'_subset_C' : ∀ (i : I), Z (some i) ⊆ C' i
C'_subset_D' : ∀ (i : I), C' i ⊆ D' i
C'_cover_D' : Subset.{u_4} (α := Set X) (⋃ (i : I), D' i) (⋃ (i : I), C' i)
C'_disj : PairwiseDisjoint univ C'
C0 : Set X := D none \ ⋃ (i : I), C' i
this_1 : IsClopen C0
this : Z none ⊆ C0
C : Option I → Set X := fun (i : Option I) ↦ Option.casesOn (motive := fun (x : Option I) ↦ Set X) i C0 C'
⊢ PairwiseDisjoint univ C
have h_option : ∀ ⦃i : Option I⦄,
  Membership.mem (γ := Set (Option I)) univ i →
    ∀ ⦃j : Option I⦄, Membership.mem (γ := Set (Option I)) univ j → (C i ∩ C j).Nonempty → i = j
Tactic: rw [Set.pairwiseDisjoint_iff]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
⊢ RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
have rw : (∀ (b : X) (a : Set X), IsClosed[inst] aᶜ → b ∉ aᶜ → Disjoint (𝓝ˢ aᶜ) (𝓝 b)) ↔
  ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
Tactic: rw [regularSpace_iff, (@compl_surjective (Set X) _).forall, forall_comm]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
⊢ [RegularSpace X, ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x),
      ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s,
      ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s, ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x,
      ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x].TFAE
have tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
Tactic: tfae_have 1 ↔ 5 := by
    rw [regularSpace_iff, (@compl_surjective (Set X) _).forall, forall_comm]
    simp only [isClosed_compl_iff, mem_compl_iff, Classical.not_not, @and_comm (_ ∈ _),
      (nhds_basis_opens _).lift'_closure.le_basis_iff (nhds_basis_opens _), and_imp,
      (nhds_basis_opens _).disjoint_iff_right, ← subset_interior_iff_mem_nhdsSet,
      interior_compl, compl_subset_compl]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
⊢ [RegularSpace X, ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x),
      ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s,
      ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s, ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x,
      ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x].TFAE
have tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
Tactic: tfae_have 5 → 6 := fun h a => (h a).antisymm (𝓝 _).le_lift'_closure
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
H : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
a : X
s : Set X
hs : s ∈ 𝓝 a
⊢ ∃ t ∈ 𝓝 a, IsClosed[inst] t ∧ t ⊆ s
have hs₁ : s ∈ (𝓝 a).lift' closure[inst]
Tactic: rw [← H] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
H : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
a : X
s : Set X
hs : s ∈ (𝓝 a).lift' closure[inst]
⊢ ∃ t ∈ 𝓝 a, IsClosed[inst] t ∧ t ⊆ s
have rcases : ∀ (U : Set X) (hU : U ∈ 𝓝 a) (hUs : closure[inst] (id U) ⊆ s), ∃ t ∈ 𝓝 a, IsClosed[inst] t ∧ t ⊆ s
Tactic: rcases (𝓝 a).basis_sets.lift'_closure.mem_iff.mp hs with ⟨U, hU, hUs⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
⊢ [RegularSpace X, ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x),
      ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s,
      ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s, ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x,
      ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x].TFAE
have tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
Tactic: tfae_have 6 → 4
  | H, a, s, hs => by
    rw [← H] at hs
    rcases (𝓝 a).basis_sets.lift'_closure.mem_iff.mp hs with ⟨U, hU, hUs⟩
    exact ⟨closure U, mem_of_superset hU subset_closure, isClosed_closure, hUs⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
H : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
s : Set X
a : X
ha : a ∉ closure[inst] s
⊢ sᶜ ∈ 𝓝 a
have rwa : a ∈ interior sᶜ
Tactic: rwa [← mem_interior_iff_mem_nhds, interior_compl]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
H : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
s : Set X
a : X
ha : a ∉ closure[inst] s
rwa : a ∈ interior sᶜ
⊢ sᶜ ∈ 𝓝 a
have rwa₁ : a ∈ (closure[inst] s)ᶜ
Tactic: rwa [← mem_interior_iff_mem_nhds, interior_compl]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
H : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
s : Set X
a : X
ha : a ∉ closure[inst] s
⊢ Disjoint (𝓝ˢ s) (𝓝 a)
have ha' : sᶜ ∈ 𝓝 a
Tactic: have ha' : sᶜ ∈ 𝓝 a := by rwa [← mem_interior_iff_mem_nhds, interior_compl]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
H : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
s : Set X
a : X
ha : a ∉ closure[inst] s
ha' : sᶜ ∈ 𝓝 a
⊢ Disjoint (𝓝ˢ s) (𝓝 a)
have rcases : ∀ (U : Set X) (hU : U ∈ 𝓝 a) (hUc : IsClosed[inst] U) (hUs : U ⊆ sᶜ), Disjoint (𝓝ˢ s) (𝓝 a)
Tactic: rcases H _ _ ha' with ⟨U, hU, hUc, hUs⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
H : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
s : Set X
a : X
ha : a ∉ closure[inst] s
ha' : sᶜ ∈ 𝓝 a
U : Set X
hU : U ∈ 𝓝 a
hUc : IsClosed[inst] U
hUs : U ⊆ sᶜ
⊢ Disjoint (𝓝ˢ s) (𝓝 a)
have refine : Uᶜ ∈ 𝓝ˢ s
Tactic: refine disjoint_of_disjoint_of_mem disjoint_compl_left ?_ hU
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
H : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
s : Set X
a : X
ha : a ∉ closure[inst] s
ha' : sᶜ ∈ 𝓝 a
U : Set X
hU : U ∈ 𝓝 a
hUc : IsClosed[inst] U
hUs : U ⊆ sᶜ
⊢ Uᶜ ∈ 𝓝ˢ s
have rwa : s ⊆ interior Uᶜ
Tactic: rwa [← subset_interior_iff_mem_nhdsSet, hUc.isOpen_compl.interior_eq, subset_compl_comm]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
H : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
s : Set X
a : X
ha : a ∉ closure[inst] s
ha' : sᶜ ∈ 𝓝 a
U : Set X
hU : U ∈ 𝓝 a
hUc : IsClosed[inst] U
hUs : U ⊆ sᶜ
rwa : s ⊆ interior Uᶜ
⊢ Uᶜ ∈ 𝓝ˢ s
have rwa₁ : s ⊆ Uᶜ
Tactic: rwa [← subset_interior_iff_mem_nhdsSet, hUc.isOpen_compl.interior_eq, subset_compl_comm]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
⊢ [RegularSpace X, ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x),
      ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s,
      ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s, ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x,
      ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x].TFAE
have tfae_4_to_2 : ∀ (a : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s) (s : Set X),
  ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)
Tactic: tfae_have 4 → 2
  | H, s, a, ha => by
    have ha' : sᶜ ∈ 𝓝 a := by rwa [← mem_interior_iff_mem_nhds, interior_compl]
    rcases H _ _ ha' with ⟨U, hU, hUc, hUs⟩
    refine disjoint_of_disjoint_of_mem disjoint_compl_left ?_ hU
    rwa [← subset_interior_iff_mem_nhdsSet, hUc.isOpen_compl.interior_eq, subset_compl_comm]
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (goal)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
tfae_4_to_2 :
  ∀ (a : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s) (s : Set X),
    ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)
⊢ ∀ (a : ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)) (x : X) (s : Set X),
    Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s
have refine : ∀ (H : ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)) (a : X) (s : Set X) (hd : Disjoint (𝓝ˢ s) (𝓝 a))
  (has : a ∈ closure[inst] s), 𝓝 a ⊓ 𝓟 s = ⊥
Tactic: refine fun H a s => ⟨fun hd has => mem_closure_iff_nhds_ne_bot.mp has ?_, H s a⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Regular (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x
tfae_5_to_6 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x) (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x
tfae_6_to_4 : ∀ (a : ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x) (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s
tfae_4_to_2 :
  ∀ (a : ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s) (s : Set X),
    ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)
⊢ [RegularSpace X, ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x),
      ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s,
      ∀ (x : X), ∀ s ∈ 𝓝 x, ∃ t ∈ 𝓝 x, IsClosed[inst] t ∧ t ⊆ s, ∀ (x : X), (𝓝 x).lift' closure[inst] ≤ 𝓝 x,
      ∀ (x : X), (𝓝 x).lift' closure[inst] = 𝓝 x].TFAE
have tfae_2_to_3 : ∀ (a : ∀ (s : Set X), ∀ x ∉ closure[inst] s, Disjoint (𝓝ˢ s) (𝓝 x)) (x : X) (s : Set X),
  Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure[inst] s
Tactic: tfae_have 2 → 3 := by
    refine fun H a s => ⟨fun hd has => mem_closure_iff_nhds_ne_bot.mp has ?_, H s a⟩
    exact (hd.symm.mono_right <| @principal_le_nhdsSet _ _ s).eq_bot