-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma Reachable.mem_subgraphVerts {u v} {H : G.Subgraph} (hr : G.Reachable u v)
    (h : ∀ v ∈ H.verts, ∀ w, G.Adj v w → H.Adj v w)
    (hu : u ∈ H.verts) : v ∈ H.verts

Proof state:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
x✝ : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v
a✝² :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    (invImage (fun x => PSigma.casesOn x fun v' hv' => PSigma.casesOn hv' fun hv' p => p.length)
            instWellFoundedRelationOfSizeOf).1
        y x✝ →
      v ∈ H.verts
v' : V
hv'✝ : (_ : v' ∈ H.verts) ×' G.Walk v' v
a✝¹ :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    (invImage (fun x => PSigma.casesOn x fun v' hv' => PSigma.casesOn hv' fun hv' p => p.length)
            instWellFoundedRelationOfSizeOf).1
        y ⟨v', hv'✝⟩ →
      v ∈ H.verts
hv' : v' ∈ H.verts
p : G.Walk v' v
a✝ :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    (invImage (fun x => PSigma.casesOn x fun v' hv' => PSigma.casesOn hv' fun hv' p => p.length)
            instWellFoundedRelationOfSizeOf).1
        y ⟨v', ⟨hv', p⟩⟩ →
      v ∈ H.verts
hnp : ¬p.Nil
⊢ p.tail.length < p.tail.length + 1

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
H : G.Subgraph
hr : G.Reachable u v
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
hu : u ∈ H.verts
v' : V
hv' : v' ∈ H.verts
p : G.Walk v' v
⊢ v ∈ H.verts

Tactic:
by_cases hnp : p.Nil

Result:
case pos
V : Type u
G : SimpleGraph V
u v : V
H : G.Subgraph
hr : G.Reachable u v
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
hu : u ∈ H.verts
v' : V
hv' : v' ∈ H.verts
p : G.Walk v' v
hnp : p.Nil
⊢ v ∈ H.verts

case neg
V : Type u
G : SimpleGraph V
u v : V
H : G.Subgraph
hr : G.Reachable u v
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
hu : u ∈ H.verts
v' : V
hv' : v' ∈ H.verts
p : G.Walk v' v
hnp : ¬p.Nil
⊢ v ∈ H.verts

Proof state:
case neg
V : Type u
G : SimpleGraph V
u v : V
H : G.Subgraph
hr : G.Reachable u v
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
hu : u ∈ H.verts
v' : V
hv' : v' ∈ H.verts
p : G.Walk v' v
hnp : ¬p.Nil
⊢ v ∈ H.verts

Tactic:
exact aux (H.edge_vert (h _ hv' _ (Walk.adj_snd hnp)).symm) p.tail

Result:
no goals

Proof state:
case pos
V : Type u
G : SimpleGraph V
u v : V
H : G.Subgraph
hr : G.Reachable u v
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
hu : u ∈ H.verts
v' : V
hv' : v' ∈ H.verts
p : G.Walk v' v
hnp : p.Nil
⊢ v ∈ H.verts

Tactic:
exact hnp.eq ▸ hv'

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
x✝ : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v
a✝² :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    (invImage (fun x => PSigma.casesOn x fun v' hv' => PSigma.casesOn hv' fun hv' p => p.length)
            instWellFoundedRelationOfSizeOf).1
        y x✝ →
      v ∈ H.verts
v' : V
hv'✝ : (_ : v' ∈ H.verts) ×' G.Walk v' v
a✝¹ :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    (invImage (fun x => PSigma.casesOn x fun v' hv' => PSigma.casesOn hv' fun hv' p => p.length)
            instWellFoundedRelationOfSizeOf).1
        y ⟨v', hv'✝⟩ →
      v ∈ H.verts
hv' : v' ∈ H.verts
p : G.Walk v' v
a✝ :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    (invImage (fun x => PSigma.casesOn x fun v' hv' => PSigma.casesOn hv' fun hv' p => p.length)
            instWellFoundedRelationOfSizeOf).1
        y ⟨v', ⟨hv', p⟩⟩ →
      v ∈ H.verts
hnp : ¬p.Nil
⊢ p.tail.length < p.length

Tactic:
rw [← Walk.length_tail_add_one hnp]

Result:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
x✝ : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v
a✝² :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    (invImage (fun x => PSigma.casesOn x fun v' hv' => PSigma.casesOn hv' fun hv' p => p.length)
            instWellFoundedRelationOfSizeOf).1
        y x✝ →
      v ∈ H.verts
v' : V
hv'✝ : (_ : v' ∈ H.verts) ×' G.Walk v' v
a✝¹ :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    (invImage (fun x => PSigma.casesOn x fun v' hv' => PSigma.casesOn hv' fun hv' p => p.length)
            instWellFoundedRelationOfSizeOf).1
        y ⟨v', hv'✝⟩ →
      v ∈ H.verts
hv' : v' ∈ H.verts
p : G.Walk v' v
a✝ :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    (invImage (fun x => PSigma.casesOn x fun v' hv' => PSigma.casesOn hv' fun hv' p => p.length)
            instWellFoundedRelationOfSizeOf).1
        y ⟨v', ⟨hv', p⟩⟩ →
      v ∈ H.verts
hnp : ¬p.Nil
⊢ p.tail.length < p.tail.length + 1

Proof state:
V : Type u
G : SimpleGraph V
u v : V
H : G.Subgraph
hr : G.Reachable u v
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
hu : u ∈ H.verts
⊢ v ∈ H.verts

Tactic:
exact aux hu hr.some

Result:
no goals