awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
t : α
ht : Membership.mem (γ := Set α) {x : α | (fun (y : α) ↦ P z y ∧ P y z) x} t
h't : t ∈ u
⊢ z ∈ u

Tactic:
h'.trans x t z h't ht.2

Premises used: Set.Mem, setOf, IsTrans.trans, And.right
-- 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
t : α
ht : Membership.mem (γ := Set α) {x : α | (fun (y : α) ↦ P z y ∧ P y z) x} t
h't : t ∈ u
⊢ z ∈ u

Tactic:
exact h'.trans x t z h't ht.2

Premises used: IsTrans.trans, And.right
-- 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}
⊢ IsClosed[inst] u

Tactic:
have A : IsClosed u := by
    apply isClosed_iff_nhds.2 (fun z hz ↦ ?_)
    rcases hz _ (h z) with ⟨t, ht, h't⟩
    exact h'.trans x t z h't ht.2
-- 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}
A : IsClosed[inst] u
apply : ∀ (z : α) (hz : z ∈ u), u ∈ 𝓝 z
⊢ IsOpen[inst] u

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

Premises used: Iff.mpr, isOpen_iff_mem_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}
A : IsClosed[inst] u
z : α
hz : z ∈ u
h₁ : ∀ (t : α) (ht : P z t ∧ P t z), t ∈ u
⊢ u ∈ 𝓝 z

Tactic:
filter_upwards [h z] with t ht
-- 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}
A : IsClosed[inst] u
z : α
hz : z ∈ u
t : α
ht : P z t ∧ P t z
⊢ t ∈ u

Tactic:
h'.trans x z t hz ht.1

Premises used: Set.Mem, setOf, IsTrans.trans, And.left
-- 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}
A : IsClosed[inst] u
z : α
hz : z ∈ u
t : α
ht : P z t ∧ P t z
⊢ t ∈ u

Tactic:
exact h'.trans x z t hz ht.1

Premises used: IsTrans.trans, And.left
-- 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}
A : IsClosed[inst] u
⊢ IsOpen[inst] u

Tactic:
have B : IsOpen u := by
    apply isOpen_iff_mem_nhds.2 (fun z hz ↦ ?_)
    filter_upwards [h z] with t ht
    exact h'.trans x z t hz ht.1
-- 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}
A : IsClosed[inst] u
B : IsOpen[inst] u
⊢ u.Nonempty

Tactic:
have C : u.Nonempty := ⟨x, (mem_of_mem_nhds (h x)).1⟩
-- 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}
A : IsClosed[inst] u
B : IsOpen[inst] u
C : u.Nonempty
⊢ u = univ

Tactic:
have D : u = Set.univ := IsClopen.eq_univ ⟨A, B⟩ C
-- 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}
A : IsClosed[inst] u
B : IsOpen[inst] u
C : u.Nonempty
D : u = univ
change : y ∈ u
⊢ P x y

Tactic:
change y ∈ u
-- 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}
A : IsClosed[inst] u
B : IsOpen[inst] u
C : u.Nonempty
D : u = univ
⊢ y ∈ u

Tactic:
simp [D]
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y
h' : IsTrans α P
h'' : Symmetric P
x y : α
⊢ P x y

Tactic:
PreconnectedSpace.induction₂' P (fun z ↦ ?_) h' x y

Premises used: PreconnectedSpace.induction₂'
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y
h' : IsTrans α P
h'' : Symmetric P
x y : α
refine : ∀ (z : α), ∀ᶠ (y : α) in 𝓝 z, P z y ∧ P y z
⊢ P x y

Tactic:
refine PreconnectedSpace.induction₂' P (fun z ↦ ?_) h' x y

Premises used: PreconnectedSpace.induction₂'
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y
h' : IsTrans α P
h'' : Symmetric P
x y z : α
h₁ : ∀ (a : α) (ha : P z a), P z a ∧ P a z
⊢ ∀ᶠ (y : α) in 𝓝 z, P z y ∧ P y z

Tactic:
filter_upwards [h z] with a ha
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y
h' : IsTrans α P
h'' : Symmetric P
x y z a : α
ha : P z a
⊢ P z a ∧ P a z

Tactic:
⟨ha, h'' ha⟩

Premises used: And.intro
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y
h' : IsTrans α P
h'' : Symmetric P
x y z a : α
ha : P z a
⊢ P z a ∧ P a z

Tactic:
exact ⟨ha, h'' ha⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x y : α
hx : x ∈ s
hy : y ∈ s
let : P x y
⊢ P x y

Tactic:
let Q : s → s → Prop := fun a b ↦ P a b
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x y : α
hx : x ∈ s
hy : y ∈ s
Q : (↑s : Type u) → (↑s : Type u) → Prop := fun (a b : (↑s : Type u)) ↦ P (↑a : α) (↑b : α)
change : Q (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)
⊢ P x y

Tactic:
change Q ⟨x, hx⟩ ⟨y, hy⟩

Premises used: Subtype.mk
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x y : α
hx : x ∈ s
hy : y ∈ s
Q : (↑s : Type u) → (↑s : Type u) → Prop := fun (a b : (↑s : Type u)) ↦ P (↑a : α) (↑b : α)
have :
  ∀ (this : PreconnectedSpace.{u} (↑s : Type u)),
    Q (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)
⊢ Q (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)

Tactic:
have : PreconnectedSpace s := Subtype.preconnectedSpace hs
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x y : α
hx : x ∈ s
hy : y ∈ s
Q : (↑s : Type u) → (↑s : Type u) → Prop := fun (a b : (↑s : Type u)) ↦ P (↑a : α) (↑b : α)
this : PreconnectedSpace.{u} (↑s : Type u)
h₁ : ∀ (x : { x : α // x ∈ s }), ∀ᶠ (y : { x : α // x ∈ s }) in 𝓝 x, Q x y ∧ Q y x
h'₁ : IsTrans { x : α // x ∈ s } Q
⊢ Q (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)

Tactic:
apply PreconnectedSpace.induction₂'

Premises used: PreconnectedSpace.induction₂'
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x_1 y : α
hx_1 : x_1 ∈ s
hy : y ∈ s
Q : (↑s : Type u) → (↑s : Type u) → Prop := fun (a b : (↑s : Type u)) ↦ P (↑a : α) (↑b : α)
this : PreconnectedSpace.{u} (↑s : Type u)
x : α
hx : x ∈ s
⊢ ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x

Tactic:
have Z := h x hx
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x_1 y : α
hx_1 : x_1 ∈ s
hy : y ∈ s
Q : (↑s : Type u) → (↑s : Type u) → Prop := fun (a b : (↑s : Type u)) ↦ P (↑a : α) (↑b : α)
this : PreconnectedSpace.{u} (↑s : Type u)
x : α
hx : x ∈ s
Z : ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h₁ :
  ∀
    (Z :
      ∀ᶠ (y : α) in
        Filter.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)),
        P x y ∧ P y x),
    ∀ᶠ (y : { x : α // x ∈ s }) in 𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx),
      Q (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) y ∧ Q y (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
h₂ : x ∈ s
h₃ :
  ∀
    (Z :
      ∀ᶠ (y : α) in
        Filter.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)),
        P x y ∧ P y x),
    ∀ᶠ (y : { x : α // x ∈ s }) in 𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx),
      Q (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) y ∧ Q y (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
h₄ : x ∈ s
h₅ :
  ∀
    (Z :
      ∀ᶠ (y : α) in
        Filter.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)),
        P x y ∧ P y x),
    ∀ᶠ (y : { x : α // x ∈ s }) in 𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx),
      Q (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) y ∧ Q y (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
h₆ : x ∈ s
h₇ :
  ∀
    (Z :
      ∀ᶠ (y : α) in
        Filter.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)),
        P x y ∧ P y x),
    ∀ᶠ (y : { x : α // x ∈ s }) in 𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx),
      Q (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) y ∧ Q y (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
h₈ : x ∈ s
⊢ ∀ᶠ (y : { x : α // x ∈ s }) in 𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx),
    Q (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) y ∧ Q y (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)

Tactic:
rwa [nhdsWithin_eq_map_subtype_coe] at Z

Premises used: nhdsWithin_eq_map_subtype_coe
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x y : α
hx : x ∈ s
hy : y ∈ s
Q : (↑s : Type u) → (↑s : Type u) → Prop := fun (a b : (↑s : Type u)) ↦ P (↑a : α) (↑b : α)
this : PreconnectedSpace.{u} (↑s : Type u)
⊢ IsTrans { x : α // x ∈ s } Q

Tactic:
⟨fun ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩ ↦ h' a b c ha hb hc⟩

Premises used: IsTrans.mk, _private.0.IsPreconnected.induction₂'.match_1
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x y : α
hx : x ∈ s
hy : y ∈ s
Q : (↑s : Type u) → (↑s : Type u) → Prop := fun (a b : (↑s : Type u)) ↦ P (↑a : α) (↑b : α)
this : PreconnectedSpace.{u} (↑s : Type u)
⊢ IsTrans { x : α // x ∈ s } Q

Tactic:
exact ⟨fun ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩ ↦ h' a b c ha hb hc⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
h'' : ∀ (x y : α), x ∈ s → y ∈ s → P x y → P y x
x y : α
hx : x ∈ s
hy : y ∈ s
apply : ∀ (z : α) (hz : z ∈ s), ∀ᶠ (y : α) in 𝓝[s] z, P z y ∧ P y z
⊢ P x y

Tactic:
apply hs.induction₂' P (fun z hz ↦ ?_) h' hx hy

Premises used: IsPreconnected.induction₂'
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
h'' : ∀ (x y : α), x ∈ s → y ∈ s → P x y → P y x
x y : α
hx : x ∈ s
hy : y ∈ s
z : α
hz : z ∈ s
h₁ : ∀ (a : α) (ha : P z a) (h'a : a ∈ s), P z a ∧ P a z
⊢ ∀ᶠ (y : α) in 𝓝[s] z, P z y ∧ P y z

Tactic:
filter_upwards [h z hz, self_mem_nhdsWithin] with a ha h'a

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
h'' : ∀ (x y : α), x ∈ s → y ∈ s → P x y → P y x
x y : α
hx : x ∈ s
hy : y ∈ s
z : α
hz : z ∈ s
a : α
ha : P z a
h'a : a ∈ s
⊢ P z a ∧ P a z

Tactic:
⟨ha, h'' z a hz h'a ha⟩

Premises used: And.intro
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
h'' : ∀ (x y : α), x ∈ s → y ∈ s → P x y → P y x
x y : α
hx : x ∈ s
hy : y ∈ s
z : α
hz : z ∈ s
a : α
ha : P z a
h'a : a ∈ s
⊢ P z a ∧ P a z

Tactic:
exact ⟨ha, h'' z a hz h'a ha⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
mp : IsPreconnected s → ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
mpr :
  (∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v) → IsPreconnected s
⊢ IsPreconnected s ↔ ∀ (u v : Set α), IsOpen[inst] u → IsOpen[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 : IsOpen[inst] u
hv : IsOpen[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 : IsOpen[inst] u
hv : IsOpen[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 : IsOpen[inst] u
hv : IsOpen[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 : IsOpen[inst] u
hv : IsOpen[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 : IsOpen[inst] u
hv : IsOpen[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 : IsOpen[inst] u
hv : IsOpen[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 : IsOpen[inst] u
hv : IsOpen[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 : IsOpen[inst] u
hv : IsOpen[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 α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[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
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsOpen[inst] u → IsOpen[inst] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
specialize h u v hu hv hs (Set.not_nonempty_iff_eq_empty.mp H)

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

Tactic:
apply H
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ u ∨ s ⊆ v
mpr : ∀ (h : s ⊆ u), (s ∩ (u ∩ v)).Nonempty
mpr₁ : ∀ (h : s ⊆ v), (s ∩ (u ∩ v)).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
rcases h with h | h
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ u
mpr : ∀ (x : α) (hxs : x ∈ s) (hxv : x ∈ v), (s ∩ (u ∩ v)).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
rcases hsv with ⟨x, hxs, hxv⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ u
x : α
hxs : x ∈ s
hxv : x ∈ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
⟨x, hxs, ⟨h hxs, hxv⟩⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ u
x : α
hxs : x ∈ s
hxv : x ∈ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
exact ⟨x, hxs, ⟨h hxs, hxv⟩⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ v
mpr : ∀ (x : α) (hxs : x ∈ s) (hxu : x ∈ u), (s ∩ (u ∩ v)).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
rcases hsu with ⟨x, hxs, hxu⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ v
x : α
hxs : x ∈ s
hxu : x ∈ u
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
⟨x, hxs, ⟨hxu, h hxs⟩⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ v
x : α
hxs : x ∈ s
hxu : x ∈ u
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
exact ⟨x, hxs, ⟨hxu, h hxs⟩⟩
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
rw :
  (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
⊢ IsConnected s ↔
    ∀ (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:
rw [IsConnected, isPreconnected_iff_subset_of_disjoint]

Premises used: IsConnected, isPreconnected_iff_subset_of_disjoint
-- Module: Mathlib.Topology.Connected.Clopen
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
⊢ (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:
⟨fun ⟨hne, h⟩ U hU hUo hsU => ?_, fun h => ⟨?_, fun u v hu hv hs hsuv => ?_⟩⟩

Premises used: Membership.mem, Exists, HasSubset.Subset, And, _private.0.isConnected_iff_sUnion_disjoint_open.match_1, And.intro, Iff.intro
-- 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
⊢ (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:
refine ⟨fun ⟨hne, h⟩ U hU hUo hsU => ?_, fun h => ⟨?_, fun u v hu hv hs hsuv => ?_⟩⟩