-- Mathlib/Topology/Connected/Basic.lean
theorem IsPreconnected.biUnion_of_reflTransGen {ι : Type*} {t : Set ι} {s : ι → Set α}
    (H : ∀ i ∈ t, IsPreconnected (s i))
    (K : ∀ i, i ∈ t → ∀ j, j ∈ t → ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t) i j) :
    IsPreconnected (⋃ n ∈ t, s n)

Proof state:
case refl
α : 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 : ι → ι → 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 (⋃ j ∈ p, s j)

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

Result:
case refl
α : 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 : ι → ι → Prop := fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j : ι
hj : i ∈ t
⊢ IsPreconnected (⋃ j ∈ {i}, s j)

Proof state:
case tail
α : 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 : ι → ι → Prop := fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j✝ j k : ι
a✝ : ReflTransGen R i j
hjk : R j k
ih : j ∈ t → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)
hj : k ∈ t
⊢ ∃ p ⊆ t, i ∈ p ∧ k ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)

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

Result:
case tail.intro.intro.intro.intro
α : 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 : ι → ι → Prop := fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j✝ j k : ι
a✝ : ReflTransGen R i j
hjk : R j k
ih : j ∈ t → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected (⋃ j ∈ p, s j)
⊢ ∃ p ⊆ t, i ∈ p ∧ k ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)

Proof state:
α : 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 : ι → ι → Prop := fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t
⊢ IsPreconnected (⋃ n ∈ t, s n)

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)

Result:
α : 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 : ι → ι → 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 (⋃ j ∈ p, s j)
⊢ IsPreconnected (⋃ n ∈ t, s n)

Proof state:
case refl
α : 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 : ι → ι → Prop := fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j : ι
hj : i ∈ t
⊢ IsPreconnected (⋃ j ∈ {i}, s j)

Tactic:
rw [biUnion_singleton]

Result:
case refl
α : 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 : ι → ι → Prop := fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j : ι
hj : i ∈ t
⊢ IsPreconnected (s i)

Proof state:
case intro.intro.intro.intro
α : 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 : ι → ι → 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 (⋃ j ∈ p, s j)
x : α
hx : x ∈ ⋃ n ∈ t, s n
y : α
hy : y ∈ ⋃ n ∈ t, s n
i : ι
hi : i ∈ t
hxi : x ∈ s i
j : ι
hj : j ∈ t
hyj : y ∈ s j
⊢ ∃ 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)

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
α : 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 : ι → ι → 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 (⋃ j ∈ p, s j)
x : α
hx : x ∈ ⋃ n ∈ t, s n
y : α
hy : y ∈ ⋃ n ∈ t, s n
i : ι
hi : i ∈ t
hxi : x ∈ s i
j : ι
hj : j ∈ t
hyj : y ∈ s j
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected (⋃ j ∈ p, s j)
⊢ ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1

Proof state:
case tail.intro.intro.intro.intro
α : 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 : ι → ι → Prop := fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t
i : ι
hi : i ∈ t
j✝ j k : ι
a✝ : ReflTransGen R i j
hjk : R j k
ih : j ∈ t → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)
hj : k ∈ t
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected (⋃ 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)

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
α : 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 : ι → ι → 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 (⋃ j ∈ p, s j)
x : α
hx : x ∈ ⋃ n ∈ t, s n
y : α
hy : y ∈ ⋃ n ∈ t, s n
i : ι
hi : i ∈ t
hxi : x ∈ s i
j : ι
hj : j ∈ t
hyj : y ∈ s j
p : Set ι
hpt : p ⊆ t
hip : i ∈ p
hjp : j ∈ p
hp : IsPreconnected (⋃ j ∈ p, s j)
⊢ ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1

Tactic:
exact ⟨⋃ j ∈ p, s j, biUnion_subset_biUnion_left hpt, mem_biUnion hip hxi,
  mem_biUnion hjp hyj, hp⟩

Result:
no goals

Proof state:
α : 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 : ι → ι → 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 (⋃ j ∈ p, s j)
⊢ IsPreconnected (⋃ n ∈ t, s n)

Tactic:
refine isPreconnected_of_forall_pair ?_

Result:
α : 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 : ι → ι → 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 (⋃ j ∈ p, s j)
⊢ ∀ x ∈ ⋃ n ∈ t, s n, ∀ y ∈ ⋃ n ∈ t, s n, ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1