case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w u✝ : V
h : u ∈ support nil
⊢ append (takeUntil nil u h) (dropUntil nil u h) = nil

case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), append (takeUntil p✝ u h) (dropUntil p✝ u h) = p✝
h : u ∈ support (cons h✝ p✝)
⊢ append (takeUntil (cons h✝ p✝) u h) (dropUntil (cons h✝ p✝) u h) = cons h✝ p✝
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
p : Walk G v w
h : u ∈ support p
⊢ append (takeUntil p u h) (dropUntil p u h) = p
induction p
case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w u✝ : V
h✝ : u ∈ support nil
h : u = u✝
⊢ append (takeUntil nil u h✝) (dropUntil nil u h✝) = nil
case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w u✝ : V
h : u ∈ support nil
⊢ append (takeUntil nil u h) (dropUntil nil u h) = nil
rw [mem_support_nil_iff] at h
case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
v w u✝ : V
h : u✝ ∈ support nil
⊢ append (takeUntil nil u✝ h) (dropUntil nil u✝ h) = nil
case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w u✝ : V
h✝ : u ∈ support nil
h : u = u✝
⊢ append (takeUntil nil u h✝) (dropUntil nil u h✝) = nil
subst u
no goals
case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
v w u✝ : V
h : u✝ ∈ support nil
⊢ append (takeUntil nil u✝ h) (dropUntil nil u✝ h) = nil
rfl
case cons.head
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w v✝ w✝ : V
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), append (takeUntil p✝ u h) (dropUntil p✝ u h) = p✝
h✝ : Adj G u v✝
⊢ append (takeUntil (cons h✝ p✝) u (_ : List.Mem u (u :: support p✝)))
      (dropUntil (cons h✝ p✝) u (_ : List.Mem u (u :: support p✝))) =
    cons h✝ p✝

case cons.tail
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), append (takeUntil p✝ u h) (dropUntil p✝ u h) = p✝
a✝ : List.Mem u (support p✝)
⊢ append (takeUntil (cons h✝ p✝) u (_ : List.Mem u (u✝ :: support p✝)))
      (dropUntil (cons h✝ p✝) u (_ : List.Mem u (u✝ :: support p✝))) =
    cons h✝ p✝
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), append (takeUntil p✝ u h) (dropUntil p✝ u h) = p✝
h : u ∈ support (cons h✝ p✝)
⊢ append (takeUntil (cons h✝ p✝) u h) (dropUntil (cons h✝ p✝) u h) = cons h✝ p✝
cases h
no goals
case cons.head
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w v✝ w✝ : V
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), append (takeUntil p✝ u h) (dropUntil p✝ u h) = p✝
h✝ : Adj G u v✝
⊢ append (takeUntil (cons h✝ p✝) u (_ : List.Mem u (u :: support p✝)))
      (dropUntil (cons h✝ p✝) u (_ : List.Mem u (u :: support p✝))) =
    cons h✝ p✝
simp!
case cons.tail
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), append (takeUntil p✝ u h) (dropUntil p✝ u h) = p✝
a✝ : List.Mem u (support p✝)
⊢ append
      (if h : u✝ = u then
        Eq.rec (motive := fun x x_1 => x ∈ u✝ :: support p✝ → Walk G u✝ x) (fun h => nil) (_ : u✝ = u)
          (_ : List.Mem u (u✝ :: support p✝))
      else cons h✝ (takeUntil p✝ u (_ : u ∈ support p✝)))
      (if h : u✝ = u then
        Eq.rec (motive := fun x x_1 => x ∈ u✝ :: support p✝ → Walk G x w✝) (fun h => cons h✝ p✝) (_ : u✝ = u)
          (_ : List.Mem u (u✝ :: support p✝))
      else dropUntil p✝ u (_ : u ∈ support p✝)) =
    cons h✝ p✝
case cons.tail
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), append (takeUntil p✝ u h) (dropUntil p✝ u h) = p✝
a✝ : List.Mem u (support p✝)
⊢ append (takeUntil (cons h✝ p✝) u (_ : List.Mem u (u✝ :: support p✝)))
      (dropUntil (cons h✝ p✝) u (_ : List.Mem u (u✝ :: support p✝))) =
    cons h✝ p✝
simp! only
no goals
case cons.tail
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : ∀ (h : u ∈ support p✝), append (takeUntil p✝ u h) (dropUntil p✝ u h) = p✝
a✝ : List.Mem u (support p✝)
⊢ append
      (if h : u✝ = u then
        Eq.rec (motive := fun x x_1 => x ∈ u✝ :: support p✝ → Walk G u✝ x) (fun h => nil) (_ : u✝ = u)
          (_ : List.Mem u (u✝ :: support p✝))
      else cons h✝ (takeUntil p✝ u (_ : u ∈ support p✝)))
      (if h : u✝ = u then
        Eq.rec (motive := fun x x_1 => x ∈ u✝ :: support p✝ → Walk G x w✝) (fun h => cons h✝ p✝) (_ : u✝ = u)
          (_ : List.Mem u (u✝ :: support p✝))
      else dropUntil p✝ u (_ : u ∈ support p✝)) =
    cons h✝ p✝
split_ifs with h' <;> subst_vars <;> simp [*]