awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
h : TotallyDisconnectedSpace α
x : α
⊢ IsPreconnected (connectedComponent x)

Tactic:
exact isPreconnected_connectedComponent

Premises used: isPreconnected_connectedComponent
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
mpr : IsTotallyDisconnected.{u} (α := α) univ
⊢ TotallyDisconnectedSpace α

Tactic:
constructor
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
s : Set α
s_sub : s ⊆ univ
hs : IsPreconnected s
mpr : ∀ (s_sub : Subset.{u} (α := Set α) ∅ univ) (hs : IsPreconnected.{u} (α := α) ∅), Set.Subsingleton.{u} (α := α) ∅
mpr₁ : ∀ (x : α) (x_in : x ∈ s), s.Subsingleton
⊢ s.Subsingleton

Tactic:
rcases eq_empty_or_nonempty s with (rfl | ⟨x, x_in⟩)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
s_sub : Subset.{u} (α := Set α) ∅ univ
hs : IsPreconnected.{u} (α := α) ∅
⊢ Set.Subsingleton.{u} (α := α) ∅

Tactic:
subsingleton_empty

Premises used: Set.subsingleton_empty
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
s_sub : Subset.{u} (α := Set α) ∅ univ
hs : IsPreconnected.{u} (α := α) ∅
⊢ Set.Subsingleton.{u} (α := α) ∅

Tactic:
exact subsingleton_empty

Premises used: Set.subsingleton_empty
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
s : Set α
s_sub : s ⊆ univ
hs : IsPreconnected s
x : α
x_in : x ∈ s
⊢ s.Subsingleton

Tactic:
(h x).anti (hs.subset_connectedComponent x_in)

Premises used: Set.Subsingleton.anti, IsPreconnected.subset_connectedComponent
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
h : ∀ (x : α), (connectedComponent x).Subsingleton
s : Set α
s_sub : s ⊆ univ
hs : IsPreconnected s
x : α
x_in : x ∈ s
⊢ s.Subsingleton

Tactic:
exact (h x).anti (hs.subset_connectedComponent x_in)

Premises used: Set.Subsingleton.anti, IsPreconnected.subset_connectedComponent
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
rw : (∀ (x : α), (connectedComponent x).Subsingleton) ↔ ∀ (x : α), connectedComponent x = {x}
⊢ TotallyDisconnectedSpace α ↔ ∀ (x : α), connectedComponent x = {x}

Tactic:
rw [totallyDisconnectedSpace_iff_connectedComponent_subsingleton]

Premises used: totallyDisconnectedSpace_iff_connectedComponent_subsingleton
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
⊢ (∀ (x : α), (connectedComponent x).Subsingleton) ↔ ∀ (x : α), connectedComponent x = {x}

Tactic:
forall_congr' fun x => ?_

Premises used: forall_congr'
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
refine : ∀ (x : α), (connectedComponent x).Subsingleton ↔ connectedComponent x = {x}
⊢ (∀ (x : α), (connectedComponent x).Subsingleton) ↔ ∀ (x : α), connectedComponent x = {x}

Tactic:
refine forall_congr' fun x => ?_

Premises used: forall_congr'
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
x : α
rw : x ∈ connectedComponent x
⊢ (connectedComponent x).Subsingleton ↔ connectedComponent x = {x}

Tactic:
rw [subsingleton_iff_singleton]

Premises used: Set.subsingleton_iff_singleton
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
x : α
⊢ x ∈ connectedComponent x

Tactic:
mem_connectedComponent

Premises used: mem_connectedComponent
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
x : α
⊢ x ∈ connectedComponent x

Tactic:
exact mem_connectedComponent

Premises used: mem_connectedComponent
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : TotallyDisconnectedSpace α
x : α
⊢ connectedComponent x = {x}

Tactic:
totallyDisconnectedSpace_iff_connectedComponent_singleton.1 ‹_› x

Premises used: totallyDisconnectedSpace_iff_connectedComponent_singleton, Iff.mp
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace β
f : α → β
h : Continuous[inst, inst_1] f
a : α
⊢ f '' connectedComponent a = {f a}

Tactic:
(Set.subsingleton_iff_singleton <| mem_image_of_mem f mem_connectedComponent).mp
    (isPreconnected_connectedComponent.image f h.continuousOn).subsingleton

Premises used: Continuous.continuousOn, mem_connectedComponent, IsPreconnected.image, IsPreconnected.subsingleton, isPreconnected_connectedComponent, Set.mem_image_of_mem, Set.subsingleton_iff_singleton, Iff.mp
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : TotallyDisconnectedSpace α
s : Set α
⊢ IsTotallyDisconnected s

Tactic:
fun t _ ht =>
  TotallyDisconnectedSpace.isTotallyDisconnected_univ _ t.subset_univ ht

Premises used: Set.subset_univ, TotallyDisconnectedSpace.isTotallyDisconnected_univ, IsTotallyDisconnected
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : PreconnectedSpace α
inst_3 : TotallyDisconnectedSpace β
f : α → β
hf : Continuous[inst, inst_1] f
i j : α
⊢ f i = f j

Tactic:
(isPreconnected_univ.image f hf.continuousOn).subsingleton ⟨i, trivial, rfl⟩ ⟨j, trivial, rfl⟩

Premises used: Continuous.continuousOn, trivial, IsPreconnected.image, IsPreconnected.subsingleton, And.intro, Exists.intro, PreconnectedSpace.isPreconnected_univ, rfl
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
ι : Type u_1
X_1 : ι → Type u_2
inst : TopologicalSpace α
s t u v : Set α
X : Type u_3
Y : Type u_4
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : TotallyDisconnectedSpace Y
inst_4 : ConnectedSpace X
y : Y
⊢ Continuous[inst_1, inst_2] fun (x : X) ↦ y

Tactic:
fun_prop
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
s : Set α
inst_1 : TopologicalSpace β
f : α → β
hf : ContinuousOn f s
hf' : Injective f
h : IsTotallyDisconnected (f '' s)
⊢ IsTotallyDisconnected s

Tactic:
fun _t hts ht _x x_in _y y_in =>
  hf' <|
    h _ (image_mono hts) (ht.image f <| hf.mono hts) (mem_image_of_mem f x_in)
      (mem_image_of_mem f y_in)

Premises used: Set.image_mono, IsPreconnected.image, Set.mem_image_of_mem, Set.Subsingleton, ContinuousOn.mono, Set.image, IsTotallyDisconnected
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
h : IsTotallyDisconnected (f '' s)
⊢ IsTotallyDisconnected s

Tactic:
isTotallyDisconnected_of_image hf.continuous.continuousOn hf.injective h

Premises used: Continuous.continuousOn, isTotallyDisconnected_of_image, Topology.IsEmbedding.injective, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
⊢ IsTotallyDisconnected (f '' s) ↔ IsTotallyDisconnected s

Tactic:
⟨hf.isTotallyDisconnected, fun hs u hus hu ↦ ?_⟩

Premises used: Iff.intro, Topology.IsEmbedding.isTotallyDisconnected
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
refine : ∀ (hs : IsTotallyDisconnected s) (u : Set β) (hus : u ⊆ f '' s) (hu : IsPreconnected u), u.Subsingleton
⊢ IsTotallyDisconnected (f '' s) ↔ IsTotallyDisconnected s

Tactic:
refine ⟨hf.isTotallyDisconnected, fun hs u hus hu ↦ ?_⟩
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
hs : IsTotallyDisconnected s
u : Set β
hus : u ⊆ f '' s
hu : IsPreconnected u
rwa : u ∩ f '' s = u
rwa₁ rwa₂ rwa₃ rwa₄ : u ⊆ f '' s
⊢ f '' (f ⁻¹' u ∩ s) = u

Tactic:
rwa [image_preimage_inter, inter_eq_left]

Premises used: Set.inter_eq_left, Set.image_preimage_inter
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
hs : IsTotallyDisconnected s
u : Set β
hus : u ⊆ f '' s
hu : IsPreconnected u
obtain : ∀ (v : Set α) (hvs : v ⊆ s) (hus : f '' v ⊆ f '' s) (hu : IsPreconnected (f '' v)), (f '' v).Subsingleton
⊢ u.Subsingleton

Tactic:
obtain ⟨v, hvs, rfl⟩ : ∃ v, v ⊆ s ∧ f '' v = u :=
    ⟨f ⁻¹' u ∩ s, inter_subset_right, by rwa [image_preimage_inter, inter_eq_left]⟩

Premises used: rfl
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
hs : IsTotallyDisconnected s
v : Set α
hvs : v ⊆ s
hus : f '' v ⊆ f '' s
hu : IsPreconnected (f '' v)
⊢ IsPreconnected v

Tactic:
rw [hf.isInducing.isPreconnected_image] at hu

Premises used: Topology.IsInducing.isPreconnected_image, Topology.IsEmbedding.isInducing
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
hs : IsTotallyDisconnected s
v : Set α
hvs : v ⊆ s
hus : f '' v ⊆ f '' s
hu : IsPreconnected v
⊢ (f '' v).Subsingleton

Tactic:
(hs v hvs hu).image _

Premises used: Set.Subsingleton.image
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
hs : IsTotallyDisconnected s
v : Set α
hvs : v ⊆ s
hus : f '' v ⊆ f '' s
hu : IsPreconnected v
⊢ (f '' v).Subsingleton

Tactic:
exact (hs v hvs hu).image _

Premises used: Set.Subsingleton.image
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsEmbedding f
rw : IsTotallyDisconnected (range f) ↔ IsTotallyDisconnected.{u} (α := α) univ
rw₁ : IsTotallyDisconnected (f '' univ) ↔ IsTotallyDisconnected.{u} (α := α) univ
rw₂ rw₃ : IsTotallyDisconnected.{u} (α := α) univ ↔ IsTotallyDisconnected.{u} (α := α) univ
⊢ IsTotallyDisconnected (range f) ↔ TotallyDisconnectedSpace α

Tactic:
rw [totallyDisconnectedSpace_iff, ← image_univ, hf.isTotallyDisconnected_image]

Premises used: Set.image_univ, Topology.IsEmbedding.isTotallyDisconnected_image, totallyDisconnectedSpace_iff
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
rw :
  IsTotallyDisconnected.{u} (α := α) (range (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) ↔
    IsTotallyDisconnected s
rw₁ rw₂ : IsTotallyDisconnected s ↔ IsTotallyDisconnected s
⊢ TotallyDisconnectedSpace.{u} (↑s : Type u) ↔ IsTotallyDisconnected s

Tactic:
rw [← IsEmbedding.subtypeVal.isTotallyDisconnected_range, Subtype.range_val]

Premises used: Subtype.range_val, Topology.IsEmbedding.isTotallyDisconnected_range, Topology.IsEmbedding.subtypeVal
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α_1 : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α_1
s t u v : Set α_1
α : Type u_3
p : α → Prop
inst_1 : TopologicalSpace α
inst_2 : TotallyDisconnectedSpace α
⊢ TotallyDisconnectedSpace.{u_3} (Subtype p)

Tactic:
totallyDisconnectedSpace_subtype_iff.2 (isTotallyDisconnected_of_totallyDisconnectedSpace _)

Premises used: Iff.mpr, Set.Mem, totallyDisconnectedSpace_subtype_iff, isTotallyDisconnected_of_totallyDisconnectedSpace
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
⊢ IsTotallySeparated.{u} (α := α) ∅

Tactic:
fun _ => False.elim

Premises used: Set.Mem, False.elim, IsTotallySeparated, Set.Pairwise
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
x : α
⊢ IsTotallySeparated (α := α) {x}

Tactic:
fun _ hp _ hq hpq =>
  (hpq <| (eq_of_mem_singleton hp).symm ▸ (eq_of_mem_singleton hq).symm).elim

Premises used: Set.eq_of_mem_singleton, False.elim, IsTotallySeparated, Eq.rec, Set.Pairwise, Eq.symm
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
by_contra : ∀ (h : ¬x = y), False
⊢ x = y

Tactic:
by_contra h
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
s : _root_.Set α
H : IsTotallySeparated s
t : _root_.Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
h : ¬x = y
Set :
  ∀ (u v : _root_.Set α) (hu : IsOpen[inst] u) (hv : IsOpen[inst] v) (hxu : x ∈ u) (hyv : y ∈ v) (hs : s ⊆ u ∪ v)
    (huv : Disjoint u v), False
⊢ False

Tactic:
obtain
    ⟨u : Set α, v : Set α, hu : IsOpen u, hv : IsOpen v, hxu : x ∈ u, hyv : y ∈ v, hs : s ⊆ u ∪ v,
      huv⟩ :=
    H (hts x_in) (hts y_in) h

Premises used: Set
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
h : ¬x = y
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hxu : x ∈ u
hyv : y ∈ v
hs : s ⊆ u ∪ v
huv : Disjoint u v
⊢ False

Tactic:
(ht _ _ hu hv (hts.trans hs) ⟨x, x_in, hxu⟩ ⟨y, y_in, hyv⟩).ne_empty ?_

Premises used: Set.Nonempty.ne_empty, HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
h : ¬x = y
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hxu : x ∈ u
hyv : y ∈ v
hs : s ⊆ u ∪ v
huv : Disjoint u v
refine : t ∩ (u ∩ v) = ∅
⊢ False

Tactic:
refine (ht _ _ hu hv (hts.trans hs) ⟨x, x_in, hxu⟩ ⟨y, y_in, hyv⟩).ne_empty ?_

Premises used: Set.Nonempty.ne_empty, HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
H : IsTotallySeparated s
t : Set α
hts : t ⊆ s
ht : IsPreconnected t
x : α
x_in : x ∈ t
y : α
y_in : y ∈ t
h : ¬x = y
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hxu : x ∈ u
hyv : y ∈ v
hs : s ⊆ u ∪ v
huv : Disjoint u v
rw : t ∩ ∅ = ∅
rw₁ rw₂ : Eq.{u + 1} (α := Set α) ∅ ∅
⊢ t ∩ (u ∩ v) = ∅

Tactic:
rw [huv.inter_eq, inter_empty]

Premises used: Set.inter_empty, Disjoint.inter_eq
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α_1 : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α_1
s t u v : Set α_1
α : Type u
inst_1 : TopologicalSpace α
inst_2 : TotallySeparatedSpace α
⊢ TotallyDisconnectedSpace α

Tactic:
⟨TotallySeparatedSpace.isTotallySeparated_univ.isTotallyDisconnected⟩

Premises used: TotallyDisconnectedSpace.mk, IsTotallySeparated.isTotallyDisconnected, TotallySeparatedSpace.isTotallySeparated_univ
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α_1 : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α_1
s t u v : Set α_1
α : Type u_3
inst_1 : TopologicalSpace α
inst_2 : DiscreteTopology α
⊢ TotallySeparatedSpace α

Tactic:
⟨fun _ _ b _ h => ⟨{b}ᶜ, {b}, isOpen_discrete _, isOpen_discrete _, h, rfl,
    (compl_union_self _).symm.subset, disjoint_compl_left⟩⟩

Premises used: Compl.compl, disjoint_compl_left, TotallySeparatedSpace.mk, Eq.subset, And.intro, isOpen_discrete, Exists.intro, Set.compl_union_self, Singleton.singleton, Eq.symm, rfl
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u_3
inst : TopologicalSpace α
simp :
  (∀ ⦃x y : α⦄,
      x ≠ y →
        ∃ (u : Set α) (v : Set α), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) ↔
    Pairwise fun (x1 x2 : α) ↦ ∃ (U : Set α), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ
⊢ TotallySeparatedSpace α ↔ Pairwise fun (x1 x2 : α) ↦ ∃ (U : Set α), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ

Tactic:
simp only [totallySeparatedSpace_iff, IsTotallySeparated, Set.Pairwise, mem_univ, true_implies]

Premises used: IsTotallySeparated, Set.Pairwise, totallySeparatedSpace_iff, true_implies, Set.mem_univ
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u_3
inst : TopologicalSpace α
⊢ (∀ ⦃x y : α⦄,
      x ≠ y →
        ∃ (u : Set α) (v : Set α), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) ↔
    Pairwise fun (x1 x2 : α) ↦ ∃ (U : Set α), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ

Tactic:
forall₃_congr fun x y _ ↦
    ⟨fun ⟨U, V, hU, hV, Ux, Vy, f, disj⟩ ↦ ?_, fun ⟨U, hU, Ux, Ucy⟩ ↦ ?_⟩

Premises used: Compl.compl, Set.univ, _private.0.totallySeparatedSpace_iff_exists_isClopen.match_3, forall₃_congr, Disjoint, Membership.mem, Exists, HasSubset.Subset, And, _private.0.totallySeparatedSpace_iff_exists_isClopen.match_2, Iff.intro, Pairwise, IsOpen, Union.union, IsClopen
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u_3
inst : TopologicalSpace α
refine_1 :
  ∀ (x y : α),
    x ≠ y →
      (∃ (u : Set α) (v : Set α), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) →
        ∀ (U V : Set α) (hU : IsOpen[inst] U) (hV : IsOpen[inst] V) (Ux : x ∈ U) (Vy : y ∈ V) (f : univ ⊆ U ∪ V)
          (disj : Disjoint U V), (fun (x1 x2 : α) ↦ ∃ (U : Set α), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ) x y
refine_2 :
  ∀ (x y : α),
    x ≠ y →
      (fun (x1 x2 : α) ↦ ∃ (U : Set α), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ) x y →
        ∀ (U : Set α) (hU : IsClopen U) (Ux : x ∈ U) (Ucy : y ∈ Uᶜ),
          ∃ (u : Set α) (v : Set α), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
⊢ (∀ ⦃x y : α⦄,
      x ≠ y →
        ∃ (u : Set α) (v : Set α), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) ↔
    Pairwise fun (x1 x2 : α) ↦ ∃ (U : Set α), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ

Tactic:
refine forall₃_congr fun x y _ ↦
    ⟨fun ⟨U, V, hU, hV, Ux, Vy, f, disj⟩ ↦ ?_, fun ⟨U, hU, Ux, Ucy⟩ ↦ ?_⟩

Premises used: forall₃_congr, Iff.intro
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u_3
inst : TopologicalSpace α
x y : α
h : x ≠ y
h_1 : ∃ (u : Set α) (v : Set α), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
U V : Set α
hU : IsOpen[inst] U
hV : IsOpen[inst] V
Ux : x ∈ U
Vy : y ∈ V
f : univ ⊆ U ∪ V
disj : Disjoint U V
⊢ (fun (x1 x2 : α) ↦ ∃ (U : Set α), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ) x y

Tactic:
⟨U, isClopen_of_disjoint_cover_open f hU hV disj,
      Ux, fun Uy ↦ Set.disjoint_iff.mp disj ⟨Uy, Vy⟩⟩

Premises used: isClopen_of_disjoint_cover_open, And.intro, Exists.intro, Iff.mp, Set.disjoint_iff
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u_3
inst : TopologicalSpace α
x y : α
h : x ≠ y
h_1 : ∃ (u : Set α) (v : Set α), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
U V : Set α
hU : IsOpen[inst] U
hV : IsOpen[inst] V
Ux : x ∈ U
Vy : y ∈ V
f : univ ⊆ U ∪ V
disj : Disjoint U V
⊢ (fun (x1 x2 : α) ↦ ∃ (U : Set α), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ) x y

Tactic:
exact ⟨U, isClopen_of_disjoint_cover_open f hU hV disj,
      Ux, fun Uy ↦ Set.disjoint_iff.mp disj ⟨Uy, Vy⟩⟩
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u_3
inst : TopologicalSpace α
x y : α
h : x ≠ y
h_1 : (fun (x1 x2 : α) ↦ ∃ (U : Set α), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ) x y
U : Set α
hU : IsClopen U
Ux : x ∈ U
Ucy : y ∈ Uᶜ
⊢ ∃ (u : Set α) (v : Set α), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
⟨U, Uᶜ, hU.2, hU.compl.2, Ux, Ucy, (Set.union_compl_self U).ge, disjoint_compl_right⟩

Premises used: Eq.ge, Compl.compl, IsClopen.compl, Set.union_compl_self, And.right, And.intro, Exists.intro, disjoint_compl_right
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u_3
inst : TopologicalSpace α
x y : α
h : x ≠ y
h_1 : (fun (x1 x2 : α) ↦ ∃ (U : Set α), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ) x y
U : Set α
hU : IsClopen U
Ux : x ∈ U
Ucy : y ∈ Uᶜ
⊢ ∃ (u : Set α) (v : Set α), IsOpen[inst] u ∧ IsOpen[inst] v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
exact ⟨U, Uᶜ, hU.2, hU.compl.2, Ux, Ucy, (Set.union_compl_self U).ge, disjoint_compl_right⟩
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : TotallySeparatedSpace α
⊢ Pairwise fun (x1 x2 : α) ↦ ∃ (U : Set α), IsClopen U ∧ x1 ∈ U ∧ x2 ∈ Uᶜ

Tactic:
totallySeparatedSpace_iff_exists_isClopen.mp ‹_›

Premises used: Iff.mp, totallySeparatedSpace_iff_exists_isClopen
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace β
f : α → β
h : Continuous[inst, inst_1] f
a b : α
hab : connectedComponent a = connectedComponent b
⊢ f a = f b

Tactic:
singleton_eq_singleton_iff.1 <|
    h.image_connectedComponent_eq_singleton a ▸
      h.image_connectedComponent_eq_singleton b ▸ hab ▸ rfl

Premises used: Eq.rec, Set.singleton_eq_singleton_iff, Iff.mp, Continuous.image_connectedComponent_eq_singleton, rfl
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace β
f : α → β
h : Continuous[inst, inst_1] f
⊢ ∀ (a b : α) (hab : connectedComponent a = connectedComponent b), f a = f b

Tactic:
h.image_eq_of_connectedComponent_eq

Premises used: Continuous.image_eq_of_connectedComponent_eq
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace β
f : α → β
h : Continuous[inst, inst_1] f
⊢ ∀ (a b : α), (connectedComponentSetoid α : α → α → Prop) a b → f a = f b

Tactic:
convert! h.image_eq_of_connectedComponent_eq

Premises used: Continuous.image_eq_of_connectedComponent_eq
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace β
f : α → β
h : Continuous[inst, inst_1] f
x : α
⊢ h.connectedComponentsLift (ConnectedComponents.mk x) = f x

Tactic:
rfl

Premises used: Quotient.liftOn', Continuous.connectedComponentsLift, rfl
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace β
f : α → β
h : Continuous[inst, inst_1] f
⊢ h.connectedComponentsLift ∘ ConnectedComponents.mk = f

Tactic:
rfl

Premises used: Quotient.liftOn', Continuous.connectedComponentsLift, rfl
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
inst : TopologicalSpace α
β : Sort u_3
g₁ g₂ : ConnectedComponents α → β
hg : g₁ ∘ ConnectedComponents.mk = g₂ ∘ ConnectedComponents.mk
⊢ g₁ = g₂

Tactic:
ConnectedComponents.surjective_coe.injective_comp_right hg

Premises used: ConnectedComponents.surjective_coe, Function.Surjective.injective_comp_right
-- Module: Mathlib.Topology.Connected.TotallyDisconnected
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TotallyDisconnectedSpace β
f : α → β
h : Continuous[inst, inst_1] f
g : ConnectedComponents α → β
hg : g ∘ ConnectedComponents.mk = f
⊢ g = h.connectedComponentsLift

Tactic:
connectedComponents_lift_unique' <| hg.trans h.connectedComponentsLift_comp_coe.symm

Premises used: connectedComponents_lift_unique', Continuous.connectedComponentsLift_comp_coe, Eq.symm, Eq.trans