-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma preconnected_iff_forall_exists_walk_subgraph (H : G.Subgraph) :
    H.Preconnected ↔ ∀ {u v}, u ∈ H.verts → v ∈ H.verts → ∃ p : G.Walk u v, p.toSubgraph ≤ H

Proof state:
case mpr
V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ (∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H) → H.Preconnected

Tactic:
intro hw

Result:
case mpr
V : Type u
G : SimpleGraph V
H : G.Subgraph
hw : ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H
⊢ H.Preconnected

Proof state:
case mp
V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ H.Preconnected → ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H

Tactic:
intro hc u v hu hv

Result:
case mp
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Preconnected
u v : V
hu : u ∈ H.verts
hv : v ∈ H.verts
⊢ ∃ p, p.toSubgraph ≤ H

Proof state:
case mp
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Preconnected
u v : V
hu : u ∈ H.verts
hv : v ∈ H.verts
p : H.coe.Walk ⟨u, hu⟩ ⟨v, hv⟩
⊢ ∃ p, p.toSubgraph ≤ H

Tactic:
exists p.map (Subgraph.hom _)

Result:
case mp
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Preconnected
u v : V
hu : u ∈ H.verts
hv : v ∈ H.verts
p : H.coe.Walk ⟨u, hu⟩ ⟨v, hv⟩
⊢ (Walk.map H.hom p).toSubgraph ≤ H

Proof state:
case mpr.mk.mk.intro
V : Type u
G : SimpleGraph V
H : G.Subgraph
hw : ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, 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 ⟨u, hu⟩ ⟨v, hv⟩

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

Result:
no goals

Proof state:
case mpr
V : Type u
G : SimpleGraph V
H : G.Subgraph
hw : ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H
⊢ H.coe.Preconnected

Tactic:
rintro ⟨u, hu⟩ ⟨v, hv⟩

Result:
case mpr.mk.mk
V : Type u
G : SimpleGraph V
H : G.Subgraph
hw : ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H
u : V
hu : u ∈ H.verts
v : V
hv : v ∈ H.verts
⊢ H.coe.Reachable ⟨u, hu⟩ ⟨v, hv⟩

Proof state:
case mpr
V : Type u
G : SimpleGraph V
H : G.Subgraph
hw : ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H
⊢ H.Preconnected

Tactic:
rw [Subgraph.preconnected_iff]

Result:
case mpr
V : Type u
G : SimpleGraph V
H : G.Subgraph
hw : ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H
⊢ H.coe.Preconnected

Proof state:
case mpr.mk.mk
V : Type u
G : SimpleGraph V
H : G.Subgraph
hw : ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H
u : V
hu : u ∈ H.verts
v : V
hv : v ∈ H.verts
⊢ H.coe.Reachable ⟨u, hu⟩ ⟨v, hv⟩

Tactic:
obtain ⟨p, h⟩ := hw hu hv

Result:
case mpr.mk.mk.intro
V : Type u
G : SimpleGraph V
H : G.Subgraph
hw : ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, 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 ⟨u, hu⟩ ⟨v, hv⟩

Proof state:
case mp
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Preconnected
u v : V
hu : u ∈ H.verts
hv : v ∈ H.verts
p : H.coe.Walk ⟨u, hu⟩ ⟨v, hv⟩
⊢ (Walk.map H.hom p).toSubgraph ≤ H

Tactic:
simp [coeSubgraph_le]

Result:
no goals

Proof state:
case mp
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Preconnected
u v : V
hu : u ∈ H.verts
hv : v ∈ H.verts
⊢ ∃ p, p.toSubgraph ≤ H

Tactic:
refine (hc ⟨_, hu⟩ ⟨_, hv⟩).elim fun p => ?_

Result:
case mp
V : Type u
G : SimpleGraph V
H : G.Subgraph
hc : H.Preconnected
u v : V
hu : u ∈ H.verts
hv : v ∈ H.verts
p : H.coe.Walk ⟨u, hu⟩ ⟨v, hv⟩
⊢ ∃ p, p.toSubgraph ≤ H

Proof state:
V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ H.Preconnected ↔ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H

Tactic:
constructor

Result:
case mp
V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ H.Preconnected → ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H

case mpr
V : Type u
G : SimpleGraph V
H : G.Subgraph
⊢ (∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, p.toSubgraph ≤ H) → H.Preconnected