-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean
lemma takeUntil_takeUntil {w x : V} (p : G.Walk u v) (hw : w ∈ p.support)
    (hx : x ∈ (p.takeUntil w hw).support) :
    (p.takeUntil w hw).takeUntil x hx = p.takeUntil x (p.support_takeUntil_subset hw hx)

Proof state:
case case2
V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
w x : V
p : G.Walk u v
w✝ v✝ : V
q : G.Walk v✝ w✝
u✝ : V
hadj : G.Adj u✝ v✝
hu' : u✝ ∈ (cons hadj q).support
x✝ : u✝ ∈ (cons hadj q).support
hx✝ : x ∈ ((cons hadj q).takeUntil u✝ hu').support
hx : x = u✝
⊢ ((cons hadj q).takeUntil u✝ hu').takeUntil x hx✝ = (cons hadj q).takeUntil x ⋯

Tactic:
subst hx

Result:
case case2
V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
w x : V
p : G.Walk u v
w✝ v✝ : V
q : G.Walk v✝ w✝
hadj : G.Adj x v✝
hu' : x ∈ (cons hadj q).support
x✝ : x ∈ (cons hadj q).support
hx : x ∈ ((cons hadj q).takeUntil x hu').support
⊢ ((cons hadj q).takeUntil x hu').takeUntil x hx = (cons hadj q).takeUntil x ⋯

Proof state:
case case3
V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
w x : V
p : G.Walk u v
a w' v' : V
hadj : G.Adj a v'
q : G.Walk v' w'
u' : V
hu' : u' ∈ (cons hadj q).support
hau'✝ : ¬a = u'
hau' : a ≠ u'
x✝ : u' ∈ (cons hadj q).support
ih : ∀ (hx : x ∈ (q.takeUntil u' ⋯).support), (q.takeUntil u' ⋯).takeUntil x hx = q.takeUntil x ⋯
hx : x ∈ ((cons hadj q).takeUntil u' hu').support
⊢ ((cons hadj q).takeUntil u' hu').takeUntil x hx = (cons hadj q).takeUntil x ⋯

Tactic:
simp only [support_cons, List.mem_cons, hau'.symm, false_or] at hu'

Result:
case case3
V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
w x : V
p : G.Walk u v
a w' v' : V
hadj : G.Adj a v'
q : G.Walk v' w'
u' : V
hu'✝ : u' ∈ (cons hadj q).support
hau'✝ : ¬a = u'
hau' : a ≠ u'
x✝ : u' ∈ (cons hadj q).support
ih : ∀ (hx : x ∈ (q.takeUntil u' ⋯).support), (q.takeUntil u' ⋯).takeUntil x hx = q.takeUntil x ⋯
hx : x ∈ ((cons hadj q).takeUntil u' hu'✝).support
hu' : u' ∈ q.support
⊢ ((cons hadj q).takeUntil u' hu'✝).takeUntil x hx = (cons hadj q).takeUntil x ⋯

Proof state:
case neg
V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
w x : V
p : G.Walk u v
a w' v' : V
hadj : G.Adj a v'
q : G.Walk v' w'
u' : V
hu'✝ : u' ∈ (cons hadj q).support
hau'✝ : ¬a = u'
hau' : a ≠ u'
x✝ : u' ∈ (cons hadj q).support
ih : ∀ (hx : x ∈ (q.takeUntil u' ⋯).support), (q.takeUntil u' ⋯).takeUntil x hx = q.takeUntil x ⋯
hx✝ : x ∈ ((cons hadj q).takeUntil u' hu'✝).support
hu' : u' ∈ q.support
hx' : x ≠ a
hx : x ∈ (q.takeUntil u' hu').support
⊢ (cons hadj (q.takeUntil u' hu')).takeUntil x ⋯ = (cons hadj q).takeUntil x ⋯

Tactic:
rw [takeUntil_cons hx hx'.symm hadj, ih _, takeUntil_cons _ hx'.symm]

Result:
no goals

Proof state:
case neg
V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
w x : V
p : G.Walk u v
a w' v' : V
hadj : G.Adj a v'
q : G.Walk v' w'
u' : V
hu'✝ : u' ∈ (cons hadj q).support
hau'✝ : ¬a = u'
hau' : a ≠ u'
x✝ : u' ∈ (cons hadj q).support
ih : ∀ (hx : x ∈ (q.takeUntil u' ⋯).support), (q.takeUntil u' ⋯).takeUntil x hx = q.takeUntil x ⋯
hx✝ : x ∈ ((cons hadj q).takeUntil u' hu'✝).support
hu' : u' ∈ q.support
hx : x = a ∨ x ∈ (q.takeUntil u' hu').support
hx' : ¬x = a
⊢ ((cons hadj q).takeUntil u' hu'✝).takeUntil x hx✝ = (cons hadj q).takeUntil x ⋯

Tactic:
replace hx : x ∈ (q.takeUntil u' hu').support := by simpa [hx'] using hx

Result:
case neg
V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
w x : V
p : G.Walk u v
a w' v' : V
hadj : G.Adj a v'
q : G.Walk v' w'
u' : V
hu'✝ : u' ∈ (cons hadj q).support
hau'✝ : ¬a = u'
hau' : a ≠ u'
x✝ : u' ∈ (cons hadj q).support
ih : ∀ (hx : x ∈ (q.takeUntil u' ⋯).support), (q.takeUntil u' ⋯).takeUntil x hx = q.takeUntil x ⋯
hx✝ : x ∈ ((cons hadj q).takeUntil u' hu'✝).support
hu' : u' ∈ q.support
hx' : ¬x = a
hx : x ∈ (q.takeUntil u' hu').support
⊢ ((cons hadj q).takeUntil u' hu'✝).takeUntil x hx✝ = (cons hadj q).takeUntil x ⋯

Proof state:
V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
w x : V
p : G.Walk u v
a w' v' : V
hadj : G.Adj a v'
q : G.Walk v' w'
u' : V
hu'✝ : u' ∈ (cons hadj q).support
hau'✝ : ¬a = u'
hau' : a ≠ u'
x✝ : u' ∈ (cons hadj q).support
ih : ∀ (hx : x ∈ (q.takeUntil u' ⋯).support), (q.takeUntil u' ⋯).takeUntil x hx = q.takeUntil x ⋯
hx✝ : x ∈ ((cons hadj q).takeUntil u' hu'✝).support
hu' : u' ∈ q.support
hx : x = a ∨ x ∈ (q.takeUntil u' hu').support
hx' : ¬x = a
⊢ x ∈ (q.takeUntil u' hu').support

Tactic:
simpa [hx'] using hx

Result:
no goals

Proof state:
case neg
V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
w x : V
p : G.Walk u v
a w' v' : V
hadj : G.Adj a v'
q : G.Walk v' w'
u' : V
hu'✝ : u' ∈ (cons hadj q).support
hau'✝ : ¬a = u'
hau' : a ≠ u'
x✝ : u' ∈ (cons hadj q).support
ih : ∀ (hx : x ∈ (q.takeUntil u' ⋯).support), (q.takeUntil u' ⋯).takeUntil x hx = q.takeUntil x ⋯
hx✝ : x ∈ ((cons hadj q).takeUntil u' hu'✝).support
hu' : u' ∈ q.support
hx' : ¬x = a
hx : x ∈ (q.takeUntil u' hu').support
⊢ ((cons hadj q).takeUntil u' hu'✝).takeUntil x hx✝ = (cons hadj q).takeUntil x ⋯

Tactic:
push_neg at hx'

Result:
case neg
V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
w x : V
p : G.Walk u v
a w' v' : V
hadj : G.Adj a v'
q : G.Walk v' w'
u' : V
hu'✝ : u' ∈ (cons hadj q).support
hau'✝ : ¬a = u'
hau' : a ≠ u'
x✝ : u' ∈ (cons hadj q).support
ih : ∀ (hx : x ∈ (q.takeUntil u' ⋯).support), (q.takeUntil u' ⋯).takeUntil x hx = q.takeUntil x ⋯
hx✝ : x ∈ ((cons hadj q).takeUntil u' hu'✝).support
hu' : u' ∈ q.support
hx' : x ≠ a
hx : x ∈ (q.takeUntil u' hu').support
⊢ ((cons hadj q).takeUntil u' hu'✝).takeUntil x hx✝ = (cons hadj q).takeUntil x ⋯