-- 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 mpr
V : Type u
G : SimpleGraph V
u v u' v' : V
w : G.Walk u v
⊢ (∃ i, s(w.getVert i, w.getVert (i + 1)) = s(u', v') ∧ i < w.length) → w.toSubgraph.Adj u' v'

Tactic:
rintro ⟨i, hi⟩

Result:
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 u' v'

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
hl : u = u' ∧ v✝ = v' ∨ u = v' ∧ v✝ = u'
⊢ u = u' ∧ v✝ = v' ∨ u = v' ∧ v✝ = u'

Tactic:
cases hl with
| inl h1 => left; exact ⟨h1.1, h1.2⟩
| inr h2 => right; exact ⟨h2.1, h2.2⟩

Result:
no goals

Proof state:
case mp
V : Type u
G : SimpleGraph V
u v u' v' : 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

Tactic:
intro hadj

Result:
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

Proof state:
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')

Tactic:
exact hi.1

Result:
no goals

Proof state:
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
hadj :
  (match v, cons h p with
      | .(u), nil => G.singletonSubgraph u
      | v, cons h p => G.subgraphOfAdj h ⊔ p.toSubgraph).Adj
    u' v'
⊢ ∃ i, s((cons h p).getVert i, (cons h p).getVert (i + 1)) = s(u', v') ∧ i < (cons h p).length

Tactic:
simp only [Subgraph.sup_adj, subgraphOfAdj_adj, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq,
  Prod.swap_prod_mk] at hadj

Result:
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
hadj : (u = u' ∧ v✝ = v' ∨ u = v' ∧ v✝ = u') ∨ p.toSubgraph.Adj u' v'
⊢ ∃ i, s((cons h p).getVert i, (cons h p).getVert (i + 1)) = s(u', v') ∧ i < (cons h p).length

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 u' v'

Tactic:
rw [← Subgraph.mem_edgeSet, ← hi.1, Subgraph.mem_edgeSet]

Result:
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))

Proof state:
case 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
hr : p.toSubgraph.Adj u' v'
⊢ ∃ i, s((cons h p).getVert i, (cons h p).getVert (i + 1)) = s(u', v') ∧ i < (cons h p).length

Tactic:
obtain ⟨i, hi⟩ := (toSubgraph_adj_iff _).mp hr

Result:
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

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
hl : u = u' ∧ v✝ = v' ∨ u = v' ∧ v✝ = u'
⊢ s((cons h p).getVert 0, (cons h p).getVert (0 + 1)) = s(u', v') ∧ 0 < (cons h p).length

Tactic:
simp only [Walk.getVert_zero, zero_add, 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
hl : u = u' ∧ v✝ = v' ∨ u = v' ∧ v✝ = u'
⊢ s(u, v✝) = s(u', v') ∧ 0 < (cons h p).length

Proof state:
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
hl : u = u' ∧ v✝ = v' ∨ u = v' ∧ v✝ = u'
⊢ 0 < (cons h p).length

Tactic:
simp only [length_cons, Nat.zero_lt_succ]

Result:
no goals

Proof state:
case h.inl.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
h1 : u = u' ∧ v✝ = v'
⊢ u = u' ∧ v✝ = v'

Tactic:
exact ⟨h1.1, h1.2⟩

Result:
no goals

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
hl : u = u' ∧ v✝ = v' ∨ u = v' ∧ v✝ = u'
⊢ s(u, v✝) = s(u', v') ∧ 0 < (cons h p).length

Tactic:
refine ⟨?_, by simp only [length_cons, Nat.zero_lt_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
hl : u = u' ∧ v✝ = v' ∨ u = v' ∧ v✝ = u'
⊢ s(u, v✝) = s(u', v')

Proof state:
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

Tactic:
simp only [Walk.length_cons, add_lt_add_iff_right, Nat.add_lt_add_right hi.2 1]

Result:
no goals

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
hl : u = u' ∧ v✝ = v' ∨ u = v' ∧ v✝ = u'
⊢ s(u, v✝) = s(u', v')

Tactic:
simp only [Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]

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
hl : u = u' ∧ v✝ = v' ∨ u = v' ∧ v✝ = u'
⊢ u = u' ∧ v✝ = v' ∨ u = v' ∧ v✝ = u'

Proof state:
case inl
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
hl : u = u' ∧ v✝ = v' ∨ u = v' ∧ v✝ = u'
⊢ ∃ i, s((cons h p).getVert i, (cons h p).getVert (i + 1)) = s(u', v') ∧ i < (cons h p).length

Tactic:
use 0

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
hl : u = u' ∧ v✝ = v' ∨ u = v' ∧ v✝ = u'
⊢ s((cons h p).getVert 0, (cons h p).getVert (0 + 1)) = s(u', v') ∧ 0 < (cons h p).length

Proof state:
case h.inl
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
h1 : u = u' ∧ v✝ = v'
⊢ u = u' ∧ v✝ = v' ∨ u = v' ∧ v✝ = u'

Tactic:
left

Result:
case h.inl.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
h1 : u = u' ∧ v✝ = v'
⊢ u = u' ∧ v✝ = v'

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

Tactic:
simp only [singletonSubgraph_adj, Pi.bot_apply, Prop.bot_eq_false] at hadj

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v u' v' : 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

Tactic:
constructor

Result:
case mp
V : Type u
G : SimpleGraph V
u v u' v' : 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

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

Proof state:
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'

Tactic:
exact ⟨h2.1, h2.2⟩

Result:
no goals