awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
hw : ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H
u : V
hu : u ∈ H.verts
v : V
hv : v ∈ H.verts
p : G.Walk u v
h : p.toSubgraph ≤ H
⊢ H.coe.Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ H.verts) v hv)

Tactic:
exact Reachable.map (Subgraph.inclusion h)
      (p.toSubgraph_connected ⟨_, p.start_mem_verts_toSubgraph⟩ ⟨_, p.end_mem_verts_toSubgraph⟩)

Premises used: SimpleGraph.Subgraph.instCoeFunConnectedForallForallReachableElemVertsCoe._proof_1, SimpleGraph.Subgraph.inclusion, Subtype.mk, SimpleGraph.Walk.end_mem_verts_toSubgraph, SimpleGraph.Reachable.map, SimpleGraph.Walk.toSubgraph_connected, SimpleGraph.Walk.start_mem_verts_toSubgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
rw :
  H.Preconnected ∧ H.verts.Nonempty ↔
    H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H
rw₁ :
  (∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H) ∧ H.verts.Nonempty ↔
    H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H
rw₂ rw₃ :
  (H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H) ↔
    H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H
⊢ H.Connected ↔ H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H

Tactic:
rw [H.connected_iff, preconnected_iff_forall_exists_walk_subgraph, and_comm]

Premises used: and_comm, SimpleGraph.Subgraph.preconnected_iff_forall_exists_walk_subgraph, SimpleGraph.Subgraph.connected_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set V
rw :
  Preconnected (V := (↑s : Type u))
      (Subgraph.coe (Subgraph.induce ⊤ s) : SimpleGraph (↑(Subgraph.verts (G := G) (Subgraph.induce ⊤ s)) : Type u)) ↔
    Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
rw₁ rw₂ : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s) ↔ Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
⊢ (induce s G).Preconnected ↔ Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)

Tactic:
rw [induce_eq_coe_induce_top, ← Subgraph.preconnected_iff]

Premises used: SimpleGraph.induce_eq_coe_induce_top, SimpleGraph.Subgraph.preconnected_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set V
rw :
  Connected (V := (↑s : Type u))
      (Subgraph.coe (Subgraph.induce ⊤ s) : SimpleGraph (↑(Subgraph.verts (G := G) (Subgraph.induce ⊤ s)) : Type u)) ↔
    Subgraph.Connected (G := G) (Subgraph.induce ⊤ s)
rw₁ rw₂ : Subgraph.Connected (G := G) (Subgraph.induce ⊤ s) ↔ Subgraph.Connected (G := G) (Subgraph.induce ⊤ s)
⊢ (induce s G).Connected ↔ Subgraph.Connected (G := G) (Subgraph.induce ⊤ s)

Tactic:
rw [induce_eq_coe_induce_top, ← Subgraph.connected_iff']

Premises used: SimpleGraph.induce_eq_coe_induce_top, SimpleGraph.Subgraph.connected_iff'
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s t : Set V
sconn : (induce s G).Preconnected
tconn : (induce t G).Preconnected
sintert : (s ∩ t).Nonempty
rw : Subgraph.Connected (G := G) (Subgraph.induce ⊤ (s ∪ t))
⊢ (induce (s ∪ t) G).Connected

Tactic:
rw [connected_induce_iff]

Premises used: SimpleGraph.connected_induce_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s t : Set V
sconn : (induce s G).Preconnected
tconn : (induce t G).Preconnected
sintert : (s ∩ t).Nonempty
⊢ Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)

Tactic:
rw [preconnected_induce_iff] at sconn tconn

Premises used: SimpleGraph.preconnected_induce_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s t : Set V
sconn : (induce s G).Preconnected
tconn : (induce t G).Preconnected
sintert : (s ∩ t).Nonempty
sconn₁ : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
⊢ Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ t)

Tactic:
rw [preconnected_induce_iff] at sconn tconn

Premises used: SimpleGraph.preconnected_induce_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s t : Set V
sconn : (induce s G).Preconnected
tconn : (induce t G).Preconnected
sintert : (s ∩ t).Nonempty
sconn₁ : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
tconn₁ : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ t)
⊢ (s ∩ t).Nonempty

Tactic:
rw [preconnected_induce_iff] at sconn tconn

Premises used: SimpleGraph.preconnected_induce_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s t : Set V
sconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
tconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ t)
sintert : (s ∩ t).Nonempty
⊢ Subgraph.Connected (G := G) (Subgraph.induce ⊤ (s ∪ t))

Tactic:
Subgraph.induce_union_connected sconn tconn sintert

Premises used: SimpleGraph.Subgraph.induce_union_connected
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s t : Set V
sconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
tconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ t)
sintert : (s ∩ t).Nonempty
⊢ Subgraph.Connected (G := G) (Subgraph.induce ⊤ (s ∪ t))

Tactic:
exact Subgraph.induce_union_connected sconn tconn sintert

Premises used: SimpleGraph.Subgraph.induce_union_connected
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
huv : G.Adj u v
rw : Subgraph.Connected (V := V) (G := G) (Subgraph.induce ⊤ {u, v})
⊢ Connected (V := (↑{u, v} : Type u)) (induce {u, v} G)

Tactic:
rw [connected_induce_iff]

Premises used: SimpleGraph.connected_induce_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
huv : G.Adj u v
⊢ Subgraph.Connected (V := V) (G := G) (Subgraph.induce ⊤ {u, v})

Tactic:
Subgraph.top_induce_pair_connected_of_adj huv

Premises used: SimpleGraph.Subgraph.top_induce_pair_connected_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
huv : G.Adj u v
⊢ Subgraph.Connected (V := V) (G := G) (Subgraph.induce ⊤ {u, v})

Tactic:
exact Subgraph.top_induce_pair_connected_of_adj huv

Premises used: SimpleGraph.Subgraph.top_induce_pair_connected_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Connected
rw : Subgraph.Connected (G := G) (induce ⊤ H.verts)
⊢ (SimpleGraph.induce H.verts G).Connected

Tactic:
rw [connected_induce_iff]

Premises used: SimpleGraph.connected_induce_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Connected
⊢ H.verts = verts (G := G) (induce ⊤ H.verts)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Connected
⊢ H.verts = verts (G := G) (induce ⊤ H.verts)

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Connected
⊢ Subgraph.Connected (G := G) (induce ⊤ H.verts)

Tactic:
exact h.mono le_induce_top_verts (by exact rfl)

Premises used: SimpleGraph.Subgraph.le_induce_top_verts, SimpleGraph.Subgraph.Connected.mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
rw : (induce p.toSubgraph.verts G).Connected
⊢ Connected (V := (↑{v_1 : V | v_1 ∈ p.support} : Type u)) (induce {v_1 : V | v_1 ∈ p.support} G)

Tactic:
rw [← p.verts_toSubgraph]

Premises used: SimpleGraph.Walk.verts_toSubgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ (induce p.toSubgraph.verts G).Connected

Tactic:
p.toSubgraph_connected.induce_verts

Premises used: SimpleGraph.Walk.toSubgraph_connected, SimpleGraph.Subgraph.Connected.induce_verts
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ (induce p.toSubgraph.verts G).Connected

Tactic:
exact p.toSubgraph_connected.induce_verts

Premises used: SimpleGraph.Walk.toSubgraph_connected, SimpleGraph.Subgraph.Connected.induce_verts
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (induce s G).Preconnected
tconn : (induce t G).Preconnected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
rw : Subgraph.Connected (G := G) (Subgraph.induce ⊤ (s ∪ t))
⊢ (induce (s ∪ t) G).Connected

Tactic:
rw [connected_induce_iff]

Premises used: SimpleGraph.connected_induce_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (induce s G).Preconnected
tconn : (induce t G).Preconnected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)

Tactic:
rw [preconnected_induce_iff] at sconn tconn

Premises used: SimpleGraph.preconnected_induce_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (induce s G).Preconnected
tconn : (induce t G).Preconnected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
sconn₁ : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
⊢ Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ t)

Tactic:
rw [preconnected_induce_iff] at sconn tconn

Premises used: SimpleGraph.preconnected_induce_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (induce s G).Preconnected
tconn : (induce t G).Preconnected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
sconn₁ : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
tconn₁ : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ t)
⊢ v ∈ s

Tactic:
rw [preconnected_induce_iff] at sconn tconn

Premises used: SimpleGraph.preconnected_induce_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (induce s G).Preconnected
tconn : (induce t G).Preconnected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
sconn₁ : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
tconn₁ : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ t)
hv₁ : v ∈ s
⊢ w ∈ t

Tactic:
rw [preconnected_induce_iff] at sconn tconn

Premises used: SimpleGraph.preconnected_induce_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : (induce s G).Preconnected
tconn : (induce t G).Preconnected
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
sconn₁ : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
tconn₁ : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ t)
hv₁ : v ∈ s
hw₁ : w ∈ t
⊢ G.Adj v w

Tactic:
rw [preconnected_induce_iff] at sconn tconn

Premises used: SimpleGraph.preconnected_induce_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
tconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
hle :
  LE.le (α := G.Subgraph) (Subgraph.induce ⊤ {v, w} ⊔ Subgraph.induce ⊤ s ⊔ Subgraph.induce ⊤ t)
    (Subgraph.induce ⊤ (s ∪ t))
hv₁ :
  Subgraph.verts (G := G) (Subgraph.induce ⊤ {v, w} ⊔ Subgraph.induce ⊤ s ⊔ Subgraph.induce ⊤ t) =
    Subgraph.verts (G := G) (Subgraph.induce ⊤ (s ∪ t))
⊢ Subgraph.Connected (G := G) (Subgraph.induce ⊤ (s ∪ t))

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

Premises used: SimpleGraph.Subgraph.connected_induce_top_sup, SimpleGraph.Subgraph.Connected.mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
tconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
hle : G.subgraphOfAdj ha ≤ Subgraph.induce ⊤ (s ∪ t)
⊢ LE.le (α := G.Subgraph) (Subgraph.induce ⊤ {v, w} ⊔ Subgraph.induce ⊤ s ⊔ Subgraph.induce ⊤ t)
    (Subgraph.induce ⊤ (s ∪ t))

Tactic:
simp only [sup_le_iff, Subgraph.le_induce_union_left,
      Subgraph.le_induce_union_right, and_true, ← Subgraph.subgraphOfAdj_eq_induce ha]

Premises used: SimpleGraph.Subgraph.le_induce_union_right, and_true, SimpleGraph.Subgraph.le_induce_union_left, sup_le_iff, SimpleGraph.Subgraph.subgraphOfAdj_eq_induce
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
tconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
hle : Subgraph.Adj (G := G) (Subgraph.induce ⊤ (s ∪ t)) v w
⊢ G.subgraphOfAdj ha ≤ Subgraph.induce ⊤ (s ∪ t)

Tactic:
apply subgraphOfAdj_le_of_adj

Premises used: SimpleGraph.subgraphOfAdj_le_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
tconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
⊢ Subgraph.Adj (G := G) (Subgraph.induce ⊤ (s ∪ t)) v w

Tactic:
simp [hv, hw, ha]
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
tconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
hv₁ : {v, w} ∪ s ∪ t = s ∪ t
⊢ Subgraph.verts (G := G) (Subgraph.induce ⊤ {v, w} ⊔ Subgraph.induce ⊤ s ⊔ Subgraph.induce ⊤ t) =
    Subgraph.verts (G := G) (Subgraph.induce ⊤ (s ∪ t))

Tactic:
simp only [Subgraph.verts_sup, Subgraph.induce_verts]

Premises used: SimpleGraph.Subgraph.verts_sup, SimpleGraph.Subgraph.induce_verts
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
tconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ t)
hv : v ∈ s
hw : w ∈ t
ha : G.Adj v w
hv₁ : {v, w} ∪ (s ∪ t) = s ∪ t
⊢ {v, w} ∪ s ∪ t = s ∪ t

Tactic:
rw [Set.union_assoc]

Premises used: Set.union_assoc
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v w : V
s t : Set V
sconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ s)
tconn : Subgraph.Preconnected (G := G) (Subgraph.induce ⊤ t)
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]

Premises used: Set.singleton_subset_iff, Set.insert_subset_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set V
u : V
hu : u ∈ s
patches :
  ∀ {v : V},
    v ∈ s →
      ∃ s' ⊆ s,
        ∃ (hu' : u ∈ s') (hv' : v ∈ s'),
          (induce s' G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s') u hu')
            (Subtype.mk (p := fun (x : V) ↦ x ∈ s') v hv')
rw : ∃ (v : (↑s : Type u)), ∀ (w : (↑s : Type u)), (induce s G).Reachable v w
⊢ (induce s G).Connected

Tactic:
rw [connected_iff_exists_forall_reachable]

Premises used: SimpleGraph.connected_iff_exists_forall_reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set V
u : V
hu : u ∈ s
patches :
  ∀ {v : V},
    v ∈ s →
      ∃ s' ⊆ s,
        ∃ (hu' : u ∈ s') (hv' : v ∈ s'),
          (induce s' G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s') u hu')
            (Subtype.mk (p := fun (x : V) ↦ x ∈ s') v hv')
⊢ ∃ (v : (↑s : Type u)), ∀ (w : (↑s : Type u)), (induce s G).Reachable v w

Tactic:
⟨⟨u, hu⟩, ?_⟩

Premises used: Subtype.mk, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set V
u : V
hu : u ∈ s
patches :
  ∀ {v : V},
    v ∈ s →
      ∃ s' ⊆ s,
        ∃ (hu' : u ∈ s') (hv' : v ∈ s'),
          (induce s' G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s') u hu')
            (Subtype.mk (p := fun (x : V) ↦ x ∈ s') v hv')
refine : ∀ (w : (↑s : Type u)), (induce s G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s) u hu) w
⊢ ∃ (v : (↑s : Type u)), ∀ (w : (↑s : Type u)), (induce s G).Reachable v w

Tactic:
refine ⟨⟨u, hu⟩, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set V
u : V
hu : u ∈ s
patches :
  ∀ {v : V},
    v ∈ s →
      ∃ s' ⊆ s,
        ∃ (hu' : u ∈ s') (hv' : v ∈ s'),
          (induce s' G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s') u hu')
            (Subtype.mk (p := fun (x : V) ↦ x ∈ s') v hv')
v : V
hv : v ∈ s
obtain :
  ∀ (sv : Set V) (svs : sv ⊆ s) (hu' : u ∈ sv) (hv' : v ∈ sv)
    (uv :
      (induce sv G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ sv) u hu')
        (Subtype.mk (p := fun (x : V) ↦ x ∈ sv) v hv')),
    (induce s G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv)
⊢ (induce s G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv)

Tactic:
obtain ⟨sv, svs, hu', hv', uv⟩ := patches hv
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set V
u : V
hu : u ∈ s
patches :
  ∀ {v : V},
    v ∈ s →
      ∃ s' ⊆ s,
        ∃ (hu' : u ∈ s') (hv' : v ∈ s'),
          (induce s' G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s') u hu')
            (Subtype.mk (p := fun (x : V) ↦ x ∈ s') v hv')
v : V
hv : v ∈ s
sv : Set V
svs : sv ⊆ s
hu' : u ∈ sv
hv' : v ∈ sv
uv :
  (induce sv G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ sv) u hu') (Subtype.mk (p := fun (x : V) ↦ x ∈ sv) v hv')
⊢ (induce s G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv)

Tactic:
uv.map (induceHomOfLE _ svs).toHom

Premises used: SimpleGraph.Reachable.map, SimpleGraph.induceHomOfLE, SimpleGraph.Embedding.toHom
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set V
u : V
hu : u ∈ s
patches :
  ∀ {v : V},
    v ∈ s →
      ∃ s' ⊆ s,
        ∃ (hu' : u ∈ s') (hv' : v ∈ s'),
          (induce s' G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s') u hu')
            (Subtype.mk (p := fun (x : V) ↦ x ∈ s') v hv')
v : V
hv : v ∈ s
sv : Set V
svs : sv ⊆ s
hu' : u ∈ sv
hv' : v ∈ sv
uv :
  (induce sv G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ sv) u hu') (Subtype.mk (p := fun (x : V) ↦ x ∈ sv) v hv')
⊢ (induce s G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s) u hu) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv)

Tactic:
exact uv.map (induceHomOfLE _ svs).toHom

Premises used: SimpleGraph.Reachable.map, SimpleGraph.induceHomOfLE, SimpleGraph.Embedding.toHom
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
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
obtain : ∀ (s : Set V) (sS : s ∈ S), (induce (⋃₀ S) G).Connected
⊢ (induce (⋃₀ S) G).Connected

Tactic:
obtain ⟨s, sS⟩ := Sn
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
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
obtain : ∀ (v : V) (vs : v ∈ s), (induce (⋃₀ S) G).Connected
⊢ (induce (⋃₀ S) G).Connected

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

Premises used: SimpleGraph.Connected.nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
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
apply :
  ∀ {v_1 : V},
    v_1 ∈ ⋃₀ S →
      ∃ s' ⊆ ⋃₀ S,
        ∃ (hu' : v ∈ s') (hv' : v_1 ∈ s'),
          (induce s' G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s') v hu')
            (Subtype.mk (p := fun (x : V) ↦ x ∈ s') v_1 hv')
⊢ (induce (⋃₀ S) G).Connected

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

Premises used: SimpleGraph.induce_connected_of_patches, Set.subset_sUnion_of_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
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
⊢ ∃ t ∈ S, w ∈ t

Tactic:
simp only [Set.mem_sUnion] at hw

Premises used: Set.mem_sUnion
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
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
obtain :
  ∀ (t : Set V) (tS : t ∈ S) (wt : w ∈ t),
    ∃ s' ⊆ ⋃₀ S,
      ∃ (hu' : v ∈ s') (hv' : w ∈ s'),
        (induce s' G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s') v hu')
          (Subtype.mk (p := fun (x : V) ↦ x ∈ s') w hv')
⊢ ∃ s' ⊆ ⋃₀ S,
    ∃ (hu' : v ∈ s') (hv' : w ∈ s'),
      (induce s' G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ s') v hu')
        (Subtype.mk (p := fun (x : V) ↦ x ∈ s') w hv')

Tactic:
obtain ⟨t, tS, wt⟩ := hw
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
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 (Subtype.mk (p := fun (x : V) ↦ x ∈ s') v hu')
        (Subtype.mk (p := fun (x : V) ↦ x ∈ s') w hv')

Tactic:
⟨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).preconnected (Sc tS).preconnected (Snd sS tS) _ _⟩

Premises used: SimpleGraph.Connected.preconnected, SimpleGraph.induce_union_connected, Set.union_subset, And.intro, Exists.intro, Set.subset_sUnion_of_mem, Or.inl, Union.union, Or.inr
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
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 (Subtype.mk (p := fun (x : V) ↦ x ∈ s') v hu')
        (Subtype.mk (p := fun (x : V) ↦ x ∈ s') 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).preconnected (Sc tS).preconnected (Snd sS tS) _ _⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
Goal:
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
tn : t.Nonempty
obtain : ∀ (u : V) (ut : u ∈ t), ∃ (t' : Finset V), t ⊆ t' ∧ (induce (↑t' : Set V) G).Connected
⊢ ∃ (t' : Finset V), t ⊆ t' ∧ (induce (↑t' : Set V) G).Connected

Tactic:
obtain ⟨u, ut⟩ := tn