awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
refine_1 : s ⊆ ⋃ (i : ℕ), (interior ∘ (⇑K : (a : ℕ) → Set X)) i
refine_2 : Directed (ι := ℕ) (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) (interior ∘ (⇑K : (a : ℕ) → Set X))
⊢ ∃ (n : ℕ), s ⊆ interior ((K : (a : ℕ) → Set X) n)

Tactic:
refine hs.elim_directed_cover (interior ∘ K) (fun _ ↦ isOpen_interior) ?_ ?_

Premises used: isOpen_interior, Function.comp, interior, DFunLike.coe, IsCompact.elim_directed_cover
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
x : X
refine_1 : x ∈ s → Membership.mem (γ := Set X) (⋃ (i : ℕ), (interior ∘ (⇑K : (a : ℕ) → Set X)) i) x
⊢ x ∈ s → Membership.mem (γ := Set X) (⋃ (i : ℕ), (interior ∘ (⇑K : (a : ℕ) → Set X)) i) x

Tactic:
_
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
x : X
h : x ∈ s
refine_1 :
  ∀ (k : ℕ) (hk : Membership.mem (γ := Set X) ((K : (a : ℕ) → Set X) k : Set X) x),
    Membership.mem (γ := Set X) (⋃ (i : ℕ), (interior ∘ (⇑K : (a : ℕ) → Set X)) i) x
⊢ Membership.mem (γ := Set X) (⋃ (i : ℕ), (interior ∘ (⇑K : (a : ℕ) → Set X)) i) x

Tactic:
rcases K.exists_mem x with ⟨k, hk⟩

Premises used: CompactExhaustion.exists_mem
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
x : X
h : x ∈ s
k : ℕ
hk : Membership.mem (γ := Set X) ((K : (a : ℕ) → Set X) k : Set X) x
⊢ Membership.mem (γ := Set X) (⋃ (i : ℕ), (interior ∘ (⇑K : (a : ℕ) → Set X)) i) x

Tactic:
mem_iUnion.2 ⟨k + 1, K.subset_interior_succ _ hk⟩

Premises used: Iff.mpr, Set.mem_iUnion, HAdd.hAdd, Exists.intro, CompactExhaustion.subset_interior_succ, OfNat.ofNat
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
x : X
h : x ∈ s
k : ℕ
hk : Membership.mem (γ := Set X) ((K : (a : ℕ) → Set X) k : Set X) x
⊢ Membership.mem (γ := Set X) (⋃ (i : ℕ), (interior ∘ (⇑K : (a : ℕ) → Set X)) i) x

Tactic:
exact mem_iUnion.2 ⟨k + 1, K.subset_interior_succ _ hk⟩

Premises used: Iff.mpr, Set.mem_iUnion, HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
⊢ Directed (ι := ℕ) (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) (interior ∘ (⇑K : (a : ℕ) → Set X))

Tactic:
Monotone.directed_le fun _ _ h ↦ interior_mono <| K.subset h

Premises used: interior_mono, CompactExhaustion.subset, Monotone.directed_le
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
⊢ Directed (ι := ℕ) (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) (interior ∘ (⇑K : (a : ℕ) → Set X))

Tactic:
exact Monotone.directed_le fun _ _ h ↦ interior_mono <| K.subset h

Premises used: interior_mono, CompactExhaustion.subset, Monotone.directed_le
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ Membership.mem (γ := Set X) ((K : (a : ℕ) → Set X) (K.find x) : Set X) x

Tactic:
Nat.find_spec (K.exists_mem x)

Premises used: CompactExhaustion.exists_mem, Set.Mem, CompactExhaustion.find, Nat.find_spec
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ Membership.mem (γ := Set X) ((K : (a : ℕ) → Set X) (K.find x) : Set X) x

Tactic:
exact Nat.find_spec (K.exists_mem x)

Premises used: CompactExhaustion.exists_mem, Nat.find_spec
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ Membership.mem (γ := Set X) ((K : (a : ℕ) → Set X) (K.find x) : Set X) x

Tactic:
classical
  exact Nat.find_spec (K.exists_mem x)
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
x : X
n : ℕ
⊢ Membership.mem (γ := Set X) ((K : (a : ℕ) → Set X) n : Set X) x ↔ K.find x ≤ n

Tactic:
⟨fun h => Nat.find_min' (K.exists_mem x) h, fun h => K.subset h <| K.mem_find x⟩

Premises used: CompactExhaustion.exists_mem, CompactExhaustion.mem_find, CompactExhaustion.subset, Nat.find_min', Iff.intro
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
x : X
n : ℕ
⊢ Membership.mem (γ := Set X) ((K : (a : ℕ) → Set X) n : Set X) x ↔ K.find x ≤ n

Tactic:
exact ⟨fun h => Nat.find_min' (K.exists_mem x) h, fun h => K.subset h <| K.mem_find x⟩
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
x : X
n : ℕ
⊢ Membership.mem (γ := Set X) ((K : (a : ℕ) → Set X) n : Set X) x ↔ K.find x ≤ n

Tactic:
classical
  exact ⟨fun h => Nat.find_min' (K.exists_mem x) h, fun h => K.subset h <| K.mem_find x⟩
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ K.shiftr.find x = K.find x + 1

Tactic:
Nat.find_comp_succ _ _ (notMem_empty _)

Premises used: Set.Mem, CompactExhaustion.find, Nat.find_comp_succ, Set.notMem_empty
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ K.shiftr.find x = K.find x + 1

Tactic:
exact Nat.find_comp_succ _ _ (notMem_empty _)

Premises used: Nat.find_comp_succ, Set.notMem_empty
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ K.shiftr.find x = K.find x + 1

Tactic:
classical
  exact Nat.find_comp_succ _ _ (notMem_empty _)

Premises used: Nat.find_comp_succ, Set.notMem_empty
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X : Type u_1
inst : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ ¬K.shiftr.find x ≤ K.find x

Tactic:
simp only [find_shiftr, not_le, Nat.lt_succ_self]

Premises used: not_le, CompactExhaustion.find_shiftr, Nat.lt_succ_self
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
K : CompactExhaustion X_1
X : Type u_4
inst_2 : TopologicalSpace X
inst_3 : WeaklyLocallyCompactSpace X
inst_4 : SigmaCompactSpace X
a : Nonempty.{u_4 + 1} (CompactExhaustion X)
⊢ CompactExhaustion X

Tactic:
apply Classical.choice

Premises used: Classical.choice
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
K_1 : CompactExhaustion X_1
X : Type u_4
inst_2 : TopologicalSpace X
inst_3 : WeaklyLocallyCompactSpace X
inst_4 : SigmaCompactSpace X
K : ℕ → { s : Set X // IsCompact s } :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ { s : Set X // IsCompact s }) n
      (Subtype.mk (p := fun (s : Set X) ↦ IsCompact s) ∅ ⋯) fun (n : ℕ) (s : { s : Set X // IsCompact s }) ↦
      Subtype.mk (p := fun (s : Set X) ↦ IsCompact s)
        (⋯.choose (p := fun (K' : Set X) ↦ IsCompact K' ∧ (↑s : Set X) ⊆ interior K') ∪ compactCovering X n) ⋯
⊢ Nonempty.{u_4 + 1} (CompactExhaustion X)

Tactic:
⟨⟨fun n ↦ (K n).1, fun n => (K n).2, fun n ↦ ?_, ?_⟩⟩

Premises used: Nonempty.intro, CompactExhaustion.mk, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
K_1 : CompactExhaustion X_1
X : Type u_4
inst_2 : TopologicalSpace X
inst_3 : WeaklyLocallyCompactSpace X
inst_4 : SigmaCompactSpace X
K : ℕ → { s : Set X // IsCompact s } :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ { s : Set X // IsCompact s }) n
      (Subtype.mk (p := fun (s : Set X) ↦ IsCompact s) ∅ ⋯) fun (n : ℕ) (s : { s : Set X // IsCompact s }) ↦
      Subtype.mk (p := fun (s : Set X) ↦ IsCompact s)
        (⋯.choose (p := fun (K' : Set X) ↦ IsCompact K' ∧ (↑s : Set X) ⊆ interior K') ∪ compactCovering X n) ⋯
a :
  ∀ (n : ℕ),
    Subset.{u_4} (α := Set X) ((fun (n : ℕ) ↦ (↑(K n) : Set X)) n) (interior ((fun (n : ℕ) ↦ (↑(K n) : Set X)) (n + 1)))
a₁ : Eq.{u_4 + 1} (α := Set X) (⋃ (n : ℕ), (fun (n : ℕ) ↦ (↑(K n) : Set X)) n) univ
⊢ Nonempty.{u_4 + 1} (CompactExhaustion X)

Tactic:
refine ⟨⟨fun n ↦ (K n).1, fun n => (K n).2, fun n ↦ ?_, ?_⟩⟩
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
K_1 : CompactExhaustion X_1
X : Type u_4
inst_2 : TopologicalSpace X
inst_3 : WeaklyLocallyCompactSpace X
inst_4 : SigmaCompactSpace X
K : ℕ → { s : Set X // IsCompact s } :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ { s : Set X // IsCompact s }) n
      (Subtype.mk (p := fun (s : Set X) ↦ IsCompact s) ∅ ⋯) fun (n : ℕ) (s : { s : Set X // IsCompact s }) ↦
      Subtype.mk (p := fun (s : Set X) ↦ IsCompact s)
        (⋯.choose (p := fun (K' : Set X) ↦ IsCompact K' ∧ (↑s : Set X) ⊆ interior K') ∪ compactCovering X n) ⋯
n : ℕ
⊢ Subset.{u_4} (α := Set X) ((fun (n : ℕ) ↦ (↑(K n) : Set X)) n) (interior ((fun (n : ℕ) ↦ (↑(K n) : Set X)) (n + 1)))

Tactic:
Subset.trans (exists_compact_superset (K n).2).choose_spec.2
      (interior_mono subset_union_left)

Premises used: Exists.choose_spec, interior_mono, Set.Subset.trans, Set.subset_union_left, And.right, exists_compact_superset, Subtype.property
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
K_1 : CompactExhaustion X_1
X : Type u_4
inst_2 : TopologicalSpace X
inst_3 : WeaklyLocallyCompactSpace X
inst_4 : SigmaCompactSpace X
K : ℕ → { s : Set X // IsCompact s } :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ { s : Set X // IsCompact s }) n
      (Subtype.mk (p := fun (s : Set X) ↦ IsCompact s) ∅ ⋯) fun (n : ℕ) (s : { s : Set X // IsCompact s }) ↦
      Subtype.mk (p := fun (s : Set X) ↦ IsCompact s)
        (⋯.choose (p := fun (K' : Set X) ↦ IsCompact K' ∧ (↑s : Set X) ⊆ interior K') ∪ compactCovering X n) ⋯
n : ℕ
⊢ Subset.{u_4} (α := Set X) ((fun (n : ℕ) ↦ (↑(K n) : Set X)) n) (interior ((fun (n : ℕ) ↦ (↑(K n) : Set X)) (n + 1)))

Tactic:
exact Subset.trans (exists_compact_superset (K n).2).choose_spec.2
      (interior_mono subset_union_left)

Premises used: Exists.choose_spec, interior_mono, Set.Subset.trans, Set.subset_union_left, And.right, exists_compact_superset, Subtype.property
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
K_1 : CompactExhaustion X_1
X : Type u_4
inst_2 : TopologicalSpace X
inst_3 : WeaklyLocallyCompactSpace X
inst_4 : SigmaCompactSpace X
K : ℕ → { s : Set X // IsCompact s } :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ { s : Set X // IsCompact s }) n
      (Subtype.mk (p := fun (s : Set X) ↦ IsCompact s) ∅ ⋯) fun (n : ℕ) (s : { s : Set X // IsCompact s }) ↦
      Subtype.mk (p := fun (s : Set X) ↦ IsCompact s)
        (⋯.choose (p := fun (K' : Set X) ↦ IsCompact K' ∧ (↑s : Set X) ⊆ interior K') ∪ compactCovering X n) ⋯
⊢ Eq.{u_4 + 1} (α := Set X) (⋃ (n : ℕ), (fun (n : ℕ) ↦ (↑(K n) : Set X)) n) univ

Tactic:
univ_subset_iff.1 (iUnion_compactCovering X ▸ ?_)

Premises used: Set.univ_subset_iff, iUnion_compactCovering, Eq.rec, Iff.mp
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
K_1 : CompactExhaustion X_1
X : Type u_4
inst_2 : TopologicalSpace X
inst_3 : WeaklyLocallyCompactSpace X
inst_4 : SigmaCompactSpace X
K : ℕ → { s : Set X // IsCompact s } :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ { s : Set X // IsCompact s }) n
      (Subtype.mk (p := fun (s : Set X) ↦ IsCompact s) ∅ ⋯) fun (n : ℕ) (s : { s : Set X // IsCompact s }) ↦
      Subtype.mk (p := fun (s : Set X) ↦ IsCompact s)
        (⋯.choose (p := fun (K' : Set X) ↦ IsCompact K' ∧ (↑s : Set X) ⊆ interior K') ∪ compactCovering X n) ⋯
a : Subset.{u_4} (α := Set X) (⋃ (n : ℕ), compactCovering X n) (⋃ (n : ℕ), (fun (n : ℕ) ↦ (↑(K n) : Set X)) n)
⊢ Eq.{u_4 + 1} (α := Set X) (⋃ (n : ℕ), (fun (n : ℕ) ↦ (↑(K n) : Set X)) n) univ

Tactic:
refine univ_subset_iff.1 (iUnion_compactCovering X ▸ ?_)

Premises used: Set.univ_subset_iff, Iff.mp
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
K_1 : CompactExhaustion X_1
X : Type u_4
inst_2 : TopologicalSpace X
inst_3 : WeaklyLocallyCompactSpace X
inst_4 : SigmaCompactSpace X
K : ℕ → { s : Set X // IsCompact s } :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ { s : Set X // IsCompact s }) n
      (Subtype.mk (p := fun (s : Set X) ↦ IsCompact s) ∅ ⋯) fun (n : ℕ) (s : { s : Set X // IsCompact s }) ↦
      Subtype.mk (p := fun (s : Set X) ↦ IsCompact s)
        (⋯.choose (p := fun (K' : Set X) ↦ IsCompact K' ∧ (↑s : Set X) ⊆ interior K') ∪ compactCovering X n) ⋯
⊢ Subset.{u_4} (α := Set X) (⋃ (n : ℕ), compactCovering X n) (⋃ (n : ℕ), (fun (n : ℕ) ↦ (↑(K n) : Set X)) n)

Tactic:
iUnion_mono' fun n => ⟨n + 1, subset_union_right⟩

Premises used: Set.subset_union_right, Set.iUnion_mono', HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.Compactness.SigmaCompact
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
s t : Set X_1
K_1 : CompactExhaustion X_1
X : Type u_4
inst_2 : TopologicalSpace X
inst_3 : WeaklyLocallyCompactSpace X
inst_4 : SigmaCompactSpace X
K : ℕ → { s : Set X // IsCompact s } :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ { s : Set X // IsCompact s }) n
      (Subtype.mk (p := fun (s : Set X) ↦ IsCompact s) ∅ ⋯) fun (n : ℕ) (s : { s : Set X // IsCompact s }) ↦
      Subtype.mk (p := fun (s : Set X) ↦ IsCompact s)
        (⋯.choose (p := fun (K' : Set X) ↦ IsCompact K' ∧ (↑s : Set X) ⊆ interior K') ∪ compactCovering X n) ⋯
⊢ Subset.{u_4} (α := Set X) (⋃ (n : ℕ), compactCovering X n) (⋃ (n : ℕ), (fun (n : ℕ) ↦ (↑(K n) : Set X)) n)

Tactic:
exact iUnion_mono' fun n => ⟨n + 1, subset_union_right⟩

Premises used: Set.subset_union_right, Set.iUnion_mono', HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h : IsConnected s
⊢ s.Nonempty

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
h : IsConnected s
⊢ IsPreconnected s

Tactic:
h.2

Premises used: And.right
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
H : IsPreirreducible s
⊢ IsPreconnected s

Tactic:
fun _ _ hu hv _ => H _ _ hu hv

Premises used: IsPreconnected
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
H : IsIrreducible s
⊢ IsConnected s

Tactic:
⟨H.nonempty, H.isPreirreducible.isPreconnected⟩

Premises used: IsConnected, IsIrreducible.nonempty, IsIrreducible.isPreirreducible, And.intro, IsPreirreducible.isPreconnected
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
⊢ IsPreconnected.{u} (α := α) ∅

Tactic:
isPreirreducible_empty.isPreconnected

Premises used: isPreirreducible_empty, IsPreirreducible.isPreconnected
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
⊢ IsConnected (α := α) {x}

Tactic:
isIrreducible_singleton.isConnected

Premises used: isIrreducible_singleton, IsIrreducible.isConnected
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
⊢ IsPreconnected (α := α) {x}

Tactic:
isConnected_singleton.isPreconnected

Premises used: isConnected_singleton, IsConnected.isPreconnected
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : s.Subsingleton
⊢ IsPreconnected s

Tactic:
hs.induction_on isPreconnected_empty fun _ => isPreconnected_singleton

Premises used: Set.Subsingleton.induction_on, isPreconnected_singleton, isPreconnected_empty
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
rcases : ∀ (t : Set α) (ts : t ⊆ s) (xt : x ∈ t), x ∈ s
⊢ x ∈ s

Tactic:
rcases H y ys with ⟨t, ts, xt, -, -⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
t : Set α
ts : t ⊆ s
xt : x ∈ t
⊢ x ∈ s

Tactic:
ts xt
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
t : Set α
ts : t ⊆ s
xt : x ∈ t
⊢ x ∈ s

Tactic:
exact ts xt
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
⊢ x ∈ s

Tactic:
have xs : x ∈ s := by
    rcases H y ys with ⟨t, ts, xt, -, -⟩
    exact ts xt
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xu : x ∈ u
inl : ∀ (t : Set α) (ts : t ⊆ s) (xt : x ∈ t) (yt : y ∈ t) (ht : IsPreconnected t), (s ∩ (u ∩ v)).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
rcases H y ys with ⟨t, ts, xt, yt, ht⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xu : x ∈ u
t : Set α
ts : t ⊆ s
xt : x ∈ t
yt : y ∈ t
ht : IsPreconnected t
⊢ (t ∩ (u ∩ v)).Nonempty

Tactic:
have := ht u v hu hv (ts.trans hs) ⟨x, xt, xu⟩ ⟨y, yt, yv⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xu : x ∈ u
t : Set α
ts : t ⊆ s
xt : x ∈ t
yt : y ∈ t
ht : IsPreconnected t
this : (t ∩ (u ∩ v)).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
this.imp fun z hz => ⟨ts hz.1, hz.2⟩

Premises used: Exists.imp, Set.Nonempty, And.intro
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xu : x ∈ u
t : Set α
ts : t ⊆ s
xt : x ∈ t
yt : y ∈ t
ht : IsPreconnected t
this : (t ∩ (u ∩ v)).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
exact this.imp fun z hz => ⟨ts hz.1, hz.2⟩

Premises used: Exists.imp
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xv : x ∈ v
inr : ∀ (t : Set α) (ts : t ⊆ s) (xt : x ∈ t) (zt : z ∈ t) (ht : IsPreconnected t), (s ∩ (u ∩ v)).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
rcases H z zs with ⟨t, ts, xt, zt, ht⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xv : x ∈ v
t : Set α
ts : t ⊆ s
xt : x ∈ t
zt : z ∈ t
ht : IsPreconnected t
rwa rwa₁ rwa₂ rwa₃ : s ⊆ u ∪ v
⊢ s ⊆ v ∪ u

Tactic:
rwa [union_comm]

Premises used: Set.union_comm
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xv : x ∈ v
t : Set α
ts : t ⊆ s
xt : x ∈ t
zt : z ∈ t
ht : IsPreconnected t
⊢ (t ∩ (v ∩ u)).Nonempty

Tactic:
have := ht v u hv hu (ts.trans <| by rwa [union_comm]) ⟨x, xt, xv⟩ ⟨z, zt, zu⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xv : x ∈ v
t : Set α
ts : t ⊆ s
xt : x ∈ t
zt : z ∈ t
ht : IsPreconnected t
this : (t ∩ (v ∩ u)).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
this.imp fun _ h => ⟨ts h.1, h.2.2, h.2.1⟩

Premises used: Exists.imp, Set.Nonempty, And.intro
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xv : x ∈ v
t : Set α
ts : t ⊆ s
xt : x ∈ t
zt : z ∈ t
ht : IsPreconnected t
this : (t ∩ (v ∩ u)).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
exact this.imp fun _ h => ⟨ts h.1, h.2.2, h.2.1⟩

Premises used: Exists.imp
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
⊢ x ∈ u ∪ v

Tactic:
cases hs xs with
  | inl xu =>
    rcases H y ys with ⟨t, ts, xt, yt, ht⟩
    have := ht u v hu hv (ts.trans hs) ⟨x, xt, xu⟩ ⟨y, yt, yv⟩
    exact this.imp fun z hz => ⟨ts hz.1, hz.2⟩
  | inr xv =>
    rcases H z zs with ⟨t, ts, xt, zt, ht⟩
    have := ht v u hv hu (ts.trans <| by rwa [union_comm]) ⟨x, xt, xv⟩ ⟨z, zt, zu⟩
    exact this.imp fun _ h => ⟨ts h.1, h.2.2, h.2.1⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
H : ∀ x ∈ s, ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
inl :
  ∀
    (H :
      ∀ (x : α),
        Membership.mem (γ := Set α) ∅ x →
          ∀ (y : α), Membership.mem (γ := Set α) ∅ y → ∃ t ⊆ ∅, x ∈ t ∧ y ∈ t ∧ IsPreconnected t),
    IsPreconnected.{u} (α := α) ∅
inr : ∀ (x : α) (hx : x ∈ s), IsPreconnected s
⊢ IsPreconnected s

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

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
H :
  ∀ (x : α),
    Membership.mem (γ := Set α) ∅ x →
      ∀ (y : α), Membership.mem (γ := Set α) ∅ y → ∃ t ⊆ ∅, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
⊢ IsPreconnected.{u} (α := α) ∅

Tactic:
isPreconnected_empty

Premises used: isPreconnected_empty
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
H : ∀ x ∈ s, ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
x : α
hx : x ∈ s
⊢ IsPreconnected s

Tactic:
isPreconnected_of_forall x fun y => H x hx y

Premises used: isPreconnected_of_forall