-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean
lemma getVert_takeUntil {u v : V} {n : ℕ} {p : G.Walk u v} (hw : w ∈ p.support)
    (hn : n ≤ (p.takeUntil w hw).length) : (p.takeUntil w hw).getVert n = p.getVert n

Proof state:
case nil
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
u : V
n : ℕ
hw✝ : w ∈ nil.support
hn : n ≤ (nil.takeUntil w hw✝).length
hw : w = u
⊢ (nil.takeUntil w hw✝).getVert n = nil.getVert n

Tactic:
aesop

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
u v : V
n : ℕ
v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hw : w ∈ (cons h q).support
hn : n ≤ ((cons h q).takeUntil w hw).length
⊢ ((cons h q).takeUntil w hw).getVert n = (cons h q).getVert n

Tactic:
by_cases huw : w = u

Result:
case pos
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
u v : V
n : ℕ
v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hw : w ∈ (cons h q).support
hn : n ≤ ((cons h q).takeUntil w hw).length
huw : w = u
⊢ ((cons h q).takeUntil w hw).getVert n = (cons h q).getVert n

case neg
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
u v : V
n : ℕ
v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hw : w ∈ (cons h q).support
hn : n ≤ ((cons h q).takeUntil w hw).length
huw : ¬w = u
⊢ ((cons h q).takeUntil w hw).getVert n = (cons h q).getVert n

Proof state:
case neg
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
u v : V
n : ℕ
v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hw✝ : w ∈ (cons h q).support
hn : n ≤ ((cons h q).takeUntil w hw✝).length
huw : ¬w = u
hw : w ∈ q.support
hn0 : ¬n = 0
⊢ ((cons h q).takeUntil w hw✝).getVert n = (cons h q).getVert n

Tactic:
simp only [takeUntil_cons hw ((Ne.eq_def _ _).mpr huw).symm, length_cons,
  getVert_cons _ _ hn0] at hn ⊢

Result:
case neg
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
u v : V
n : ℕ
v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hw✝ : w ∈ (cons h q).support
huw : ¬w = u
hw : w ∈ q.support
hn0 : ¬n = 0
hn : n ≤ (q.takeUntil w hw).length + 1
⊢ (q.takeUntil w hw).getVert (n - 1) = q.getVert (n - 1)

Proof state:
case neg
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
u v : V
n : ℕ
v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hw✝ : w ∈ (cons h q).support
hn : n ≤ ((cons h q).takeUntil w hw✝).length
huw : ¬w = u
hw : w ∈ q.support
⊢ ((cons h q).takeUntil w hw✝).getVert n = (cons h q).getVert n

Tactic:
by_cases hn0 : n = 0

Result:
case pos
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
u v : V
n : ℕ
v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hw✝ : w ∈ (cons h q).support
hn : n ≤ ((cons h q).takeUntil w hw✝).length
huw : ¬w = u
hw : w ∈ q.support
hn0 : n = 0
⊢ ((cons h q).takeUntil w hw✝).getVert n = (cons h q).getVert n

case neg
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
u v : V
n : ℕ
v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hw✝ : w ∈ (cons h q).support
hn : n ≤ ((cons h q).takeUntil w hw✝).length
huw : ¬w = u
hw : w ∈ q.support
hn0 : ¬n = 0
⊢ ((cons h q).takeUntil w hw✝).getVert n = (cons h q).getVert n

Proof state:
case pos
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
u v : V
n : ℕ
v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hw✝ : w ∈ (cons h q).support
hn : n ≤ ((cons h q).takeUntil w hw✝).length
huw : ¬w = u
hw : w ∈ q.support
hn0 : n = 0
⊢ ((cons h q).takeUntil w hw✝).getVert n = (cons h q).getVert n

Tactic:
aesop

Result:
no goals

Proof state:
case neg
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
u v : V
n : ℕ
v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hw✝ : w ∈ (cons h q).support
huw : ¬w = u
hw : w ∈ q.support
hn0 : ¬n = 0
hn : n ≤ (q.takeUntil w hw).length + 1
⊢ n - 1 ≤ (q.takeUntil w hw).length

Tactic:
omega

Result:
no goals

Proof state:
case neg
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
u v : V
n : ℕ
v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hw : w ∈ (cons h q).support
hn : n ≤ ((cons h q).takeUntil w hw).length
huw : ¬w = u
⊢ ((cons h q).takeUntil w hw).getVert n = (cons h q).getVert n

Tactic:
simp only [support_cons, List.mem_cons, huw, false_or] at hw

Result:
case neg
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
u v : V
n : ℕ
v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hw✝ : w ∈ (cons h q).support
hn : n ≤ ((cons h q).takeUntil w hw✝).length
huw : ¬w = u
hw : w ∈ q.support
⊢ ((cons h q).takeUntil w hw✝).getVert n = (cons h q).getVert n

Proof state:
case neg
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
u v : V
n : ℕ
v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hw✝ : w ∈ (cons h q).support
huw : ¬w = u
hw : w ∈ q.support
hn0 : ¬n = 0
hn : n ≤ (q.takeUntil w hw).length + 1
⊢ (q.takeUntil w hw).getVert (n - 1) = q.getVert (n - 1)

Tactic:
apply q.getVert_takeUntil hw

Result:
case neg
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
u v : V
n : ℕ
v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hw✝ : w ∈ (cons h q).support
huw : ¬w = u
hw : w ∈ q.support
hn0 : ¬n = 0
hn : n ≤ (q.takeUntil w hw).length + 1
⊢ n - 1 ≤ (q.takeUntil w hw).length

Proof state:
case nil
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
u : V
n : ℕ
hw : w ∈ nil.support
hn : n ≤ (nil.takeUntil w hw).length
⊢ (nil.takeUntil w hw).getVert n = nil.getVert n

Tactic:
simp only [support_nil, List.mem_singleton] at hw

Result:
case nil
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
u : V
n : ℕ
hw✝ : w ∈ nil.support
hn : n ≤ (nil.takeUntil w hw✝).length
hw : w = u
⊢ (nil.takeUntil w hw✝).getVert n = nil.getVert n

Proof state:
case pos
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
u v : V
n : ℕ
v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hw : w ∈ (cons h q).support
hn : n ≤ ((cons h q).takeUntil w hw).length
huw : w = u
⊢ ((cons h q).takeUntil w hw).getVert n = (cons h q).getVert n

Tactic:
subst huw

Result:
case pos
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
v : V
n : ℕ
v✝ : V
q : G.Walk v✝ v
h : G.Adj w v✝
hw : w ∈ (cons h q).support
hn : n ≤ ((cons h q).takeUntil w hw).length
⊢ ((cons h q).takeUntil w hw).getVert n = (cons h q).getVert n

Proof state:
case pos
V : Type u
G : SimpleGraph V
w : V
inst✝ : DecidableEq V
v : V
n : ℕ
v✝ : V
q : G.Walk v✝ v
h : G.Adj w v✝
hw : w ∈ (cons h q).support
hn : n ≤ ((cons h q).takeUntil w hw).length
⊢ ((cons h q).takeUntil w hw).getVert n = (cons h q).getVert n

Tactic:
simp_all

Result:
no goals