-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma IsCycles.snd_of_mem_support_of_isPath_of_adj [Finite V] {v w w' : V}
    (hcyc : G.IsCycles) (p : G.Walk v w) (hw : w ≠ w') (hw' : w' ∈ p.support) (hp : p.IsPath)
    (hadj : G.Adj v w') : p.snd = w'

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
⊢ n ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : ∃ n, p.getVert n = w' ∧ n ≤ p.length
hp : p.IsPath
hadj : G.Adj v w'
⊢ p.toSubgraph.Adj v w'

Tactic:
obtain ⟨n, ⟨rfl, hnl⟩⟩ := hw'

Result:
case intro.intro
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
⊢ p.toSubgraph.Adj v (p.getVert n)

Proof state:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
⊢ p.toSubgraph.Adj v (p.getVert n)

Tactic:
have e : G.neighborSet (p.getVert n) ≃ p.toSubgraph.neighborSet (p.getVert n) := by
  refine @Classical.ofNonempty _ ?_
  rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
      hp.ncard_neighborSet_toSubgraph_internal_eq_two (by omega) (by omega),
      hcyc (Set.nonempty_of_mem hadj.symm)]

Result:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
e : ↑(G.neighborSet (p.getVert n)) ≃ ↑(p.toSubgraph.neighborSet (p.getVert n))
⊢ p.toSubgraph.Adj v (p.getVert n)

Proof state:
case intro.intro
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
⊢ p.toSubgraph.Adj v (p.getVert n)

Tactic:
by_cases hn : n = 0 ∨ n = p.length

Result:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : n = 0 ∨ n = p.length
⊢ p.toSubgraph.Adj v (p.getVert n)

case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
⊢ p.toSubgraph.Adj v (p.getVert n)

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
⊢ ↑(G.neighborSet (p.getVert n)) ≃ ↑(p.toSubgraph.neighborSet (p.getVert n))

Tactic:
refine @Classical.ofNonempty _ ?_

Result:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
⊢ Nonempty (↑(G.neighborSet (p.getVert n)) ≃ ↑(p.toSubgraph.neighborSet (p.getVert n)))

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : w' ∈ p.support
hp : p.IsPath
hadj : G.Adj v w'
⊢ p.toSubgraph.Adj v w'

Tactic:
rw [Walk.mem_support_iff_exists_getVert] at hw'

Result:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : ∃ n, p.getVert n = w' ∧ n ≤ p.length
hp : p.IsPath
hadj : G.Adj v w'
⊢ p.toSubgraph.Adj v w'

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
⊢ Nonempty (↑(G.neighborSet (p.getVert n)) ≃ ↑(p.toSubgraph.neighborSet (p.getVert n)))

Tactic:
rw [← Cardinal.eq, ← Set.cast_ncard (Set.toFinite _), ← Set.cast_ncard (Set.toFinite _),
    hp.ncard_neighborSet_toSubgraph_internal_eq_two (by omega) (by omega),
    hcyc (Set.nonempty_of_mem hadj.symm)]

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : w' ∈ p.support
hp : p.IsPath
hadj : G.Adj v w'
⊢ p.snd = w'

Tactic:
apply hp.snd_of_toSubgraph_adj

Result:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w w' : V
hcyc : G.IsCycles
p : G.Walk v w
hw : w ≠ w'
hw' : w' ∈ p.support
hp : p.IsPath
hadj : G.Adj v w'
⊢ p.toSubgraph.Adj v w'

Proof state:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
e : ↑(G.neighborSet (p.getVert n)) ≃ ↑(p.toSubgraph.neighborSet (p.getVert n))
⊢ G.Adj (p.getVert n) v

Tactic:
exact hadj.symm

Result:
no goals

Proof state:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : n = 0 ∨ n = p.length
⊢ p.toSubgraph.Adj v (p.getVert n)

Tactic:
aesop

Result:
no goals

Proof state:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
e : ↑(G.neighborSet (p.getVert n)) ≃ ↑(p.toSubgraph.neighborSet (p.getVert n))
⊢ p.toSubgraph.Adj v (p.getVert n)

Tactic:
rw [Subgraph.adj_comm, Subgraph.adj_iff_of_neighborSet_equiv e (Set.toFinite _)]

Result:
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
e : ↑(G.neighborSet (p.getVert n)) ≃ ↑(p.toSubgraph.neighborSet (p.getVert n))
⊢ G.Adj (p.getVert n) v

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
n : ℕ
hnl : n ≤ p.length
hw : w ≠ p.getVert n
hadj : G.Adj v (p.getVert n)
hn : ¬(n = 0 ∨ n = p.length)
⊢ n < p.length

Tactic:
omega

Result:
no goals