awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X)
hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : Eq.{u_2 + 1} (α := Set X) (⋃ (i : Fin n), (↑(W i) : Set X)) (⋃ (i : Fin n), (↑(V i) : Set X))
t : Finset (Fin n) := {j : Fin n | W j ≠ ⊥}
refine_1 :
  ∀ (k : Fin #t),
    Ne.{u_2 + 1} (α := Clopens X) ((fun (k : Fin #t) ↦ W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n)) k) ⊥
refine_2 :
  ∀ (k : Fin #t),
    ∃ (i : ι),
      (↑((fun (k : Fin #t) ↦ W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n)) k) : Set X) ⊆ (↑(U i) : Set X)
⊢ ∃ (n : ℕ) (W : Fin n → Clopens X),
    (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ι), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)) ∧
      Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X)) ∧ Pairwise (Disjoint on W)
have refine_3 : ∀ (x : X) (hx : Membership.mem (γ := Set X) univ x),
  Membership.mem (γ := Set X)
    (⋃ (j : Fin #t), (↑((fun (k : Fin #t) ↦ W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n)) j) : Set X)) x
Tactic: refine ⟨#t, fun k ↦ W (t.equivFin.symm k), fun k ↦ ⟨?_, ?_⟩, fun x hx ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X)
hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : Eq.{u_2 + 1} (α := Set X) (⋃ (i : Fin n), (↑(W i) : Set X)) (⋃ (i : Fin n), (↑(V i) : Set X))
t : Finset (Fin n) := {j : Fin n | W j ≠ ⊥}
refine_1 :
  ∀ (k : Fin #t),
    Ne.{u_2 + 1} (α := Clopens X) ((fun (k : Fin #t) ↦ W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n)) k) ⊥
refine_2 :
  ∀ (k : Fin #t),
    ∃ (i : ι),
      (↑((fun (k : Fin #t) ↦ W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n)) k) : Set X) ⊆ (↑(U i) : Set X)
refine_3 :
  ∀ (x : X) (hx : Membership.mem (γ := Set X) univ x),
    Membership.mem (γ := Set X)
      (⋃ (j : Fin #t), (↑((fun (k : Fin #t) ↦ W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n)) j) : Set X)) x
⊢ ∃ (n : ℕ) (W : Fin n → Clopens X),
    (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ι), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)) ∧
      Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X)) ∧ Pairwise (Disjoint on W)
have refine_4 : Pairwise (α := Fin #t)
  (Function.onFun.{1, u_2 + 1, 1} (β := Clopens X) Disjoint fun (k : Fin #t) ↦
    W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n))
Tactic: refine ⟨#t, fun k ↦ W (t.equivFin.symm k), fun k ↦ ⟨?_, ?_⟩, fun x hx ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X)
hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : Eq.{u_2 + 1} (α := Set X) (⋃ (i : Fin n), (↑(W i) : Set X)) (⋃ (i : Fin n), (↑(V i) : Set X))
t : Finset (Fin n) := {j : Fin n | W j ≠ ⊥}
x : X
hx : Membership.mem (γ := Set X) univ x
⊢ Membership.mem (γ := Set X)
    (⋃ (j : Fin #t), (↑((fun (k : Fin #t) ↦ W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n)) j) : Set X)) x
have refine_3 : ∀ (j : Fin n) (hj : x ∈ (↑(W j) : Set X)),
  Membership.mem (γ := Set X)
    (⋃ (j : Fin #t), (↑((fun (k : Fin #t) ↦ W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n)) j) : Set X)) x
Tactic: obtain ⟨j, hj⟩ := mem_iUnion.mp <| (hWun ▸ hVun) hx
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (hypothesis)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X)
hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : Eq.{u_2 + 1} (α := Set X) (⋃ (i : Fin n), (↑(W i) : Set X)) (⋃ (i : Fin n), (↑(V i) : Set X))
t : Finset (Fin n) := {j : Fin n | W j ≠ ⊥}
x : X
hx : Membership.mem (γ := Set X) univ x
j : Fin n
hj : x ∈ (↑(W j) : Set X)
⊢ Membership.mem (γ := Set X)
    (⋃ (j : Fin #t), (↑((fun (k : Fin #t) ↦ W (↑((t.equivFin.symm : (a : Fin #t) → ↥t) k) : Fin n)) j) : Set X)) x
have this : W j ≠ ⊥
Tactic: have : W j ≠ ⊥ := by simpa [← SetLike.coe_ne_coe, ← Set.nonempty_iff_ne_empty] using ⟨x, hj⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
⊢ ∃ (n : ℕ) (W : Fin n → Clopens X),
    (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ι), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)) ∧
      Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X)) ∧ Pairwise (Disjoint on W)
have obtain : ∀ (n : ℕ) (V : Fin n → Clopens X) (hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X))
  (hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))),
  ∃ (n : ℕ) (W : Fin n → Clopens X),
    (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ι), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)) ∧
      Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X)) ∧ Pairwise (Disjoint on W)
Tactic: classical
  obtain ⟨n, V, hVle, hVun⟩ := hU.exists_finite_clopen_cover
  obtain ⟨W, hWle, hWun, hWd⟩ := Fintype.exists_disjointed_le V
  simp only [← SetLike.coe_set_eq, Clopens.coe_finset_sup, Finset.mem_univ, iUnion_true] at hWun
  let t : Finset (Fin n) := {j | W j ≠ ⊥}
  refine ⟨#t, fun k ↦ W (t.equivFin.symm k), fun k ↦ ⟨?_, ?_⟩, fun x hx ↦ ?_, ?_⟩
  · exact (Finset.mem_filter.mp (t.equivFin.symm k).2).2
  · exact match hVle (t.equivFin.symm k) with | ⟨i, hi⟩ => ⟨i, subset_trans (hWle _) hi⟩
  · obtain ⟨j, hj⟩ := mem_iUnion.mp <| (hWun ▸ hVun) hx
    have : W j ≠ ⊥ := by simpa [← SetLike.coe_ne_coe, ← Set.nonempty_iff_ne_empty] using ⟨x, hj⟩
    exact mem_iUnion.mpr ⟨t.equivFin ⟨j, Finset.mem_filter.mpr ⟨Finset.mem_univ _, this⟩⟩, by simpa⟩
  · exact hWd.comp_of_injective <| Subtype.val_injective.comp t.equivFin.symm.injective
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
obtain :
  ∀ (n : ℕ) (V : Fin n → Clopens X) (hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X))
    (hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))),
    ∃ (n : ℕ) (W : Fin n → Clopens X),
      (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ι), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)) ∧
        Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X)) ∧ Pairwise (Disjoint on W)
⊢ ∃ (n : ℕ) (W : Fin n → Clopens X),
    (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ι), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)) ∧
      Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X)) ∧ Pairwise (Disjoint on W)
have obtain₁ : ∀ (n : ℕ) (V : Fin n → Clopens X) (hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X))
  (hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))) (W : Fin n → Clopens X) (hWle : W ≤ V)
  (hWun : Finset.sup Finset.univ W = Finset.sup Finset.univ V) (hWd : Pairwise (Disjoint on W)),
  ∃ (n : ℕ) (W : Fin n → Clopens X),
    (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ι), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)) ∧
      Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X)) ∧ Pairwise (Disjoint on W)
Tactic: classical
  obtain ⟨n, V, hVle, hVun⟩ := hU.exists_finite_clopen_cover
  obtain ⟨W, hWle, hWun, hWd⟩ := Fintype.exists_disjointed_le V
  simp only [← SetLike.coe_set_eq, Clopens.coe_finset_sup, Finset.mem_univ, iUnion_true] at hWun
  let t : Finset (Fin n) := {j | W j ≠ ⊥}
  refine ⟨#t, fun k ↦ W (t.equivFin.symm k), fun k ↦ ⟨?_, ?_⟩, fun x hx ↦ ?_, ?_⟩
  · exact (Finset.mem_filter.mp (t.equivFin.symm k).2).2
  · exact match hVle (t.equivFin.symm k) with | ⟨i, hi⟩ => ⟨i, subset_trans (hWle _) hi⟩
  · obtain ⟨j, hj⟩ := mem_iUnion.mp <| (hWun ▸ hVun) hx
    have : W j ≠ ⊥ := by simpa [← SetLike.coe_ne_coe, ← Set.nonempty_iff_ne_empty] using ⟨x, hj⟩
    exact mem_iUnion.mpr ⟨t.equivFin ⟨j, Finset.mem_filter.mpr ⟨Finset.mem_univ _, this⟩⟩, by simpa⟩
  · exact hWd.comp_of_injective <| Subtype.val_injective.comp t.equivFin.symm.injective
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
ι : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : TotallyDisconnectedSpace X
inst_2 : T2Space X
inst_3 : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
obtain :
  ∀ (n : ℕ) (V : Fin n → Clopens X) (hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X))
    (hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))),
    ∃ (n : ℕ) (W : Fin n → Clopens X),
      (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ι), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)) ∧
        Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X)) ∧ Pairwise (Disjoint on W)
obtain₁ :
  ∀ (n : ℕ) (V : Fin n → Clopens X) (hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X))
    (hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))) (W : Fin n → Clopens X) (hWle : W ≤ V)
    (hWun : Finset.sup Finset.univ W = Finset.sup Finset.univ V) (hWd : Pairwise (Disjoint on W)),
    ∃ (n : ℕ) (W : Fin n → Clopens X),
      (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ι), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)) ∧
        Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X)) ∧ Pairwise (Disjoint on W)
⊢ ∃ (n : ℕ) (W : Fin n → Clopens X),
    (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ι), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)) ∧
      Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X)) ∧ Pairwise (Disjoint on W)
have obtain₂ : ∀ (n : ℕ) (V : Fin n → Clopens X) (hVle : ∀ (j : Fin n), ∃ (i : ι), (↑(V j) : Set X) ⊆ (↑(U i) : Set X))
  (hVun : Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(V j) : Set X))) (W : Fin n → Clopens X) (hWle : W ≤ V)
  (hWd : Pairwise (Disjoint on W))
  (hWun : Eq.{u_2 + 1} (α := Set X) (⋃ (i : Fin n), (↑(W i) : Set X)) (⋃ (i : Fin n), (↑(V i) : Set X))),
  ∃ (n : ℕ) (W : Fin n → Clopens X),
    (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ι), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)) ∧
      Subset.{u_2} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X)) ∧ Pairwise (Disjoint on W)
Tactic: classical
  obtain ⟨n, V, hVle, hVun⟩ := hU.exists_finite_clopen_cover
  obtain ⟨W, hWle, hWun, hWd⟩ := Fintype.exists_disjointed_le V
  simp only [← SetLike.coe_set_eq, Clopens.coe_finset_sup, Finset.mem_univ, iUnion_true] at hWun
  let t : Finset (Fin n) := {j | W j ≠ ⊥}
  refine ⟨#t, fun k ↦ W (t.equivFin.symm k), fun k ↦ ⟨?_, ?_⟩, fun x hx ↦ ?_, ?_⟩
  · exact (Finset.mem_filter.mp (t.equivFin.symm k).2).2
  · exact match hVle (t.equivFin.symm k) with | ⟨i, hi⟩ => ⟨i, subset_trans (hWle _) hi⟩
  · obtain ⟨j, hj⟩ := mem_iUnion.mp <| (hWun ▸ hVun) hx
    have : W j ≠ ⊥ := by simpa [← SetLike.coe_ne_coe, ← Set.nonempty_iff_ne_empty] using ⟨x, hj⟩
    exact mem_iUnion.mpr ⟨t.equivFin ⟨j, Finset.mem_filter.mpr ⟨Finset.mem_univ _, this⟩⟩, by simpa⟩
  · exact hWd.comp_of_injective <| Subtype.val_injective.comp t.equivFin.symm.injective
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
hS : S ∈ 𝓝ˢ (diagonal X)
x : X
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ U ×ˢ U ⊆ S
have this : S ∈ 𝓝 (x, x)
Tactic: have : S ∈ 𝓝 (x, x) := mem_nhdsSet_iff_forall.mp hS _ rfl
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
hS : S ∈ 𝓝ˢ (diagonal X)
x : X
this : S ∈ 𝓝 (x, x)
⊢ ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ x ∈ u ∧ IsOpen[inst] v ∧ x ∈ v ∧ u ×ˢ v ⊆ S
have rwa : ∀ (this : ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ x ∈ u ∧ IsOpen[inst] v ∧ x ∈ v ∧ u ×ˢ v ⊆ S),
  ∃ (u : Set X) (v : Set X), IsOpen[inst] u ∧ x ∈ u ∧ IsOpen[inst] v ∧ x ∈ v ∧ u ×ˢ v ⊆ S
Tactic: rwa [mem_nhds_prod_iff'] at this
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
hS : S ∈ 𝓝ˢ (diagonal X)
x : X
this : S ∈ 𝓝 (x, x)
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ U ×ˢ U ⊆ S
have obtain : ∀ (u v : Set X) (huo : IsOpen[inst] u) (hux : x ∈ u) (hvo : IsOpen[inst] v) (hvx : x ∈ v) (H : u ×ˢ v ⊆ S),
  ∃ (U : Set X), IsOpen[inst] U ∧ x ∈ U ∧ U ×ˢ U ⊆ S
Tactic: obtain ⟨u, v, huo, hux, hvo, hvx, H⟩ := by rwa [mem_nhds_prod_iff'] at this
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
inst_1 : CompactSpace X
hS : S ∈ 𝓝ˢ (diagonal X)
⊢ ∃ (t : Finset X) (U : ↥t → Opens X), IsOpenCover U ∧ ∀ (i : ↥t), (↑(U i) : Set X) ×ˢ (↑(U i) : Set X) ⊆ S
have choose : ∀ (U : (x : X) → Set X) (hUo : ∀ (x : X), IsOpen[inst] (U x)) (hUx : ∀ (x : X), x ∈ U x)
  (hUp : ∀ (x : X), U x ×ˢ U x ⊆ S),
  ∃ (t : Finset X) (U : ↥t → Opens X), IsOpenCover U ∧ ∀ (i : ↥t), (↑(U i) : Set X) ×ˢ (↑(U i) : Set X) ⊆ S
Tactic: choose U hUo hUx hUp using exists_open_prod_subset_of_mem_nhds_diagonal hS
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
inst_1 : CompactSpace X
hS : S ∈ 𝓝ˢ (diagonal X)
U : (x : X) → Set X
hUo : ∀ (x : X), IsOpen[inst] (U x)
hUx : ∀ (x : X), x ∈ U x
hUp : ∀ (x : X), U x ×ˢ U x ⊆ S
⊢ ∃ (t : Finset X) (U : ↥t → Opens X), IsOpenCover U ∧ ∀ (i : ↥t), (↑(U i) : Set X) ×ˢ (↑(U i) : Set X) ⊆ S
have obtain : ∀ (t : Finset X) (ht : Subset.{u_1} (α := Set X) univ (⋃ i ∈ t, U i)),
  ∃ (t : Finset X) (U : ↥t → Opens X), IsOpenCover U ∧ ∀ (i : ↥t), (↑(U i) : Set X) ×ˢ (↑(U i) : Set X) ⊆ S
Tactic: obtain ⟨t, ht⟩ := isCompact_univ.elim_finite_subcover _ hUo (fun x _ ↦ mem_iUnion.mpr ⟨_, hUx x⟩)
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
inst_1 : CompactSpace X
hS : S ∈ 𝓝ˢ (diagonal X)
U : (x : X) → Set X
hUo : ∀ (x : X), IsOpen[inst] (U x)
hUx : ∀ (x : X), x ∈ U x
hUp : ∀ (x : X), U x ×ˢ U x ⊆ S
t : Finset X
ht : Subset.{u_1} (α := Set X) univ (⋃ i ∈ t, U i)
⊢ ∃ (t : Finset X) (U : ↥t → Opens X), IsOpenCover U ∧ ∀ (i : ↥t), (↑(U i) : Set X) ×ˢ (↑(U i) : Set X) ⊆ S
have refine : Eq.{u_1 + 1} (α := Set X) (⋃ (i : ↥t), U (↑i : X)) univ
Tactic: refine ⟨t, fun i ↦ ⟨_, hUo i⟩, .of_sets _ ?_, (hUp ·)⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
inst_1 : CompactSpace X
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
hS : S ∈ 𝓝ˢ (diagonal X)
⊢ ∃ (n : ℕ) (D : Fin n → Clopens X),
    (∀ (i : Fin n), D i ≠ ⊥) ∧
      (∀ (i : Fin n), ∀ y ∈ D i, ∀ z ∈ D i, (y, z) ∈ S) ∧
        Subset.{u_1} (α := Set X) univ (⋃ (i : Fin n), (↑(D i) : Set X)) ∧ Pairwise (Disjoint on D)
have obtain : ∀ (t : Finset X) (U : ↥t → Opens X) (hUc : IsOpenCover U) (hUS : ∀ (i : ↥t), (↑(U i) : Set X) ×ˢ (↑(U i) : Set X) ⊆ S),
  ∃ (n : ℕ) (D : Fin n → Clopens X),
    (∀ (i : Fin n), D i ≠ ⊥) ∧
      (∀ (i : Fin n), ∀ y ∈ D i, ∀ z ∈ D i, (y, z) ∈ S) ∧
        Subset.{u_1} (α := Set X) univ (⋃ (i : Fin n), (↑(D i) : Set X)) ∧ Pairwise (Disjoint on D)
Tactic: obtain ⟨t, U, hUc, hUS⟩ := exists_finite_open_cover_prod_subset_of_mem_nhds_diagonal_of_compact hS
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
inst_1 : CompactSpace X
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
hS : S ∈ 𝓝ˢ (diagonal X)
t : Finset X
U : ↥t → Opens X
hUc : IsOpenCover U
hUS : ∀ (i : ↥t), (↑(U i) : Set X) ×ˢ (↑(U i) : Set X) ⊆ S
⊢ ∃ (n : ℕ) (D : Fin n → Clopens X),
    (∀ (i : Fin n), D i ≠ ⊥) ∧
      (∀ (i : Fin n), ∀ y ∈ D i, ∀ z ∈ D i, (y, z) ∈ S) ∧
        Subset.{u_1} (α := Set X) univ (⋃ (i : Fin n), (↑(D i) : Set X)) ∧ Pairwise (Disjoint on D)
have obtain : ∀ (n : ℕ) (W : Fin n → Clopens X) (hW₁ : ∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ↥t), (↑(W j) : Set X) ⊆ (↑(U i) : Set X))
  (hW₂ : Subset.{u_1} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X))) (hW₃ : Pairwise (Disjoint on W)),
  ∃ (n : ℕ) (D : Fin n → Clopens X),
    (∀ (i : Fin n), D i ≠ ⊥) ∧
      (∀ (i : Fin n), ∀ y ∈ D i, ∀ z ∈ D i, (y, z) ∈ S) ∧
        Subset.{u_1} (α := Set X) univ (⋃ (i : Fin n), (↑(D i) : Set X)) ∧ Pairwise (Disjoint on D)
Tactic: obtain ⟨n, W, hW₁, hW₂, hW₃⟩ := hUc.exists_finite_nonempty_disjoint_clopen_cover
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (X × X)
inst_1 : CompactSpace X
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
hS : S ∈ 𝓝ˢ (diagonal X)
t : Finset X
U : ↥t → Opens X
hUc : IsOpenCover U
hUS : ∀ (i : ↥t), (↑(U i) : Set X) ×ˢ (↑(U i) : Set X) ⊆ S
n : ℕ
W : Fin n → Clopens X
hW₁ : ∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ (i : ↥t), (↑(W j) : Set X) ⊆ (↑(U i) : Set X)
hW₂ : Subset.{u_1} (α := Set X) univ (⋃ (j : Fin n), (↑(W j) : Set X))
hW₃ : Pairwise (Disjoint on W)
⊢ ∃ (n : ℕ) (D : Fin n → Clopens X),
    (∀ (i : Fin n), D i ≠ ⊥) ∧
      (∀ (i : Fin n), ∀ y ∈ D i, ∀ z ∈ D i, (y, z) ∈ S) ∧
        Subset.{u_1} (α := Set X) univ (⋃ (i : Fin n), (↑(D i) : Set X)) ∧ Pairwise (Disjoint on D)
have refine : ∀ (j : Fin n) (y : X) (hy : y ∈ W j) (z : X) (hz : z ∈ W j), (y, z) ∈ S
Tactic: refine ⟨n, W, fun j ↦ (hW₁ j).1, fun j y hy z hz ↦ ?_, hW₂, hW₃⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
X : Type u_1
V : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace V
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
inst_4 : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
⊢ (⇑(f.prodMap f) : (a : X × X) → V × V) ⁻¹' S ∈ 𝓝ˢ (diagonal X)
have rw : ∀ (hS : ∀ x ∈ diagonal V, S ∈ 𝓝 x), ∀ x ∈ diagonal X, (⇑(f.prodMap f) : (a : X × X) → V × V) ⁻¹' S ∈ 𝓝 x
Tactic: rw [mem_nhdsSet_iff_forall] at hS ⊢
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (hypothesis)
Goal:
X : Type u_1
V : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace V
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
inst_4 : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
⊢ ∃ (n : ℕ) (D : Fin n → Clopens X),
    (∀ (i : Fin n), D i ≠ ⊥) ∧
      (∀ (i : Fin n),
          ∀ y ∈ D i, ∀ z ∈ D i, Membership.mem (α := V × V) S (((f : (a : X) → V) y, (f : (a : X) → V) z) : V × V)) ∧
        Subset.{u_1} (α := Set X) univ (⋃ (i : Fin n), (↑(D i) : Set X)) ∧ Pairwise (Disjoint on D)
have this : (⇑(f.prodMap f) : (a : X × X) → V × V) ⁻¹' S ∈ 𝓝ˢ (diagonal X)
Tactic: have : (f.prodMap f) ⁻¹' S ∈ nhdsSet (diagonal X) := by
    rw [mem_nhdsSet_iff_forall] at hS ⊢
    rintro ⟨x, y⟩ (rfl : x = y)
    exact (map_continuous _).continuousAt.preimage_mem_nhds (hS _ rfl)
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
X : Type u_1
V : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace V
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
inst_4 : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
⊢ ∃ (n : ℕ) (g : X → Fin n) (h : Fin n → V),
    Continuous[inst, _] g ∧ ∀ (x : X), Membership.mem (α := V × V) S (((f : (a : X) → V) x, h (g x)) : V × V)
have obtain : ∀ (n : ℕ) (E : Fin n → Clopens X) (hEne : ∀ (i : Fin n), E i ≠ ⊥)
  (hES :
    ∀ (i : Fin n),
      ∀ y ∈ E i, ∀ z ∈ E i, Membership.mem (α := V × V) S (((f : (a : X) → V) y, (f : (a : X) → V) z) : V × V))
  (hEuniv : Subset.{u_1} (α := Set X) univ (⋃ (i : Fin n), (↑(E i) : Set X))) (hEdis : Pairwise (Disjoint on E)),
  ∃ (n : ℕ) (g : X → Fin n) (h : Fin n → V),
    Continuous[inst, _] g ∧ ∀ (x : X), Membership.mem (α := V × V) S (((f : (a : X) → V) x, h (g x)) : V × V)
Tactic: obtain ⟨n, E, hEne, hES, hEuniv, hEdis⟩ :=
    exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal f hS
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
X : Type u_1
V : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace V
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
inst_4 : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
E : Fin n → Clopens X
hEne : ∀ (i : Fin n), E i ≠ ⊥
hES :
  ∀ (i : Fin n),
    ∀ y ∈ E i, ∀ z ∈ E i, Membership.mem (α := V × V) S (((f : (a : X) → V) y, (f : (a : X) → V) z) : V × V)
hEuniv : Subset.{u_1} (α := Set X) univ (⋃ (i : Fin n), (↑(E i) : Set X))
hEdis : Pairwise (Disjoint on E)
x : X
⊢ ∃! i : Fin n, x ∈ E i
have refine : ∀ (i : Fin n) (hi : x ∈ (↑(E i) : Set X)) (j : Fin n) (hj : (fun (i : Fin n) ↦ x ∈ E i) j), ¬(Disjoint on E) j i
Tactic: refine match mem_iUnion.mp (hEuniv <| mem_univ x) with
      | ⟨i, hi⟩ => ⟨i, hi, fun j hj ↦ hEdis.eq ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (hypothesis)
Goal:
X : Type u_1
V : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace V
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
inst_4 : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
E : Fin n → Clopens X
hEne : ∀ (i : Fin n), E i ≠ ⊥
hES :
  ∀ (i : Fin n),
    ∀ y ∈ E i, ∀ z ∈ E i, Membership.mem (α := V × V) S (((f : (a : X) → V) y, (f : (a : X) → V) z) : V × V)
hEuniv : Subset.{u_1} (α := Set X) univ (⋃ (i : Fin n), (↑(E i) : Set X))
hEdis : Pairwise (Disjoint on E)
⊢ ∃ (n : ℕ) (g : X → Fin n) (h : Fin n → V),
    Continuous[inst, _] g ∧ ∀ (x : X), Membership.mem (α := V × V) S (((f : (a : X) → V) x, h (g x)) : V × V)
have h_uniq : ∀ (x : X), ∃! i : Fin n, x ∈ E i
Tactic: have h_uniq (x) : ∃! i, x ∈ E i := by
    refine match mem_iUnion.mp (hEuniv <| mem_univ x) with
      | ⟨i, hi⟩ => ⟨i, hi, fun j hj ↦ hEdis.eq ?_⟩
    simpa [← Clopens.coe_disjoint, not_disjoint_iff] using ⟨x, hj, hi⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.DisjointCover (goal)
Goal:
X : Type u_1
V : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace V
inst_2 : TotallyDisconnectedSpace X
inst_3 : T2Space X
inst_4 : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
E : Fin n → Clopens X
hEne : ∀ (i : Fin n), E i ≠ ⊥
hES :
  ∀ (i : Fin n),
    ∀ y ∈ E i, ∀ z ∈ E i, Membership.mem (α := V × V) S (((f : (a : X) → V) y, (f : (a : X) → V) z) : V × V)
hEuniv : Subset.{u_1} (α := Set X) univ (⋃ (i : Fin n), (↑(E i) : Set X))
hEdis : Pairwise (Disjoint on E)
h_uniq : ∀ (x : X), ∃! i : Fin n, x ∈ E i
⊢ ∃ (n : ℕ) (g : X → Fin n) (h : Fin n → V),
    Continuous[inst, _] g ∧ ∀ (x : X), Membership.mem (α := V × V) S (((f : (a : X) → V) x, h (g x)) : V × V)
have choose : ∀ (g : (x : X) → Fin n) (hg : ∀ (x : X), (fun (i : Fin n) ↦ x ∈ E i) (g x))
  (hg' : ∀ (x : X) (y : Fin n), (fun (i : Fin n) ↦ x ∈ E i) y → y = g x),
  ∃ (n : ℕ) (g : X → Fin n) (h : Fin n → V),
    Continuous[inst, _] g ∧ ∀ (x : X), Membership.mem (α := V × V) S (((f : (a : X) → V) x, h (g x)) : V × V)
Tactic: choose g hg hg' using h_uniq
Cleared hypotheses: h_uniq