-- 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 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
hx : x = a ∨ x ∈ (q.takeUntil u' hu').support
⊢ ((cons hadj q).takeUntil u' hu'✝).takeUntil x hx✝ = (cons hadj q).takeUntil x ⋯

Tactic:
by_cases hx' : x = a

Result:
case pos
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 ⋯

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 ⋯

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:
conv_lhs =>
  enter [1]
  rw [takeUntil_cons hu' hau' hadj]

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 ⋯ = (cons hadj q).takeUntil x ⋯

Proof state:
case case1
V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
w x : V
p : G.Walk u v
a✝ u✝ : V
h✝ : u✝ ∈ nil.support
x✝ : u✝ ∈ nil.support
hx : x ∈ (nil.takeUntil u✝ h✝).support
⊢ (nil.takeUntil u✝ h✝).takeUntil x hx = nil.takeUntil x ⋯

Tactic:
aesop

Result:
no goals

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
hu' : u' ∈ q.support
⊢ ((cons hadj q).takeUntil u' hu'✝).takeUntil x hx = (cons hadj q).takeUntil x ⋯

Tactic:
simp only [takeUntil_cons hu' hau' hadj, support_cons, List.mem_cons] at hx

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
hx : x = a ∨ x ∈ (q.takeUntil u' hu').support
⊢ ((cons hadj q).takeUntil u' hu'✝).takeUntil x hx✝ = (cons hadj q).takeUntil x ⋯

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
⊢ ((cons hadj q).takeUntil u✝ hu').takeUntil x hx = (cons hadj q).takeUntil x ⋯

Tactic:
simp only [takeUntil_first, support_nil, List.mem_singleton] at 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✝
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 ⋯

Proof state:
case pos
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:
aesop

Result:
no goals

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✝
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 ⋯

Tactic:
simp

Result:
no goals

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'
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:
rw [← Ne.eq_def] at hau'

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
⊢ ((cons hadj q).takeUntil u' hu').takeUntil x hx = (cons hadj q).takeUntil x ⋯