awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
t : Set β
ht : IsPreconnected t
⊢ IsPreconnected (α := α ⊕ β) (inr '' t)

Tactic:
exact ht.image _ continuous_inr.continuousOn

Premises used: Continuous.continuousOn, continuous_inr, IsPreconnected.image
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
inst_1 : ConnectedSpace α
inst_2 : (i : ι) → TopologicalSpace (X i)
f : α → (i : ι) × X i
hf : Continuous[inst, instTopologicalSpaceSigma] f
rcases :
  ∀ (i : ι) (s : Set (X i)) (hs : range f = Sigma.mk (β := fun (i : ι) ↦ X i) i '' s),
    ∃ (i : ι), range f ⊆ range (Sigma.mk (β := fun (i : ι) ↦ X i) i)
⊢ ∃ (i : ι), range f ⊆ range (Sigma.mk (β := fun (i : ι) ↦ X i) i)

Tactic:
rcases Sigma.isConnected_iff.1 (isConnected_range hf) with ⟨i, s, -, hs⟩

Premises used: isConnected_range, Iff.mp, Sigma.isConnected_iff
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
inst_1 : ConnectedSpace α
inst_2 : (i : ι) → TopologicalSpace (X i)
f : α → (i : ι) × X i
hf : Continuous[inst, instTopologicalSpaceSigma] f
i : ι
s : Set (X i)
hs : range f = Sigma.mk (β := fun (i : ι) ↦ X i) i '' s
⊢ ∃ (i : ι), range f ⊆ range (Sigma.mk (β := fun (i : ι) ↦ X i) i)

Tactic:
⟨i, hs.trans_subset (image_subset_range _ _)⟩

Premises used: Set.image_subset_range, Exists.intro, Eq.trans_subset
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
inst_1 : ConnectedSpace α
inst_2 : (i : ι) → TopologicalSpace (X i)
f : α → (i : ι) × X i
hf : Continuous[inst, instTopologicalSpaceSigma] f
i : ι
s : Set (X i)
hs : range f = Sigma.mk (β := fun (i : ι) ↦ X i) i '' s
⊢ ∃ (i : ι), range f ⊆ range (Sigma.mk (β := fun (i : ι) ↦ X i) i)

Tactic:
exact ⟨i, hs.trans_subset (image_subset_range _ _)⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
inst_1 : ConnectedSpace α
inst_2 : (i : ι) → TopologicalSpace (X i)
f : α → (i : ι) × X i
hf : Continuous[inst, instTopologicalSpaceSigma] f
obtain :
  ∀ (i : ι) (hi : range f ⊆ range (Sigma.mk (β := fun (i : ι) ↦ X i) i)),
    ∃ (i : ι) (g : α → X i), Continuous[inst, inst_2 i] g ∧ f = Sigma.mk (β := X) i ∘ g
⊢ ∃ (i : ι) (g : α → X i), Continuous[inst, inst_2 i] g ∧ f = Sigma.mk (β := X) i ∘ g

Tactic:
obtain ⟨i, hi⟩ : ∃ i, range f ⊆ range (.mk i) := by
    rcases Sigma.isConnected_iff.1 (isConnected_range hf) with ⟨i, s, -, hs⟩
    exact ⟨i, hs.trans_subset (image_subset_range _ _)⟩

Premises used: Set.range
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
inst_1 : ConnectedSpace α
inst_2 : (i : ι) → TopologicalSpace (X i)
f : α → (i : ι) × X i
hf : Continuous[inst, instTopologicalSpaceSigma] f
i : ι
hi : range f ⊆ range (Sigma.mk (β := fun (i : ι) ↦ X i) i)
rcases :
  ∀ (g : α → X i) (hf : Continuous[inst, instTopologicalSpaceSigma] (Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ g))
    (hi : range (Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ g) ⊆ range (Sigma.mk (β := fun (i : ι) ↦ X i) i)),
    ∃ (i_1 : ι) (g_1 : α → X i_1),
      Continuous[inst, inst_2 i_1] g_1 ∧ Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ g = Sigma.mk (β := X) i_1 ∘ g_1
⊢ ∃ (i : ι) (g : α → X i), Continuous[inst, inst_2 i] g ∧ f = Sigma.mk (β := X) i ∘ g

Tactic:
rcases range_subset_range_iff_exists_comp.1 hi with ⟨g, rfl⟩

Premises used: Set.range_subset_range_iff_exists_comp, Iff.mp, rfl
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
inst_1 : ConnectedSpace α
inst_2 : (i : ι) → TopologicalSpace (X i)
i : ι
g : α → X i
hf : Continuous[inst, instTopologicalSpaceSigma] (Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ g)
hi : range (Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ g) ⊆ range (Sigma.mk (β := fun (i : ι) ↦ X i) i)
⊢ ∃ (i_1 : ι) (g_1 : α → X i_1),
    Continuous[inst, inst_2 i_1] g_1 ∧ Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ g = Sigma.mk (β := X) i_1 ∘ g_1

Tactic:
⟨i, g, ?_, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
inst_1 : ConnectedSpace α
inst_2 : (i : ι) → TopologicalSpace (X i)
i : ι
g : α → X i
hf : Continuous[inst, instTopologicalSpaceSigma] (Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ g)
hi : range (Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ g) ⊆ range (Sigma.mk (β := fun (i : ι) ↦ X i) i)
refine : Continuous[inst, inst_2 i] g
⊢ ∃ (i_1 : ι) (g_1 : α → X i_1),
    Continuous[inst, inst_2 i_1] g_1 ∧ Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ g = Sigma.mk (β := X) i_1 ∘ g_1

Tactic:
refine ⟨i, g, ?_, rfl⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
X : ι → Type u_2
inst : TopologicalSpace α
inst_1 : ConnectedSpace α
inst_2 : (i : ι) → TopologicalSpace (X i)
i : ι
g : α → X i
hf : Continuous[inst, instTopologicalSpaceSigma] (Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ g)
hi : range (Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ g) ⊆ range (Sigma.mk (β := fun (i : ι) ↦ X i) i)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hf : Continuous[inst, inst_2 i] g)
    (hi : range (Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ g) ⊆ range (Sigma.mk (β := fun (i : ι) ↦ X i) i)),
    Continuous[inst, inst_2 i] g
⊢ Continuous[inst, inst_2 i] g

Tactic:
rwa [← IsEmbedding.sigmaMk.continuous_iff] at hf

Premises used: Topology.IsEmbedding.sigmaMk, Topology.IsEmbedding.continuous_iff
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s t : Set α
⊢ IsOpen[inst] s → IsOpen[inst] t → s ∪ t = univ → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty

Tactic:
simpa only [univ_inter, univ_subset_iff] using @PreconnectedSpace.isPreconnected_univ α _ _ s t

Premises used: Set.univ_subset_iff, Set.univ_inter, PreconnectedSpace.isPreconnected_univ
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : Set α
hs : IsClopen s
h : ¬(s = ∅ ∨ s = univ)
⊢ s.Nonempty ∧ sᶜ.Nonempty

Tactic:
simpa [nonempty_iff_ne_empty] using h

Premises used: Set.nonempty_iff_ne_empty
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
⊢ IsClopen.{u} (X := α) ∅

Tactic:
isClopen_empty

Premises used: isClopen_empty
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
⊢ IsClopen.{u} (X := α) univ

Tactic:
isClopen_univ

Premises used: isClopen_univ
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
⊢ IsClopen.{u} (X := α) ∅

Tactic:
exacts [isClopen_empty, isClopen_univ]

Premises used: isClopen_univ, isClopen_empty
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : Set α
h' : IsClopen s
h : s.Nonempty
⊢ s = univ

Tactic:
(isClopen_iff.mp h').resolve_left h.ne_empty

Premises used: Set.Nonempty.ne_empty, Or.resolve_left, isClopen_iff, Iff.mp
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsOpen[inst] u
huv : Disjoint (frontier u) v
⊢ IsClopen (X := (↑v : Type u_3)) (v ↓∩ u)

Tactic:
⟨?_, isOpen_induced hu (f := Subtype.val)⟩

Premises used: isOpen_induced, And.intro, IsClopen
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsOpen[inst] u
huv : Disjoint (frontier u) v
refine : IsClosed[instTopologicalSpaceSubtype] (v ↓∩ u)
⊢ IsClopen (X := (↑v : Type u_3)) (v ↓∩ u)

Tactic:
refine ⟨?_, isOpen_induced hu (f := Subtype.val)⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsOpen[inst] u
huv : Disjoint (frontier u) v
⊢ IsClosed[instTopologicalSpaceSubtype] (v ↓∩ u)

Tactic:
isClosed_induced_iff.mpr ⟨closure u, isClosed_closure, ?_⟩

Premises used: Iff.mpr, isClosed_induced_iff, closure, And.intro, Exists.intro, isClosed_closure
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsOpen[inst] u
huv : Disjoint (frontier u) v
refine : Eq (α := Set (↑v : Type u_3)) (v ↓∩ closure[inst] u) (v ↓∩ u)
⊢ IsClosed[instTopologicalSpaceSubtype] (v ↓∩ u)

Tactic:
refine isClosed_induced_iff.mpr ⟨closure u, isClosed_closure, ?_⟩

Premises used: Iff.mpr, isClosed_induced_iff, closure, And.intro, Exists.intro, isClosed_closure
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsOpen[inst] u
huv : Disjoint (frontier u) v
a :
  image (α := { x : X // x ∈ v }) (Subtype.val (p := fun (x : X) ↦ x ∈ v)) (v ↓∩ closure[inst] u) =
    image (α := { x : X // x ∈ v }) (Subtype.val (p := fun (x : X) ↦ x ∈ v)) (v ↓∩ u)
⊢ Eq (α := Set (↑v : Type u_3)) (v ↓∩ closure[inst] u) (v ↓∩ u)

Tactic:
apply image_val_injective

Premises used: Set.image_val_injective
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsOpen[inst] u
huv : Disjoint (frontier u) v
a : v ∩ closure[inst] u = v ∩ u
⊢ image (α := { x : X // x ∈ v }) (Subtype.val (p := fun (x : X) ↦ x ∈ v)) (v ↓∩ closure[inst] u) =
    image (α := { x : X // x ∈ v }) (Subtype.val (p := fun (x : X) ↦ x ∈ v)) (v ↓∩ u)

Tactic:
simp only [Subtype.image_preimage_coe]

Premises used: Subtype.image_preimage_coe
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
X : Type u_3
inst : TopologicalSpace X
u v : Set X
hu : IsOpen[inst] u
huv : Disjoint (frontier u) v
a : v ∩ (u ∪ frontier u) = v ∩ u
a₁ : v ∩ u ∪ v ∩ frontier u = v ∩ u
a₂ : v ∩ u ∪ frontier u ∩ v = v ∩ u
a₃ : v ∩ u ∪ ∅ = v ∩ u
a₄ a₅ : v ∩ u = v ∩ u
⊢ v ∩ closure[inst] u = v ∩ u

Tactic:
rw [closure_eq_self_union_frontier, inter_union_distrib_left, inter_comm _ (frontier u),
    huv.inter_eq, union_empty]

Premises used: frontier, Set.union_empty, Set.inter_comm, closure_eq_self_union_frontier, Disjoint.inter_eq, Set.inter_union_distrib_left
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
rw : ¬Nontrivial ι
⊢ Subsingleton ι

Tactic:
rw [← not_nontrivial_iff_subsingleton]

Premises used: not_nontrivial_iff_subsingleton
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
by_contra : ∀ (i j : ι) (h_ne : i ≠ j), False
⊢ ¬Nontrivial ι

Tactic:
by_contra ⟨i, j, h_ne⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : i ≠ j
⊢ s i ∩ s j = ∅

Tactic:
simpa only [← bot_eq_empty, eq_bot_iff, ← inf_eq_inter, ← disjoint_iff_inf_le] using h_disj h_ne

Premises used: Set.bot_eq_empty, Set.inf_eq_inter, disjoint_iff_inf_le, eq_bot_iff
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : i ≠ j
⊢ s i ∩ s j = ∅

Tactic:
replace h_ne : s i ∩ s j = ∅ := by
    simpa only [← bot_eq_empty, eq_bot_iff, ← inf_eq_inter, ← disjoint_iff_inf_le] using h_disj h_ne
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : s i ∩ s j = ∅
inl : ∀ (hi : s i = ∅), False
inr : ∀ (hi : s i = univ), False
⊢ False

Tactic:
rcases isClopen_iff.mp (h_clopen i) with hi | hi

Premises used: isClopen_iff, Iff.mp
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : s i ∩ s j = ∅
hi : s i = ∅
⊢ False

Tactic:
(h_nonempty i).ne_empty hi

Premises used: Set.Nonempty.ne_empty
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : s i ∩ s j = ∅
hi : s i = ∅
⊢ False

Tactic:
exact (h_nonempty i).ne_empty hi

Premises used: Set.Nonempty.ne_empty
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : s i ∩ s j = ∅
hi : s i = univ
⊢ s j = ∅

Tactic:
rw [hi, univ_inter] at h_ne

Premises used: Set.univ_inter
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : s i ∩ s j = ∅
hi : s i = univ
h_ne₁ : s j = ∅
⊢ s i = univ

Tactic:
rw [hi, univ_inter] at h_ne

Premises used: Set.univ_inter
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : s j = ∅
hi : s i = univ
⊢ False

Tactic:
(h_nonempty j).ne_empty h_ne

Premises used: Set.Nonempty.ne_empty
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : s j = ∅
hi : s i = univ
⊢ False

Tactic:
exact (h_nonempty j).ne_empty h_ne

Premises used: Set.Nonempty.ne_empty
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
⊢ Subsingleton ι

Tactic:
subsingleton_of_disjoint_isClopen h_nonempty h_disj (fun i ↦ ⟨?_, h_open i⟩)

Premises used: subsingleton_of_disjoint_isClopen, And.intro
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
refine : ∀ (i : ι), IsClosed[inst] (s i)
⊢ Subsingleton ι

Tactic:
refine subsingleton_of_disjoint_isClopen h_nonempty h_disj (fun i ↦ ⟨?_, h_open i⟩)

Premises used: subsingleton_of_disjoint_isClopen, And.intro
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
i : ι
rw : IsOpen[inst] (⋃ (i_1 : ι), s i_1 \ s i)
⊢ IsClosed[inst] (s i)

Tactic:
rw [← isOpen_compl_iff, compl_eq_univ_diff, ← h_Union, iUnion_diff]

Premises used: Set.iUnion_diff, Set.compl_eq_univ_diff, isOpen_compl_iff
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
i : ι
⊢ IsOpen[inst] (⋃ (i_1 : ι), s i_1 \ s i)

Tactic:
isOpen_iUnion (fun j ↦ ?_)

Premises used: isOpen_iUnion
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
i : ι
refine : ∀ (j : ι), IsOpen[inst] (s j \ s i)
⊢ IsOpen[inst] (⋃ (i_1 : ι), s i_1 \ s i)

Tactic:
refine isOpen_iUnion (fun j ↦ ?_)

Premises used: isOpen_iUnion
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
i j : ι
inl : IsOpen[inst] (s i \ s i)
inr : ∀ (h_ne : i ≠ j), IsOpen[inst] (s j \ s i)
⊢ IsOpen[inst] (s j \ s i)

Tactic:
rcases eq_or_ne i j with rfl | h_ne

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
i : ι
⊢ IsOpen[inst] (s i \ s i)

Tactic:
simp
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
i j : ι
h_ne : i ≠ j
⊢ IsOpen[inst] (s j \ s i)

Tactic:
simpa only [(h_disj h_ne.symm).sdiff_eq_left] using h_open j

Premises used: Ne.symm, Disjoint.sdiff_eq_left
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst_2 : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
⊢ Subsingleton ι

Tactic:
subsingleton_of_disjoint_isClopen h_nonempty h_disj (fun i ↦ ⟨h_closed i, ?_⟩)

Premises used: subsingleton_of_disjoint_isClopen, And.intro
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst_2 : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
refine : ∀ (i : ι), IsOpen[inst] (s i)
⊢ Subsingleton ι

Tactic:
refine subsingleton_of_disjoint_isClopen h_nonempty h_disj (fun i ↦ ⟨h_closed i, ?_⟩)

Premises used: subsingleton_of_disjoint_isClopen, And.intro
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst_2 : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
i : ι
rw : IsClosed[inst] (⋃ (i_1 : ι), s i_1 \ s i)
⊢ IsOpen[inst] (s i)

Tactic:
rw [← isClosed_compl_iff, compl_eq_univ_diff, ← h_Union, iUnion_diff]

Premises used: Set.iUnion_diff, Set.compl_eq_univ_diff, isClosed_compl_iff
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst_2 : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
i : ι
⊢ IsClosed[inst] (⋃ (i_1 : ι), s i_1 \ s i)

Tactic:
isClosed_iUnion_of_finite (fun j ↦ ?_)

Premises used: isClosed_iUnion_of_finite
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst_2 : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
i : ι
refine : ∀ (j : ι), IsClosed[inst] (s j \ s i)
⊢ IsClosed[inst] (⋃ (i_1 : ι), s i_1 \ s i)

Tactic:
refine isClosed_iUnion_of_finite (fun j ↦ ?_)

Premises used: isClosed_iUnion_of_finite
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst_2 : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
i j : ι
inl : IsClosed[inst] (s i \ s i)
inr : ∀ (h_ne : i ≠ j), IsClosed[inst] (s j \ s i)
⊢ IsClosed[inst] (s j \ s i)

Tactic:
rcases eq_or_ne i j with rfl | h_ne

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst_2 : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
i : ι
⊢ IsClosed[inst] (s i \ s i)

Tactic:
simp
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
ι : Type u_1
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst_2 : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst] (s i)
h_Union : Eq.{u + 1} (α := Set α) (⋃ (i : ι), s i) univ
i j : ι
h_ne : i ≠ j
⊢ IsClosed[inst] (s j \ s i)

Tactic:
simpa only [(h_disj h_ne.symm).sdiff_eq_left] using h_closed j

Premises used: Ne.symm, Disjoint.sdiff_eq_left
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : Set α
⊢ frontier s = ∅ ↔ s = ∅ ∨ s = univ

Tactic:
isClopen_iff_frontier_eq_empty.symm.trans isClopen_iff

Premises used: isClopen_iff, Iff.trans, isClopen_iff_frontier_eq_empty, Iff.symm
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
s : Set α
⊢ (frontier s).Nonempty ↔ s.Nonempty ∧ s ≠ univ

Tactic:
simp only [nonempty_iff_ne_empty, Ne, frontier_eq_empty_iff, not_or]

Premises used: Ne, not_or, frontier_eq_empty_iff, Set.nonempty_iff_ne_empty
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x
h' : IsTrans α P
x y : α
let : P x y
⊢ P x y

Tactic:
let u := {z | P x z}
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x
h' : IsTrans α P
x y : α
u : Set α := {z : α | P x z}
apply : ∀ (z : α) (hz : ∀ U ∈ 𝓝 z, (U ∩ u).Nonempty), z ∈ u
⊢ IsClosed[inst] u

Tactic:
apply isClosed_iff_nhds.2 (fun z hz ↦ ?_)

Premises used: Iff.mpr, isClosed_iff_nhds
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x
h' : IsTrans α P
x y : α
u : Set α := {z : α | P x z}
z : α
hz : ∀ U ∈ 𝓝 z, (U ∩ u).Nonempty
rcases : ∀ (t : α) (ht : Membership.mem (γ := Set α) {x : α | (fun (y : α) ↦ P z y ∧ P y z) x} t) (h't : t ∈ u), z ∈ u
⊢ z ∈ u

Tactic:
rcases hz _ (h z) with ⟨t, ht, h't⟩