-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma induce_connected_adj_union {v w : V} {s t : Set V}
    (sconn : (G.induce s).Connected) (tconn : (G.induce t).Connected)
    (hv : v ∈ s) (hw : w ∈ t) (ha : G.Adj v w) :
    (G.induce (s ∪ t)).Connected

Proof state:
case hle
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (⊤.induce s).Connected
tconn : (⊤.induce t).Connected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ ⊤.induce {v, w} ⊔ ⊤.induce s ⊔ ⊤.induce t ≤ ⊤.induce (s ∪ t)

Tactic:
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]

Result:
case hle
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (⊤.induce s).Connected
tconn : (⊤.induce t).Connected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ G.subgraphOfAdj ha ≤ ⊤.induce (s ∪ t)

Proof state:
case hle
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (⊤.induce s).Connected
tconn : (⊤.induce t).Connected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ G.subgraphOfAdj ha ≤ ⊤.induce (s ∪ t)

Tactic:
apply subgraphOfAdj_le_of_adj

Result:
case hle.h
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (⊤.induce s).Connected
tconn : (⊤.induce t).Connected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ (⊤.induce (s ∪ t)).Adj v w

Proof state:
case hv
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (⊤.induce s).Connected
tconn : (⊤.induce t).Connected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ {v, w} ∪ (s ∪ t) = s ∪ t

Tactic:
simp [Set.insert_subset_iff, Set.singleton_subset_iff, hv, hw]

Result:
no goals

Proof state:
case hle.h
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (⊤.induce s).Connected
tconn : (⊤.induce t).Connected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ (⊤.induce (s ∪ t)).Adj v w

Tactic:
simp [hv, hw, ha]

Result:
no goals

Proof state:
case hv
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (⊤.induce s).Connected
tconn : (⊤.induce t).Connected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ {v, w} ∪ s ∪ t = s ∪ t

Tactic:
rw [Set.union_assoc]

Result:
case hv
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (⊤.induce s).Connected
tconn : (⊤.induce t).Connected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ {v, w} ∪ (s ∪ t) = s ∪ t

Proof state:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (⊤.induce s).Connected
tconn : (⊤.induce t).Connected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ (⊤.induce (s ∪ t)).Connected

Tactic:
apply (sconn.adj_union tconn hv hw ha).mono

Result:
case hle
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (⊤.induce s).Connected
tconn : (⊤.induce t).Connected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ ⊤.induce {v, w} ⊔ ⊤.induce s ⊔ ⊤.induce t ≤ ⊤.induce (s ∪ t)

case hv
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (⊤.induce s).Connected
tconn : (⊤.induce t).Connected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ (⊤.induce {v, w} ⊔ ⊤.induce s ⊔ ⊤.induce t).verts = (⊤.induce (s ∪ t)).verts

Proof state:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (induce s G).Connected
tconn : (induce t G).Connected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ (induce (s ∪ t) G).Connected

Tactic:
rw [connected_induce_iff] at sconn tconn ⊢

Result:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (⊤.induce s).Connected
tconn : (⊤.induce t).Connected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ (⊤.induce (s ∪ t)).Connected

Proof state:
case hv
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (⊤.induce s).Connected
tconn : (⊤.induce t).Connected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ (⊤.induce {v, w} ⊔ ⊤.induce s ⊔ ⊤.induce t).verts = (⊤.induce (s ∪ t)).verts

Tactic:
simp only [Set.mem_singleton_iff, sup_le_iff, Subgraph.verts_sup, Subgraph.induce_verts]

Result:
case hv
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (⊤.induce s).Connected
tconn : (⊤.induce t).Connected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ {v, w} ∪ s ∪ t = s ∪ t