-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma extend_finset_to_connected (Gpc : G.Preconnected) {t : Finset V} (tn : t.Nonempty) :
    ∃ (t' : Finset V), t ⊆ t' ∧ (G.induce (t' : Set V)).Connected

Proof state:
case intro.refine_2.patches
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v : V
hv : v ∈ ↑(t.biUnion fun v => (Nonempty.some ⋯).support.toFinset)
⊢ ∃ s' ⊆ ↑(t.biUnion fun v => (Nonempty.some ⋯).support.toFinset),
    ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩

Tactic:
simp only [Finset.mem_coe, Finset.mem_biUnion, List.mem_toFinset, exists_prop] at hv

Result:
case intro.refine_2.patches
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v : V
hv : ∃ a ∈ t, v ∈ (Nonempty.some ⋯).support
⊢ ∃ s' ⊆ ↑(t.biUnion fun v => (Nonempty.some ⋯).support.toFinset),
    ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩

Proof state:
case intro.refine_2.patches.intro.intro.refine_2
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
⊢ ∃ (hu' : u ∈ {x | x ∈ (Nonempty.some ⋯).support}) (hv' : v ∈ {x | x ∈ (Nonempty.some ⋯).support}),
    (induce {x | x ∈ (Nonempty.some ⋯).support} G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩

Tactic:
simp only [Set.mem_setOf_eq, Walk.start_mem_support, exists_true_left]

Result:
case intro.refine_2.patches.intro.intro.refine_2
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
⊢ ∃ (h : v ∈ (Nonempty.some ⋯).support), (induce {x | x ∈ (Nonempty.some ⋯).support} G).Reachable ⟨u, ⋯⟩ ⟨v, ⋯⟩

Proof state:
case intro
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
⊢ ∃ t', t ⊆ t' ∧ (induce (↑t') G).Connected

Tactic:
refine ⟨t.biUnion (fun v => (Gpc u v).some.support.toFinset), fun v vt => ?_, ?_⟩

Result:
case intro.refine_1
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v : V
vt : v ∈ t
⊢ v ∈ t.biUnion fun v => (Nonempty.some ⋯).support.toFinset

case intro.refine_2
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
⊢ (induce (↑(t.biUnion fun v => (Nonempty.some ⋯).support.toFinset)) G).Connected

Proof state:
case intro.refine_2.patches.intro.intro.refine_1
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
⊢ {x | x ∈ (Nonempty.some ⋯).support} ⊆ ⋃ x ∈ t, {a | a ∈ (Nonempty.some ⋯).support}

Tactic:
exact fun x xw => Set.mem_iUnion₂.mpr ⟨w,wt,xw⟩

Result:
no goals

Proof state:
case intro.refine_2.hu
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
⊢ u ∈ ↑(t.biUnion fun v => (Nonempty.some ⋯).support.toFinset)

Tactic:
simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset, Set.mem_iUnion,
           Set.mem_setOf_eq, Walk.start_mem_support, exists_prop, and_true]

Result:
case intro.refine_2.hu
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
⊢ ∃ i, i ∈ t

Proof state:
case intro.refine_1
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v : V
vt : v ∈ t
⊢ ∃ a ∈ t, v ∈ (Nonempty.some ⋯).support

Tactic:
exact ⟨v, vt, Walk.end_mem_support _⟩

Result:
no goals

Proof state:
case intro.refine_2.patches.intro.intro.refine_2
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
⊢ ∃ (h : v ∈ (Nonempty.some ⋯).support), (induce {x | x ∈ (Nonempty.some ⋯).support} G).Reachable ⟨u, ⋯⟩ ⟨v, ⋯⟩

Tactic:
refine ⟨hw, Walk.connected_induce_support _ _ _⟩

Result:
no goals

Proof state:
case intro.refine_2.hu
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
⊢ ∃ i, i ∈ t

Tactic:
exact ⟨u, ut⟩

Result:
no goals

Proof state:
case intro.refine_2.patches
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
⊢ ∀ {v : V},
    v ∈ ↑(t.biUnion fun v => (Nonempty.some ⋯).support.toFinset) →
      ∃ s' ⊆ ↑(t.biUnion fun v => (Nonempty.some ⋯).support.toFinset),
        ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩

Tactic:
intros v hv

Result:
case intro.refine_2.patches
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v : V
hv : v ∈ ↑(t.biUnion fun v => (Nonempty.some ⋯).support.toFinset)
⊢ ∃ s' ⊆ ↑(t.biUnion fun v => (Nonempty.some ⋯).support.toFinset),
    ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩

Proof state:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
tn : t.Nonempty
⊢ ∃ t', t ⊆ t' ∧ (induce (↑t') G).Connected

Tactic:
obtain ⟨u, ut⟩ := tn

Result:
case intro
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
⊢ ∃ t', t ⊆ t' ∧ (induce (↑t') G).Connected

Proof state:
case intro.refine_2
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
⊢ (induce (↑(t.biUnion fun v => (Nonempty.some ⋯).support.toFinset)) G).Connected

Tactic:
apply G.induce_connected_of_patches u

Result:
case intro.refine_2.hu
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
⊢ u ∈ ↑(t.biUnion fun v => (Nonempty.some ⋯).support.toFinset)

case intro.refine_2.patches
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
⊢ ∀ {v : V},
    v ∈ ↑(t.biUnion fun v => (Nonempty.some ⋯).support.toFinset) →
      ∃ s' ⊆ ↑(t.biUnion fun v => (Nonempty.some ⋯).support.toFinset),
        ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩

Proof state:
case intro.refine_1
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v : V
vt : v ∈ t
⊢ v ∈ t.biUnion fun v => (Nonempty.some ⋯).support.toFinset

Tactic:
simp only [Finset.mem_biUnion, List.mem_toFinset, exists_prop]

Result:
case intro.refine_1
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v : V
vt : v ∈ t
⊢ ∃ a ∈ t, v ∈ (Nonempty.some ⋯).support

Proof state:
case intro.refine_2.patches.intro.intro.refine_1
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
⊢ {x | x ∈ (Nonempty.some ⋯).support} ⊆ ↑(t.biUnion fun v => (Nonempty.some ⋯).support.toFinset)

Tactic:
simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset]

Result:
case intro.refine_2.patches.intro.intro.refine_1
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
⊢ {x | x ∈ (Nonempty.some ⋯).support} ⊆ ⋃ x ∈ t, {a | a ∈ (Nonempty.some ⋯).support}

Proof state:
case intro.refine_2.patches
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v : V
hv : ∃ a ∈ t, v ∈ (Nonempty.some ⋯).support
⊢ ∃ s' ⊆ ↑(t.biUnion fun v => (Nonempty.some ⋯).support.toFinset),
    ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩

Tactic:
obtain ⟨w, wt, hw⟩ := hv

Result:
case intro.refine_2.patches.intro.intro
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ (Nonempty.some ⋯).support
⊢ ∃ s' ⊆ ↑(t.biUnion fun v => (Nonempty.some ⋯).support.toFinset),
    ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩