[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
⊢ Subgraph.Connected H ↔ Subgraph.Preconnected H ∧ Set.Nonempty H.verts
[PROOFSTEP]
rw [H.connected_iff', connected_iff, H.preconnected_iff, Set.nonempty_coe_sort]
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
h : Subgraph.Connected H
⊢ Subgraph.Preconnected H
[PROOFSTEP]
rw [H.connected_iff] at h 
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
h : Subgraph.Preconnected H ∧ Set.Nonempty H.verts
⊢ Subgraph.Preconnected H
[PROOFSTEP]
exact h.1
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
h : Subgraph.Connected H
⊢ Set.Nonempty H.verts
[PROOFSTEP]
rw [H.connected_iff] at h 
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
h : Subgraph.Preconnected H ∧ Set.Nonempty H.verts
⊢ Set.Nonempty H.verts
[PROOFSTEP]
exact h.2
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v : V
⊢ Subgraph.Connected (SimpleGraph.singletonSubgraph G v)
[PROOFSTEP]
refine ⟨⟨?_⟩⟩
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v : V
⊢ Preconnected (Subgraph.coe (SimpleGraph.singletonSubgraph G v))
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case mk.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v a : V
ha : a ∈ (SimpleGraph.singletonSubgraph G v).verts
b : V
hb : b ∈ (SimpleGraph.singletonSubgraph G v).verts
⊢ Reachable (Subgraph.coe (SimpleGraph.singletonSubgraph G v)) { val := a, property := ha } { val := b, property := hb }
[PROOFSTEP]
simp only [singletonSubgraph_verts, Set.mem_singleton_iff] at ha hb 
[GOAL]
case mk.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v a : V
ha✝ : a ∈ (SimpleGraph.singletonSubgraph G v).verts
b : V
hb✝ : b ∈ (SimpleGraph.singletonSubgraph G v).verts
ha : a = v
hb : b = v
⊢ Reachable (Subgraph.coe (SimpleGraph.singletonSubgraph G v)) { val := a, property := ha✝ }
    { val := b, property := hb✝ }
[PROOFSTEP]
subst_vars
[GOAL]
case mk.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
b : V
ha hb : b = b
⊢ Reachable (Subgraph.coe (SimpleGraph.singletonSubgraph G b)) { val := b, property := (_ : b = b) }
    { val := b, property := (_ : b = b) }
[PROOFSTEP]
rfl
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w : V
hvw : SimpleGraph.Adj G v w
⊢ Subgraph.Connected (subgraphOfAdj G hvw)
[PROOFSTEP]
refine ⟨⟨?_⟩⟩
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w : V
hvw : SimpleGraph.Adj G v w
⊢ Preconnected (Subgraph.coe (subgraphOfAdj G hvw))
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case mk.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w : V
hvw : SimpleGraph.Adj G v w
a : V
ha : a ∈ (subgraphOfAdj G hvw).verts
b : V
hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb }
[PROOFSTEP]
simp only [subgraphOfAdj_verts, Set.mem_insert_iff, Set.mem_singleton_iff] at ha hb 
[GOAL]
case mk.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w : V
hvw : SimpleGraph.Adj G v w
a : V
ha✝ : a ∈ (subgraphOfAdj G hvw).verts
b : V
hb✝ : b ∈ (subgraphOfAdj G hvw).verts
ha : a = v ∨ a = w
hb : b = v ∨ b = w
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha✝ } { val := b, property := hb✝ }
[PROOFSTEP]
obtain rfl | rfl := ha
[GOAL]
case mk.mk.inl
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
w a b : V
hvw : SimpleGraph.Adj G a w
ha : a ∈ (subgraphOfAdj G hvw).verts
hb✝ : b ∈ (subgraphOfAdj G hvw).verts
hb : b = a ∨ b = w
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb✝ }
[PROOFSTEP]
obtain rfl | rfl := hb
[GOAL]
case mk.mk.inr
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v a b : V
hvw : SimpleGraph.Adj G v a
ha : a ∈ (subgraphOfAdj G hvw).verts
hb✝ : b ∈ (subgraphOfAdj G hvw).verts
hb : b = v ∨ b = a
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb✝ }
[PROOFSTEP]
obtain rfl | rfl := hb
[GOAL]
case mk.mk.inl.inl
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
w b : V
hvw : SimpleGraph.Adj G b w
ha hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := b, property := ha } { val := b, property := hb }
[PROOFSTEP]
first
| rfl
| (apply Adj.reachable; simp)
[GOAL]
case mk.mk.inl.inl
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
w b : V
hvw : SimpleGraph.Adj G b w
ha hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := b, property := ha } { val := b, property := hb }
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.inl.inr
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
a b : V
hvw : SimpleGraph.Adj G a b
ha : a ∈ (subgraphOfAdj G hvw).verts
hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb }
[PROOFSTEP]
first
| rfl
| (apply Adj.reachable; simp)
[GOAL]
case mk.mk.inl.inr
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
a b : V
hvw : SimpleGraph.Adj G a b
ha : a ∈ (subgraphOfAdj G hvw).verts
hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb }
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.inl.inr
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
a b : V
hvw : SimpleGraph.Adj G a b
ha : a ∈ (subgraphOfAdj G hvw).verts
hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb }
[PROOFSTEP]
apply Adj.reachable
[GOAL]
case mk.mk.inl.inr.h
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
a b : V
hvw : SimpleGraph.Adj G a b
ha : a ∈ (subgraphOfAdj G hvw).verts
hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ SimpleGraph.Adj (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb }
[PROOFSTEP]
simp
[GOAL]
case mk.mk.inr.inl
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
a b : V
hvw : SimpleGraph.Adj G b a
ha : a ∈ (subgraphOfAdj G hvw).verts
hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb }
[PROOFSTEP]
first
| rfl
| (apply Adj.reachable; simp)
[GOAL]
case mk.mk.inr.inl
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
a b : V
hvw : SimpleGraph.Adj G b a
ha : a ∈ (subgraphOfAdj G hvw).verts
hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb }
[PROOFSTEP]
rfl
[GOAL]
case mk.mk.inr.inl
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
a b : V
hvw : SimpleGraph.Adj G b a
ha : a ∈ (subgraphOfAdj G hvw).verts
hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb }
[PROOFSTEP]
apply Adj.reachable
[GOAL]
case mk.mk.inr.inl.h
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
a b : V
hvw : SimpleGraph.Adj G b a
ha : a ∈ (subgraphOfAdj G hvw).verts
hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ SimpleGraph.Adj (Subgraph.coe (subgraphOfAdj G hvw)) { val := a, property := ha } { val := b, property := hb }
[PROOFSTEP]
simp
[GOAL]
case mk.mk.inr.inr
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v b : V
hvw : SimpleGraph.Adj G v b
ha hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := b, property := ha } { val := b, property := hb }
[PROOFSTEP]
first
| rfl
| (apply Adj.reachable; simp)
[GOAL]
case mk.mk.inr.inr
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v b : V
hvw : SimpleGraph.Adj G v b
ha hb : b ∈ (subgraphOfAdj G hvw).verts
⊢ Reachable (Subgraph.coe (subgraphOfAdj G hvw)) { val := b, property := ha } { val := b, property := hb }
[PROOFSTEP]
rfl
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
huv : SimpleGraph.Adj G u v
⊢ Subgraph.Connected (induce ⊤ {u, v})
[PROOFSTEP]
rw [← subgraphOfAdj_eq_induce huv]
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
huv : SimpleGraph.Adj G u v
⊢ Subgraph.Connected (subgraphOfAdj G huv)
[PROOFSTEP]
exact subgraphOfAdj_connected huv
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H H' : Subgraph G
hle : H ≤ H'
hv : H.verts = H'.verts
h : Subgraph.Connected H
⊢ Subgraph.Connected H'
[PROOFSTEP]
rw [← Subgraph.copy_eq H' H.verts hv H'.Adj rfl]
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H H' : Subgraph G
hle : H ≤ H'
hv : H.verts = H'.verts
h : Subgraph.Connected H
⊢ Subgraph.Connected (copy H' H.verts hv H'.Adj (_ : H'.Adj = H'.Adj))
[PROOFSTEP]
refine ⟨h.coe.mono ?_⟩
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H H' : Subgraph G
hle : H ≤ H'
hv : H.verts = H'.verts
h : Subgraph.Connected H
⊢ Subgraph.coe H ≤ Subgraph.coe (copy H' H.verts hv H'.Adj (_ : H'.Adj = H'.Adj))
[PROOFSTEP]
rintro ⟨v, hv⟩ ⟨w, hw⟩ hvw
[GOAL]
case mk.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H H' : Subgraph G
hle : H ≤ H'
hv✝ : H.verts = H'.verts
h : Subgraph.Connected H
v : V
hv : v ∈ H.verts
w : V
hw : w ∈ H.verts
hvw : SimpleGraph.Adj (Subgraph.coe H) { val := v, property := hv } { val := w, property := hw }
⊢ SimpleGraph.Adj (Subgraph.coe (copy H' H.verts hv✝ H'.Adj (_ : H'.Adj = H'.Adj))) { val := v, property := hv }
    { val := w, property := hw }
[PROOFSTEP]
exact hle.2 hvw
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H H' : Subgraph G
hle : ∀ (v w : V), Adj H v w → Adj H' v w
hv : H.verts = H'.verts
h : Subgraph.Connected H
⊢ Subgraph.Connected H'
[PROOFSTEP]
exact h.mono ⟨hv.le, hle⟩ hv
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H K : Subgraph G
hH : Subgraph.Connected H
hK : Subgraph.Connected K
hn : Set.Nonempty (H ⊓ K).verts
⊢ Subgraph.Connected (H ⊔ K)
[PROOFSTEP]
rw [Subgraph.connected_iff', connected_iff_exists_forall_reachable]
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H K : Subgraph G
hH : Subgraph.Connected H
hK : Subgraph.Connected K
hn : Set.Nonempty (H ⊓ K).verts
⊢ ∃ v, ∀ (w : ↑(H ⊔ K).verts), Reachable (Subgraph.coe (H ⊔ K)) v w
[PROOFSTEP]
obtain ⟨u, hu, hu'⟩ := hn
[GOAL]
case intro.intro
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H K : Subgraph G
hH : Subgraph.Connected H
hK : Subgraph.Connected K
u : V
hu : u ∈ H.verts
hu' : u ∈ K.verts
⊢ ∃ v, ∀ (w : ↑(H ⊔ K).verts), Reachable (Subgraph.coe (H ⊔ K)) v w
[PROOFSTEP]
exists ⟨u, Or.inl hu⟩
[GOAL]
case intro.intro
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H K : Subgraph G
hH : Subgraph.Connected H
hK : Subgraph.Connected K
u : V
hu : u ∈ H.verts
hu' : u ∈ K.verts
⊢ ∀ (w : ↑(H ⊔ K).verts), Reachable (Subgraph.coe (H ⊔ K)) { val := u, property := (_ : u ∈ H.verts ∨ u ∈ K.verts) } w
[PROOFSTEP]
rintro ⟨v, (hv | hv)⟩
[GOAL]
case intro.intro.mk.inl
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H K : Subgraph G
hH : Subgraph.Connected H
hK : Subgraph.Connected K
u : V
hu : u ∈ H.verts
hu' : u ∈ K.verts
v : V
hv : v ∈ H.verts
⊢ Reachable (Subgraph.coe (H ⊔ K)) { val := u, property := (_ : u ∈ H.verts ∨ u ∈ K.verts) }
    { val := v, property := (_ : v ∈ H.verts ∨ v ∈ K.verts) }
[PROOFSTEP]
exact Reachable.map (Subgraph.inclusion (le_sup_left : H ≤ H ⊔ K)) (hH ⟨u, hu⟩ ⟨v, hv⟩)
[GOAL]
case intro.intro.mk.inr
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H K : Subgraph G
hH : Subgraph.Connected H
hK : Subgraph.Connected K
u : V
hu : u ∈ H.verts
hu' : u ∈ K.verts
v : V
hv : v ∈ K.verts
⊢ Reachable (Subgraph.coe (H ⊔ K)) { val := u, property := (_ : u ∈ H.verts ∨ u ∈ K.verts) }
    { val := v, property := (_ : v ∈ H.verts ∨ v ∈ K.verts) }
[PROOFSTEP]
exact Reachable.map (Subgraph.inclusion (le_sup_right : K ≤ H ⊔ K)) (hK ⟨u, hu'⟩ ⟨v, hv⟩)
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
p : Walk G u v
⊢ Subgraph.Connected (Walk.toSubgraph p)
[PROOFSTEP]
induction p with
| nil => apply singletonSubgraph_connected
| cons h p ih =>
  apply (subgraphOfAdj_connected h).sup ih
  rename_i w _
  exists w
  simp
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
p : Walk G u v
⊢ Subgraph.Connected (Walk.toSubgraph p)
[PROOFSTEP]
induction p with
| nil => apply singletonSubgraph_connected
| cons h p ih =>
  apply (subgraphOfAdj_connected h).sup ih
  rename_i w _
  exists w
  simp
[GOAL]
case nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v u✝ : V
⊢ Subgraph.Connected (Walk.toSubgraph Walk.nil)
[PROOFSTEP]

| nil => apply singletonSubgraph_connected
[GOAL]
case nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v u✝ : V
⊢ Subgraph.Connected (Walk.toSubgraph Walk.nil)
[PROOFSTEP]
apply singletonSubgraph_connected
[GOAL]
case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v u✝ v✝ w✝ : V
h : SimpleGraph.Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Subgraph.Connected (Walk.toSubgraph p)
⊢ Subgraph.Connected (Walk.toSubgraph (Walk.cons h p))
[PROOFSTEP]

| cons h p ih =>
  apply (subgraphOfAdj_connected h).sup ih
  rename_i w _
  exists w
  simp
[GOAL]
case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v u✝ v✝ w✝ : V
h : SimpleGraph.Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Subgraph.Connected (Walk.toSubgraph p)
⊢ Subgraph.Connected (Walk.toSubgraph (Walk.cons h p))
[PROOFSTEP]
apply (subgraphOfAdj_connected h).sup ih
[GOAL]
case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v u✝ v✝ w✝ : V
h : SimpleGraph.Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Subgraph.Connected (Walk.toSubgraph p)
⊢ Set.Nonempty (subgraphOfAdj G h ⊓ Walk.toSubgraph p).verts
[PROOFSTEP]
rename_i w _
[GOAL]
case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v u✝ w w✝ : V
h : SimpleGraph.Adj G u✝ w
p : Walk G w w✝
ih : Subgraph.Connected (Walk.toSubgraph p)
⊢ Set.Nonempty (subgraphOfAdj G h ⊓ Walk.toSubgraph p).verts
[PROOFSTEP]
exists w
[GOAL]
case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v u✝ w w✝ : V
h : SimpleGraph.Adj G u✝ w
p : Walk G w w✝
ih : Subgraph.Connected (Walk.toSubgraph p)
⊢ w ∈ (subgraphOfAdj G h ⊓ Walk.toSubgraph p).verts
[PROOFSTEP]
simp
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
s t : Set V
sconn : Subgraph.Connected (induce H s)
tconn : Subgraph.Connected (induce H t)
sintert : Set.Nonempty (s ⊓ t)
⊢ Subgraph.Connected (induce H (s ∪ t))
[PROOFSTEP]
refine (sconn.sup tconn sintert).mono ?_ ?_
[GOAL]
case refine_1
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
s t : Set V
sconn : Subgraph.Connected (induce H s)
tconn : Subgraph.Connected (induce H t)
sintert : Set.Nonempty (s ⊓ t)
⊢ induce H s ⊔ induce H t ≤ induce H (s ∪ t)
[PROOFSTEP]
apply le_induce_union
[GOAL]
case refine_2
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
s t : Set V
sconn : Subgraph.Connected (induce H s)
tconn : Subgraph.Connected (induce H t)
sintert : Set.Nonempty (s ⊓ t)
⊢ (induce H s ⊔ induce H t).verts = (induce H (s ∪ t)).verts
[PROOFSTEP]
simp
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H K : Subgraph G
Hconn : Subgraph.Connected H
Kconn : Subgraph.Connected K
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : SimpleGraph.Adj G u v
⊢ Subgraph.Connected (induce ⊤ {u, v} ⊔ H ⊔ K)
[PROOFSTEP]
refine ((top_induce_pair_connected_of_adj huv).sup Hconn ?_).sup Kconn ?_
[GOAL]
case refine_1
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H K : Subgraph G
Hconn : Subgraph.Connected H
Kconn : Subgraph.Connected K
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : SimpleGraph.Adj G u v
⊢ Set.Nonempty (induce ⊤ {u, v} ⊓ H).verts
[PROOFSTEP]
exact ⟨u, by simp [uH]⟩
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H K : Subgraph G
Hconn : Subgraph.Connected H
Kconn : Subgraph.Connected K
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : SimpleGraph.Adj G u v
⊢ u ∈ (induce ⊤ {u, v} ⊓ H).verts
[PROOFSTEP]
simp [uH]
[GOAL]
case refine_2
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H K : Subgraph G
Hconn : Subgraph.Connected H
Kconn : Subgraph.Connected K
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : SimpleGraph.Adj G u v
⊢ Set.Nonempty ((induce ⊤ {u, v} ⊔ H) ⊓ K).verts
[PROOFSTEP]
exact ⟨v, by simp [vK]⟩
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H K : Subgraph G
Hconn : Subgraph.Connected H
Kconn : Subgraph.Connected K
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : SimpleGraph.Adj G u v
⊢ v ∈ ((induce ⊤ {u, v} ⊔ H) ⊓ K).verts
[PROOFSTEP]
simp [vK]
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
⊢ Subgraph.Preconnected H ↔ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, Walk.toSubgraph p ≤ H
[PROOFSTEP]
constructor
[GOAL]
case mp
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
⊢ Subgraph.Preconnected H → ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, Walk.toSubgraph p ≤ H
[PROOFSTEP]
intro hc u v hu hv
[GOAL]
case mp
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
hc : Subgraph.Preconnected H
u v : V
hu : u ∈ H.verts
hv : v ∈ H.verts
⊢ ∃ p, Walk.toSubgraph p ≤ H
[PROOFSTEP]
refine (hc ⟨_, hu⟩ ⟨_, hv⟩).elim fun p => ?_
[GOAL]
case mp
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
hc : Subgraph.Preconnected H
u v : V
hu : u ∈ H.verts
hv : v ∈ H.verts
p : Walk (Subgraph.coe H) { val := u, property := hu } { val := v, property := hv }
⊢ ∃ p, Walk.toSubgraph p ≤ H
[PROOFSTEP]
exists p.map (Subgraph.hom _)
[GOAL]
case mp
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
hc : Subgraph.Preconnected H
u v : V
hu : u ∈ H.verts
hv : v ∈ H.verts
p : Walk (Subgraph.coe H) { val := u, property := hu } { val := v, property := hv }
⊢ Walk.toSubgraph (Walk.map (Subgraph.hom H) p) ≤ H
[PROOFSTEP]
simp [coeSubgraph_le]
[GOAL]
case mpr
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
⊢ (∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, Walk.toSubgraph p ≤ H) → Subgraph.Preconnected H
[PROOFSTEP]
intro hw
[GOAL]
case mpr
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
hw : ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, Walk.toSubgraph p ≤ H
⊢ Subgraph.Preconnected H
[PROOFSTEP]
rw [Subgraph.preconnected_iff]
[GOAL]
case mpr
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
hw : ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, Walk.toSubgraph p ≤ H
⊢ Preconnected (Subgraph.coe H)
[PROOFSTEP]
rintro ⟨u, hu⟩ ⟨v, hv⟩
[GOAL]
case mpr.mk.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
hw : ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, Walk.toSubgraph p ≤ H
u : V
hu : u ∈ H.verts
v : V
hv : v ∈ H.verts
⊢ Reachable (Subgraph.coe H) { val := u, property := hu } { val := v, property := hv }
[PROOFSTEP]
obtain ⟨p, h⟩ := hw hu hv
[GOAL]
case mpr.mk.mk.intro
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
hw : ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, Walk.toSubgraph p ≤ H
u : V
hu : u ∈ H.verts
v : V
hv : v ∈ H.verts
p : Walk G u v
h : Walk.toSubgraph p ≤ H
⊢ Reachable (Subgraph.coe H) { val := u, property := hu } { val := v, property := hv }
[PROOFSTEP]
exact
  Reachable.map (Subgraph.inclusion h)
    (p.toSubgraph_connected ⟨_, p.start_mem_verts_toSubgraph⟩ ⟨_, p.end_mem_verts_toSubgraph⟩)
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
⊢ Subgraph.Connected H ↔ Set.Nonempty H.verts ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, Walk.toSubgraph p ≤ H
[PROOFSTEP]
rw [H.connected_iff, preconnected_iff_forall_exists_walk_subgraph, and_comm]
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
s : Set V
⊢ Connected (induce s G) ↔ Subgraph.Connected (Subgraph.induce ⊤ s)
[PROOFSTEP]
rw [induce_eq_coe_induce_top, ← Subgraph.connected_iff']
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
s t : Set V
sconn : Connected (induce s G)
tconn : Connected (induce t G)
sintert : Set.Nonempty (s ∩ t)
⊢ Connected (induce (s ∪ t) G)
[PROOFSTEP]
rw [connected_induce_iff] at sconn tconn ⊢
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
s t : Set V
sconn : Subgraph.Connected (Subgraph.induce ⊤ s)
tconn : Subgraph.Connected (Subgraph.induce ⊤ t)
sintert : Set.Nonempty (s ∩ t)
⊢ Subgraph.Connected (Subgraph.induce ⊤ (s ∪ t))
[PROOFSTEP]
exact Subgraph.induce_union_connected sconn tconn sintert
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
huv : Adj G u v
⊢ Connected (induce {u, v} G)
[PROOFSTEP]
rw [connected_induce_iff]
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
huv : Adj G u v
⊢ Subgraph.Connected (Subgraph.induce ⊤ {u, v})
[PROOFSTEP]
exact Subgraph.top_induce_pair_connected_of_adj huv
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
h : Subgraph.Connected H
⊢ Connected (SimpleGraph.induce H.verts G)
[PROOFSTEP]
rw [connected_induce_iff]
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
h : Subgraph.Connected H
⊢ Subgraph.Connected (induce ⊤ H.verts)
[PROOFSTEP]
exact h.mono le_induce_top_verts (by exact rfl)
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
H : Subgraph G
h : Subgraph.Connected H
⊢ H.verts = (induce ⊤ H.verts).verts
[PROOFSTEP]
exact rfl
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
p : Walk G u v
⊢ Connected (induce {v_1 | v_1 ∈ support p} G)
[PROOFSTEP]
rw [← p.verts_toSubgraph]
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
p : Walk G u v
⊢ Connected (induce (Walk.toSubgraph p).verts G)
[PROOFSTEP]
exact p.toSubgraph_connected.induce_verts
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w : V
s t : Set V
sconn : Connected (induce s G)
tconn : Connected (induce t G)
hv : v ∈ s
hw : w ∈ t
ha : Adj G v w
⊢ Connected (induce (s ∪ t) G)
[PROOFSTEP]
rw [connected_induce_iff] at sconn tconn ⊢
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w : V
s t : Set V
sconn : Subgraph.Connected (Subgraph.induce ⊤ s)
tconn : Subgraph.Connected (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : Adj G v w
⊢ Subgraph.Connected (Subgraph.induce ⊤ (s ∪ t))
[PROOFSTEP]
apply (sconn.adj_union tconn hv hw ha).mono
[GOAL]
case hle
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w : V
s t : Set V
sconn : Subgraph.Connected (Subgraph.induce ⊤ s)
tconn : Subgraph.Connected (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : Adj G v w
⊢ Subgraph.induce ⊤ {v, w} ⊔ Subgraph.induce ⊤ s ⊔ Subgraph.induce ⊤ t ≤ Subgraph.induce ⊤ (s ∪ t)
[PROOFSTEP]
simp only [Set.mem_singleton_iff, sup_le_iff, Subgraph.le_induce_union_left, Subgraph.le_induce_union_right, and_true, ←
  Subgraph.subgraphOfAdj_eq_induce ha]
[GOAL]
case hle
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w : V
s t : Set V
sconn : Subgraph.Connected (Subgraph.induce ⊤ s)
tconn : Subgraph.Connected (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : Adj G v w
⊢ subgraphOfAdj G ha ≤ Subgraph.induce ⊤ (s ∪ t)
[PROOFSTEP]
apply subgraphOfAdj_le_of_adj
[GOAL]
case hle.h
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w : V
s t : Set V
sconn : Subgraph.Connected (Subgraph.induce ⊤ s)
tconn : Subgraph.Connected (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : Adj G v w
⊢ Subgraph.Adj (Subgraph.induce ⊤ (s ∪ t)) v w
[PROOFSTEP]
simp [hv, hw, ha]
[GOAL]
case hv
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w : V
s t : Set V
sconn : Subgraph.Connected (Subgraph.induce ⊤ s)
tconn : Subgraph.Connected (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : Adj G v w
⊢ (Subgraph.induce ⊤ {v, w} ⊔ Subgraph.induce ⊤ s ⊔ Subgraph.induce ⊤ t).verts = (Subgraph.induce ⊤ (s ∪ t)).verts
[PROOFSTEP]
simp only [Set.mem_singleton_iff, sup_le_iff, Subgraph.verts_sup, Subgraph.induce_verts]
[GOAL]
case hv
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w : V
s t : Set V
sconn : Subgraph.Connected (Subgraph.induce ⊤ s)
tconn : Subgraph.Connected (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : Adj G v w
⊢ {v, w} ∪ s ∪ t = s ∪ t
[PROOFSTEP]
rw [Set.union_assoc]
[GOAL]
case hv
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w : V
s t : Set V
sconn : Subgraph.Connected (Subgraph.induce ⊤ s)
tconn : Subgraph.Connected (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : Adj G v w
⊢ {v, w} ∪ (s ∪ t) = s ∪ t
[PROOFSTEP]
simp [Set.insert_subset_iff, Set.singleton_subset_iff, hv, hw]
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
s : Set V
u : V
hu : u ∈ s
patches :
  ∀ {v : V}, v ∈ s → ∃ s' x hu' hv', Reachable (induce s' G) { val := u, property := hu' } { val := v, property := hv' }
⊢ Connected (induce s G)
[PROOFSTEP]
rw [connected_iff_exists_forall_reachable]
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
s : Set V
u : V
hu : u ∈ s
patches :
  ∀ {v : V}, v ∈ s → ∃ s' x hu' hv', Reachable (induce s' G) { val := u, property := hu' } { val := v, property := hv' }
⊢ ∃ v, ∀ (w : ↑s), Reachable (induce s G) v w
[PROOFSTEP]
refine ⟨⟨u, hu⟩, ?_⟩
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
s : Set V
u : V
hu : u ∈ s
patches :
  ∀ {v : V}, v ∈ s → ∃ s' x hu' hv', Reachable (induce s' G) { val := u, property := hu' } { val := v, property := hv' }
⊢ ∀ (w : ↑s), Reachable (induce s G) { val := u, property := hu } w
[PROOFSTEP]
rintro ⟨v, hv⟩
[GOAL]
case mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
s : Set V
u : V
hu : u ∈ s
patches :
  ∀ {v : V}, v ∈ s → ∃ s' x hu' hv', Reachable (induce s' G) { val := u, property := hu' } { val := v, property := hv' }
v : V
hv : v ∈ s
⊢ Reachable (induce s G) { val := u, property := hu } { val := v, property := hv }
[PROOFSTEP]
obtain ⟨sv, svs, hu', hv', uv⟩ := patches hv
[GOAL]
case mk.intro.intro.intro.intro
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
s : Set V
u : V
hu : u ∈ s
patches :
  ∀ {v : V}, v ∈ s → ∃ s' x hu' hv', Reachable (induce s' G) { val := u, property := hu' } { val := v, property := hv' }
v : V
hv : v ∈ s
sv : Set V
svs : sv ⊆ s
hu' : u ∈ sv
hv' : v ∈ sv
uv : Reachable (induce sv G) { val := u, property := hu' } { val := v, property := hv' }
⊢ Reachable (induce s G) { val := u, property := hu } { val := v, property := hv }
[PROOFSTEP]
exact uv.map (induceHomOfLE _ svs).toHom
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
S : Set (Set V)
Sn : Set.Nonempty S
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → Set.Nonempty (s ∩ t)
Sc : ∀ {s : Set V}, s ∈ S → Connected (induce s G)
⊢ Connected (induce (⋃₀ S) G)
[PROOFSTEP]
obtain ⟨s, sS⟩ := Sn
[GOAL]
case intro
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → Set.Nonempty (s ∩ t)
Sc : ∀ {s : Set V}, s ∈ S → Connected (induce s G)
s : Set V
sS : s ∈ S
⊢ Connected (induce (⋃₀ S) G)
[PROOFSTEP]
obtain ⟨v, vs⟩ := (Sc sS).nonempty
[GOAL]
case intro.intro.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → Set.Nonempty (s ∩ t)
Sc : ∀ {s : Set V}, s ∈ S → Connected (induce s G)
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
⊢ Connected (induce (⋃₀ S) G)
[PROOFSTEP]
apply G.induce_connected_of_patches _ (Set.subset_sUnion_of_mem sS vs)
[GOAL]
case intro.intro.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → Set.Nonempty (s ∩ t)
Sc : ∀ {s : Set V}, s ∈ S → Connected (induce s G)
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
⊢ ∀ {v_1 : V},
    v_1 ∈ ⋃₀ S → ∃ s' x hu' hv', Reachable (induce s' G) { val := v, property := hu' } { val := v_1, property := hv' }
[PROOFSTEP]
rintro w hw
[GOAL]
case intro.intro.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → Set.Nonempty (s ∩ t)
Sc : ∀ {s : Set V}, s ∈ S → Connected (induce s G)
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
w : V
hw : w ∈ ⋃₀ S
⊢ ∃ s' x hu' hv', Reachable (induce s' G) { val := v, property := hu' } { val := w, property := hv' }
[PROOFSTEP]
simp only [Set.mem_sUnion, exists_prop] at hw 
[GOAL]
case intro.intro.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → Set.Nonempty (s ∩ t)
Sc : ∀ {s : Set V}, s ∈ S → Connected (induce s G)
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
w : V
hw : ∃ t, t ∈ S ∧ w ∈ t
⊢ ∃ s' x hu' hv', Reachable (induce s' G) { val := v, property := hu' } { val := w, property := hv' }
[PROOFSTEP]
obtain ⟨t, tS, wt⟩ := hw
[GOAL]
case intro.intro.mk.intro.intro
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
S : Set (Set V)
Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → Set.Nonempty (s ∩ t)
Sc : ∀ {s : Set V}, s ∈ S → Connected (induce s G)
s : Set V
sS : s ∈ S
v : V
vs : v ∈ s
w : V
t : Set V
tS : t ∈ S
wt : w ∈ t
⊢ ∃ s' x hu' hv', Reachable (induce s' G) { val := v, property := hu' } { val := w, property := hv' }
[PROOFSTEP]
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) _ _⟩
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
tn : Finset.Nonempty t
⊢ ∃ t', t ⊆ t' ∧ Connected (induce (↑t') G)
[PROOFSTEP]
classical
obtain ⟨u, ut⟩ := tn
refine ⟨t.biUnion (fun v => (Gpc u v).some.support.toFinset), fun v vt => ?_, ?_⟩
· simp only [Finset.mem_biUnion, List.mem_toFinset, exists_prop]
  refine ⟨v, vt, Walk.end_mem_support _⟩
· apply G.induce_connected_of_patches u
  · 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]
    exact ⟨u, ut⟩
  intros v hv
  simp only [Finset.mem_coe, Finset.mem_biUnion, List.mem_toFinset, exists_prop] at hv 
  obtain ⟨w, wt, hw⟩ := hv
  refine ⟨{x | x ∈ (Gpc u w).some.support}, ?_, ?_⟩
  · simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset]
    exact fun x xw => Set.mem_iUnion₂.mpr ⟨w, wt, xw⟩
  · simp only [Set.mem_setOf_eq, Walk.start_mem_support, exists_true_left]
    refine ⟨hw, Walk.connected_induce_support _ _ _⟩
[GOAL]
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
tn : Finset.Nonempty t
⊢ ∃ t', t ⊆ t' ∧ Connected (induce (↑t') G)
[PROOFSTEP]
obtain ⟨u, ut⟩ := tn
[GOAL]
case intro
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
⊢ ∃ t', t ⊆ t' ∧ Connected (induce (↑t') G)
[PROOFSTEP]
refine ⟨t.biUnion (fun v => (Gpc u v).some.support.toFinset), fun v vt => ?_, ?_⟩
[GOAL]
case intro.refine_1
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
v : V
vt : v ∈ t
⊢ v ∈ Finset.biUnion t fun v => List.toFinset (Walk.support (Nonempty.some (_ : Reachable G u v)))
[PROOFSTEP]
simp only [Finset.mem_biUnion, List.mem_toFinset, exists_prop]
[GOAL]
case intro.refine_1
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
v : V
vt : v ∈ t
⊢ ∃ a, a ∈ t ∧ v ∈ Walk.support (Nonempty.some (_ : Reachable G u a))
[PROOFSTEP]
refine ⟨v, vt, Walk.end_mem_support _⟩
[GOAL]
case intro.refine_2
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
⊢ Connected (induce (↑(Finset.biUnion t fun v => List.toFinset (Walk.support (Nonempty.some (_ : Reachable G u v))))) G)
[PROOFSTEP]
apply G.induce_connected_of_patches u
[GOAL]
case intro.refine_2.hu
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
⊢ u ∈ ↑(Finset.biUnion t fun v => List.toFinset (Walk.support (Nonempty.some (_ : Reachable G u v))))
[PROOFSTEP]
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]
[GOAL]
case intro.refine_2.hu
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
⊢ ∃ i, i ∈ t
[PROOFSTEP]
exact ⟨u, ut⟩
[GOAL]
case intro.refine_2.patches
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
⊢ ∀ {v : V},
    v ∈ ↑(Finset.biUnion t fun v => List.toFinset (Walk.support (Nonempty.some (_ : Reachable G u v)))) →
      ∃ s' x hu' hv', Reachable (induce s' G) { val := u, property := hu' } { val := v, property := hv' }
[PROOFSTEP]
intros v hv
[GOAL]
case intro.refine_2.patches
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
v : V
hv : v ∈ ↑(Finset.biUnion t fun v => List.toFinset (Walk.support (Nonempty.some (_ : Reachable G u v))))
⊢ ∃ s' x hu' hv', Reachable (induce s' G) { val := u, property := hu' } { val := v, property := hv' }
[PROOFSTEP]
simp only [Finset.mem_coe, Finset.mem_biUnion, List.mem_toFinset, exists_prop] at hv 
[GOAL]
case intro.refine_2.patches
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
v : V
hv : ∃ a, a ∈ t ∧ v ∈ Walk.support (Nonempty.some (_ : Reachable G u a))
⊢ ∃ s' x hu' hv', Reachable (induce s' G) { val := u, property := hu' } { val := v, property := hv' }
[PROOFSTEP]
obtain ⟨w, wt, hw⟩ := hv
[GOAL]
case intro.refine_2.patches.intro.intro
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ Walk.support (Nonempty.some (_ : Reachable G u w))
⊢ ∃ s' x hu' hv', Reachable (induce s' G) { val := u, property := hu' } { val := v, property := hv' }
[PROOFSTEP]
refine ⟨{x | x ∈ (Gpc u w).some.support}, ?_, ?_⟩
[GOAL]
case intro.refine_2.patches.intro.intro.refine_1
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ Walk.support (Nonempty.some (_ : Reachable G u w))
⊢ {x | x ∈ Walk.support (Nonempty.some (_ : Reachable G u w))} ⊆
    ↑(Finset.biUnion t fun v => List.toFinset (Walk.support (Nonempty.some (_ : Reachable G u v))))
[PROOFSTEP]
simp only [Finset.coe_biUnion, Finset.mem_coe, List.coe_toFinset]
[GOAL]
case intro.refine_2.patches.intro.intro.refine_1
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ Walk.support (Nonempty.some (_ : Reachable G u w))
⊢ {x | x ∈ Walk.support (Nonempty.some (_ : Reachable G u w))} ⊆
    ⋃ (x : V) (_ : x ∈ t), {a | a ∈ Walk.support (Nonempty.some (_ : Reachable G u x))}
[PROOFSTEP]
exact fun x xw => Set.mem_iUnion₂.mpr ⟨w, wt, xw⟩
[GOAL]
case intro.refine_2.patches.intro.intro.refine_2
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ Walk.support (Nonempty.some (_ : Reachable G u w))
⊢ ∃ hu' hv',
    Reachable (induce {x | x ∈ Walk.support (Nonempty.some (_ : Reachable G u w))} G) { val := u, property := hu' }
      { val := v, property := hv' }
[PROOFSTEP]
simp only [Set.mem_setOf_eq, Walk.start_mem_support, exists_true_left]
[GOAL]
case intro.refine_2.patches.intro.intro.refine_2
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
Gpc : Preconnected G
t : Finset V
u : V
ut : u ∈ t
v w : V
wt : w ∈ t
hw : v ∈ Walk.support (Nonempty.some (_ : Reachable G u w))
⊢ ∃ hv',
    Reachable (induce {x | x ∈ Walk.support (Nonempty.some (_ : Reachable G u w))} G)
      { val := u, property := (_ : u ∈ {x | x ∈ Walk.support (Nonempty.some (_ : Reachable G u w))}) }
      { val := v, property := hv' }
[PROOFSTEP]
refine ⟨hw, Walk.connected_induce_support _ _ _⟩
