awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h_1 : s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
hne : s.Nonempty
h : ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
hU :
  ∀ (u v : Set α),
    Membership.mem (γ := Finset (Set α)) ∅ u → Membership.mem (γ := Finset (Set α)) ∅ v → (s ∩ (u ∩ v)).Nonempty → u = v
hUo : ∀ (u : Set α), Membership.mem (γ := Finset (Set α)) ∅ u → IsOpen[inst] u
hsU : s ⊆ ⋃₀ (↑∅ : Set (Set α))
⊢ s ⊆ ∅

Tactic:
simpa using hsU
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h_1 : s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
hne : s.Nonempty
h : ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
hU :
  ∀ (u v : Set α),
    Membership.mem (γ := Finset (Set α)) ∅ u → Membership.mem (γ := Finset (Set α)) ∅ v → (s ∩ (u ∩ v)).Nonempty → u = v
hUo : ∀ (u : Set α), Membership.mem (γ := Finset (Set α)) ∅ u → IsOpen[inst] u
hsU : s ⊆ ⋃₀ (↑∅ : Set (Set α))
⊢ ∃ (u : Set α), Membership.mem (γ := Finset (Set α)) ∅ u ∧ s ⊆ u

Tactic:
exact absurd (by simpa using hsU) hne.not_subset_empty

Premises used: absurd, Set.Nonempty.not_subset_empty
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h_1 : s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
hne : s.Nonempty
h : ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u : Set α
U : Finset (Set α)
uU : u ∉ U
IH :
  ∀ (hU : ∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) (hUo : ∀ u ∈ U, IsOpen[inst] u)
    (hsU : s ⊆ ⋃₀ (↑U : Set (Set α))), ∃ u ∈ U, s ⊆ u
hU : ∀ (u_1 v : Set α), u_1 ∈ insert u U → v ∈ insert u U → (s ∩ (u_1 ∩ v)).Nonempty → u_1 = v
hUo : ∀ u_1 ∈ insert u U, IsOpen[inst] u_1
hsU : s ⊆ ⋃₀ (↑(insert u U) : Set (Set α))
refine_1 :
  (s.Nonempty ∧
      ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b) →
    ∀ (h : ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b)
      (IH :
        ∀ (hU : ∀ a ∈ U, ∀ b ∈ U, (s ∩ (a ∩ b)).Nonempty → a = b) (hUo : ∀ u ∈ U, IsOpen[inst] u)
          (hsU : s ⊆ ⋃₀ (↑U : Set (Set α))), ∃ u ∈ U, s ⊆ u)
      (hU :
        (∀ x ∈ U, (s ∩ (u ∩ x)).Nonempty → u = x) ∧
          ∀ x ∈ U, ((s ∩ (x ∩ u)).Nonempty → x = u) ∧ ∀ x_1 ∈ U, (s ∩ (x ∩ x_1)).Nonempty → x = x_1)
      (hUo : IsOpen[inst] u ∧ ∀ x ∈ U, IsOpen[inst] x) (hsU : s ⊆ u ∪ ⋃₀ (↑U : Set (Set α))), s ⊆ u ∨ ∃ x ∈ U, s ⊆ x
⊢ ∃ u_1 ∈ insert u U, s ⊆ u_1

Tactic:
simp only [← forall_cond_comm, Finset.forall_mem_insert, Finset.exists_mem_insert,
        Finset.coe_insert, sUnion_insert, implies_true, true_and] at *

Premises used: forall_cond_comm, Set.sUnion_insert, Finset.forall_mem_insert, Finset.exists_mem_insert, implies_true, Finset.coe_insert, true_and
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hne : s.Nonempty
u : Set α
U : Finset (Set α)
uU : u ∉ U
h_1 :
  s.Nonempty ∧
    ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
h : ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
IH :
  ∀ (hU : ∀ a ∈ U, ∀ b ∈ U, (s ∩ (a ∩ b)).Nonempty → a = b) (hUo : ∀ u ∈ U, IsOpen[inst] u)
    (hsU : s ⊆ ⋃₀ (↑U : Set (Set α))), ∃ u ∈ U, s ⊆ u
hU :
  (∀ x ∈ U, (s ∩ (u ∩ x)).Nonempty → u = x) ∧
    ∀ x ∈ U, ((s ∩ (x ∩ u)).Nonempty → x = u) ∧ ∀ x_1 ∈ U, (s ∩ (x ∩ x_1)).Nonempty → x = x_1
hUo : IsOpen[inst] u ∧ ∀ x ∈ U, IsOpen[inst] x
hsU : s ⊆ u ∪ ⋃₀ (↑U : Set (Set α))
⊢ s ⊆ u ∨ ∃ x ∈ U, s ⊆ x

Tactic:
(h _ hUo.1 (⋃₀ ↑U) (isOpen_sUnion hUo.2) hsU ?_).imp_right ?_

Premises used: Set.sUnion, SetLike.coe, And.right, And.left, isOpen_sUnion, Or.imp_right
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hne : s.Nonempty
u : Set α
U : Finset (Set α)
uU : u ∉ U
h_1 :
  s.Nonempty ∧
    ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
h : ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
IH :
  ∀ (hU : ∀ a ∈ U, ∀ b ∈ U, (s ∩ (a ∩ b)).Nonempty → a = b) (hUo : ∀ u ∈ U, IsOpen[inst] u)
    (hsU : s ⊆ ⋃₀ (↑U : Set (Set α))), ∃ u ∈ U, s ⊆ u
hU :
  (∀ x ∈ U, (s ∩ (u ∩ x)).Nonempty → u = x) ∧
    ∀ x ∈ U, ((s ∩ (x ∩ u)).Nonempty → x = u) ∧ ∀ x_1 ∈ U, (s ∩ (x ∩ x_1)).Nonempty → x = x_1
hUo : IsOpen[inst] u ∧ ∀ x ∈ U, IsOpen[inst] x
hsU : s ⊆ u ∪ ⋃₀ (↑U : Set (Set α))
refine_1 : s ∩ (u ∩ ⋃₀ (↑U : Set (Set α))) = ∅
refine_1₁ : s ⊆ ⋃₀ (↑U : Set (Set α)) → ∃ x ∈ U, s ⊆ x
⊢ s ⊆ u ∨ ∃ x ∈ U, s ⊆ x

Tactic:
refine (h _ hUo.1 (⋃₀ ↑U) (isOpen_sUnion hUo.2) hsU ?_).imp_right ?_

Premises used: Set.sUnion, SetLike.coe, And.right, And.left, isOpen_sUnion, Or.imp_right
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hne : s.Nonempty
u : Set α
U : Finset (Set α)
uU : u ∉ U
h_1 :
  s.Nonempty ∧
    ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
h : ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
IH :
  ∀ (hU : ∀ a ∈ U, ∀ b ∈ U, (s ∩ (a ∩ b)).Nonempty → a = b) (hUo : ∀ u ∈ U, IsOpen[inst] u)
    (hsU : s ⊆ ⋃₀ (↑U : Set (Set α))), ∃ u ∈ U, s ⊆ u
hU :
  (∀ x ∈ U, (s ∩ (u ∩ x)).Nonempty → u = x) ∧
    ∀ x ∈ U, ((s ∩ (x ∩ u)).Nonempty → x = u) ∧ ∀ x_1 ∈ U, (s ∩ (x ∩ x_1)).Nonempty → x = x_1
hUo : IsOpen[inst] u ∧ ∀ x ∈ U, IsOpen[inst] x
hsU : s ⊆ u ∪ ⋃₀ (↑U : Set (Set α))
⊢ s ∩ (u ∩ ⋃₀ (↑U : Set (Set α))) = ∅

Tactic:
subset_empty_iff.1 fun x ⟨hxs, hxu, v, hvU, hxv⟩ => ?_

Premises used: Membership.mem, _private.0.isConnected_iff_sUnion_disjoint_open.match_3, Iff.mp, Set.subset_empty_iff, EmptyCollection.emptyCollection
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hne : s.Nonempty
u : Set α
U : Finset (Set α)
uU : u ∉ U
h_1 :
  s.Nonempty ∧
    ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
h : ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
IH :
  ∀ (hU : ∀ a ∈ U, ∀ b ∈ U, (s ∩ (a ∩ b)).Nonempty → a = b) (hUo : ∀ u ∈ U, IsOpen[inst] u)
    (hsU : s ⊆ ⋃₀ (↑U : Set (Set α))), ∃ u ∈ U, s ⊆ u
hU :
  (∀ x ∈ U, (s ∩ (u ∩ x)).Nonempty → u = x) ∧
    ∀ x ∈ U, ((s ∩ (x ∩ u)).Nonempty → x = u) ∧ ∀ x_1 ∈ U, (s ∩ (x ∩ x_1)).Nonempty → x = x_1
hUo : IsOpen[inst] u ∧ ∀ x ∈ U, IsOpen[inst] x
hsU : s ⊆ u ∪ ⋃₀ (↑U : Set (Set α))
refine_1 :
  ∀ x ∈ s ∩ (u ∩ ⋃₀ (↑U : Set (Set α))),
    ∀ (hxs : x ∈ s) (hxu : x ∈ u) (v : Set α) (hvU : v ∈ (↑U : Set (Set α))) (hxv : x ∈ v),
      Membership.mem (γ := Set α) ∅ x
⊢ s ∩ (u ∩ ⋃₀ (↑U : Set (Set α))) = ∅

Tactic:
refine subset_empty_iff.1 fun x ⟨hxs, hxu, v, hvU, hxv⟩ => ?_
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hne : s.Nonempty
u : Set α
U : Finset (Set α)
uU : u ∉ U
h_1 :
  s.Nonempty ∧
    ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
h : ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
IH :
  ∀ (hU : ∀ a ∈ U, ∀ b ∈ U, (s ∩ (a ∩ b)).Nonempty → a = b) (hUo : ∀ u ∈ U, IsOpen[inst] u)
    (hsU : s ⊆ ⋃₀ (↑U : Set (Set α))), ∃ u ∈ U, s ⊆ u
hU :
  (∀ x ∈ U, (s ∩ (u ∩ x)).Nonempty → u = x) ∧
    ∀ x ∈ U, ((s ∩ (x ∩ u)).Nonempty → x = u) ∧ ∀ x_1 ∈ U, (s ∩ (x ∩ x_1)).Nonempty → x = x_1
hUo : IsOpen[inst] u ∧ ∀ x ∈ U, IsOpen[inst] x
hsU : s ⊆ u ∪ ⋃₀ (↑U : Set (Set α))
x : α
h_2 : x ∈ s ∩ (u ∩ ⋃₀ (↑U : Set (Set α)))
hxs : x ∈ s
hxu : x ∈ u
v : Set α
hvU : v ∈ (↑U : Set (Set α))
hxv : x ∈ v
⊢ Membership.mem (γ := Set α) ∅ x

Tactic:
ne_of_mem_of_not_mem hvU uU (hU.1 v hvU ⟨x, hxs, hxu, hxv⟩).symm

Premises used: Set.Mem, ne_of_mem_of_not_mem, And.left, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hne : s.Nonempty
u : Set α
U : Finset (Set α)
uU : u ∉ U
h_1 :
  s.Nonempty ∧
    ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
h : ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
IH :
  ∀ (hU : ∀ a ∈ U, ∀ b ∈ U, (s ∩ (a ∩ b)).Nonempty → a = b) (hUo : ∀ u ∈ U, IsOpen[inst] u)
    (hsU : s ⊆ ⋃₀ (↑U : Set (Set α))), ∃ u ∈ U, s ⊆ u
hU :
  (∀ x ∈ U, (s ∩ (u ∩ x)).Nonempty → u = x) ∧
    ∀ x ∈ U, ((s ∩ (x ∩ u)).Nonempty → x = u) ∧ ∀ x_1 ∈ U, (s ∩ (x ∩ x_1)).Nonempty → x = x_1
hUo : IsOpen[inst] u ∧ ∀ x ∈ U, IsOpen[inst] x
hsU : s ⊆ u ∪ ⋃₀ (↑U : Set (Set α))
x : α
h_2 : x ∈ s ∩ (u ∩ ⋃₀ (↑U : Set (Set α)))
hxs : x ∈ s
hxu : x ∈ u
v : Set α
hvU : v ∈ (↑U : Set (Set α))
hxv : x ∈ v
⊢ Membership.mem (γ := Set α) ∅ x

Tactic:
exact ne_of_mem_of_not_mem hvU uU (hU.1 v hvU ⟨x, hxs, hxu, hxv⟩).symm

Premises used: ne_of_mem_of_not_mem, And.left, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hne : s.Nonempty
u : Set α
U : Finset (Set α)
uU : u ∉ U
h_1 :
  s.Nonempty ∧
    ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
h : ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
IH :
  ∀ (hU : ∀ a ∈ U, ∀ b ∈ U, (s ∩ (a ∩ b)).Nonempty → a = b) (hUo : ∀ u ∈ U, IsOpen[inst] u)
    (hsU : s ⊆ ⋃₀ (↑U : Set (Set α))), ∃ u ∈ U, s ⊆ u
hU :
  (∀ x ∈ U, (s ∩ (u ∩ x)).Nonempty → u = x) ∧
    ∀ x ∈ U, ((s ∩ (x ∩ u)).Nonempty → x = u) ∧ ∀ x_1 ∈ U, (s ∩ (x ∩ x_1)).Nonempty → x = x_1
hUo : IsOpen[inst] u ∧ ∀ x ∈ U, IsOpen[inst] x
hsU : s ⊆ u ∪ ⋃₀ (↑U : Set (Set α))
⊢ s ⊆ ⋃₀ (↑U : Set (Set α)) → ∃ x ∈ U, s ⊆ x

Tactic:
IH (fun u hu => (hU.2 u hu).2) hUo.2

Premises used: And.right
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hne : s.Nonempty
u : Set α
U : Finset (Set α)
uU : u ∉ U
h_1 :
  s.Nonempty ∧
    ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
h : ∀ (a : Set α), IsOpen[inst] a → ∀ (b : Set α), IsOpen[inst] b → s ⊆ a ∪ b → s ∩ (a ∩ b) = ∅ → s ⊆ a ∨ s ⊆ b
IH :
  ∀ (hU : ∀ a ∈ U, ∀ b ∈ U, (s ∩ (a ∩ b)).Nonempty → a = b) (hUo : ∀ u ∈ U, IsOpen[inst] u)
    (hsU : s ⊆ ⋃₀ (↑U : Set (Set α))), ∃ u ∈ U, s ⊆ u
hU :
  (∀ x ∈ U, (s ∩ (u ∩ x)).Nonempty → u = x) ∧
    ∀ x ∈ U, ((s ∩ (x ∩ u)).Nonempty → x = u) ∧ ∀ x_1 ∈ U, (s ∩ (x ∩ x_1)).Nonempty → x = x_1
hUo : IsOpen[inst] u ∧ ∀ x ∈ U, IsOpen[inst] x
hsU : s ⊆ u ∪ ⋃₀ (↑U : Set (Set α))
⊢ s ⊆ ⋃₀ (↑U : Set (Set α)) → ∃ x ∈ U, s ⊆ x

Tactic:
exact IH (fun u hu => (hU.2 u hu).2) hUo.2

Premises used: And.right
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h_1 : s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
U : Finset (Set α)
hU : ∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v
hUo : ∀ u ∈ U, IsOpen[inst] u
hsU : s ⊆ ⋃₀ (↑U : Set (Set α))
hne : s.Nonempty
h : ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
refine_1 :
  ∀
    (hU :
      ∀ (u v : Set α),
        Membership.mem (γ := Finset (Set α)) ∅ u →
          Membership.mem (γ := Finset (Set α)) ∅ v → (s ∩ (u ∩ v)).Nonempty → u = v)
    (hUo : ∀ (u : Set α), Membership.mem (γ := Finset (Set α)) ∅ u → IsOpen[inst] u) (hsU : s ⊆ ⋃₀ (↑∅ : Set (Set α))),
    ∃ (u : Set α), Membership.mem (γ := Finset (Set α)) ∅ u ∧ s ⊆ u
refine_1₁ :
  ∀ (u : Set α) (U : Finset (Set α)) (uU : u ∉ U)
    (IH :
      ∀ (hU : ∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) (hUo : ∀ u ∈ U, IsOpen[inst] u)
        (hsU : s ⊆ ⋃₀ (↑U : Set (Set α))), ∃ u ∈ U, s ⊆ u)
    (hU : ∀ (u_1 v : Set α), u_1 ∈ insert u U → v ∈ insert u U → (s ∩ (u_1 ∩ v)).Nonempty → u_1 = v)
    (hUo : ∀ u_1 ∈ insert u U, IsOpen[inst] u_1) (hsU : s ⊆ ⋃₀ (↑(insert u U) : Set (Set α))),
    ∃ u_1 ∈ insert u U, s ⊆ u_1
⊢ ∃ u ∈ U, s ⊆ u

Tactic:
induction U using Finset.induction_on with
    | empty => exact absurd (by simpa using hsU) hne.not_subset_empty
    | insert u U uU IH =>
      simp only [← forall_cond_comm, Finset.forall_mem_insert, Finset.exists_mem_insert,
        Finset.coe_insert, sUnion_insert, implies_true, true_and] at *
      refine (h _ hUo.1 (⋃₀ ↑U) (isOpen_sUnion hUo.2) hsU ?_).imp_right ?_
      · refine subset_empty_iff.1 fun x ⟨hxs, hxu, v, hvU, hxv⟩ => ?_
        exact ne_of_mem_of_not_mem hvU uU (hU.1 v hvU ⟨x, hxs, hxu, hxv⟩).symm
      · exact IH (fun u hu => (hU.2 u hu).2) hUo.2

Premises used: forall_cond_comm, Set.sUnion_insert, Finset.forall_mem_insert, Finset.exists_mem_insert, Insert.insert, absurd, implies_true, Finset.coe_insert, true_and, Set.Nonempty.not_subset_empty
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
      (∀ u ∈ U, IsOpen[inst] u) → s ⊆ ⋃₀ (↑U : Set (Set α)) → ∃ u ∈ U, s ⊆ u
⊢ s.Nonempty

Tactic:
simpa [subset_empty_iff, nonempty_iff_ne_empty] using h ∅

Premises used: Set.nonempty_iff_ne_empty, Set.subset_empty_iff, EmptyCollection.emptyCollection
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
      (∀ u ∈ U, IsOpen[inst] u) → s ⊆ ⋃₀ (↑U : Set (Set α)) → ∃ u ∈ U, s ⊆ u
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
hsuv : s ∩ (u ∩ v) = ∅
⊢ ¬(s ∩ (u ∩ v)).Nonempty

Tactic:
rw [← not_nonempty_iff_eq_empty] at hsuv

Premises used: Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
      (∀ u ∈ U, IsOpen[inst] u) → s ⊆ ⋃₀ (↑U : Set (Set α)) → ∃ u ∈ U, s ⊆ u
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
hsuv : ¬(s ∩ (u ∩ v)).Nonempty
⊢ ¬(s ∩ (u ∩ v)).Nonempty

Tactic:
have := hsuv
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
      (∀ u ∈ U, IsOpen[inst] u) → s ⊆ ⋃₀ (↑U : Set (Set α)) → ∃ u ∈ U, s ⊆ u
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
hsuv this : ¬(s ∩ (u ∩ v)).Nonempty
⊢ ¬(s ∩ (v ∩ u)).Nonempty

Tactic:
rw [inter_comm u] at this

Premises used: Set.inter_comm
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
      (∀ u ∈ U, IsOpen[inst] u) → s ⊆ ⋃₀ (↑U : Set (Set α)) → ∃ u ∈ U, s ⊆ u
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
hsuv : ¬(s ∩ (u ∩ v)).Nonempty
this : ¬(s ∩ (v ∩ u)).Nonempty
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
simpa [*, or_imp, forall_and] using h {u, v}

Premises used: Insert.insert, or_imp, Singleton.singleton, forall_and
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
refine_1 :
  (s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) →
    ∀ (U : Finset (Set α)) (hU : ∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v)
      (hUo : ∀ u ∈ U, IsOpen[inst] u) (hsU : s ⊆ ⋃₀ (↑U : Set (Set α))) (hne : s.Nonempty)
      (h : ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v),
      ∃ u ∈ U, s ⊆ u
refine_2 :
  ∀
    (h :
      ∀ (U : Finset (Set α)),
        (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
          (∀ u ∈ U, IsOpen[inst] u) → s ⊆ ⋃₀ (↑U : Set (Set α)) → ∃ u ∈ U, s ⊆ u),
    s.Nonempty
refine_3 :
  ∀
    (h :
      ∀ (U : Finset (Set α)),
        (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
          (∀ u ∈ U, IsOpen[inst] u) → s ⊆ ⋃₀ (↑U : Set (Set α)) → ∃ u ∈ U, s ⊆ u)
    (u v : Set α) (hu : IsOpen[inst] u) (hv : IsOpen[inst] v) (hs : s ⊆ u ∪ v) (hsuv : s ∩ (u ∩ v) = ∅), s ⊆ u ∨ s ⊆ v
refine_2₁ :
  ∀
    (h :
      ∀ (U : Finset (Set α)),
        (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
          (∀ u ∈ U, IsOpen[inst] u) → s ⊆ ⋃₀ (↑U : Set (Set α)) → ∃ u ∈ U, s ⊆ u),
    s.Nonempty
refine_3₁ refine_3₂ :
  ∀
    (h :
      ∀ (U : Finset (Set α)),
        (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
          (∀ u ∈ U, IsOpen[inst] u) → s ⊆ ⋃₀ (↑U : Set (Set α)) → ∃ u ∈ U, s ⊆ u)
    (u v : Set α) (hu : IsOpen[inst] u) (hv : IsOpen[inst] v) (hs : s ⊆ u ∪ v) (hsuv : s ∩ (u ∩ v) = ∅), s ⊆ u ∨ s ⊆ v
⊢ (s.Nonempty ∧ ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) ↔
    ∀ (U : Finset (Set α)),
      (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
        (∀ u ∈ U, IsOpen[inst] u) → s ⊆ ⋃₀ (↑U : Set (Set α)) → ∃ u ∈ U, s ⊆ u

Tactic:
classical
  refine ⟨fun ⟨hne, h⟩ U hU hUo hsU => ?_, fun h => ⟨?_, fun u v hu hv hs hsuv => ?_⟩⟩
  · induction U using Finset.induction_on with
    | empty => exact absurd (by simpa using hsU) hne.not_subset_empty
    | insert u U uU IH =>
      simp only [← forall_cond_comm, Finset.forall_mem_insert, Finset.exists_mem_insert,
        Finset.coe_insert, sUnion_insert, implies_true, true_and] at *
      refine (h _ hUo.1 (⋃₀ ↑U) (isOpen_sUnion hUo.2) hsU ?_).imp_right ?_
      · refine subset_empty_iff.1 fun x ⟨hxs, hxu, v, hvU, hxv⟩ => ?_
        exact ne_of_mem_of_not_mem hvU uU (hU.1 v hvU ⟨x, hxs, hxu, hxv⟩).symm
      · exact IH (fun u hu => (hU.2 u hu).2) hUo.2
  · simpa [subset_empty_iff, nonempty_iff_ne_empty] using h ∅
  · rw [← not_nonempty_iff_eq_empty] at hsuv
    have := hsuv; rw [inter_comm u] at this
    simpa [*, or_imp, forall_and] using h {u, v}

Premises used: forall_cond_comm, Set.not_nonempty_iff_eq_empty, Set.sUnion_insert, Finset.forall_mem_insert, Finset.exists_mem_insert, Insert.insert, or_imp, Set.nonempty_iff_ne_empty, Set.subset_empty_iff, implies_true, Finset.coe_insert, true_and, forall_and
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s t : Set α
hs : IsPreconnected s
ht : IsClopen t
⊢ Disjoint s t ∨ s ⊆ t

Tactic:
(disjoint_or_nonempty_inter s t).imp_right <| hs.subset_isClopen ht

Premises used: Set.disjoint_or_nonempty_inter, IsPreconnected.subset_isClopen, Or.imp_right
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
mp :
  IsPreconnected s → ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
mpr :
  (∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) →
    IsPreconnected s
⊢ IsPreconnected s ↔ ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

Tactic:
constructor
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h : IsPreconnected s
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
mp :
  ∀
    (h :
      ∀ (t t' : Set α),
        IsClosed[inst] t →
          IsClosed[inst] t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty)
    (u v : Set α) (hu : IsClosed[inst] u) (hv : IsClosed[inst] v) (hs : s ⊆ u ∪ v) (huv : s ∩ (u ∩ v) = ∅),
    s ⊆ u ∨ s ⊆ v
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
rw [isPreconnected_closed_iff] at h

Premises used: isPreconnected_closed_iff
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h :
  ∀ (t t' : Set α),
    IsClosed[inst] t → IsClosed[inst] t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

Tactic:
specialize h u v hu hv hs
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
mp : ∀ (huv : ¬s ⊆ u ∧ ¬s ⊆ v), (s ∩ (u ∩ v)).Nonempty
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
contrapose! huv
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hs : s ⊆ u ∪ v
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
huv : ¬s ⊆ u ∧ ¬s ⊆ v
⊢ (∃ a ∈ s, a ∉ u) ∧ ∃ a ∈ s, a ∉ v

Tactic:
simp only [not_subset] at huv

Premises used: Set.not_subset
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hs : s ⊆ u ∪ v
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
huv : (∃ a ∈ s, a ∉ u) ∧ ∃ a ∈ s, a ∉ v
mp : ∀ (x : α) (hxs : x ∈ s) (hxu : x ∉ u) (y : α) (hys : y ∈ s) (hyv : y ∉ v), (s ∩ (u ∩ v)).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
rcases huv with ⟨⟨x, hxs, hxu⟩, ⟨y, hys, hyv⟩⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hs : s ⊆ u ∪ v
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
x : α
hxs : x ∈ s
hxu : x ∉ u
y : α
hys : y ∈ s
hyv : y ∉ v
⊢ x ∈ v

Tactic:
have hxv : x ∈ v := or_iff_not_imp_left.mp (hs hxs) hxu
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hs : s ⊆ u ∪ v
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
x : α
hxs : x ∈ s
hxu : x ∉ u
y : α
hys : y ∈ s
hyv : y ∉ v
hxv : x ∈ v
⊢ y ∈ u

Tactic:
have hyu : y ∈ u := or_iff_not_imp_right.mp (hs hys) hyv
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hs : s ⊆ u ∪ v
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
x : α
hxs : x ∈ s
hxu : x ∉ u
y : α
hys : y ∈ s
hyv : y ∉ v
hxv : x ∈ v
hyu : y ∈ u
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
h ⟨y, hys, hyu⟩ ⟨x, hxs, hxv⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hs : s ⊆ u ∪ v
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
x : α
hxs : x ∈ s
hxu : x ∉ u
y : α
hys : y ∈ s
hyv : y ∉ v
hxv : x ∈ v
hyu : y ∈ u
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
exact h ⟨y, hys, hyu⟩ ⟨x, hxs, hxv⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
mpr :
  ∀ (t t' : Set α),
    IsClosed[inst] t → IsClosed[inst] t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty
⊢ IsPreconnected s

Tactic:
rw [isPreconnected_closed_iff]

Premises used: isPreconnected_closed_iff
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsClosed[inst] u → IsClosed[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst] u
hv : IsClosed[inst] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
mpr : ∀ (H : ¬(s ∩ (u ∩ v)).Nonempty), False
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
by_contra H