-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma induce_sUnion_connected_of_pairwise_not_disjoint {S : Set (Set V)} (Sn : S.Nonempty)
    (Snd : ∀ {s t}, s ∈ S → t ∈ S → (s ∩ t).Nonempty)
    (Sc : ∀ {s}, s ∈ S → (G.induce s).Connected) :
    (G.induce (⋃₀ S)).Connected

Proof state:
case intro.intro.mk
V : Type u
G : SimpleGraph V
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
w : V
hw : ∃ t ∈ S, w ∈ t
⊢ ∃ s' ⊆ ⋃₀ S, ∃ (hu' : v ∈ s') (hv' : w ∈ s'), (induce s' G).Reachable ⟨v, hu'⟩ ⟨w, hv'⟩

Tactic:
obtain ⟨t, tS, wt⟩ := hw

Result:
case intro.intro.mk.intro.intro
V : Type u
G : SimpleGraph V
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
w : V
t : Set V
tS : t ∈ S
wt : w ∈ t
⊢ ∃ s' ⊆ ⋃₀ S, ∃ (hu' : v ∈ s') (hv' : w ∈ s'), (induce s' G).Reachable ⟨v, hu'⟩ ⟨w, hv'⟩

Proof state:
case intro
V : Type u
G : SimpleGraph V
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
s : Set V
sS : s ∈ S
⊢ (induce (⋃₀ S) G).Connected

Tactic:
obtain ⟨v, vs⟩ := (Sc sS).nonempty

Result:
case intro.intro.mk
V : Type u
G : SimpleGraph V
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
⊢ (induce (⋃₀ S) G).Connected

Proof state:
V : Type u
G : SimpleGraph V
S : Set (Set V)
Sn : S.Nonempty
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
⊢ (induce (⋃₀ S) G).Connected

Tactic:
obtain ⟨s, sS⟩ := Sn

Result:
case intro
V : Type u
G : SimpleGraph V
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
s : Set V
sS : s ∈ S
⊢ (induce (⋃₀ S) G).Connected

Proof state:
case intro.intro.mk
V : Type u
G : SimpleGraph V
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
⊢ ∀ {v_1 : V}, v_1 ∈ ⋃₀ S → ∃ s' ⊆ ⋃₀ S, ∃ (hu' : v ∈ s') (hv' : v_1 ∈ s'), (induce s' G).Reachable ⟨v, hu'⟩ ⟨v_1, hv'⟩

Tactic:
rintro w hw

Result:
case intro.intro.mk
V : Type u
G : SimpleGraph V
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
w : V
hw : w ∈ ⋃₀ S
⊢ ∃ s' ⊆ ⋃₀ S, ∃ (hu' : v ∈ s') (hv' : w ∈ s'), (induce s' G).Reachable ⟨v, hu'⟩ ⟨w, hv'⟩

Proof state:
case intro.intro.mk.intro.intro
V : Type u
G : SimpleGraph V
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
w : V
t : Set V
tS : t ∈ S
wt : w ∈ t
⊢ ∃ s' ⊆ ⋃₀ S, ∃ (hu' : v ∈ s') (hv' : w ∈ s'), (induce s' G).Reachable ⟨v, hu'⟩ ⟨w, hv'⟩

Tactic:
refine ⟨s ∪ t, Set.union_subset (Set.subset_sUnion_of_mem sS) (Set.subset_sUnion_of_mem tS),
        Or.inl vs, Or.inr wt, induce_union_connected (Sc sS) (Sc tS) (Snd sS tS) _ _⟩

Result:
no goals

Proof state:
case intro.intro.mk
V : Type u
G : SimpleGraph V
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
⊢ (induce (⋃₀ S) G).Connected

Tactic:
apply G.induce_connected_of_patches _ (Set.subset_sUnion_of_mem sS vs)

Result:
case intro.intro.mk
V : Type u
G : SimpleGraph V
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
⊢ ∀ {v_1 : V}, v_1 ∈ ⋃₀ S → ∃ s' ⊆ ⋃₀ S, ∃ (hu' : v ∈ s') (hv' : v_1 ∈ s'), (induce s' G).Reachable ⟨v, hu'⟩ ⟨v_1, hv'⟩

Proof state:
case intro.intro.mk
V : Type u
G : SimpleGraph V
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
w : V
hw : w ∈ ⋃₀ S
⊢ ∃ s' ⊆ ⋃₀ S, ∃ (hu' : v ∈ s') (hv' : w ∈ s'), (induce s' G).Reachable ⟨v, hu'⟩ ⟨w, hv'⟩

Tactic:
simp only [Set.mem_sUnion, exists_prop] at hw

Result:
case intro.intro.mk
V : Type u
G : SimpleGraph V
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty
Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
w : V
hw : ∃ t ∈ S, w ∈ t
⊢ ∃ s' ⊆ ⋃₀ S, ∃ (hu' : v ∈ s') (hv' : w ∈ s'), (induce s' G).Reachable ⟨v, hu'⟩ ⟨w, hv'⟩