-- Mathlib/Topology/Connected/Basic.lean
theorem IsPreconnected.sUnion_directed {S : Set (Set α)} (K : DirectedOn (· ⊆ ·) S)
    (H : ∀ s ∈ S, IsPreconnected s) : IsPreconnected (⋃₀ S)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
S : Set (Set α)
K : DirectedOn (fun x1 x2 => x1 ⊆ x2) S
H : ∀ s ∈ S, IsPreconnected s
u v : Set α
hu : IsOpen u
hv : IsOpen 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
⊢ (⋃₀ S ∩ (u ∩ v)).Nonempty

Tactic:
obtain ⟨r, hrS, hsr, htr⟩ : ∃ r ∈ S, s ⊆ r ∧ t ⊆ r := K s hsS t htS

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
S : Set (Set α)
K : DirectedOn (fun x1 x2 => x1 ⊆ x2) S
H : ∀ s ∈ S, IsPreconnected s
u v : Set α
hu : IsOpen u
hv : IsOpen 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
⊢ (⋃₀ S ∩ (u ∩ v)).Nonempty

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
S : Set (Set α)
K : DirectedOn (fun x1 x2 => x1 ⊆ x2) S
H : ∀ s ∈ S, IsPreconnected s
u v : Set α
hu : IsOpen u
hv : IsOpen 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
⊢ (⋃₀ S ∩ (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⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
S : Set (Set α)
K : DirectedOn (fun x1 x2 => x1 ⊆ x2) S
H : ∀ s ∈ S, IsPreconnected s
u v : Set α
hu : IsOpen u
hv : IsOpen 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
⊢ (⋃₀ S ∩ (u ∩ v)).Nonempty

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
S : Set (Set α)
K : DirectedOn (fun x1 x2 => x1 ⊆ x2) S
H : ∀ s ∈ S, IsPreconnected s
u v : Set α
hu : IsOpen u
hv : IsOpen 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

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
S : Set (Set α)
K : DirectedOn (fun x1 x2 => x1 ⊆ x2) S
H : ∀ s ∈ S, IsPreconnected s
⊢ IsPreconnected (⋃₀ S)

Tactic:
rintro u v hu hv Huv ⟨a, ⟨s, hsS, has⟩, hau⟩ ⟨b, ⟨t, htS, hbt⟩, hbv⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
S : Set (Set α)
K : DirectedOn (fun x1 x2 => x1 ⊆ x2) S
H : ∀ s ∈ S, IsPreconnected s
u v : Set α
hu : IsOpen u
hv : IsOpen 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
⊢ (⋃₀ S ∩ (u ∩ v)).Nonempty

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
S : Set (Set α)
K : DirectedOn (fun x1 x2 => x1 ⊆ x2) S
H : ∀ s ∈ S, IsPreconnected s
u v : Set α
hu : IsOpen u
hv : IsOpen 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
⊢ (⋃₀ S ∩ (u ∩ v)).Nonempty

Tactic:
have Kruv : r ∩ (u ∩ v) ⊆ ⋃₀ S ∩ (u ∩ v) := inter_subset_inter_left _ (subset_sUnion_of_mem hrS)

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
S : Set (Set α)
K : DirectedOn (fun x1 x2 => x1 ⊆ x2) S
H : ∀ s ∈ S, IsPreconnected s
u v : Set α
hu : IsOpen u
hv : IsOpen 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