-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
theorem toSubgraph_adj_iff {u v u' v'} (w : G.Walk u v) :
    w.toSubgraph.Adj u' v' ↔ ∃ i, s(w.getVert i, w.getVert (i + 1)) =
      s(u', v') ∧ i < w.length

Proof state:
case inr.intro
V : Type u
G : SimpleGraph V
u v✝¹ u' v' : V
w : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
hr : p.toSubgraph.Adj u' v'
i : ℕ
hi : s(p.getVert i, p.getVert (i + 1)) = s(u', v') ∧ i < p.length
⊢ ∃ i, s((cons h p).getVert i, (cons h p).getVert (i + 1)) = s(u', v') ∧ i < (cons h p).length

Tactic:
use i + 1

Result:
case h
V : Type u
G : SimpleGraph V
u v✝¹ u' v' : V
w : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
hr : p.toSubgraph.Adj u' v'
i : ℕ
hi : s(p.getVert i, p.getVert (i + 1)) = s(u', v') ∧ i < p.length
⊢ s((cons h p).getVert (i + 1), (cons h p).getVert (i + 1 + 1)) = s(u', v') ∧ i + 1 < (cons h p).length

Proof state:
case h
V : Type u
G : SimpleGraph V
u v✝¹ u' v' : V
w : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
hr : p.toSubgraph.Adj u' v'
i : ℕ
hi : s(p.getVert i, p.getVert (i + 1)) = s(u', v') ∧ i < p.length
⊢ s((cons h p).getVert (i + 1), (cons h p).getVert (i + 1 + 1)) = s(u', v') ∧ i + 1 < (cons h p).length

Tactic:
simp only [getVert_cons_succ]

Result:
case h
V : Type u
G : SimpleGraph V
u v✝¹ u' v' : V
w : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
hr : p.toSubgraph.Adj u' v'
i : ℕ
hi : s(p.getVert i, p.getVert (i + 1)) = s(u', v') ∧ i < p.length
⊢ s(p.getVert i, p.getVert (i + 1)) = s(u', v') ∧ i + 1 < (cons h p).length

Proof state:
case mp
V : Type u
G : SimpleGraph V
u v u' v' : V
w : G.Walk u v
hadj : w.toSubgraph.Adj u' v'
⊢ ∃ i, s(w.getVert i, w.getVert (i + 1)) = s(u', v') ∧ i < w.length

Tactic:
unfold Walk.toSubgraph at hadj

Result:
case mp
V : Type u
G : SimpleGraph V
u v u' v' : V
w : G.Walk u v
hadj :
  (match v, w with
      | .(u), nil => G.singletonSubgraph u
      | v, cons h p => G.subgraphOfAdj h ⊔ p.toSubgraph).Adj
    u' v'
⊢ ∃ i, s(w.getVert i, w.getVert (i + 1)) = s(u', v') ∧ i < w.length

Proof state:
case h
V : Type u
G : SimpleGraph V
u v✝¹ u' v' : V
w : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
hr : p.toSubgraph.Adj u' v'
i : ℕ
hi : s(p.getVert i, p.getVert (i + 1)) = s(u', v') ∧ i < p.length
⊢ s(p.getVert i, p.getVert (i + 1)) = s(u', v') ∧ i + 1 < (cons h p).length

Tactic:
constructor

Result:
case h.left
V : Type u
G : SimpleGraph V
u v✝¹ u' v' : V
w : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
hr : p.toSubgraph.Adj u' v'
i : ℕ
hi : s(p.getVert i, p.getVert (i + 1)) = s(u', v') ∧ i < p.length
⊢ s(p.getVert i, p.getVert (i + 1)) = s(u', v')

case h.right
V : Type u
G : SimpleGraph V
u v✝¹ u' v' : V
w : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
hr : p.toSubgraph.Adj u' v'
i : ℕ
hi : s(p.getVert i, p.getVert (i + 1)) = s(u', v') ∧ i < p.length
⊢ i + 1 < (cons h p).length

Proof state:
case h.inr
V : Type u
G : SimpleGraph V
u v✝¹ u' v' : V
w : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
h2 : u = v' ∧ v✝ = u'
⊢ u = u' ∧ v✝ = v' ∨ u = v' ∧ v✝ = u'

Tactic:
right

Result:
case h.inr.h
V : Type u
G : SimpleGraph V
u v✝¹ u' v' : V
w : G.Walk u v✝¹
v v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
h2 : u = v' ∧ v✝ = u'
⊢ u = v' ∧ v✝ = u'

Proof state:
case mpr.intro
V : Type u
G : SimpleGraph V
u v u' v' : V
w : G.Walk u v
i : ℕ
hi : s(w.getVert i, w.getVert (i + 1)) = s(u', v') ∧ i < w.length
⊢ w.toSubgraph.Adj (w.getVert i) (w.getVert (i + 1))

Tactic:
exact toSubgraph_adj_getVert _ hi.2

Result:
no goals