awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exacts [isPreconnected_empty, isPreconnected_of_forall x fun y => H x hx y]

Premises used: isPreconnected_empty
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
c : Set (Set α)
H1 : ∀ s ∈ c, x ∈ s
H2 : ∀ s ∈ c, IsPreconnected s
apply : ∀ y ∈ ⋃₀ c, ∃ t ⊆ ⋃₀ c, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
⊢ IsPreconnected (⋃₀ c)

Tactic:
apply isPreconnected_of_forall x

Premises used: isPreconnected_of_forall
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
c : Set (Set α)
H1 : ∀ s ∈ c, x ∈ s
H2 : ∀ s ∈ c, IsPreconnected s
y : α
s : Set α
sc : s ∈ c
ys : y ∈ s
⊢ ∃ t ⊆ ⋃₀ c, x ∈ t ∧ y ∈ t ∧ IsPreconnected t

Tactic:
⟨s, subset_sUnion_of_mem sc, H1 s sc, ys, H2 s sc⟩

Premises used: And.intro, Exists.intro, Set.subset_sUnion_of_mem
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
c : Set (Set α)
H1 : ∀ s ∈ c, x ∈ s
H2 : ∀ s ∈ c, IsPreconnected s
y : α
s : Set α
sc : s ∈ c
ys : y ∈ s
⊢ ∃ t ⊆ ⋃₀ c, x ∈ t ∧ y ∈ t ∧ IsPreconnected t

Tactic:
exact ⟨s, subset_sUnion_of_mem sc, H1 s sc, ys, H2 s sc⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Sort u_3
s : ι → Set α
h₁ : Set.Nonempty.{u} (α := α) (⋂ (i : ι), s i)
h₂ : ∀ (i : ι), IsPreconnected (s i)
⊢ IsPreconnected.{u} (α := α) (⋃ (i : ι), s i)

Tactic:
Exists.elim h₁ fun f hf => isPreconnected_sUnion f _ hf (forall_mem_range.2 h₂)

Premises used: Iff.mpr, Set.forall_mem_range, isPreconnected_sUnion, Set.range, Exists.elim
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
t : Set α
H2 : x ∈ t
H4 : IsPreconnected t
r : Set α
H1 : x ∈ r
H3 : IsPreconnected r
⊢ x ∈ r

Tactic:
assumption
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
s t : Set α
H1 : x ∈ s
H2 : x ∈ t
H3 : IsPreconnected s
H4 : IsPreconnected t
⊢ x ∈ t

Tactic:
assumption
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
t : Set α
H2 : x ∈ t
H4 : IsPreconnected t
r : Set α
H1 : x ∈ r
H3 : IsPreconnected r
⊢ IsPreconnected r

Tactic:
assumption
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
x : α
s t : Set α
H1 : x ∈ s
H2 : x ∈ t
H3 : IsPreconnected s
H4 : IsPreconnected t
⊢ IsPreconnected t

Tactic:
assumption
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s t : Set α
H : (s ∩ t).Nonempty
hs : IsPreconnected s
ht : IsPreconnected t
rcases : ∀ (x : α) (hxs : x ∈ s) (hxt : x ∈ t), IsPreconnected (s ∪ t)
⊢ IsPreconnected (s ∪ t)

Tactic:
rcases H with ⟨x, hxs, hxt⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s t : Set α
hs : IsPreconnected s
ht : IsPreconnected t
x : α
hxs : x ∈ s
hxt : x ∈ t
⊢ IsPreconnected (s ∪ t)

Tactic:
hs.union x hxs hxt ht

Premises used: IsPreconnected.union
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s t : Set α
hs : IsPreconnected s
ht : IsPreconnected t
x : α
hxs : x ∈ s
hxt : x ∈ t
⊢ IsPreconnected (s ∪ t)

Tactic:
exact hs.union x hxs hxt ht

Premises used: IsPreconnected.union
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s t : Set α
H : (s ∩ t).Nonempty
Hs : IsConnected s
Ht : IsConnected t
rcases : ∀ (x : α) (hx : x ∈ s ∩ t), IsConnected (s ∪ t)
⊢ IsConnected (s ∪ t)

Tactic:
rcases H with ⟨x, hx⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s t : Set α
Hs : IsConnected s
Ht : IsConnected t
x : α
hx : x ∈ s ∩ t
⊢ IsConnected (s ∪ t)

Tactic:
⟨⟨x, mem_union_left t (mem_of_mem_inter_left hx)⟩, ?_⟩

Premises used: IsConnected, Set.mem_of_mem_inter_left, And.intro, Exists.intro, Set.mem_union_left
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s t : Set α
Hs : IsConnected s
Ht : IsConnected t
x : α
hx : x ∈ s ∩ t
refine : IsPreconnected (s ∪ t)
⊢ IsConnected (s ∪ t)

Tactic:
refine ⟨⟨x, mem_union_left t (mem_of_mem_inter_left hx)⟩, ?_⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s t : Set α
Hs : IsConnected s
Ht : IsConnected t
x : α
hx : x ∈ s ∩ t
⊢ IsPreconnected (s ∪ t)

Tactic:
Hs.isPreconnected.union x (mem_of_mem_inter_left hx) (mem_of_mem_inter_right hx)
    Ht.isPreconnected

Premises used: IsPreconnected.union, Set.mem_of_mem_inter_left, IsConnected.isPreconnected, Set.mem_of_mem_inter_right
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
s t : Set α
Hs : IsConnected s
Ht : IsConnected t
x : α
hx : x ∈ s ∩ t
⊢ IsPreconnected (s ∪ t)

Tactic:
exact Hs.isPreconnected.union x (mem_of_mem_inter_left hx) (mem_of_mem_inter_right hx)
    Ht.isPreconnected

Premises used: IsPreconnected.union, Set.mem_of_mem_inter_left, IsConnected.isPreconnected, Set.mem_of_mem_inter_right
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
S : Set (Set α)
K : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) S
H : ∀ s ∈ S, IsPreconnected s
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
Huv : ⋃₀ S ⊆ u ∪ v
a : α
hau : a ∈ u
s : Set α
hsS : s ∈ S
has : a ∈ s
b : α
hbv : b ∈ v
t : Set α
htS : t ∈ S
hbt : b ∈ t
⊢ ∃ r ∈ S, s ⊆ r ∧ t ⊆ r

Tactic:
K s hsS t htS
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
S : Set (Set α)
K : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) S
H : ∀ s ∈ S, IsPreconnected s
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
Huv : ⋃₀ S ⊆ u ∪ v
a : α
hau : a ∈ u
s : Set α
hsS : s ∈ S
has : a ∈ s
b : α
hbv : b ∈ v
t : Set α
htS : t ∈ S
hbt : b ∈ t
obtain : ∀ (r : Set α) (hrS : r ∈ S) (hsr : s ⊆ r) (htr : t ⊆ r), (⋃₀ S ∩ (u ∩ v)).Nonempty
⊢ (⋃₀ S ∩ (u ∩ v)).Nonempty

Tactic:
obtain ⟨r, hrS, hsr, htr⟩ : ∃ r ∈ S, s ⊆ r ∧ t ⊆ r := K s hsS t htS
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
S : Set (Set α)
K : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) S
H : ∀ s ∈ S, IsPreconnected s
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
Huv : ⋃₀ S ⊆ u ∪ v
a : α
hau : a ∈ u
s : Set α
hsS : s ∈ S
has : a ∈ s
b : α
hbv : b ∈ v
t : Set α
htS : t ∈ S
hbt : b ∈ t
r : Set α
hrS : r ∈ S
hsr : s ⊆ r
htr : t ⊆ r
⊢ (r ∩ (u ∩ v)).Nonempty

Tactic:
have Hnuv : (r ∩ (u ∩ v)).Nonempty :=
    H _ hrS u v hu hv ((subset_sUnion_of_mem hrS).trans Huv) ⟨a, hsr has, hau⟩ ⟨b, htr hbt, hbv⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
S : Set (Set α)
K : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) S
H : ∀ s ∈ S, IsPreconnected s
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
Huv : ⋃₀ S ⊆ u ∪ v
a : α
hau : a ∈ u
s : Set α
hsS : s ∈ S
has : a ∈ s
b : α
hbv : b ∈ v
t : Set α
htS : t ∈ S
hbt : b ∈ t
r : Set α
hrS : r ∈ S
hsr : s ⊆ r
htr : t ⊆ r
Hnuv : (r ∩ (u ∩ v)).Nonempty
⊢ r ∩ (u ∩ v) ⊆ ⋃₀ S ∩ (u ∩ v)

Tactic:
have Kruv : r ∩ (u ∩ v) ⊆ ⋃₀ S ∩ (u ∩ v) := inter_subset_inter_left _ (subset_sUnion_of_mem hrS)
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
S : Set (Set α)
K : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) S
H : ∀ s ∈ S, IsPreconnected s
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
Huv : ⋃₀ S ⊆ u ∪ v
a : α
hau : a ∈ u
s : Set α
hsS : s ∈ S
has : a ∈ s
b : α
hbv : b ∈ v
t : Set α
htS : t ∈ S
hbt : b ∈ t
r : Set α
hrS : r ∈ S
hsr : s ⊆ r
htr : t ⊆ r
Hnuv : (r ∩ (u ∩ v)).Nonempty
Kruv : r ∩ (u ∩ v) ⊆ ⋃₀ S ∩ (u ∩ v)
⊢ (⋃₀ S ∩ (u ∩ v)).Nonempty

Tactic:
Hnuv.mono Kruv

Premises used: Set.Nonempty.mono
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
S : Set (Set α)
K : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) S
H : ∀ s ∈ S, IsPreconnected s
u v : Set α
hu : IsOpen[inst] u
hv : IsOpen[inst] v
Huv : ⋃₀ S ⊆ u ∪ v
a : α
hau : a ∈ u
s : Set α
hsS : s ∈ S
has : a ∈ s
b : α
hbv : b ∈ v
t : Set α
htS : t ∈ S
hbt : b ∈ t
r : Set α
hrS : r ∈ S
hsr : s ⊆ r
htr : t ⊆ r
Hnuv : (r ∩ (u ∩ v)).Nonempty
Kruv : r ∩ (u ∩ v) ⊆ ⋃₀ S ∩ (u ∩ v)
⊢ (⋃₀ S ∩ (u ∩ v)).Nonempty

Tactic:
exact Hnuv.mono Kruv

Premises used: Set.Nonempty.mono
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : (i j : ι) → Prop := fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j : ι
hj : i ∈ t
⊢ ∃ p ⊆ t, i ∈ p ∧ i ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)

Tactic:
⟨{i}, singleton_subset_iff.mpr hi, mem_singleton i, mem_singleton i, ?_⟩

Premises used: Iff.mpr, Set.mem_singleton, Set.singleton_subset_iff, And.intro, Exists.intro, Singleton.singleton
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : (i j : ι) → Prop := fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j : ι
hj : i ∈ t
refl : IsPreconnected.{u} (α := α) (⋃ (j : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i} j), s j)
⊢ ∃ p ⊆ t, i ∈ p ∧ i ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)

Tactic:
refine ⟨{i}, singleton_subset_iff.mpr hi, mem_singleton i, mem_singleton i, ?_⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : (i j : ι) → Prop := fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j : ι
hj : i ∈ t
refl : IsPreconnected (s i)
⊢ IsPreconnected.{u} (α := α) (⋃ (j : ι), ⋃ (_ : Membership.mem (γ := Set ι) {i} j), s j)

Tactic:
rw [biUnion_singleton]

Premises used: Set.biUnion_singleton
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : (i j : ι) → Prop := fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j : ι
hj : i ∈ t
⊢ IsPreconnected (s i)

Tactic:
H i hi
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : (i j : ι) → Prop := fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j : ι
hj : i ∈ t
⊢ IsPreconnected (s i)

Tactic:
exact H i hi
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : (i j : ι) → Prop := fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j_1 j k : ι
h : ReflTransGen R i j
hjk : R j k
ih : ∀ (hj : j ∈ t), ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
hj : k ∈ t
tail :
  ∀ (p : Set ι) (hpt : p ⊆ t) (hip : i ∈ p) (hjp : j ∈ p) (hp : IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)),
    ∃ p ⊆ t, i ∈ p ∧ k ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
⊢ ∃ p ⊆ t, i ∈ p ∧ k ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)

Tactic:
obtain ⟨p, hpt, hip, hjp, hp⟩ := ih hjk.2

Premises used: And.right
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : (i j : ι) → Prop := fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j_1 j k : ι
h : ReflTransGen R i j
hjk : R j k
ih : ∀ (hj : j ∈ t), ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
⊢ ∃ p ⊆ t, i ∈ p ∧ k ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)

Tactic:
⟨insert k p, insert_subset_iff.mpr ⟨hj, hpt⟩, mem_insert_of_mem k hip,
        mem_insert k p, ?_⟩

Premises used: Iff.mpr, Set.mem_insert_of_mem, Insert.insert, Set.insert_subset_iff, And.intro, Exists.intro, Set.mem_insert
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : (i j : ι) → Prop := fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j_1 j k : ι
h : ReflTransGen R i j
hjk : R j k
ih : ∀ (hj : j ∈ t), ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
tail : IsPreconnected.{u} (α := α) (⋃ j ∈ insert k p, s j)
⊢ ∃ p ⊆ t, i ∈ p ∧ k ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)

Tactic:
refine ⟨insert k p, insert_subset_iff.mpr ⟨hj, hpt⟩, mem_insert_of_mem k hip,
        mem_insert k p, ?_⟩
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : (i j : ι) → Prop := fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j_1 j k : ι
h : ReflTransGen R i j
hjk : R j k
ih : ∀ (hj : j ∈ t), ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
tail : IsPreconnected (s k ∪ ⋃ x ∈ p, s x)
⊢ IsPreconnected.{u} (α := α) (⋃ j ∈ insert k p, s j)

Tactic:
rw [biUnion_insert]

Premises used: Set.biUnion_insert
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : (i j : ι) → Prop := fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j_1 j k : ι
h : ReflTransGen R i j
hjk : R j k
ih : ∀ (hj : j ∈ t), ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
⊢ IsPreconnected (s k ∪ ⋃ x ∈ p, s x)

Tactic:
(H k hj).union' (hjk.1.mono ?_) hp

Premises used: Set.Nonempty.mono, And.left, IsPreconnected.union'
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : (i j : ι) → Prop := fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j_1 j k : ι
h : ReflTransGen R i j
hjk : R j k
ih : ∀ (hj : j ∈ t), ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
tail : s j ∩ s k ⊆ s k ∩ ⋃ x ∈ p, s x
⊢ IsPreconnected (s k ∪ ⋃ x ∈ p, s x)

Tactic:
refine (H k hj).union' (hjk.1.mono ?_) hp

Premises used: Set.Nonempty.mono, And.left, IsPreconnected.union'
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : (i j : ι) → Prop := fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j_1 j k : ι
h : ReflTransGen R i j
hjk : R j k
ih : ∀ (hj : j ∈ t), ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
tail : s k ∩ s j ⊆ s k ∩ ⋃ x ∈ p, s x
⊢ s j ∩ s k ⊆ s k ∩ ⋃ x ∈ p, s x

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : (i j : ι) → Prop := fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j_1 j k : ι
h : ReflTransGen R i j
hjk : R j k
ih : ∀ (hj : j ∈ t), ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
⊢ s k ∩ s j ⊆ s k ∩ ⋃ x ∈ p, s x

Tactic:
inter_subset_inter_right _ (subset_biUnion_of_mem hjp)

Premises used: Set.inter_subset_inter_right, Set.subset_biUnion_of_mem
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : (i j : ι) → Prop := fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j_1 j k : ι
h : ReflTransGen R i j
hjk : R j k
ih : ∀ (hj : j ∈ t), ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
⊢ s k ∩ s j ⊆ s k ∩ ⋃ x ∈ p, s x

Tactic:
exact inter_subset_inter_right _ (subset_biUnion_of_mem hjp)

Premises used: Set.inter_subset_inter_right, Set.subset_biUnion_of_mem
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : (i j : ι) → Prop := fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j : ι
hj : j ∈ t
h : ReflTransGen R i j
refl : ∀ (hj : i ∈ t), ∃ p ⊆ t, i ∈ p ∧ i ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
tail :
  ∀ {j k : ι},
    ReflTransGen R i j →
      ∀ (hjk : R j k) (ih : ∀ (hj : j ∈ t), ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j))
        (hj : k ∈ t), ∃ p ⊆ t, i ∈ p ∧ k ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
⊢ ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)

Tactic:
induction h with
    | refl =>
      refine ⟨{i}, singleton_subset_iff.mpr hi, mem_singleton i, mem_singleton i, ?_⟩
      rw [biUnion_singleton]
      exact H i hi
    | @tail j k _ hjk ih =>
      obtain ⟨p, hpt, hip, hjp, hp⟩ := ih hjk.2
      refine ⟨insert k p, insert_subset_iff.mpr ⟨hj, hpt⟩, mem_insert_of_mem k hip,
        mem_insert k p, ?_⟩
      rw [biUnion_insert]
      refine (H k hj).union' (hjk.1.mono ?_) hp
      rw [inter_comm]
      exact inter_subset_inter_right _ (subset_biUnion_of_mem hjp)

Premises used: Set.biUnion_singleton, Set.biUnion_insert, Set.inter_comm, refl
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : (i j : ι) → Prop := fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
⊢ ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)

Tactic:
have P : ∀ i, i ∈ t → ∀ j, j ∈ t → ReflTransGen R i j →
      ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j) := fun i hi j hj h => by
    induction h with
    | refl =>
      refine ⟨{i}, singleton_subset_iff.mpr hi, mem_singleton i, mem_singleton i, ?_⟩
      rw [biUnion_singleton]
      exact H i hi
    | @tail j k _ hjk ih =>
      obtain ⟨p, hpt, hip, hjp, hp⟩ := ih hjk.2
      refine ⟨insert k p, insert_subset_iff.mpr ⟨hj, hpt⟩, mem_insert_of_mem k hip,
        mem_insert k p, ?_⟩
      rw [biUnion_insert]
      refine (H k hj).union' (hjk.1.mono ?_) hp
      rw [inter_comm]
      exact inter_subset_inter_right _ (subset_biUnion_of_mem hjp)
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : (i j : ι) → Prop := fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
P : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
⊢ IsPreconnected.{u} (α := α) (⋃ n ∈ t, s n)

Tactic:
isPreconnected_of_forall_pair ?_

Premises used: isPreconnected_of_forall_pair
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : (i j : ι) → Prop := fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
P : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
refine :
  ∀ (x : α),
    Membership.mem (γ := Set α) (⋃ n ∈ t, s n) x →
      ∀ (y : α),
        Membership.mem (γ := Set α) (⋃ n ∈ t, s n) y → ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
⊢ IsPreconnected.{u} (α := α) (⋃ n ∈ t, s n)

Tactic:
refine isPreconnected_of_forall_pair ?_

Premises used: isPreconnected_of_forall_pair
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : (i j : ι) → Prop := fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
P : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
x : α
hx : Membership.mem (γ := Set α) (⋃ n ∈ t, s n) x
y : α
hy : Membership.mem (γ := Set α) (⋃ n ∈ t, s n) y
obtain : ∀ (i : ι) (hi : i ∈ t) (hxi : x ∈ s i), ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
⊢ ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1

Tactic:
obtain ⟨i : ι, hi : i ∈ t, hxi : x ∈ s i⟩ := mem_iUnion₂.1 hx

Premises used: Set.mem_iUnion₂, Iff.mp
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : (i j : ι) → Prop := fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
P : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
x : α
hx : Membership.mem (γ := Set α) (⋃ n ∈ t, s n) x
y : α
hy : Membership.mem (γ := Set α) (⋃ n ∈ t, s n) y
i : ι
hi : i ∈ t
hxi : x ∈ s i
obtain : ∀ (j : ι) (hj : j ∈ t) (hyj : y ∈ s j), ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
⊢ ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1

Tactic:
obtain ⟨j : ι, hj : j ∈ t, hyj : y ∈ s j⟩ := mem_iUnion₂.1 hy

Premises used: Set.mem_iUnion₂, Iff.mp
-- Module: Mathlib.Topology.Connected.Basic
Goal:
α : Type u
inst : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : (i j : ι) → Prop := fun (i j : ι) ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
P : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)
x : α
hx : Membership.mem (γ := Set α) (⋃ n ∈ t, s n) x
y : α
hy : Membership.mem (γ := Set α) (⋃ n ∈ t, s n) y
i : ι
hi : i ∈ t
hxi : x ∈ s i
j : ι
hj : j ∈ t
hyj : y ∈ s j
obtain :
  ∀ (p : Set ι) (hpt : p ⊆ t) (hip : i ∈ p) (hjp : j ∈ p) (hp : IsPreconnected.{u} (α := α) (⋃ j ∈ p, s j)),
    ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
⊢ ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1

Tactic:
obtain ⟨p, hpt, hip, hjp, hp⟩ := P i hi j hj (K i hi j hj)