Theorem: IsPreconnected.sUnion_of_pairwise_exists_isPreconnected (Ray/Misc/Topology.lean)

State before:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
⊢ IsPreconnected S.sUnion
Tactic:
refine isPreconnected_of_forall_pair fun x hx y hy ↦ ?_
State after:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
⊢ ∃ t ⊆ S.sUnion, x ∈ t ∧ y ∈ t ∧ IsPreconnected t

State before:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
⊢ ∃ t ⊆ S.sUnion, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
Tactic:
rcases mem_sUnion.1 hx with ⟨s, hs, hxs⟩
State after:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
⊢ ∃ t ⊆ S.sUnion, x ∈ t ∧ y ∈ t ∧ IsPreconnected t

State before:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
⊢ ∃ t ⊆ S.sUnion, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
Tactic:
rcases mem_sUnion.1 hy with ⟨t, ht, hyt⟩
State after:
case intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
⊢ ∃ t ⊆ S.sUnion, x ∈ t ∧ y ∈ t ∧ IsPreconnected t

State before:
case intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
⊢ ∃ t ⊆ S.sUnion, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
Tactic:
rcases eq_or_ne s t with rfl | hst
State after:
case intro.intro.intro.intro.inl
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
ht : s ∈ S
hyt : y ∈ s
⊢ ∃ t ⊆ S.sUnion, x ∈ t ∧ y ∈ t ∧ IsPreconnected t

case intro.intro.intro.intro.inr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
⊢ ∃ t ⊆ S.sUnion, x ∈ t ∧ y ∈ t ∧ IsPreconnected t

State before:
case intro.intro.intro.intro.inl
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
ht : s ∈ S
hyt : y ∈ s
⊢ ∃ t ⊆ S.sUnion, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
Tactic:
exact ⟨s, subset_sUnion_of_mem hs, hxs, hyt, hSc s hs⟩
State after:
no goals

State before:
case intro.intro.intro.intro.inr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
⊢ ∃ t ⊆ S.sUnion, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
Tactic:
rcases h hs ht hst ⟨x, hxs⟩ ⟨y, hyt⟩ with ⟨u, huS, hsu, hut, hu⟩
State after:
case intro.intro.intro.intro.inr.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
u : Set X
huS : u ⊆ S.sUnion
hsu : (s ∩ u).Nonempty
hut : (u ∩ t).Nonempty
hu : IsPreconnected u
⊢ ∃ t ⊆ S.sUnion, x ∈ t ∧ y ∈ t ∧ IsPreconnected t

State before:
case intro.intro.intro.intro.inr.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
u : Set X
huS : u ⊆ S.sUnion
hsu : (s ∩ u).Nonempty
hut : (u ∩ t).Nonempty
hu : IsPreconnected u
⊢ ∃ t ⊆ S.sUnion, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
Tactic:
refine ⟨s ∪ u ∪ t, ?_, ?_, ?_, ?_⟩
State after:
case intro.intro.intro.intro.inr.intro.intro.intro.intro.refine_1
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
u : Set X
huS : u ⊆ S.sUnion
hsu : (s ∩ u).Nonempty
hut : (u ∩ t).Nonempty
hu : IsPreconnected u
⊢ s ∪ u ∪ t ⊆ S.sUnion

case intro.intro.intro.intro.inr.intro.intro.intro.intro.refine_2
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
u : Set X
huS : u ⊆ S.sUnion
hsu : (s ∩ u).Nonempty
hut : (u ∩ t).Nonempty
hu : IsPreconnected u
⊢ x ∈ s ∪ u ∪ t

case intro.intro.intro.intro.inr.intro.intro.intro.intro.refine_3
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
u : Set X
huS : u ⊆ S.sUnion
hsu : (s ∩ u).Nonempty
hut : (u ∩ t).Nonempty
hu : IsPreconnected u
⊢ y ∈ s ∪ u ∪ t

case intro.intro.intro.intro.inr.intro.intro.intro.intro.refine_4
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
u : Set X
huS : u ⊆ S.sUnion
hsu : (s ∩ u).Nonempty
hut : (u ∩ t).Nonempty
hu : IsPreconnected u
⊢ IsPreconnected (s ∪ u ∪ t)

State before:
case intro.intro.intro.intro.inr.intro.intro.intro.intro.refine_1
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
u : Set X
huS : u ⊆ S.sUnion
hsu : (s ∩ u).Nonempty
hut : (u ∩ t).Nonempty
hu : IsPreconnected u
⊢ s ∪ u ∪ t ⊆ S.sUnion
Tactic:
simp [*, subset_sUnion_of_mem]
State after:
no goals

State before:
case intro.intro.intro.intro.inr.intro.intro.intro.intro.refine_2
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
u : Set X
huS : u ⊆ S.sUnion
hsu : (s ∩ u).Nonempty
hut : (u ∩ t).Nonempty
hu : IsPreconnected u
⊢ x ∈ s ∪ u ∪ t
Tactic:
simp [*]
State after:
no goals

State before:
case intro.intro.intro.intro.inr.intro.intro.intro.intro.refine_3
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
u : Set X
huS : u ⊆ S.sUnion
hsu : (s ∩ u).Nonempty
hut : (u ∩ t).Nonempty
hu : IsPreconnected u
⊢ y ∈ s ∪ u ∪ t
Tactic:
simp [*]
State after:
no goals

State before:
case intro.intro.intro.intro.inr.intro.intro.intro.intro.refine_4
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
u : Set X
huS : u ⊆ S.sUnion
hsu : (s ∩ u).Nonempty
hut : (u ∩ t).Nonempty
hu : IsPreconnected u
⊢ IsPreconnected (s ∪ u ∪ t)
Tactic:
refine ((hSc s hs).union' hsu hu).union' (hut.mono ?_) (hSc t ht)
State after:
case intro.intro.intro.intro.inr.intro.intro.intro.intro.refine_4
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
u : Set X
huS : u ⊆ S.sUnion
hsu : (s ∩ u).Nonempty
hut : (u ∩ t).Nonempty
hu : IsPreconnected u
⊢ u ∩ t ⊆ (s ∪ u) ∩ t

State before:
case intro.intro.intro.intro.inr.intro.intro.intro.intro.refine_4
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
u : Set X
huS : u ⊆ S.sUnion
hsu : (s ∩ u).Nonempty
hut : (u ∩ t).Nonempty
hu : IsPreconnected u
⊢ u ∩ t ⊆ (s ∪ u) ∩ t
Tactic:
exact inter_subset_inter_left _ (subset_union_right _ _)
State after:
no goals