awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.DisjointCover
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)
this : (⇑(f.prodMap f) : (a : X × X) → V × V) ⁻¹' S ∈ 𝓝ˢ (diagonal X)
⊢ ∃ (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)

Tactic:
exact exists_finite_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal_of_profinite this

Premises used: _private.0.TopologicalSpace.exists_finite_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal_of_profinite
-- Module: Mathlib.Topology.Separation.DisjointCover
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)
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)
⊢ ∃ (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

Premises used: ContinuousMap.exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal
-- Module: Mathlib.Topology.Separation.DisjointCover
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

Tactic:
match mem_iUnion.mp (hEuniv <| mem_univ x) with
      | ⟨i, hi⟩ => ⟨i, hi, fun j hj ↦ hEdis.eq ?_⟩

Premises used: Set.mem_iUnion, Membership.mem, Pairwise.eq, ExistsUnique, And.intro, Exists.intro, Iff.mp, Set.mem_univ, _private.0.ContinuousMap.exists_finite_approximation_of_mem_nhds_diagonal.match_1
-- Module: Mathlib.Topology.Separation.DisjointCover
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
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
⊢ ∃! i : Fin n, x ∈ E i

Tactic:
refine match mem_iUnion.mp (hEuniv <| mem_univ x) with
      | ⟨i, hi⟩ => ⟨i, hi, fun j hj ↦ hEdis.eq ?_⟩
-- Module: Mathlib.Topology.Separation.DisjointCover
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
hi : x ∈ (↑(E i) : Set X)
j : Fin n
hj : (fun (i : Fin n) ↦ x ∈ E i) j
⊢ ¬(Disjoint on E) j i

Tactic:
simpa [← Clopens.coe_disjoint, not_disjoint_iff] using ⟨x, hj, hi⟩

Premises used: TopologicalSpace.Clopens.coe_disjoint, Set.not_disjoint_iff
-- Module: Mathlib.Topology.Separation.DisjointCover
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

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⟩
-- Module: Mathlib.Topology.Separation.DisjointCover
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
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)
⊢ ∃ (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
-- Module: Mathlib.Topology.Separation.DisjointCover
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)
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
i : Fin n
⊢ ∃ (x : X), x ∈ E i

Tactic:
simpa [← SetLike.coe_set_eq, ← nonempty_iff_ne_empty] using hEne i

Premises used: Set.nonempty_iff_ne_empty, SetLike.coe_set_eq
-- Module: Mathlib.Topology.Separation.DisjointCover
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)
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
⊢ ∀ (i : Fin n), ∃ (x : X), x ∈ E i

Tactic:
have h_ex (i) : ∃ x, x ∈ E i := by
    simpa [← SetLike.coe_set_eq, ← nonempty_iff_ne_empty] using hEne i
-- Module: Mathlib.Topology.Separation.DisjointCover
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)
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
h_ex : ∀ (i : Fin n), ∃ (x : X), x ∈ E i
choose :
  ∀ (r : (i : Fin n) → X) (hr : ∀ (i : Fin n), r i ∈ 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)
⊢ ∃ (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 r hr using h_ex
-- Module: Mathlib.Topology.Separation.DisjointCover
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)
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
r : (i : Fin n) → X
hr : ∀ (i : Fin n), r i ∈ 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)

Tactic:
⟨n, g, f ∘ r, continuous_discrete_rng.mpr fun j ↦ ?_, fun x ↦ (hES _) _ (hg _) _ (hr _)⟩

Premises used: Iff.mpr, Function.comp, And.intro, Exists.intro, DFunLike.coe, continuous_discrete_rng
-- Module: Mathlib.Topology.Separation.DisjointCover
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)
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
r : (i : Fin n) → X
hr : ∀ (i : Fin n), r i ∈ E i
refine : ∀ (j : Fin n), IsOpen[inst] (g ⁻¹' {j})
⊢ ∃ (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:
refine ⟨n, g, f ∘ r, continuous_discrete_rng.mpr fun j ↦ ?_, fun x ↦ (hES _) _ (hg _) _ (hr _)⟩
-- Module: Mathlib.Topology.Separation.DisjointCover
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)
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
r : (i : Fin n) → X
hr : ∀ (i : Fin n), r i ∈ E i
j : Fin n
⊢ IsOpen[inst] (↑(E j) : Set X)

Tactic:
(E j).isOpen

Premises used: TopologicalSpace.Clopens.isOpen
-- Module: Mathlib.Topology.Separation.DisjointCover
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)
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
r : (i : Fin n) → X
hr : ∀ (i : Fin n), r i ∈ E i
j : Fin n
h : g ⁻¹' {j} = (↑(E j) : Set X)
⊢ IsOpen[inst] (g ⁻¹' {j})

Tactic:
convert! (E j).isOpen

Premises used: TopologicalSpace.Clopens.isOpen
-- Module: Mathlib.Topology.Separation.DisjointCover
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)
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
r : (i : Fin n) → X
hr : ∀ (i : Fin n), r i ∈ E i
j : Fin n
⊢ g ⁻¹' {j} = (↑(E j) : Set X)

Tactic:
Set.ext fun x ↦ ⟨fun hj ↦ hj ▸ hg x, fun hx ↦ (hg' _ _ hx).symm⟩

Premises used: Set.ext, Eq.rec, Iff.intro, Eq.symm
-- Module: Mathlib.Topology.Separation.DisjointCover
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)
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
r : (i : Fin n) → X
hr : ∀ (i : Fin n), r i ∈ E i
j : Fin n
⊢ g ⁻¹' {j} = (↑(E j) : Set X)

Tactic:
exact Set.ext fun x ↦ ⟨fun hj ↦ hj ▸ hg x, fun hx ↦ (hg' _ _ hx).symm⟩

Premises used: Set.ext, Iff.intro, Eq.symm
-- Module: Mathlib.Topology.Separation.DisjointCover
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)
inst_5 : CommMonoid V
hS : S ∈ 𝓝ˢ (diagonal V)
obtain :
  ∀ (n : ℕ) (g : X → Fin n) (h : Fin n → V) (hg : Continuous[inst, _] g)
    (hgh : ∀ (x : X), Membership.mem (α := V × V) S (((f : (a : X) → V) x, h (g x)) : V × V)),
    ∃ (n : ℕ) (U : Fin n → Clopens X) (v : Fin n → V),
      ∀ (x : X),
        Membership.mem (α := V × V) S
          (((f : (a : X) → V) x, ∏ n : Fin n, (↑(U n) : Set X).mulIndicator (fun (x : X) ↦ v n) x) : V × V)
⊢ ∃ (n : ℕ) (U : Fin n → Clopens X) (v : Fin n → V),
    ∀ (x : X),
      Membership.mem (α := V × V) S
        (((f : (a : X) → V) x, ∏ n : Fin n, (↑(U n) : Set X).mulIndicator (fun (x : X) ↦ v n) x) : V × V)

Tactic:
obtain ⟨n, g, h, hg, hgh⟩ := exists_finite_approximation_of_mem_nhds_diagonal f hS

Premises used: ContinuousMap.exists_finite_approximation_of_mem_nhds_diagonal
-- Module: Mathlib.Topology.Separation.DisjointCover
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)
inst_5 : CommMonoid V
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
g : X → Fin n
h : Fin n → V
hg : Continuous[inst, _] g
hgh : ∀ (x : X), Membership.mem (α := V × V) S (((f : (a : X) → V) x, h (g x)) : V × V)
⊢ ∃ (n : ℕ) (U : Fin n → Clopens X) (v : Fin n → V),
    ∀ (x : X),
      Membership.mem (α := V × V) S
        (((f : (a : X) → V) x, ∏ n : Fin n, (↑(U n) : Set X).mulIndicator (fun (x : X) ↦ v n) x) : V × V)

Tactic:
⟨n, fun i ↦ ⟨_, (isClopen_discrete {i}).preimage hg⟩, h, fun x ↦ ?_⟩

Premises used: isClopen_discrete, Set.preimage, TopologicalSpace.Clopens.mk, Exists.intro, Singleton.singleton, IsClopen.preimage
-- Module: Mathlib.Topology.Separation.DisjointCover
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)
inst_5 : CommMonoid V
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
g : X → Fin n
h : Fin n → V
hg : Continuous[inst, _] g
hgh : ∀ (x : X), Membership.mem (α := V × V) S (((f : (a : X) → V) x, h (g x)) : V × V)
refine :
  ∀ (x : X),
    Membership.mem (α := V × V) S
      (((f : (a : X) → V) x,
          ∏ n_1 : Fin n,
            (↑((fun (i : Fin n) ↦ { carrier := g ⁻¹' {i}, isClopen' := ⋯ : Clopens X }) n_1) : Set X).mulIndicator
              (fun (x : X) ↦ h n_1) x) :
        V × V)
⊢ ∃ (n : ℕ) (U : Fin n → Clopens X) (v : Fin n → V),
    ∀ (x : X),
      Membership.mem (α := V × V) S
        (((f : (a : X) → V) x, ∏ n : Fin n, (↑(U n) : Set X).mulIndicator (fun (x : X) ↦ v n) x) : V × V)

Tactic:
refine ⟨n, fun i ↦ ⟨_, (isClopen_discrete {i}).preimage hg⟩, h, fun x ↦ ?_⟩
-- Module: Mathlib.Topology.Separation.DisjointCover
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)
inst_5 : CommMonoid V
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
g : X → Fin n
h : Fin n → V
hg : Continuous[inst, _] g
hgh : ∀ (x : X), Membership.mem (α := V × V) S (((f : (a : X) → V) x, h (g x)) : V × V)
x : X
⊢ Membership.mem (α := V × V) S (((f : (a : X) → V) x, h (g x)) : V × V)

Tactic:
hgh x
-- Module: Mathlib.Topology.Separation.DisjointCover
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)
inst_5 : CommMonoid V
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
g : X → Fin n
h : Fin n → V
hg : Continuous[inst, _] g
hgh : ∀ (x : X), Membership.mem (α := V × V) S (((f : (a : X) → V) x, h (g x)) : V × V)
x : X
h₁ :
  ∏ n_1 : Fin n,
      (↑((fun (i : Fin n) ↦ { carrier := g ⁻¹' {i}, isClopen' := ⋯ : Clopens X }) n_1) : Set X).mulIndicator
        (fun (x : X) ↦ h n_1) x =
    h (g x)
⊢ Membership.mem (α := V × V) S
    (((f : (a : X) → V) x,
        ∏ n_1 : Fin n,
          (↑((fun (i : Fin n) ↦ { carrier := g ⁻¹' {i}, isClopen' := ⋯ : Clopens X }) n_1) : Set X).mulIndicator
            (fun (x : X) ↦ h n_1) x) :
      V × V)

Tactic:
convert! hgh x
-- Module: Mathlib.Topology.Separation.DisjointCover
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)
inst_5 : CommMonoid V
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
g : X → Fin n
h : Fin n → V
hg : Continuous[inst, _] g
hgh : ∀ (x : X), Membership.mem (α := V × V) S (((f : (a : X) → V) x, h (g x)) : V × V)
x : X
⊢ ∏ n_1 : Fin n,
      (↑((fun (i : Fin n) ↦ { carrier := g ⁻¹' {i}, isClopen' := ⋯ : Clopens X }) n_1) : Set X).mulIndicator
        (fun (x : X) ↦ h n_1) x =
    h (g x)

Tactic:
(Fintype.prod_eq_single _ fun i hi ↦ mulIndicator_of_notMem hi.symm _).trans
    (mulIndicator_of_mem rfl _)

Premises used: Set.Mem, Set.mulIndicator, setOf, Set.mulIndicator_of_notMem, Ne.symm, Set.preimage, Set.singleton, Set.mulIndicator_of_mem, rfl, Fintype.prod_eq_single, Eq.trans
-- Module: Mathlib.Topology.Separation.DisjointCover
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)
inst_5 : CommMonoid V
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
g : X → Fin n
h : Fin n → V
hg : Continuous[inst, _] g
hgh : ∀ (x : X), Membership.mem (α := V × V) S (((f : (a : X) → V) x, h (g x)) : V × V)
x : X
⊢ ∏ n_1 : Fin n,
      (↑((fun (i : Fin n) ↦ { carrier := g ⁻¹' {i}, isClopen' := ⋯ : Clopens X }) n_1) : Set X).mulIndicator
        (fun (x : X) ↦ h n_1) x =
    h (g x)

Tactic:
exact (Fintype.prod_eq_single _ fun i hi ↦ mulIndicator_of_notMem hi.symm _).trans
    (mulIndicator_of_mem rfl _)

Premises used: Set.mulIndicator_of_notMem, Ne.symm, Set.mulIndicator_of_mem, rfl, Fintype.prod_eq_single, Eq.trans
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
inst_1 : T1Space X
⊢ IsGδ (X := X) {x}ᶜ

Tactic:
isOpen_compl_singleton.isGδ

Premises used: isOpen_compl_singleton, IsOpen.isGδ
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : T1Space X
hs : s.Countable
rw : IsGδ.{u_1} (X := X) (⋂ i ∈ s, {i}ᶜ)
⊢ IsGδ sᶜ

Tactic:
rw [← biUnion_of_singleton s, compl_iUnion₂]

Premises used: Set.biUnion_of_singleton, Set.compl_iUnion₂
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : T1Space X
hs : s.Countable
⊢ IsGδ.{u_1} (X := X) (⋂ i ∈ s, {i}ᶜ)

Tactic:
.biInter hs fun x _ => .compl_singleton x

Premises used: IsGδ.compl_singleton, IsGδ.biInter
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : T1Space X
hs : s.Countable
⊢ IsGδ.{u_1} (X := X) (⋂ i ∈ s, {i}ᶜ)

Tactic:
exact .biInter hs fun x _ => .compl_singleton x
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : T1Space X
hs : s.Finite
⊢ IsGδ sᶜ

Tactic:
hs.countable.isGδ_compl

Premises used: Set.Countable.isGδ_compl, Set.Finite.countable
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
inst_1 : T1Space X
hs : s.Subsingleton
⊢ IsGδ sᶜ

Tactic:
hs.finite.isGδ_compl

Premises used: Set.Finite.isGδ_compl, Set.Subsingleton.finite
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Finset X
⊢ IsGδ (↑s : Set X)ᶜ

Tactic:
s.finite_toSet.isGδ_compl

Premises used: Set.Finite.isGδ_compl, Finset.finite_toSet
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : FirstCountableTopology X
inst_2 : T1Space X
x : X
rcases :
  ∀ (U : ℕ → Set X) (hU : ∀ (i : ℕ), x ∈ U i ∧ IsOpen[inst] (U i)) (h_basis : (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ U i),
    IsGδ (X := X) {x}
⊢ IsGδ (X := X) {x}

Tactic:
rcases (nhds_basis_opens x).exists_antitone_subbasis with ⟨U, hU, h_basis⟩

Premises used: Filter.HasBasis.exists_antitone_subbasis, nhds_basis_opens
-- Module: Mathlib.Topology.Separation.GDelta
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : FirstCountableTopology X
inst_2 : T1Space X
x : X
U : ℕ → Set X
hU : ∀ (i : ℕ), x ∈ U i ∧ IsOpen[inst] (U i)
h_basis : (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ U i
rw : IsGδ.{u_1} (X := X) (⋂ (i : ℕ), ⋂ (_ : True), U i)
⊢ IsGδ (X := X) {x}

Tactic:
rw [← biInter_basis_nhds h_basis.toHasBasis]

Premises used: Filter.HasAntitoneBasis.toHasBasis, biInter_basis_nhds