-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean
@[simp]
lemma nil_takeUntil (p : G.Walk u v) (hwp : w ∈ p.support) :
    (p.takeUntil w hwp).Nil ↔ u = w

Proof state:
case nil
V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
hwp : w ∈ nil.support
hnil : (cast ⋯ nil).Nil
⊢ v = w

Tactic:
exact hnil.eq

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk u v
hwp : w ∈ p.support
⊢ (p.takeUntil w hwp).Nil → u = w

Tactic:
intro hnil

Result:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk u v
hwp : w ∈ p.support
hnil : (p.takeUntil w hwp).Nil
⊢ u = w

Proof state:
case cons.inl
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hwp : w ∈ (cons h q).support
hnil : ((cons h q).takeUntil w hwp).Nil
hl : w = u
⊢ u = w

Tactic:
exact hl.symm

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk u v
hwp : w ∈ p.support
⊢ (p.takeUntil w hwp).Nil ↔ u = w

Tactic:
refine ⟨?_, fun h => by subst h; simp⟩

Result:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk u v
hwp : w ∈ p.support
⊢ (p.takeUntil w hwp).Nil → u = w

Proof state:
case cons
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hwp : w ∈ (cons h q).support
hnil : ((cons h q).takeUntil w hwp).Nil
⊢ u = w

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

Result:
case cons
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hwp✝ : w ∈ (cons h q).support
hnil : ((cons h q).takeUntil w hwp✝).Nil
hwp : w = u ∨ w ∈ q.support
⊢ u = w

Proof state:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk u v
hwp : w ∈ p.support
h : u = w
⊢ (p.takeUntil w hwp).Nil

Tactic:
subst h

Result:
V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
p : G.Walk u v
hwp : u ∈ p.support
⊢ (p.takeUntil u hwp).Nil

Proof state:
case cons.inr
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hwp : w ∈ (cons h q).support
hnil : ((cons h q).takeUntil w hwp).Nil
hr : w ∈ q.support
hc : u ≠ w
⊢ False

Tactic:
simp [takeUntil_cons hr hc] at hnil

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hwp✝ : w ∈ (cons h q).support
hnil : ((cons h q).takeUntil w hwp✝).Nil
hwp : w = u ∨ w ∈ q.support
⊢ u = w

Tactic:
obtain hl | hr := hwp

Result:
case cons.inl
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hwp : w ∈ (cons h q).support
hnil : ((cons h q).takeUntil w hwp).Nil
hl : w = u
⊢ u = w

case cons.inr
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hwp : w ∈ (cons h q).support
hnil : ((cons h q).takeUntil w hwp).Nil
hr : w ∈ q.support
⊢ u = w

Proof state:
case nil
V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
hwp : w ∈ nil.support
hnil : (nil.takeUntil w hwp).Nil
⊢ v = w

Tactic:
simp only [takeUntil, eq_mpr_eq_cast] at hnil

Result:
case nil
V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
hwp : w ∈ nil.support
hnil : (cast ⋯ nil).Nil
⊢ v = w

Proof state:
V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
p : G.Walk u v
hwp : u ∈ p.support
⊢ (p.takeUntil u hwp).Nil

Tactic:
simp

Result:
no goals

Proof state:
case cons.inr
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hwp : w ∈ (cons h q).support
hnil : ((cons h q).takeUntil w hwp).Nil
hr : w ∈ q.support
⊢ u = w

Tactic:
by_contra! hc

Result:
case cons.inr
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
v✝ : V
h : G.Adj u v✝
q : G.Walk v✝ v
hwp : w ∈ (cons h q).support
hnil : ((cons h q).takeUntil w hwp).Nil
hr : w ∈ q.support
hc : u ≠ w
⊢ False